ReidemeisterSchreier.Profinite.OpenSubgroups.RightQuotient
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
abbrev OpenSubgroupRightQuotient (H : OpenSubgroup F) :=
_root_.ReidemeisterSchreier.RightQuotient (H : Subgroup F)The right-coset space \(F/H\), encoded via right quotients.
def openSubgroupRightCoset (H : OpenSubgroup F) (g : F) : OpenSubgroupRightQuotient H :=
_root_.ReidemeisterSchreier.rightCoset (H : Subgroup F) gThe right coset of an element modulo an open subgroup.
theorem openSubgroupRightCoset_eq_basepoint_iff_mem
{H : OpenSubgroup F} {g : F} :
openSubgroupRightCoset H g = openSubgroupRightCoset H (1 : F) ↔
g ∈ (H : Subgroup F)A right coset is the base coset exactly when its representative lies in the subgroup.
Show proof
by
exact _root_.ReidemeisterSchreier.rightCoset_eq_basepoint_iff_mem (H := (H : Subgroup F))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. 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. 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. 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.
□@[simp] theorem openSubgroupRightCoset_smul
(H : OpenSubgroup F) (g a : F) :
letI : MulAction F (OpenSubgroupRightQuotient H)The open-subgroup right-coset action sends the coset of \(a\) by \(g\) to the coset of \(a g^{-1}\).
Show proof
_root_.ReidemeisterSchreier.rightCosetMulAction (H : Subgroup F)
g • openSubgroupRightCoset H a = openSubgroupRightCoset H (a * g⁻¹) :=
_root_.ReidemeisterSchreier.rightCosetMulAction_mk_smul (H := (H : Subgroup F)) g aProof. 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. 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. 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.
□@[simp] theorem openSubgroupRightCoset_inv_smul
(H : OpenSubgroup F) (g a : F) :
letI : MulAction F (OpenSubgroupRightQuotient H)The open-subgroup right-coset action sends the coset of \(a\) by \(g^{-1}\) to the coset of \(a g\).
Show proof
_root_.ReidemeisterSchreier.rightCosetMulAction (H : Subgroup F)
g⁻¹ • openSubgroupRightCoset H a = openSubgroupRightCoset H (a * g) :=
_root_.ReidemeisterSchreier.rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F)) g aProof. 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. 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. 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.
□instance finite_openSubgroupRightQuotient (H : OpenSubgroup F) [CompactSpace F] :
Finite (OpenSubgroupRightQuotient H) := by
let e :=
QuotientGroup.quotientRightRelEquivQuotientLeftRel (H : Subgroup F)
exact Finite.of_equiv (F ⧸ (H : Subgroup F)) e.symmRight cosets of an open subgroup are finite because they are equivalent to the left quotient.
noncomputable instance fintype_openSubgroupRightQuotient (H : OpenSubgroup F) [CompactSpace F] :
Fintype (OpenSubgroupRightQuotient H) :=
Fintype.ofFinite (OpenSubgroupRightQuotient H)Right cosets of an open subgroup inherit a Fintype from compactness.
instance discreteTopology_openSubgroupRightQuotient (H : OpenSubgroup F) :
DiscreteTopology (OpenSubgroupRightQuotient H) := by
classical
refine discreteTopology_iff_isOpen_singleton.2 ?_
intro q
rw [← isQuotientMap_quotient_mk'.isOpen_preimage]
let qmk : F → OpenSubgroupRightQuotient H :=
@Quotient.mk' F (QuotientGroup.rightRel (H : Subgroup F))
let a : F := q.out
have hpre :
qmk ⁻¹' ({q} : Set (OpenSubgroupRightQuotient H)) =
(fun x : F => a * x⁻¹) ⁻¹' ((H : Subgroup F) : Set F) := by
ext x
constructor
· intro hx
have hEq : (Quotient.mk'' x : OpenSubgroupRightQuotient H) = Quotient.mk'' a := by
calc
(Quotient.mk'' x : OpenSubgroupRightQuotient H) = q := hx
_ = Quotient.mk'' a := (Quotient.out_eq' q).symm
have hrel : QuotientGroup.rightRel (H : Subgroup F) x a := Quotient.eq''.mp hEq
simpa [a] using (QuotientGroup.rightRel_apply.mp hrel)
· intro hx
have hrel : QuotientGroup.rightRel (H : Subgroup F) x a := by
rw [QuotientGroup.rightRel_apply]
simpa [a] using hx
change (Quotient.mk'' x : OpenSubgroupRightQuotient H) = q
calc
(Quotient.mk'' x : OpenSubgroupRightQuotient H) = Quotient.mk'' a :=
Quotient.eq''.mpr hrel
_ = q := by simp only [Quotient.out_eq, a]
have hpreOpen : IsOpen (qmk ⁻¹' ({q} : Set (OpenSubgroupRightQuotient H))) := by
rw [hpre]
exact H.isOpen'.preimage (continuous_const.mul continuous_inv)
simpa [qmk] using hpreOpenThe quotient topology on right cosets of an open subgroup is discrete.
noncomputable def openSubgroupRightCosetSection
(H : OpenSubgroup F) : OpenSubgroupRightQuotient H → F := by
classical
intro q
exact
if hq : q = openSubgroupRightCoset H (1 : F) then
1
else
q.outA normalized section of the right-coset projection, sending the trivial coset to \(1\).
@[simp] theorem openSubgroupRightCosetSection_spec
(H : OpenSubgroup F) (q : OpenSubgroupRightQuotient H) :
Quotient.mk'' (openSubgroupRightCosetSection (F := F) H q) = qThe chosen section of the open-subgroup right quotient projects back to the given right coset.
Show proof
by
classical
by_cases hq : q = openSubgroupRightCoset H (1 : F)
· subst hq
simp only [openSubgroupRightCosetSection, openSubgroupRightCoset, rightCoset, ↓reduceDIte]
· simp only [openSubgroupRightCosetSection, hq, ↓reduceDIte, Quotient.out_eq]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. 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. 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.
□@[simp] theorem openSubgroupRightCosetSection_one
(H : OpenSubgroup F) :
openSubgroupRightCosetSection (F := F) H (openSubgroupRightCoset H (1 : F)) = 1The chosen section of the open-subgroup right quotient sends the identity coset to the identity representative.
Show proof
by
classical
simp only [openSubgroupRightCosetSection, ↓reduceDIte]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. 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. 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 continuous_openSubgroupRightCosetSection
(H : OpenSubgroup F) :
Continuous (openSubgroupRightCosetSection (F := F) H)The normalized right-coset section is continuous because the right quotient is discrete. It is a continuity claim, checked through the topology generated by finite-stage projections.
Show proof
continuous_of_discreteTopologyProof. 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. 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. 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.
□