ReidemeisterSchreier.Discrete.Presentations.KernelQuotient
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.
theorem presentedGroup_toGroup_ker_eq_map_freeGroupLift_ker
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
(PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker =
Subgroup.map (PresentedGroup.mk rels) (FreeGroup.lift f).kerThe presented-kernel quotient is identified with the Reidemeister--Schreier relator quotient.
Show proof
by
exact QuotientGroup.ker_lift (Subgroup.normalClosure rels) (FreeGroup.lift f)
(PresentedGroup.to_group_eq_one_of_mem_closure hrels)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. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. 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.
□def presentedFreeKernelToPresentedKernelHom
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
(FreeGroup.lift f).ker →*
(PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker where
toFun k :=
⟨PresentedGroup.mk rels k, by
change FreeGroup.lift f (k : FreeGroup X) = 1
exact k.property⟩
map_one' := by
ext
simp only [OneMemClass.coe_one, map_one]
map_mul' k l := by
ext
simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]The Reidemeister--Schreier map is determined on generators and respects the rewritten relator relations.
theorem presentedFreeKernelToPresentedKernelHom_surjective
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
Function.Surjective (presentedFreeKernelToPresentedKernelHom hrels)The Reidemeister--Schreier identity follows from the corresponding rewriting calculation.
Show proof
by
intro y
have hy :
(y : PresentedGroup rels) ∈
Subgroup.map (PresentedGroup.mk rels) (FreeGroup.lift f).ker := by
rw [← presentedGroup_toGroup_ker_eq_map_freeGroupLift_ker hrels]
exact y.property
rcases hy with ⟨x, hx, hxy⟩
refine ⟨⟨x, hx⟩, ?_⟩
ext
exact hxyProof. 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 surjectivity, choose a representative of the target coordinate and lift it through the underlying surjective group, quotient, or coefficient map. The defining formula for the induced map sends the constructed preimage to the chosen representative at every finite stage, so inverse-limit extensionality gives the required global preimage. 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 presentedFreeKernelToPresentedKernelHom_ker_eq_comap_normalClosure
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
(presentedFreeKernelToPresentedKernelHom hrels).ker =
Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels)The indicated normal closure agrees with the normal closure transported through the Reidemeister--Schreier relator comparison.
Show proof
by
ext k
constructor
· intro hk
rw [MonoidHom.mem_ker] at hk
have hkval := congrArg Subtype.val hk
change PresentedGroup.mk rels (k : FreeGroup X) = 1 at hkval
exact PresentedGroup.mk_eq_one_iff.mp hkval
· intro hk
rw [MonoidHom.mem_ker]
apply Subtype.ext
change PresentedGroup.mk rels (k : FreeGroup X) = 1
exact PresentedGroup.mk_eq_one_iff.mpr hkProof. 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. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. 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.
□noncomputable def presentedFreeKernelRelatorQuotientEquivPresentedKernel
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
(FreeGroup.lift f).ker ⧸
Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels) ≃*
(PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker :=
(QuotientGroup.quotientMulEquivOfEq
(presentedFreeKernelToPresentedKernelHom_ker_eq_comap_normalClosure hrels).symm).trans
(QuotientGroup.quotientKerEquivOfSurjective
(φ := presentedFreeKernelToPresentedKernelHom hrels)
(presentedFreeKernelToPresentedKernelHom_surjective hrels))The presented-kernel quotient is identified with the Reidemeister--Schreier relator quotient.
def freeKernelConjugateRelatorSet
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A} :
Set (FreeGroup.lift f).ker :=
{ z | ∃ g : FreeGroup X, ∃ r ∈ rels, (z : FreeGroup X) = g * r * g⁻¹ }The Reidemeister--Schreier relator identity is obtained by rewriting the original relator with the chosen transversal.
def freeKernelTransversalRelatorSet
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(T : Set (FreeGroup X)) :
Set (FreeGroup.lift f).ker :=
{ z | ∃ t ∈ T, ∃ r ∈ rels, (z : FreeGroup X) = t * r * t⁻¹ }The Reidemeister--Schreier relator identity is obtained by rewriting the original relator with the chosen transversal.
theorem freeKernelTransversalRelatorSet_subset_conjugateRelatorSet
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(T : Set (FreeGroup X)) :
freeKernelTransversalRelatorSet (f := f) (rels := rels) T ⊆
freeKernelConjugateRelatorSet (f := f) (rels := rels)The Reidemeister--Schreier relator identity is obtained by rewriting the original relator with the chosen transversal.
Show proof
by
intro z hz
rcases hz with ⟨t, _ht, r, hr, hzval⟩
exact ⟨t, r, hr, hzval⟩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 freeKernelTransversalRelatorSet_normalClosure_eq_conjugateRelatorSet
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}
(hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T) :
Subgroup.normalClosure (freeKernelTransversalRelatorSet (f := f) (rels := rels) T) =
Subgroup.normalClosure (freeKernelConjugateRelatorSet (f := f) (rels := rels))The normal closure of the free-kernel transversal relator set equals the normal closure of the corresponding conjugate relator set.
Show proof
by
let L : Subgroup (FreeGroup X) := (FreeGroup.lift f).ker
let Sₜ : Set L := freeKernelTransversalRelatorSet (f := f) (rels := rels) T
let S : Set L := freeKernelConjugateRelatorSet (f := f) (rels := rels)
refine le_antisymm ?_ ?_
· exact Subgroup.normalClosure_le_normal
(fun z hz => Subgroup.subset_normalClosure
(freeKernelTransversalRelatorSet_subset_conjugateRelatorSet T hz))
· refine Subgroup.normalClosure_le_normal ?_
intro z hz
rcases hz with ⟨g, r, hr, hzval⟩
rcases (hT.existsUnique g).exists with ⟨kt, hkt⟩
let k : L := ⟨kt.1.1, kt.1.2⟩
let t : FreeGroup X := kt.2.1
have ht : t ∈ T := kt.2.2
have hg : (k : FreeGroup X) * t = g := hkt
have hwL : t * r * t⁻¹ ∈ L := by
change FreeGroup.lift f (t * r * t⁻¹) = 1
simp only [map_mul, hrels r hr, mul_one, map_inv, mul_inv_cancel]
let w : L := ⟨t * r * t⁻¹, hwL⟩
have hwSₜ : w ∈ Sₜ := by
refine ⟨t, ht, r, hr, ?_⟩
rfl
let N : Subgroup L := Subgroup.normalClosure Sₜ
have hwN : w ∈ N := Subgroup.subset_normalClosure hwSₜ
have hconj : k * w * k⁻¹ ∈ N := by
simpa [MulAut.conj_apply] using (Subgroup.normalClosure_normal.conj_mem w hwN k)
have hzconj : z = k * w * k⁻¹ := by
apply Subtype.ext
change (z : FreeGroup X) =
(k : FreeGroup X) * (w : FreeGroup X) * (k : FreeGroup X)⁻¹
rw [hzval, ← hg]
change ((k : FreeGroup X) * t) * r * ((k : FreeGroup X) * t)⁻¹ =
(k : FreeGroup X) * (t * r * t⁻¹) * (k : FreeGroup X)⁻¹
group
simpa [Sₜ, N, hzconj] using hconjProof. 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. Finiteness is supplied by the finite quotient or finite list of Schreier generators used by the construction. 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 topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. 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 freeKernelConjugateRelatorSet_subset_comap_normalClosure
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A} :
freeKernelConjugateRelatorSet (f := f) (rels := rels) ⊆
Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels)The free-kernel relators map into the corresponding normal closure.
Show proof
by
intro z hz
rcases hz with ⟨g, r, hr, hz⟩
change (z : FreeGroup X) ∈ Subgroup.normalClosure rels
rw [hz]
exact Subgroup.conjugatesOfSet_subset_normalClosure
(Group.mem_conjugatesOfSet_iff.mpr ⟨r, hr, isConj_iff.2 ⟨g, rfl⟩⟩)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. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. 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.
□theorem freeKernelConjugateRelatorSet_normalClosure_le_comap_normalClosure
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A} :
Subgroup.normalClosure (freeKernelConjugateRelatorSet (f := f) (rels := rels)) ≤
Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels)The free-kernel relators map into the corresponding normal closure.
Show proof
by
exact Subgroup.normalClosure_le_normal
(freeKernelConjugateRelatorSet_subset_comap_normalClosure (f := f) (rels := rels))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. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. 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.
□theorem freeKernelConjugateRelatorSet_normalClosure_eq_comap_normalClosure
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
Subgroup.normalClosure (freeKernelConjugateRelatorSet (f := f) (rels := rels)) =
Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels)The indicated normal closure agrees with the normal closure transported through the Reidemeister--Schreier relator comparison.
Show proof
by
let L : Subgroup (FreeGroup X) := (FreeGroup.lift f).ker
let S : Set L := freeKernelConjugateRelatorSet (f := f) (rels := rels)
let N : Subgroup L := Subgroup.normalClosure S
have hle :
N ≤ Subgroup.comap L.subtype (Subgroup.normalClosure rels) := by
simpa [L, S, N] using
freeKernelConjugateRelatorSet_normalClosure_le_comap_normalClosure (f := f) (rels := rels)
have hconj :
∀ (g : FreeGroup X) (n : L), n ∈ N →
MulAut.conjNormal (H := L) g n ∈ N := by
intro g
let θ : MulAut L := MulAut.conjNormal (H := L) g
have hSmap : S ⊆ Subgroup.comap θ.toMonoidHom N := by
intro z hz
rcases hz with ⟨a, r, hr, hzval⟩
refine Subgroup.subset_normalClosure ?_
refine ⟨g * a, r, hr, ?_⟩
calc
↑((MulEquiv.toMonoidHom θ) z) = g * (z : FreeGroup X) * g⁻¹ := by
simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, MulAut.conjNormal_apply, θ]
_ = g * a * r * (g * a)⁻¹ := by
rw [hzval]
group
have hNmap : N ≤ Subgroup.comap θ.toMonoidHom N := by
simpa [N] using Subgroup.normalClosure_le_normal hSmap
exact fun n hn => hNmap hn
let H : Subgroup (FreeGroup X) := Subgroup.map L.subtype N
have hHnormal : H.Normal := by
refine ⟨?_⟩
intro x hx g
rcases hx with ⟨n, hn, rfl⟩
refine ⟨MulAut.conjNormal (H := L) g n, hconj g n hn, ?_⟩
exact MulAut.conjNormal_apply g n
have hrels_le_H : rels ⊆ H := by
intro r hr
have hrL : r ∈ L := by
exact MonoidHom.mem_ker.mpr (hrels r hr)
let z : L := ⟨r, hrL⟩
have hzS : z ∈ S := by
refine ⟨1, r, hr, ?_⟩
simp only [one_mul, inv_one, mul_one, z]
refine ⟨z, Subgroup.subset_normalClosure hzS, ?_⟩
rfl
have hnormalClosure_le_H : Subgroup.normalClosure rels ≤ H := by
exact Subgroup.normalClosure_le_normal hrels_le_H
refine le_antisymm hle ?_
intro k hk
have hkH : (k : FreeGroup X) ∈ H := hnormalClosure_le_H hk
rcases hkH with ⟨n, hn, hnval⟩
have hkn : k = n := Subtype.ext hnval.symm
simpa [hkn] using hnProof. 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. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. 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.
□theorem freeKernelTransversalRelatorSet_normalClosure_eq_comap_normalClosure
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}
(hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T) :
Subgroup.normalClosure (freeKernelTransversalRelatorSet (f := f) (rels := rels) T) =
Subgroup.comap ((FreeGroup.lift f).ker.subtype) (Subgroup.normalClosure rels)The indicated normal closure agrees with the normal closure transported through the Reidemeister--Schreier relator comparison.
Show proof
(freeKernelTransversalRelatorSet_normalClosure_eq_conjugateRelatorSet hrels hT).trans
(freeKernelConjugateRelatorSet_normalClosure_eq_comap_normalClosure hrels)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. When a quotient map is present, both sides use the same image coset and the same rewritten letter, so the chosen-representative equality descends to the quotient presentation. 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.
□noncomputable def presentedFreeKernelTransversalRelatorQuotientEquivPresentedKernel
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}
(hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T) :
(FreeGroup.lift f).ker ⧸
Subgroup.normalClosure (freeKernelTransversalRelatorSet (f := f) (rels := rels) T) ≃*
(PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker :=
(QuotientGroup.quotientMulEquivOfEq
(freeKernelTransversalRelatorSet_normalClosure_eq_comap_normalClosure hrels hT)).trans
(presentedFreeKernelRelatorQuotientEquivPresentedKernel hrels)The presented-kernel quotient is identified with the Reidemeister--Schreier relator quotient.
noncomputable def presentedFreeKernelSchreierRelatorQuotientEquivPresentedKernel
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}
(hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T)
{Y : Type*} (e : FreeGroup Y ≃* (FreeGroup.lift f).ker) :
FreeGroup Y ⧸
Subgroup.normalClosure
(freeGroupPullbackRelatorSet e
(freeKernelTransversalRelatorSet (f := f) (rels := rels) T)) ≃*
(PresentedGroup.toGroup (rels := rels) (f := f) hrels).ker :=
(freeGroupPullbackRelatorQuotientEquiv e
(freeKernelTransversalRelatorSet (f := f) (rels := rels) T)).trans
(presentedFreeKernelTransversalRelatorQuotientEquivPresentedKernel hrels hT)The presented-kernel quotient is identified with the Reidemeister--Schreier relator quotient.
@[simp] theorem mem_freeGroupPullbackRelatorSet_iff
{Y G : Type*} [Group G] {e : FreeGroup Y ≃* G} {S : Set G} {y : FreeGroup Y} :
y ∈ freeGroupPullbackRelatorSet e S ↔ e y ∈ SMembership in the free-group pullback relator set is equivalent to the displayed relator condition.
Show proof
by
constructor
· rintro ⟨s, hs, hsy⟩
have hs_eq : s = e y := by
calc
s = e (e.symm s) := by simp only [MulEquiv.apply_symm_apply]
_ = e y := congrArg e hsy
simpa [hs_eq] using hs
· intro hy
exact ⟨e y, hy, by simp only [MulEquiv.symm_apply_apply]⟩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 freeKernelTransversalRelatorSet_mem
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1)
{T : Set (FreeGroup X)} {t : FreeGroup X} (ht : t ∈ T)
{r : FreeGroup X} (hr : r ∈ rels) :
(⟨t * r * t⁻¹, by
change FreeGroup.lift f (t * r * t⁻¹) = 1
simp only [map_mul, hrels r hr, mul_one, map_inv, mul_inv_cancel]⟩ : (FreeGroup.lift f).ker) ∈
freeKernelTransversalRelatorSet (f := f) (rels := rels) TThe Reidemeister--Schreier relator identity is obtained by rewriting the original relator with the chosen transversal.
Show proof
by
exact ⟨t, ht, r, hr, rfl⟩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 freeGroupPullbackRelator_mem
{Y G : Type*} [Group G] (e : FreeGroup Y ≃* G) {S : Set G} {s : G}
(hs : s ∈ S) :
e.symm s ∈ freeGroupPullbackRelatorSet e SThe Reidemeister--Schreier relator identity is obtained by rewriting the original relator with the chosen transversal.
Show proof
by
exact (mem_freeGroupPullbackRelatorSet_iff (e := e) (S := S) (y := e.symm s)).2
(by simpa using hs)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 freeGroupPullbackRelator_mem_normalClosure
{Y G : Type*} [Group G] (e : FreeGroup Y ≃* G) {S : Set G} {s : G}
(hs : s ∈ S) :
e.symm s ∈ Subgroup.normalClosure (freeGroupPullbackRelatorSet e S)A pullback of an original relator lies in the normal closure of the pulled-back relator set.
Show proof
Subgroup.subset_normalClosure (freeGroupPullbackRelator_mem e hs)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. Finiteness is supplied by the finite quotient or finite list of Schreier generators used by the construction. 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 topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. 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 freeGroupPullback_transversalRelator_mem_normalClosure
{X A Y : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1)
{T : Set (FreeGroup X)} (e : FreeGroup Y ≃* (FreeGroup.lift f).ker)
{t : FreeGroup X} (ht : t ∈ T) {r : FreeGroup X} (hr : r ∈ rels) :
e.symm
(⟨t * r * t⁻¹, by
change FreeGroup.lift f (t * r * t⁻¹) = 1
simp only [map_mul, hrels r hr, mul_one, map_inv, mul_inv_cancel]⟩ : (FreeGroup.lift f).ker) ∈
Subgroup.normalClosure
(freeGroupPullbackRelatorSet e
(freeKernelTransversalRelatorSet (f := f) (rels := rels) T))A pulled-back transversal relator lies in the normal closure of the pulled-back transversal relator set.
Show proof
freeGroupPullbackRelator_mem_normalClosure e
(freeKernelTransversalRelatorSet_mem hrels ht hr)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. Finiteness is supplied by the finite quotient or finite list of Schreier generators used by the construction. 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 topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. 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 freeKernelElement_mem_transversalRelator_normalClosure_of_mem_normalClosure
{X A : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}
(hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T)
{k : (FreeGroup.lift f).ker}
(hk : (k : FreeGroup X) ∈ Subgroup.normalClosure rels) :
k ∈ Subgroup.normalClosure
(freeKernelTransversalRelatorSet (f := f) (rels := rels) T)A kernel word whose image lies in the target normal closure lies in the normal closure of the transversal relators.
Show proof
by
rw [freeKernelTransversalRelatorSet_normalClosure_eq_comap_normalClosure hrels hT]
exact hkProof. 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 freeGroupPullback_mem_normalClosure_of_image_mem
{Y G : Type*} [Group G] (e : FreeGroup Y ≃* G) (S : Set G)
{y : FreeGroup Y} (hy : e y ∈ Subgroup.normalClosure S) :
y ∈ Subgroup.normalClosure (freeGroupPullbackRelatorSet e S)A pulled-back free-group word lies in the source normal closure when its image lies in the target normal closure.
Show proof
by
have hyMap :
e y ∈
Subgroup.map e.toMonoidHom
(Subgroup.normalClosure (freeGroupPullbackRelatorSet e S)) := by
rw [map_normalClosure_freeGroupPullbackRelatorSet e S]
exact hy
rcases hyMap with ⟨z, hz, hzmap⟩
have hzy : z = y := e.injective hzmap
simpa [hzy] using hzProof. 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 freeGroupPullback_transversalRelator_mem_normalClosure_of_mem_normalClosure
{X A Y : Type*} [Group A] {rels : Set (FreeGroup X)} {f : X → A}
(hrels : ∀ r ∈ rels, FreeGroup.lift f r = 1) {T : Set (FreeGroup X)}
(hT : Subgroup.IsComplement ((FreeGroup.lift f).ker : Set (FreeGroup X)) T)
(e : FreeGroup Y ≃* (FreeGroup.lift f).ker) {k : (FreeGroup.lift f).ker}
(hk : (k : FreeGroup X) ∈ Subgroup.normalClosure rels) :
e.symm k ∈
Subgroup.normalClosure
(freeGroupPullbackRelatorSet e
(freeKernelTransversalRelatorSet (f := f) (rels := rels) T))A pulled-back transversal relator lies in the source normal closure whenever the original word lies in the target normal closure.
Show proof
by
have hkSchreier :
k ∈ Subgroup.normalClosure
(freeKernelTransversalRelatorSet (f := f) (rels := rels) T) :=
freeKernelElement_mem_transversalRelator_normalClosure_of_mem_normalClosure hrels hT hk
apply freeGroupPullback_mem_normalClosure_of_image_mem e
(freeKernelTransversalRelatorSet (f := f) (rels := rels) T)
simpa using hkSchreierProof. 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.
□