ReidemeisterSchreier.Discrete.OpenSubgroups.ClassicalGeneratorBasis
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.
private theorem IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv
{X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T) :
∃ e : FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L,
∀ z : ↥(schreierGeneratorSet (X := X) hT),
e (FreeGroup.of z) = (z : L)⁻¹A strengthened Schreier-basis existence statement exposing the value of the chosen basis map on free generators. This inverse-valued statement records the internal basis orientation used by the proof: the standard free generator corresponding to a Schreier generator \(z\) is sent to \(z^{-1}\) in the subgroup. Use the corresponding existence theorem for the positive-valued compatibility theorem.
Show proof
by
classical
letI := schreierTransversalRightCosetAction (X := X) hT
letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
let C :
Set (Quiver.Total
(IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T))) :=
((Quiver.wideSubquiverEquivSetTotal <|
Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT))ᶜ : Set _)
let b : FreeGroupBasis ↑C L :=
(IsFreeGroupoid.SpanningTree.endBasis (schreierPrefixTree (X := X) hT)).map
(schreierRootEndMulEquiv (X := X) hT)
let toSch : ↑C → ↥(schreierGeneratorSet (X := X) hT) := fun i =>
⟨schreierGenerator (X := X) hT (((i.1.left.back : T) : FreeGroup X)) i.1.hom.1,
by
refine ⟨
((i.1.left.back : T) : FreeGroup X), (i.1.left.back : T).property,
i.1.hom.1, rfl, ?_⟩
intro hgen
exact i.2 (show i.1 ∈ Quiver.wideSubquiverEquivSetTotal
(Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)) from
schreierGenerator_eq_one_implies_mem_prefixTree (X := X) hT i.1.hom hgen)⟩
have hval : ∀ i : ↑C, (b i : L) =
(((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) := by
intro i
rw [FreeGroupBasis.map_apply, IsFreeGroupoid.SpanningTree.endBasis_apply]
have htree : ∀ {a b : IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T)}
(e : a ⟶ b),
e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b →
(schreierLabelFunctor (X := X) hT).map (IsFreeGroupoid.of e) = (1 : L) := by
intro a b e he
exact schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he
have hloop := IsFreeGroupoid.SpanningTree.map_loopOfHom_eq_map
(T := schreierPrefixTree (X := X) hT)
(F := schreierLabelFunctor (X := X) hT)
(hTree := by
intro a b e he
exact htree e he)
(q := IsFreeGroupoid.of i.1.hom)
let loop := IsFreeGroupoid.SpanningTree.loopOfHom (schreierPrefixTree (X := X) hT)
(IsFreeGroupoid.of i.1.hom)
have hrootEq : (schreierRootEndMulEquiv (X := X) hT loop : L) =
(schreierLabelFunctor (X := X) hT).map loop := by
apply Subtype.ext
change loop.1 = (1 : FreeGroup X) * loop.1 * (1 : FreeGroup X)⁻¹
simp only [CategoryTheory.actionAsFunctor_obj, CategoryTheory.actionAsFunctor_map, one_mul, inv_one, mul_one]
exact hrootEq.trans <| hloop.trans <| schreierLabelFunctor_map_of (X := X) hT i.1.hom
have hto_inj : Function.Injective toSch := by
intro i j hij
apply b.injective
have hz : ((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L) =
((toSch j : ↥(schreierGeneratorSet (X := X) hT)) : L) := congrArg Subtype.val hij
have hz_inv : (((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) =
(((toSch j : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) := congrArg Inv.inv hz
exact (hval i).trans (hz_inv.trans (hval j).symm)
have hto_surj : Function.Surjective toSch := by
intro z
rcases z.2 with ⟨t, ht, x, hz, hne⟩
let a : CategoryTheory.ActionCategory (FreeGroup X) T :=
((⟨t, ht⟩ : T) : CategoryTheory.ActionCategory (FreeGroup X) T)
let b0 : CategoryTheory.ActionCategory (FreeGroup X) T :=
(schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T)
let e :
(show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T) from
a) ⟶ b0 :=
⟨x, by
rw [FreeGroup.inverseBasis_apply]
change (FreeGroup.of x)⁻¹ • (show T from CategoryTheory.ActionCategory.back a) =
(show T from CategoryTheory.ActionCategory.back b0)
simpa [a, b0] using
(schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ (⟨t, ht⟩ : T))⟩
have he_not : ⟨a, b0, e⟩ ∈ C := by
change ¬ e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b0
intro he
have hgen1_inv :
(schreierGenerator (X := X) hT
((show T from CategoryTheory.ActionCategory.back a) : FreeGroup X) e.1)⁻¹ = 1 := by
have htreeLabel :=
schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he
rw [schreierLabelFunctor_map_of (X := X) hT e] at htreeLabel
exact htreeLabel
have hgen1 :
schreierGenerator (X := X) hT
((show T from CategoryTheory.ActionCategory.back a) : FreeGroup X) e.1 = 1 :=
inv_eq_one.mp hgen1_inv
exact hne (by simpa [a, e, hz] using hgen1)
refine ⟨⟨⟨a, b0, e⟩, he_not⟩, ?_⟩
apply Subtype.ext
simpa [toSch, a, e] using hz.symm
let eC : ↑C ≃ ↥(schreierGeneratorSet (X := X) hT) := Equiv.ofBijective toSch ⟨hto_inj, hto_surj⟩
refine ⟨(b.reindex eC).repr.symm, ?_⟩
intro z
have hbasis :
(b.reindex eC).repr.symm (FreeGroup.of z) = (b.reindex eC) z := by
apply (b.reindex eC).repr.injective
calc
(b.reindex eC).repr ((b.reindex eC).repr.symm (FreeGroup.of z))
= FreeGroup.of z := by simp only [MulEquiv.apply_symm_apply]
_ = (b.reindex eC).repr ((b.reindex eC) z) :=
(FreeGroupBasis.repr_apply_coe (b.reindex eC) z).symm
calc
(b.reindex eC).repr.symm (FreeGroup.of z)
= (b.reindex eC) z := hbasis
_ = b (eC.symm z) := by
rw [FreeGroupBasis.reindex_apply]
_ = (((toSch (eC.symm z) : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) :=
hval (eC.symm z)
_ = (z : L)⁻¹ := by
exact congrArg (fun w : ↥(schreierGeneratorSet (X := X) hT) => ((w : L)⁻¹))
(eC.apply_symm_apply z)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 IsRightSchreierTransversal.exists_schreierBasisEquiv
{X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T) :
∃ e : FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L,
∀ z : ↥(schreierGeneratorSet (X := X) hT),
e (FreeGroup.of z) = (z : L)Positive-valued Schreier-basis existence statement on the classical Schreier generator set. It is equivalent to the nontrivial Schreier-pair basis equivalence used in the main formulation.
Show proof
by
classical
rcases Internal.IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv hT with
⟨eInverse, hInverse⟩
let e : FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L :=
(FreeGroup.generatorInversionEquiv ↥(schreierGeneratorSet (X := X) hT)).trans eInverse
refine ⟨e, ?_⟩
intro z
dsimp [e]
calc
eInverse ((FreeGroup.of z)⁻¹) = (eInverse (FreeGroup.of z))⁻¹ := by simp only [map_inv]
_ = ((z : L)⁻¹)⁻¹ := by rw [hInverse z]
_ = (z : L) := inv_inv _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.
□noncomputable def schreierGeneratorInverseBasisEquiv
{X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T) :
FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L :=
Classical.choose (Internal.IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv hT)The inverse-valued free-group equivalence on the classical Schreier generator value set is equivalent to the nontrivial Schreier-pair basis equivalence used in the main formulation.
theorem schreierGeneratorInverseBasisEquiv_of
{X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
(hT : IsRightSchreierTransversal (X := X) L T)
(z : ↥(schreierGeneratorSet (X := X) hT)) :
schreierGeneratorInverseBasisEquiv (X := X) hT (FreeGroup.of z) = (z : L)⁻¹Show proof
Classical.choose_spec (Internal.IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv hT) zProof. 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.
□