ReidemeisterSchreier.Discrete.OpenSubgroups.Generators
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.
noncomputable def schreierTransversalRightCosetAction {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T) :
MulAction (FreeGroup X) T := by
letI : MulAction (FreeGroup X) (Quotient (QuotientGroup.rightRel L)) :=
rightCosetLeftMulActionByInverse L
let e : T ≃ Quotient (QuotientGroup.rightRel L) := hT.1.rightQuotientEquiv.symm
refine
{ smul := fun g t => e.symm (g • e t)
one_smul := by
intro t
change e.symm (1 • e t) = t
rw [one_smul]
exact e.left_inv t
mul_smul := by
intro g h t
change e.symm ((g * h) • e t) = e.symm (g • e (e.symm (h • e t)))
rw [mul_smul, e.apply_symm_apply] }The Schreier transversal itself carries the same right-coset action, transported along the equivalence with right cosets.
noncomputable def schreierRepresentative {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T) :
FreeGroup X → T :=
hT.1.toRightFunThe chosen representative of a right coset attached to a right Schreier transversal.
@[simp] theorem schreierRepresentative_eq_of_mem {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
{t : FreeGroup X} (ht : t ∈ T) :
schreierRepresentative (X := X) hT t = ⟨t, ht⟩The Schreier representative is the chosen transversal element determined by the stated subgroup-membership condition.
Show proof
by
apply (Subgroup.isComplement_iff_existsUnique_mul_inv_mem.mp hT.1 t).unique
· exact hT.1.mul_inv_toRightFun_mem t
· simp only [mul_inv_cancel, SetLike.mem_coe, one_mem]Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. 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.
□@[simp] theorem schreierRepresentative_eq_one_of_mem {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
{g : FreeGroup X} (hg : g ∈ L) :
schreierRepresentative (X := X) hT g = ⟨1, hT.2.1⟩The Schreier representative is the chosen transversal element determined by the stated subgroup-membership condition.
Show proof
by
apply (Subgroup.isComplement_iff_existsUnique_mul_inv_mem.mp hT.1 g).unique
· exact hT.1.mul_inv_toRightFun_mem g
· simpa using hgProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. 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.
□theorem schreierRepresentative_eq_of_mem_mul_inv_mem {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
{g t : FreeGroup X} (ht : t ∈ T) (hgt : g * t⁻¹ ∈ L) :
schreierRepresentative (X := X) hT g = ⟨t, ht⟩The Schreier representative is the chosen transversal element determined by the stated subgroup-membership condition.
Show proof
by
apply (Subgroup.isComplement_iff_existsUnique_mul_inv_mem.mp hT.1 g).unique
· exact hT.1.mul_inv_toRightFun_mem g
· exact hgtProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. Relator and normal-closure claims follow because rewriting the defining relators gives the subgroup presentation relators, and conjugating by transversal representatives stays inside the generated normal closure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. 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 prefixParent_mem_of_mem {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
{t : FreeGroup X} (ht : t ∈ T) :
FreeGroup.prefixParent t ∈ TMembership of a word in the prefix tree implies membership of its prefix parent.
Show proof
by
refine hT.2.2 ht ?_
refine ⟨(FreeGroup.toWord t).length - 1, Nat.sub_le (FreeGroup.toWord t).length 1, ?_⟩
simp only [prefixParent, List.dropLast_eq_take]Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. Relator and normal-closure claims follow because rewriting the defining relators gives the subgroup presentation relators, and conjugating by transversal representatives stays inside the generated normal closure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. 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 schreierTransversalRightCosetAction_smul {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
(g : FreeGroup X) (t : T) :
letIThe right-coset action updates a Schreier representative by multiplying on the right and then choosing the representative of the resulting coset.
Show proof
schreierTransversalRightCosetAction (X := X) hT
g • t = schreierRepresentative (X := X) hT ((t : FreeGroup X) * g⁻¹) := by
let e : T ≃ Quotient (QuotientGroup.rightRel L) := hT.1.rightQuotientEquiv.symm
have ht : e t = Quotient.mk'' (t : FreeGroup X) := by
simpa [e] using hT.1.mk''_rightQuotientEquiv (e t)
change
hT.1.rightQuotientEquiv (g • hT.1.rightQuotientEquiv.symm t) =
hT.1.rightQuotientEquiv (Quotient.mk'' ((t : FreeGroup X) * g⁻¹))
rw [ht, rightCosetLeftMulActionByInverse_mk_smul]Proof. Unfold the right-coset action and the Schreier representative function. The action formula is obtained by multiplying the chosen representative by the generator and then applying the transversal representative map to the resulting right coset.
□noncomputable def schreierGenerator {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T) (t : FreeGroup X) (x : X) : L := by
refine
⟨t * FreeGroup.of x *
((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X)⁻¹, ?_⟩
exact hT.1.mul_inv_toRightFun_mem (t * FreeGroup.of x)The Schreier expression attached to any word \(t\) and basis element \(x\).
abbrev NontrivialSchreierPair {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T) : Type u :=
{p : T × X // schreierGenerator (X := X) hT ((p.1 : T) : FreeGroup X) p.2 ≠ 1}The canonical index type for the nontrivial Schreier generators attached to a right Schreier transversal. This pair-indexed type is the preferred basis index; the value-set Schreier generator set records the same nontrivial generators by their subgroup values.
noncomputable def nontrivialSchreierPairGenerator {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T) :
NontrivialSchreierPair (X := X) hT → L :=
fun p => schreierGenerator (X := X) hT ((p.1.1 : T) : FreeGroup X) p.1.2The Schreier generator value represented by a nontrivial Schreier pair.
@[simp] theorem nontrivialSchreierPairGenerator_apply {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
(p : NontrivialSchreierPair (X := X) hT) :
nontrivialSchreierPairGenerator (X := X) hT p =
schreierGenerator (X := X) hT ((p.1.1 : T) : FreeGroup X) p.1.2The Schreier generator or pair map is evaluated by the chosen section and coset representative.
Show proof
rflProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. 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.
□def schreierGeneratorSet {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T) : Set L :=
{z | ∃ t ∈ T, ∃ x : X, z = schreierGenerator (X := X) hT t x ∧ z ≠ 1}The classical Schreier generator value set attached to a right Schreier transversal. This value set records the resulting Schreier generators, while the nontrivial Schreier pairs provide the preferred basis index.
@[simp] theorem mem_schreierGeneratorSet_iff {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T) {z : L} :
z ∈ schreierGeneratorSet (X := X) hT ↔
∃ t ∈ T, ∃ x : X, z = schreierGenerator (X := X) hT t x ∧ z ≠ 1Show proof
Iff.rflProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. Relator and normal-closure claims follow because rewriting the defining relators gives the subgroup presentation relators, and conjugating by transversal representatives stays inside the generated normal closure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. 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 schreierGenerator_mem_schreierGeneratorSet_of_mem_of_ne_one
{X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
{t : FreeGroup X} (ht : t ∈ T) (x : X)
(hne : schreierGenerator (X := X) hT t x ≠ 1) :
schreierGenerator (X := X) hT t x ∈ schreierGeneratorSet (X := X) hTShow proof
⟨t, ht, x, rfl, hne⟩Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. Relator and normal-closure claims follow because rewriting the defining relators gives the subgroup presentation relators, and conjugating by transversal representatives stays inside the generated normal closure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. 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 schreierGenerator_mem_schreierGeneratorSet_of_ne_one
{X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
(t : T) (x : X)
(hne : schreierGenerator (X := X) hT (t : FreeGroup X) x ≠ 1) :
schreierGenerator (X := X) hT (t : FreeGroup X) x ∈
schreierGeneratorSet (X := X) hTShow proof
schreierGenerator_mem_schreierGeneratorSet_of_mem_of_ne_one
(X := X) hT t.property x hneProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. Relator and normal-closure claims follow because rewriting the defining relators gives the subgroup presentation relators, and conjugating by transversal representatives stays inside the generated normal closure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. 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 schreierGeneratorSet_eq_range_nontrivialSchreierPairGenerator
{X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T) :
schreierGeneratorSet (X := X) hT =
Set.range (nontrivialSchreierPairGenerator (X := X) hT)The value-set formulation is precisely the range of the pair-indexed generator map.
Show proof
by
ext z
constructor
· intro hz
rcases hz with ⟨t, ht, x, hz, hne⟩
refine ⟨⟨(⟨t, ht⟩, x), ?_⟩, ?_⟩
· simpa [hz] using hne
· simp only [nontrivialSchreierPairGenerator, hz]
· rintro ⟨p, rfl⟩
exact schreierGenerator_mem_schreierGeneratorSet_of_ne_one
(X := X) hT p.1.1 p.1.2 p.2Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. 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.
□@[simp] theorem schreierGenerator_eq_one_of_mem {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
{t : FreeGroup X} {x : X}
(htx : t * FreeGroup.of x ∈ T) :
schreierGenerator (X := X) hT t x = 1The Schreier generator is trivial exactly in the corresponding subgroup-membership case.
Show proof
by
apply Subtype.ext
simp only [schreierGenerator, schreierRepresentative_eq_of_mem (X := X) hT htx, mul_inv_rev, mul_assoc,
mul_inv_cancel_left, mul_inv_cancel, OneMemClass.coe_one]Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. 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.
□@[simp] theorem schreierGenerator_eq_of_mul_mem {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
{t : FreeGroup X} {x : X}
(htx : t * FreeGroup.of x ∈ L) :
schreierGenerator (X := X) hT t x = ⟨t * FreeGroup.of x, htx⟩If the representative-generator product lies in the subgroup, the corresponding Schreier generator is the represented subgroup element.
Show proof
by
apply Subtype.ext
simp only [schreierGenerator, schreierRepresentative_eq_one_of_mem (X := X) hT htx, inv_one, mul_one]Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. 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.
□theorem schreierGenerator_eq_one_iff {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
{hT : IsRightSchreierTransversal (X := X) L T}
{t : FreeGroup X} {x : X} :
schreierGenerator (X := X) hT t x = 1 ↔
((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X) =
t * FreeGroup.of xThe Schreier generator is trivial exactly under the corresponding coset condition.
Show proof
by
constructor
· intro h
have hval : t * FreeGroup.of x *
(((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X))⁻¹ = 1 := by
exact congrArg Subtype.val h
have hmul := congrArg
(fun g : FreeGroup X =>
g * ((schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T) : FreeGroup X)) hval
simpa [mul_assoc] using hmul.symm
· intro hrep
apply Subtype.ext
simp only [schreierGenerator, hrep, mul_inv_rev, mul_assoc, mul_inv_cancel_left, mul_inv_cancel,
OneMemClass.coe_one]Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. 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.
□theorem exists_rightSchreierTransversal_of_minimalGeneratorPower
{X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} (x : X) {N : ℕ}
(hN : 0 < N)
(hpow : (FreeGroup.of x) ^ N ∈ L)
(hmin : ∀ m : ℕ, 0 < m → m < N → (FreeGroup.of x) ^ m ∉ L) :
∃ T : Set (FreeGroup X), ∃ hT : IsRightSchreierTransversal (X := X) L T,
(FreeGroup.of x) ^ (N - 1) ∈ T ∧
schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x =
⟨(FreeGroup.of x) ^ N, hpow⟩Show proof
by
let T₀ : Set (FreeGroup X) := Set.range fun i : Fin N => (FreeGroup.of x) ^ (i : ℕ)
have hT₀ : IsRightPartialSchreierTransversal (X := X) L T₀ :=
isRightPartialSchreierTransversal_generatorPowers_of_minimalPower
(X := X) (L := L) x hN hmin
rcases exists_rightSchreierTransversal_of_partial (X := X) (L := L) hT₀ with
⟨T, hsub, hT⟩
have hpred : (FreeGroup.of x) ^ (N - 1) ∈ T := by
apply hsub
exact ⟨⟨N - 1, Nat.pred_lt (Nat.ne_of_gt hN)⟩, rfl⟩
have hmul :
(FreeGroup.of x) ^ (N - 1) * FreeGroup.of x = (FreeGroup.of x) ^ N := by
calc
(FreeGroup.of x) ^ (N - 1) * FreeGroup.of x = (FreeGroup.of x) ^ ((N - 1).succ) := by
rw [pow_succ]
_ = (FreeGroup.of x) ^ N := by
simpa using congrArg (fun n : ℕ => (FreeGroup.of x) ^ n) (Nat.succ_pred_eq_of_pos hN)
have hmul_mem : (FreeGroup.of x) ^ (N - 1) * FreeGroup.of x ∈ L := by
rw [hmul]
exact hpow
refine ⟨T, hT, hpred, ?_⟩
calc
schreierGenerator (X := X) hT ((FreeGroup.of x) ^ (N - 1)) x =
⟨(FreeGroup.of x) ^ (N - 1) * FreeGroup.of x, hmul_mem⟩ := by
exact schreierGenerator_eq_of_mul_mem (X := X) hT hmul_mem
_ = ⟨(FreeGroup.of x) ^ N, hpow⟩ := by
apply Subtype.ext
exact hmulProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem schreierRepresentative_eq_prefixParent_of_cancels {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
{t : FreeGroup X} {x : X}
(ht : t ∈ T) (hw : FreeGroup.toWord t ≠ [])
(hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
schreierRepresentative (X := X) hT (t * FreeGroup.of x) =
⟨FreeGroup.prefixParent t, prefixParent_mem_of_mem (X := X) hT ht⟩If the last letter of a transversal word cancels with x, the Schreier representative of t x is the prefix parent of t.
Show proof
by
rw [Internal.FreeGroupWord.FreeGroup.mul_of_eq_prefixParent_of_cancels t x hw hlast]
exact schreierRepresentative_eq_of_mem (X := X) hT (prefixParent_mem_of_mem (X := X) hT ht)Proof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. 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.
□theorem schreierRepresentative_eq_of_prefixParent_last_pos {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
{t : FreeGroup X} (ht : t ∈ T) {x : X}
(hw : FreeGroup.toWord t ≠ [])
(hlast : (FreeGroup.toWord t).getLast hw = (x, true)) :
schreierRepresentative (X := X) hT (FreeGroup.prefixParent t * FreeGroup.of x) = ⟨t, ht⟩If a transversal word ends in x, the Schreier representative of its prefix parent multiplied by x is the original word.
Show proof
by
rw [Internal.FreeGroupWord.FreeGroup.prefixParent_mul_of_of_last_pos t x hw hlast]
exact schreierRepresentative_eq_of_mem (X := X) hT htProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. 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.
□@[simp] theorem schreierGenerator_eq_one_of_cancels {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
{t : FreeGroup X} {x : X}
(ht : t ∈ T) (hw : FreeGroup.toWord t ≠ [])
(hlast : (FreeGroup.toWord t).getLast hw = (x, false)) :
schreierGenerator (X := X) hT t x = 1If the last letter of a transversal word cancels with x, the corresponding Schreier generator is trivial.
Show proof
by
apply schreierGenerator_eq_one_of_mem (X := X) hT
rw [Internal.FreeGroupWord.FreeGroup.mul_of_eq_prefixParent_of_cancels t x hw hlast]
exact prefixParent_mem_of_mem (X := X) hT htProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. 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.
□@[simp] theorem schreierGenerator_eq_one_of_prefixParent_last_pos {X : Type u} [DecidableEq X]
{L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
{t : FreeGroup X} (ht : t ∈ T) {x : X}
(hw : FreeGroup.toWord t ≠ [])
(hlast : (FreeGroup.toWord t).getLast hw = (x, true)) :
schreierGenerator (X := X) hT (FreeGroup.prefixParent t) x = 1If a transversal word ends in x, the Schreier generator attached to its prefix parent and x is trivial.
Show proof
by
apply schreierGenerator_eq_one_of_mem (X := X) hT
rw [Internal.FreeGroupWord.FreeGroup.prefixParent_mul_of_of_last_pos t x hw hlast]
exact htProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. 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.
□