A canonical quotient of a directed relation

Abstract

The least successor-compatible quotient controls both assignments and all relation symmetries.

The relation R may contain loops. An admissible equivalence puts all successors of one vertex in one class, and puts successors of equivalent vertices in equivalent classes. Intersecting all such equivalences gives the least one. PositiveOutdegree(R) means every x has some y with R(x,y); PositiveIndegree(R) means every y has some x with R(x,y). Positive outdegree defines the successor on its classes; positive indegree makes that successor onto. On a finite vertex type the successor is therefore a permutation beta.

Definition 1.1 (Exact descent of assignments).

$$\forall V\in Typeu,\forall R\in V\to \left(V\to Prop\right),\forall K\in Typeu,\forall u\in K\to K,\mathrm{PositiveOutdegree}\left(R\right)\Rightarrow \mathrm{Equiv}\left(\mathrm{Assignments}\left(R,u\right),\mathrm{QuotientAssignments}\left(R,u\right)\right)$$

Formalization. D5/S3/FiniteGroups/SuccessorQuotient.assignmentEquiv (✓ std3).

Source. Repository-derived.

Commentary.

Assignments satisfy t(y)=u(t(x)) on every arrow x to y. Their equality relation is admissible directly from these equations. They consequently descend uniquely to the least quotient. Pullback is the inverse; no constancy hypothesis is assumed.

Theorem 1.2 (Functorial successor).

$$\forall V\in Typeu,\forall R\in V\to \left(V\to Prop\right),\mathrm{PositiveOutdegree}\left(R\right)\Rightarrow \left(\forall g\in \mathrm{relationAut}\left(R\right),\forall q\in \mathrm{Blocks}\left(R\right),\mathrm{blockHom}\left(R,g,\mathrm{successor}\left(R,q\right)\right)=\mathrm{successor}\left(R,\mathrm{blockHom}\left(R,g,q\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/SuccessorQuotient.block_successor_commute (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every relation automorphism preserves the least equivalence and induces a permutation of its classes. This induced action commutes with the successor.

Definition 1.3 (The actual block-action kernel).

$$\forall V\in Typeu,\forall R\in V\to \left(V\to Prop\right),\ker \left(\mathrm{blockHom}\left(R\right)\right)\to \left(\forall q\in \mathrm{Blocks}\left(R\right),\mathrm{Perm}\left(\mathrm{Fiber}\left(R,q\right)\right)\right)$$

Formalization. D5/S3/FiniteGroups/SuccessorQuotient.kernelRestriction (✓ std3).

Source. Repository-derived.

Commentary.

An element of the kernel preserves each actual fiber of the quotient map, so restriction defines a permutation of each fiber. These restrictions together determine the original permutation. The action on classes need not be faithful.

Theorem 1.4 (The centralizer and fiber bound).

$$\forall V\in Typeu,\forall R\in V\to \left(V\to Prop\right),\left(\mathrm{Finite}\left(V\right)\wedge \left(\mathrm{PositiveOutdegree}\left(R\right)\wedge \mathrm{PositiveIndegree}\left(R\right)\right)\right)\Rightarrow \mathrm{card}\left(\mathrm{relationAut}\left(R\right)\right)\le \mathrm{card}\left(\mathrm{centralizer}\left(\mathrm{beta}\left(R\right)\right)\right)\cdot \mathrm{card}\left(\mathrm{BlockPermutationProduct}\left(R\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/SuccessorQuotient.relation_aut_joint_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Here BlockPermutationProduct is the dependent product, over quotient classes q, of the symmetric group on Fiber(R,q); centralizer(beta) is the centralizer of the singleton containing beta inside the symmetric group on Blocks(R). The image of the block action lies in this centralizer. Its kernel injects into the displayed product. Kernel times image gives the bound, retaining all block permutations.

References

• Truth anchor: D5/S3/FiniteGroups/SuccessorQuotient.assignmentEquiv
• Truth anchor: D5/S3/FiniteGroups/SuccessorQuotient.block_successor_commute
• Truth anchor: D5/S3/FiniteGroups/SuccessorQuotient.kernelRestriction
• Truth anchor: D5/S3/FiniteGroups/SuccessorQuotient.relation_aut_joint_bound