FenchelNielsenZomorrodian.Discrete.Singerman.CyclicQuotientActions
This module develops the rewriting and basis constructions behind the subgroup calculations. It tracks words and relations through the chosen transversal to obtain the required presentation or basis statements.
import
noncomputable def cyclicQuotientRightRep
{G : Type*} [Group G] {N : ℕ}
(φ : G →* Multiplicative (ZMod N)) (t : G) :
Quotient (QuotientGroup.rightRel φ.ker) → G :=
Quotient.lift
(fun g => t ^ (Multiplicative.toAdd (φ g)).val)
(by
intro a b hab
have hab' : QuotientGroup.rightRel φ.ker a b := hab
rw [QuotientGroup.rightRel_apply] at hab'
have habφ : φ a = φ b := by
have habφ' : φ b = φ a := by
apply eq_of_mul_inv_eq_one
simpa [map_mul, map_inv] using MonoidHom.mem_ker.mp hab'
exact habφ'.symm
have hval :
(Multiplicative.toAdd (φ a)).val = (Multiplicative.toAdd (φ b)).val := by
exact congrArg ZMod.val (congrArg Multiplicative.toAdd habφ)
simp only [hval])The cyclic quotient acts by the right-regular representation on the quotient index set.
@[simp 900] theorem cyclicQuotientRightRep_spec
{G : Type*} [Group G] {N : ℕ} [NeZero N]
(φ : G →* Multiplicative (ZMod N)) (t : G)
(ht : φ t = Multiplicative.ofAdd (1 : ZMod N))
(q : Quotient (QuotientGroup.rightRel φ.ker)) :
Quotient.mk'' (cyclicQuotientRightRep φ t q) = qThe cyclic quotient right representation has the prescribed action on generators.
Show proof
by
refine Quotient.inductionOn' q ?_
intro g
apply Quotient.sound'
rw [QuotientGroup.rightRel_apply]
rw [MonoidHom.mem_ker]
have hk :
Multiplicative.ofAdd (((Multiplicative.toAdd (φ g)).val : ℕ) : ZMod N) = φ g := by
exact congrArg Multiplicative.ofAdd
(ZMod.natCast_zmod_val (Multiplicative.toAdd (φ g)))
rw [show cyclicQuotientRightRep φ t (Quotient.mk'' g) =
t ^ (Multiplicative.toAdd (φ g)).val by rfl]
rw [map_mul, MonoidHom.map_inv, MonoidHom.map_pow, ← hk, ht]
apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective
simp only [ZMod.natCast_val, ZMod.cast_id', id_eq, ofAdd_toAdd, toAdd_mul, toAdd_inv, toAdd_pow, toAdd_ofAdd,
nsmul_eq_mul, mul_one, add_neg_cancel, toAdd_one]Proof. Check the quotient data on the named elliptic, surface, cusp, and boundary generators. The period, power, and product relators follow from the displayed order and product calculations, so the presentation universal property supplies the quotient map; derived-length, smoothness, and profinite fields are inherited from the finite or profinite quotient construction.
□theorem ker_isComplement_range_cyclicQuotientRightRep
{G : Type*} [Group G] {N : ℕ} [NeZero N]
(φ : G →* Multiplicative (ZMod N)) (t : G)
(ht : φ t = Multiplicative.ofAdd (1 : ZMod N)) :
Subgroup.IsComplement (φ.ker : Set G) (Set.range (cyclicQuotientRightRep φ t))The cyclic right representative set complements the kernel.
Show proof
Subgroup.isComplement_range_right (cyclicQuotientRightRep_spec φ t ht)Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Kernel and normal-closure claims are proved by showing that each rewritten relator lies in the generated normal subgroup and that the quotient map kills exactly those relations required by the presentation. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem one_mem_range_cyclicQuotientRightRep
{G : Type*} [Group G] {N : ℕ}
(φ : G →* Multiplicative (ZMod N)) (t : G) :
(1 : G) ∈ Set.range (cyclicQuotientRightRep φ t)The chosen right-representative set for the cyclic quotient contains the identity element.
Show proof
by
refine ⟨Quotient.mk'' (1 : G), ?_⟩
simp only [cyclicQuotientRightRep, Quotient.lift_mk, map_one, toAdd_one, ZMod.val_zero, pow_zero]Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Kernel and normal-closure claims are proved by showing that each rewritten relator lies in the generated normal subgroup and that the quotient map kills exactly those relations required by the presentation. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□theorem generatorPower_mem_range_cyclicQuotientRightRep
{X : Type*} {N : ℕ} [NeZero N]
(φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)
(hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))
{m : ℕ} (hm : m < N) :
(FreeGroup.of x) ^ m ∈ Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))Powers below the modulus of the distinguished free generator lie in the representative set.
Show proof
by
classical
refine ⟨Quotient.mk'' ((FreeGroup.of x) ^ m), ?_⟩
have hφm : φ ((FreeGroup.of x) ^ m) = Multiplicative.ofAdd ((m : ℕ) : ZMod N) := by
rw [map_pow, hx]
apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective
simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, mul_one]
have hval : (Multiplicative.toAdd (φ ((FreeGroup.of x) ^ m))).val = m := by
rw [hφm]
simpa using (ZMod.val_natCast_of_lt hm)
change (FreeGroup.of x) ^ (Multiplicative.toAdd (φ ((FreeGroup.of x) ^ m))).val =
(FreeGroup.of x) ^ m
rw [hval]Proof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Kernel and normal-closure claims are proved by showing that each rewritten relator lies in the generated normal subgroup and that the quotient map kills exactly those relations required by the presentation. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□theorem mem_range_cyclicQuotientRightRep_iff_generatorPower
{X : Type*} {N : ℕ} [NeZero N]
(φ : FreeGroup X →* Multiplicative (ZMod N)) {x : X}
(hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))
{t : FreeGroup X} :
t ∈ Set.range (cyclicQuotientRightRep φ (FreeGroup.of x)) ↔
∃ k : Fin N, t = (FreeGroup.of x) ^ k.valMembership in the range of the cyclic quotient right representative is equivalent to being a bounded power of the distinguished generator.
Show proof
by
constructor
· intro ht
rcases ht with ⟨q, rfl⟩
refine Quotient.inductionOn' q ?_
intro g
exact
⟨⟨(Multiplicative.toAdd (φ g)).val,
ZMod.val_lt (Multiplicative.toAdd (φ g))⟩, rfl⟩
· rintro ⟨k, rfl⟩
exact generatorPower_mem_range_cyclicQuotientRightRep φ x hx k.isLtProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Kernel and normal-closure claims are proved by showing that each rewritten relator lies in the generated normal subgroup and that the quotient map kills exactly those relations required by the presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. The Reidemeister--Schreier step tracks the transversal representative before and after each letter. Trivial Schreier generators are removed when the next representative is unchanged, while nontrivial generators record exactly the subgroup correction; products of these corrections reconstruct the original word inside the subgroup presentation.
□theorem cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator
{X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]
(φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)
(hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N)) :
let TThe chosen Schreier representative is compatible with the quotient class and the induced right-coset action.
Show proof
Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
IsRightSchreierTransversal φ.ker T := by
let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
refine ⟨?_, ?_, ?_⟩
· simpa [T] using
ker_isComplement_range_cyclicQuotientRightRep φ (FreeGroup.of x) hx
· simpa [T] using
one_mem_range_cyclicQuotientRightRep φ (FreeGroup.of x)
· intro t ht
rcases ht with ⟨q, rfl⟩
refine Quotient.inductionOn' q ?_
intro g u hu
have hrep :
cyclicQuotientRightRep φ (FreeGroup.of x) (Quotient.mk'' g) =
(FreeGroup.of x) ^ (Multiplicative.toAdd (φ g)).val := rfl
rw [hrep] at hu
rcases hu with ⟨m, hm, rfl⟩
have hm' : m ≤ (Multiplicative.toAdd (φ g)).val := by
simpa [FreeGroup.toWord_of_pow, List.length_replicate] using hm
have hmlt : m < N := lt_of_le_of_lt hm' (ZMod.val_lt (Multiplicative.toAdd (φ g)))
rw [FreeGroup.toWord_of_pow, List.take_replicate, min_eq_left hm',
← FreeGroup.toWord_of_pow, FreeGroup.mk_toWord]
exact generatorPower_mem_range_cyclicQuotientRightRep φ x hx hmltProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□noncomputable def freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator
{X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]
(φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)
(hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N)) :
let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker := by
let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
exact schreierGeneratorInverseBasisEquiv (X := X) hT@[simp 900] theorem freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator_of
{X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]
(φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)
(hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N)) :
let TShow proof
Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
∀ z : ↥(schreierGeneratorSet hT),
freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator φ x hx (FreeGroup.of z) =
(z : φ.ker)⁻¹ := by
classical
dsimp
let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
intro z
exact schreierGeneratorInverseBasisEquiv_of (X := X) hT zProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Kernel and normal-closure claims are proved by showing that each rewritten relator lies in the generated normal subgroup and that the quotient map kills exactly those relations required by the presentation. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□noncomputable def presentedFreeKernelCyclicSchreierRelatorQuotientEquivPresentedKernel
{X : Type*} [DecidableEq X] {N : ℕ} [NeZero N] {rels : Set (FreeGroup X)}
{f : X → Multiplicative (ZMod N)}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1)
(x : X)
(hx : FreeGroup.lift f (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N)) :
let φ := FreeGroup.lift f
let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator φ x hx
FreeGroup ↥(schreierGeneratorSet hT) ⧸
Subgroup.normalClosure
(ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e
(ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet (f := f) (rels := rels) T)) ≃*
(PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker := by
classical
let φ : FreeGroup X →* Multiplicative (ZMod N) := FreeGroup.lift f
let T : Set (FreeGroup X) := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
let e : FreeGroup ↥(schreierGeneratorSet hT) ≃* φ.ker :=
freeGroupKernelSchreierBasisEquivOfCyclicQuotientGenerator φ x hx
simpa [φ, T, hT, e] using
ReidemeisterSchreier.Discrete.Presentations.presentedFreeKernelSchreierRelatorQuotientEquivPresentedKernel hrels hT.1 eThe relator quotient built from the cyclic Schreier kernel presentation is equivalent to the presented kernel.