FenchelNielsenZomorrodian.Discrete.Singerman.CyclicSchreierKernel
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
def CyclicSchreierRelatorData
{X Y : Type} [DecidableEq X] {N : ℕ} [NeZero N] {rels : Set (FreeGroup X)}
(f : X → Multiplicative (ZMod N))
(x : X)
(hx : FreeGroup.lift f (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))
(targetRelators : Set (FreeGroup Y)) : Type :=
(let φ : FreeGroup X →* Multiplicative (ZMod N) := 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
ReidemeisterSchreier.Discrete.Presentations.RelatorQuotientMutualMapData
(ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e
(ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet (f := f) (rels := rels) T))
targetRelators)Relator-quotient mutual map data for the cyclic Schreier kernel presentation.
noncomputable def cyclicSchreierKernelEquivPresentedGroupOfRelatorData
{X Y : 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))
(targetRelators : Set (FreeGroup Y))
(hData : CyclicSchreierRelatorData (rels := rels) f x hx targetRelators) :
(PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker ≃*
PresentedGroup targetRelators := by
classical
let φ : FreeGroup X →* Multiplicative (ZMod N) := 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
let R : Set (FreeGroup ↥(schreierGeneratorSet hT)) :=
ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet e
(ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet (f := f) (rels := rels) T)
let hTarget :
FreeGroup ↥(schreierGeneratorSet hT) ⧸ Subgroup.normalClosure R ≃*
PresentedGroup targetRelators :=
ReidemeisterSchreier.Discrete.Presentations.quotientEquivOfRelatorQuotientMutualMapData R targetRelators
(by simpa [CyclicSchreierRelatorData, φ, T, hT, e, R] using hData)
let hKernel :
FreeGroup ↥(schreierGeneratorSet hT) ⧸ Subgroup.normalClosure R ≃*
(PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker := by
simpa [φ, T, hT, e, R] using
(presentedFreeKernelCyclicSchreierRelatorQuotientEquivPresentedKernel
(N := N) (rels := rels) (f := f) hrels x hx)
exact hKernel.symm.trans hTargetCyclic Schreier relator data identifies the presented kernel of a cyclic quotient with the target presented group.
def FuchsianEllipticCyclicRelatorData
{p : ℕ} [NeZero p] {Y : Type} (σ : FuchsianSignature)
(ξ : Fin σ.numPeriods → Multiplicative (ZMod p))
(i₀ : Fin σ.numPeriods)
(hi₀ : ξ i₀ = Multiplicative.ofAdd (1 : ZMod p))
(targetRelators : Set (FreeGroup Y)) : Type :=
(letI := Classical.decEq (FuchsianGenerator σ)
let f := ellipticQuotientGeneratorImage σ ξ
let x := FuchsianGenerator.elliptic i₀
let hx :
FreeGroup.lift f (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
simp only [FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage, hi₀, f, x]
CyclicSchreierRelatorData (N := p) (rels := relators σ) f x hx targetRelators)Cyclic Schreier relator data for an elliptic quotient of a Fuchsian presentation and the chosen target relators.
def FuchsianEllipticCyclicSchreierRelatorData
{p : ℕ} [NeZero p] (σ τ : FuchsianSignature)
(ξ : Fin σ.numPeriods → Multiplicative (ZMod p))
(i₀ : Fin σ.numPeriods)
(hi₀ : ξ i₀ = Multiplicative.ofAdd (1 : ZMod p)) : Type :=
FuchsianEllipticCyclicRelatorData σ ξ i₀ hi₀ (relators τ)noncomputable def fuchsianEllipticCyclicKernelEquivPresentedGroupOfRelatorData
{p : ℕ} [NeZero p] {Y : Type} (σ : FuchsianSignature)
(ξ : Fin σ.numPeriods → Multiplicative (ZMod p))
(hpow : ∀ i, ξ i ^ σ.periods i = 1)
(hprod : ∏ i : Fin σ.numPeriods, ξ i = 1)
(i₀ : Fin σ.numPeriods)
(hi₀ : ξ i₀ = Multiplicative.ofAdd (1 : ZMod p))
(targetRelators : Set (FreeGroup Y))
(D : FuchsianEllipticCyclicRelatorData σ ξ i₀ hi₀ targetRelators) :
(ellipticQuotientHom σ ξ hpow hprod).ker ≃*
PresentedGroup targetRelators := by
classical
letI := Classical.decEq (FuchsianGenerator σ)
let f := ellipticQuotientGeneratorImage σ ξ
let x := FuchsianGenerator.elliptic i₀
let hx :
FreeGroup.lift f (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod p) := by
simp only [FreeGroup.lift_apply_of, ellipticQuotientGeneratorImage, hi₀, f, x]
let hrels : ∀ r ∈ relators σ, FreeGroup.lift f r = 1 :=
ellipticQuotientGeneratorImage_respects_relators σ ξ hpow hprod
have hD :
CyclicSchreierRelatorData (N := p) (rels := relators σ) f x hx targetRelators := by
simpa [FuchsianEllipticCyclicRelatorData, f, x, hx] using D
simpa [ellipticQuotientHom, f, x, hx, hrels] using
cyclicSchreierKernelEquivPresentedGroupOfRelatorData
(N := p) (rels := relators σ) f hrels x hx targetRelators hDFuchsian elliptic cyclic relator data identifies the elliptic-quotient kernel with the target presented group.
noncomputable def fuchsianEllipticCyclicKernelEquivOfRelatorData
{p : ℕ} [NeZero p] (σ τ : FuchsianSignature)
(ξ : Fin σ.numPeriods → Multiplicative (ZMod p))
(hpow : ∀ i, ξ i ^ σ.periods i = 1)
(hprod : ∏ i : Fin σ.numPeriods, ξ i = 1)
(i₀ : Fin σ.numPeriods)
(hi₀ : ξ i₀ = Multiplicative.ofAdd (1 : ZMod p))
(D : FuchsianEllipticCyclicSchreierRelatorData σ τ ξ i₀ hi₀) :
(ellipticQuotientHom σ ξ hpow hprod).ker ≃*
FuchsianPresentedGroup τ :=
fuchsianEllipticCyclicKernelEquivPresentedGroupOfRelatorData
σ ξ hpow hprod i₀ hi₀ (relators τ) DFuchsian elliptic cyclic Schreier relator data identifies the elliptic-quotient kernel with the target Fuchsian presented group.
theorem freeGroupGeneratorPower_mem_range_cyclicQuotientRightRep
{X : Type*} {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))Show proof
by
classical
letI : NeZero N := ⟨Nat.ne_of_gt (lt_of_le_of_lt (Nat.zero_le m) hm)⟩
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. 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.
□private theorem freeGroupGeneratorPower_mul_generator_mem_range_cyclicQuotientRightRep
{X : Type*} {N : ℕ}
(φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)
(hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))
{k : ℕ} (hk : k + 1 < N) :
(FreeGroup.of x) ^ k * FreeGroup.of x ∈
Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))A distinguished-generator power followed by the generator lies in the range of the cyclic quotient right representative before wraparound.
Show proof
by
simpa [pow_succ] using
freeGroupGeneratorPower_mem_range_cyclicQuotientRightRep φ x hx (m := k + 1) hkProof. 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 cyclicQuotient_distinguished_schreierGenerator_eq_one_of_succ_lt
{X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]
(φ : FreeGroup X →* Multiplicative (ZMod N)) (x : X)
(hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))
{k : ℕ} (hk : k + 1 < N) :
let TShow proof
Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
schreierGenerator hT ((FreeGroup.of x) ^ k) x = 1 := by
classical
let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
exact schreierGenerator_eq_one_of_mem hT
(freeGroupGeneratorPower_mul_generator_mem_range_cyclicQuotientRightRep φ x hx hk)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. 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. 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 cyclicQuotient_distinguished_schreierGenerator_wrap_eq
{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
schreierGenerator hT ((FreeGroup.of x) ^ (N - 1)) x =
(⟨(FreeGroup.of x) ^ N, by
rw [MonoidHom.mem_ker]
rw [map_pow, hx]
apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective
simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]⟩ : φ.ker) := by
classical
let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
apply Subtype.ext
have hpowKer : (FreeGroup.of x) ^ N ∈ φ.ker := by
rw [MonoidHom.mem_ker]
rw [map_pow, hx]
apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective
simp only [toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, CharP.cast_eq_zero, mul_one, toAdd_one]
have hNpos : 0 < N := Nat.pos_of_ne_zero (NeZero.ne N)
have hsucc : N - 1 + 1 = N := Nat.sub_add_cancel (Nat.succ_le_iff.mpr hNpos)
have hprod : (FreeGroup.of x) ^ (N - 1) * FreeGroup.of x = (FreeGroup.of x) ^ N := by
rw [← pow_succ, hsucc]
have hprodKer : (FreeGroup.of x) ^ (N - 1) * FreeGroup.of x ∈ φ.ker := by
simpa [hprod] using hpowKer
simp only [schreierGenerator, hprod, schreierRepresentative_eq_one_of_mem hT hpowKer, inv_one, mul_one]Proof. Unfold the named Fenchel--Nielsen reduction, cyclic-Schreier word, or total-relation definition. The equality or membership follows by evaluating the relevant generator branch, simplifying the period or product formula, and using that normal closures are closed under products, inverses, and conjugation when a relator membership is involved.
□theorem cyclicQuotient_trivialImage_schreierGenerator_eq_conj
{X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]
(φ : FreeGroup X →* Multiplicative (ZMod N)) (x y : X)
(hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))
(hy : φ (FreeGroup.of y) = 1) (k : Fin N) :
let TShow proof
Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
schreierGenerator hT ((FreeGroup.of x) ^ k.val) y =
(⟨(FreeGroup.of x) ^ k.val * FreeGroup.of y *
((FreeGroup.of x) ^ k.val)⁻¹, by
rw [MonoidHom.mem_ker]
simp only [map_mul, map_pow, hx, hy, mul_one, map_inv, mul_inv_cancel]⟩ : φ.ker) := by
classical
let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
let t : FreeGroup X := (FreeGroup.of x) ^ k.val
have ht : t ∈ T := by
simpa [T, t] using
freeGroupGeneratorPower_mem_range_cyclicQuotientRightRep φ x hx (m := k.val) k.isLt
have hker : (t * FreeGroup.of y) * t⁻¹ ∈ φ.ker := by
rw [MonoidHom.mem_ker]
simp only [map_mul, map_pow, hx, hy, mul_one, map_inv, mul_inv_cancel, t]
apply Subtype.ext
simp only [schreierGenerator, schreierRepresentative_eq_of_mem_mul_inv_mem hT ht hker, t]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. 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. 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 cyclicQuotient_negOneImage_schreierGenerator_eq
{X : Type*} [DecidableEq X] {N : ℕ} [NeZero N]
(φ : FreeGroup X →* Multiplicative (ZMod N)) (x y : X)
(hx : φ (FreeGroup.of x) = Multiplicative.ofAdd (1 : ZMod N))
(hy : φ (FreeGroup.of y) = Multiplicative.ofAdd (-1 : ZMod N)) (k : Fin N) :
let TShow proof
Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
let r : ℕ := ((k.val : ZMod N) - 1).val
schreierGenerator hT ((FreeGroup.of x) ^ k.val) y =
(⟨(FreeGroup.of x) ^ k.val * FreeGroup.of y *
((FreeGroup.of x) ^ r)⁻¹, by
rw [MonoidHom.mem_ker]
rw [map_mul, map_inv, map_mul, map_pow, map_pow, hx, hy]
apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective
simp only [ofAdd_neg, toAdd_mul, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, mul_one, toAdd_inv, ZMod.natCast_val,
dvd_refl, ZMod.cast_sub, ZMod.cast_natCast, ZMod.cast_one, neg_sub, toAdd_one, r]
ring⟩ : φ.ker) := by
classical
let T := Set.range (cyclicQuotientRightRep φ (FreeGroup.of x))
let hT : IsRightSchreierTransversal φ.ker T :=
cyclicQuotientRightRep_isRightSchreierTransversal_of_freeGroupGenerator φ x hx
let r : ℕ := ((k.val : ZMod N) - 1).val
let t : FreeGroup X := (FreeGroup.of x) ^ k.val
let u : FreeGroup X := (FreeGroup.of x) ^ r
have hu : u ∈ T := by
simpa [T, u, r] using
freeGroupGeneratorPower_mem_range_cyclicQuotientRightRep
φ x hx (m := r) (ZMod.val_lt ((k.val : ZMod N) - 1))
have hker : (t * FreeGroup.of y) * u⁻¹ ∈ φ.ker := by
rw [MonoidHom.mem_ker]
rw [map_mul, map_inv, map_mul, map_pow, map_pow, hx, hy]
apply (Multiplicative.toAdd : Multiplicative (ZMod N) ≃ ZMod N).injective
simp only [ofAdd_neg, toAdd_mul, toAdd_pow, toAdd_ofAdd, nsmul_eq_mul, mul_one, toAdd_inv, ZMod.natCast_val,
dvd_refl, ZMod.cast_sub, ZMod.cast_natCast, ZMod.cast_one, neg_sub, toAdd_one, r]
ring
apply Subtype.ext
simp only [schreierGenerator, schreierRepresentative_eq_of_mem_mul_inv_mem hT hu hker, u, r, t]Proof. Unfold the named Fenchel--Nielsen reduction, cyclic-Schreier word, or total-relation definition. The equality or membership follows by evaluating the relevant generator branch, simplifying the period or product formula, and using that normal closures are closed under products, inverses, and conjugation when a relator membership is involved.
□