ReidemeisterSchreier.Profinite.OpenSubgroups.DenseFreeModel
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
import
theorem rightRel_map_of_comap
(π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
(K : Subgroup P) (hβ : π.comp βF = β)
{a b : FreeGroup Y}
(hab : QuotientGroup.rightRel (Subgroup.comap β K) a b) :
QuotientGroup.rightRel (Subgroup.comap π K) (βF a) (βF b)The right relator map is compatible with comap of the open subgroup.
Show proof
by
have ha : π (βF a) = β a := by
simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f a) hβ
have hb : π (βF b) = β b := by
simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f b) hβ
rw [QuotientGroup.rightRel_apply] at hab ⊢
simpa [MonoidHom.map_mul, MonoidHom.map_inv, ha, hb] using habProof. 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.
□noncomputable def mapRightQuotientOfComap :
(π : F →* P) → (βF : FreeGroup Y →* F) → (β : FreeGroup Y →* P) →
(K : Subgroup P) → (hβ : π.comp βF = β) →
Quotient (QuotientGroup.rightRel (Subgroup.comap β K)) →
Quotient (QuotientGroup.rightRel (Subgroup.comap π K))
| π, βF, β, K, hβ =>
Quotient.map' βF (fun _a _b hab => rightRel_map_of_comap π βF β K hβ hab)Transport right-coset classes along a homomorphism compatible with two subgroup preimages.
theorem surjective_mapRightQuotientOfComap
(π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
(K : Subgroup P) (hβ : π.comp βF = β)
(hβsurj : Function.Surjective β) :
Function.Surjective
(mapRightQuotientOfComap π βF β K hβ)The Reidemeister--Schreier identity follows from the corresponding rewriting calculation.
Show proof
by
intro q
refine Quotient.inductionOn' q ?_
intro p
rcases hβsurj (π p) with ⟨w, hw⟩
refine ⟨Quotient.mk'' w, ?_⟩
change Quotient.mk'' (βF w) = Quotient.mk'' p
apply Quotient.sound'
have hw' : π (βF w) = π p := by
calc
π (βF w) = β w := by
simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f w) hβ
_ = π p := hw
rw [QuotientGroup.rightRel_apply]
simp only [Subgroup.comap, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk, mem_preimage,
MonoidHom.map_mul, MonoidHom.map_inv, hw', 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. 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. 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. 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.
□theorem injective_mapRightQuotientOfComap
(π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
(K : Subgroup P) (hβ : π.comp βF = β) :
Function.Injective (mapRightQuotientOfComap π βF β K hβ)The Reidemeister--Schreier identity follows from the corresponding rewriting calculation.
Show proof
by
intro a b hab
revert hab
refine Quotient.inductionOn₂' a b ?_
intro x y hxy
apply Quotient.sound'
have hrel :
QuotientGroup.rightRel (Subgroup.comap π K) (βF x) (βF y) := Quotient.exact' hxy
have hx : π (βF x) = β x := by
simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f x) hβ
have hy : π (βF y) = β y := by
simpa [MonoidHom.comp_apply] using congrArg (fun f : FreeGroup Y →* P => f y) hβ
rw [QuotientGroup.rightRel_apply] at hrel ⊢
change π (βF y * (βF x)⁻¹) ∈ K at hrel
change β (y * x⁻¹) ∈ K
simpa [MonoidHom.map_mul, MonoidHom.map_inv, hx, hy] using hrelProof. 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. For injectivity, suppose two source elements have the same image. After projecting to every finite quotient stage the corresponding finite-stage map is injective, or the equality is simply equality of subtype carriers; hence all source coordinates agree, and the inverse-limit extensionality principle identifies the original elements. 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.
□noncomputable def rightQuotientEquivOfComap
(π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
(K : Subgroup P) (hβ : π.comp βF = β)
(hβsurj : Function.Surjective β) :
Quotient (QuotientGroup.rightRel (Subgroup.comap β K)) ≃
Quotient (QuotientGroup.rightRel (Subgroup.comap π K)) :=
Equiv.ofBijective
(mapRightQuotientOfComap π βF β K hβ)
⟨injective_mapRightQuotientOfComap π βF β K hβ,
surjective_mapRightQuotientOfComap π βF β K hβ hβsurj⟩If \(\beta : \mathrm{FreeGroup}(Y) \to P\) is surjective and \(\beta = \pi \circ \beta_F\), then the right cosets of \(\beta^{-1}(K)\) are canonically identified with the right cosets of \(\pi^{-1}(K)\).
@[simp] theorem rightQuotientEquivOfComap_mk
(π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
(K : Subgroup P) (hβ : π.comp βF = β)
(hβsurj : Function.Surjective β) (w : FreeGroup Y) :
rightQuotientEquivOfComap π βF β K hβ hβsurj
(Quotient.mk'' w) =
Quotient.mk'' (βF w)The right-quotient comparison induced by comap is an equivalence.
Show proof
by
simp only [rightQuotientEquivOfComap, mapRightQuotientOfComap, Equiv.ofBijective_apply, Quotient.map'_mk'']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.
□noncomputable def rightSchreierSectionOfComap
(π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
(K : Subgroup P) (hβ : π.comp βF = β)
(hβsurj : Function.Surjective β)
(hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T) :
Quotient (QuotientGroup.rightRel (Subgroup.comap π K)) → F :=
fun q =>
βF <|
rightTransversalSection (H := Subgroup.comap β K) hT.1
((rightQuotientEquivOfComap π βF β K hβ hβsurj).symm q)Transport a discrete Schreier transversal for \(\beta^{-1}(K)\) to a right-coset section for \(\pi^{-1}(K)\) in the ambient group \(F\).
@[simp 900] theorem rightSchreierSectionOfComap_spec
(π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
(K : Subgroup P) (hβ : π.comp βF = β)
(hβsurj : Function.Surjective β)
(hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T)
(q : Quotient (QuotientGroup.rightRel (Subgroup.comap π K))) :
Quotient.mk'' (rightSchreierSectionOfComap π βF β K hβ hβsurj hT q) = qThe transported right Schreier section satisfies its defining specification.
Show proof
by
let e := rightQuotientEquivOfComap π βF β K hβ hβsurj
let τT := rightTransversalSection (H := Subgroup.comap β K) hT.1
calc
Quotient.mk'' (rightSchreierSectionOfComap π βF β K hβ hβsurj hT q)
= e (Quotient.mk'' (τT (e.symm q))) := by
simpa [rightSchreierSectionOfComap, e, τT] using
(rightQuotientEquivOfComap_mk π βF β K hβ hβsurj (τT (e.symm q))).symm
_ = e (e.symm q) := by
rw [rightTransversalSection_spec (H := Subgroup.comap β K) hT.1]
_ = q := e.apply_symm_apply qProof. 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 900] theorem rightSchreierSectionOfComap_eq_of_mem
(π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
(K : Subgroup P) (hβ : π.comp βF = β)
(hβsurj : Function.Surjective β)
(hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T)
{t : FreeGroup Y} (ht : t ∈ T) :
rightSchreierSectionOfComap π βF β K hβ hβsurj hT
(Quotient.mk'' (βF t)) =
βF tOn a coset represented by an element of the chosen Schreier transversal, the transported section returns the image of that representative.
Show proof
by
let e := rightQuotientEquivOfComap π βF β K hβ hβsurj
have heq :
e.symm (Quotient.mk'' (βF t)) = Quotient.mk'' t := by
apply e.injective
simp only [Equiv.apply_symm_apply, rightQuotientEquivOfComap_mk, e]
have hsec :
rightTransversalSection (H := Subgroup.comap β K) hT.1
(Quotient.mk'' t) = t := by
have hsub :
hT.1.rightQuotientEquiv (Quotient.mk'' t) = ⟨t, ht⟩ := by
have hq :
Quotient.mk'' t = hT.1.rightQuotientEquiv.symm ⟨t, ht⟩ := by
simpa using
(hT.1.mk''_rightQuotientEquiv (hT.1.rightQuotientEquiv.symm ⟨t, ht⟩)).symm
apply hT.1.rightQuotientEquiv.symm.injective
simpa using hq
simpa [rightTransversalSection] using congrArg Subtype.val hsub
rw [rightSchreierSectionOfComap, heq, hsec]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 900] theorem rightSchreierSectionOfComap_one
(π : F →* P) (βF : FreeGroup Y →* F) (β : FreeGroup Y →* P)
(K : Subgroup P) (hβ : π.comp βF = β)
(hβsurj : Function.Surjective β)
(hT : IsRightSchreierTransversal (X := Y) (Subgroup.comap β K) T) :
rightSchreierSectionOfComap π βF β K hβ hβsurj hT
(Quotient.mk'' (1 : F)) =
1The transported Schreier section is normalized at the trivial right coset.
Show proof
by
have hβFone : βF (1 : FreeGroup Y) = 1 := by simp only [map_one]
rw [← hβFone]
exact rightSchreierSectionOfComap_eq_of_mem π βF β K hβ hβsurj hT hT.2.1Proof. 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 denseRange_freeGroupLift_of_topologicallyGenerates
(hgen : ProCGroups.Generation.TopologicallyGenerates (G := F) (Set.range ι)) :
DenseRange (FreeGroup.lift ι : FreeGroup X →* F)The abstract free-group lift of a topologically generating family has dense range.
Show proof
by
let φ : FreeGroup X →* F := FreeGroup.lift ι
have hsub : Set.range ι ⊆ (φ.range : Set F) := by
rintro _ ⟨x, rfl⟩
exact ⟨FreeGroup.of x, by simp only [FreeGroup.lift_apply_of, φ]⟩
have hφgen :
ProCGroups.Generation.TopologicallyGenerates (G := F) (φ.range : Set F) :=
ProCGroups.Generation.topologicallyGenerates_mono (G := F) hgen hsub
have hdense : Dense ((φ.range : Subgroup F) : Set F) := by
rw [← Subgroup.closure_eq φ.range]
exact (ProCGroups.Generation.topologicallyGenerates_iff_dense
(G := F) (X := (φ.range : Set F))).1 hφgen
simpa [DenseRange, MonoidHom.coe_range] using hdenseProof. 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 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. 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 topologicallyGenerates_range_of_denseAbstractFreeLift
{Y : Type u}
{H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
{φ : FreeGroup Y →* H}
(hφ : DenseRange φ) :
ProCGroups.Generation.TopologicallyGenerates
(G := H) (Set.range fun y : Y => φ (FreeGroup.of y))A dense abstract free-group lift topologically generates through the images of the free generators.
Show proof
by
let j : Y → H := fun y => φ (FreeGroup.of y)
have himage :
φ '' Set.range (FreeGroup.of : Y → FreeGroup Y) = Set.range j := by
simpa [j, Function.comp] using
(Set.range_comp φ (FreeGroup.of : Y → FreeGroup Y)).symm
have hclosure :
Subgroup.closure (Set.range j) = φ.range := by
calc
Subgroup.closure (Set.range j)
= Subgroup.map φ (Subgroup.closure (Set.range (FreeGroup.of : Y → FreeGroup Y))) := by
simpa [himage] using
(φ.map_closure (Set.range (FreeGroup.of : Y → FreeGroup Y))).symm
_ = φ.range := by
rw [FreeGroup.closure_range_of Y, MonoidHom.range_eq_map]
rw [ProCGroups.Generation.TopologicallyGenerates, hclosure]
rw [SetLike.ext'_iff, Subgroup.topologicalClosure_coe, Subgroup.coe_top]
simpa [DenseRange, MonoidHom.coe_range, dense_iff_closure_eq] using hφ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 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. 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 denseRange_comapMap_of_openSubgroup
{G : Type u} [Group G]
{H : Type u} [Group H] [TopologicalSpace H]
{φ : G →* H} (hφ : DenseRange φ)
{U : Subgroup H} (hU : IsOpen (U : Set H)) :
DenseRange
({ toFun := fun g : Subgroup.comap φ U => ⟨φ g.1, g.2⟩
map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
map_mul' := by
intro a b
ext
simp only [Subgroup.coe_mul, map_mul]} : Subgroup.comap φ U →* U)Restricting a dense homomorphism to the preimage of an open subgroup still has dense range in that subgroup.
Show proof
by
let ψ : Subgroup.comap φ U →* U :=
{ toFun := fun g => ⟨φ g.1, g.2⟩
map_one' := by simp only [OneMemClass.coe_one, map_one, Subgroup.mk_eq_one]
map_mul' := by
intro a b
ext
simp only [Subgroup.coe_mul, map_mul]}
have hdense : Dense (Set.range φ) := by
simpa [DenseRange] using hφ
have himage :
((↑) : U → H) '' Set.range ψ = (U : Set H) ∩ Set.range φ := by
ext h
constructor
· rintro ⟨_, hu, rfl⟩
rcases hu with ⟨g, rfl⟩
exact ⟨g.2, ⟨g.1, rfl⟩⟩
· rintro ⟨hu, g, rfl⟩
exact ⟨⟨φ g, hu⟩, ⟨⟨g, hu⟩, rfl⟩, rfl⟩
have hsubset :
(U : Set H) ⊆ closure (((↑) : U → H) '' Set.range ψ) := by
rw [himage]
simpa [Set.inter_comm] using hdense.open_subset_closure_inter hU
have hDenseU : Dense (Set.range ψ : Set U) := by
exact (Subtype.dense_iff).2 hsubset
simpa [DenseRange] using hDenseUProof. 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. 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. 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. 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.
□theorem surjective_of_denseRange
{φ : F →* P} (hφ : DenseRange φ) :
Function.Surjective φA homomorphism into a finite discrete group is surjective as soon as it has dense range.
Show proof
by
have hclosed : IsClosed (Set.range φ) := isClosed_discrete _
have hclosure : closure (Set.range φ) = Set.univ := hφ.closure_range
have hrange : Set.range φ = Set.univ := by
rw [← hclosure]
exact (closure_eq_iff_isClosed.mpr hclosed).symm
intro p
have hp : p ∈ Set.range φ := by
simp only [hrange, mem_univ]
exact hpProof. 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. 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 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 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. 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.
□theorem exists_freeBasis_comap_freeGroupLift_of_openSubgroup_of_rankTransform
{X : Type u} [Finite X]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F] [CompactSpace F]
{ι : X → F}
(hgen : ProCGroups.Generation.TopologicallyGenerates (G := F) (Set.range ι))
(H : OpenSubgroup F) :
∃ Y : Type u,
Nonempty (FreeGroupBasis Y (Subgroup.comap (FreeGroup.lift ι) (H : Subgroup F))) ∧
Nat.card Y = _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (F ⧸ (H : Subgroup F)))The abstract subgroup of \(\mathrm{FreeGroup}(X)\) lying over an open subgroup of a compact group via the dense free-group lift has the corresponding Schreier-transformed rank.
Show proof
by
classical
let βF : FreeGroup X →* F := FreeGroup.lift ι
let L : Subgroup (FreeGroup X) := Subgroup.comap βF (H : Subgroup F)
let nQ : ℕ := Nat.card (F ⧸ (H : Subgroup F))
let P := openSubgroupIndexActionRange (G := F) H
(show Nat.card (F ⧸ (H : Subgroup F)) = nQ by rfl)
let ρ : F →ₜ* P :=
openSubgroupIndexActionRangeContinuousHom (G := F) H
(show Nat.card (F ⧸ (H : Subgroup F)) = nQ by rfl)
let q0 : F ⧸ (H : Subgroup F) := QuotientGroup.mk (s := (H : Subgroup F)) (1 : F)
let K : Subgroup P := MulAction.stabilizer P q0
let β : FreeGroup X →* P := ρ.toMonoidHom.comp βF
letI : TopologicalSpace (FreeGroup X) := ⊥
letI : DiscreteTopology (FreeGroup X) := ⟨rfl⟩
letI : IsTopologicalGroup (FreeGroup X) := by infer_instance
have hcomap : Subgroup.comap ρ.toMonoidHom K = (H : Subgroup F) := by
ext g
constructor
· intro hg
change ρ g • q0 = q0 at hg
rw [openSubgroupIndexActionRangeContinuousHom_smul_basepoint (G := F) H
(show Nat.card (F ⧸ (H : Subgroup F)) = nQ by rfl) g] at hg
change (QuotientGroup.mk (s := (H : Subgroup F)) g : F ⧸ (H : Subgroup F)) =
QuotientGroup.mk (s := (H : Subgroup F)) (1 : F) at hg
simpa [QuotientGroup.eq] using hg
· intro hg
change ρ g • q0 = q0
exact openSubgroupIndexActionRangeContinuousHom_smul_basepoint_of_mem
(G := F) H (show Nat.card (F ⧸ (H : Subgroup F)) = nQ by rfl) hg
have hβFdense : DenseRange βF :=
denseRange_freeGroupLift_of_topologicallyGenerates (F := F) (X := X) hgen
have hρsurj : Function.Surjective ρ := by
intro p
rcases p.down.2 with ⟨g, hg⟩
refine ⟨g, ?_⟩
apply ULift.ext
apply Subtype.ext
exact hg
have hβdense : DenseRange β := by
simpa [β, MonoidHom.comp_apply] using
(Function.Surjective.denseRange hρsurj).comp hβFdense ρ.continuous_toFun
have hβsurj : Function.Surjective β :=
surjective_of_denseRange (F := FreeGroup X) (P := P) hβdense
let H0 : Subgroup F := Subgroup.comap ρ.toMonoidHom K
have hH0 : H0 = (H : Subgroup F) := by
simpa [H0] using hcomap
let eQ :
Quotient (QuotientGroup.rightRel (Subgroup.comap β K)) ≃
Quotient (QuotientGroup.rightRel H0) :=
rightQuotientEquivOfComap ρ.toMonoidHom βF β K rfl hβsurj
have hcomapL : Subgroup.comap β K = L := by
ext w
change β w ∈ K ↔ βF w ∈ (H : Subgroup F)
change βF w ∈ Subgroup.comap ρ.toMonoidHom K ↔ βF w ∈ (H : Subgroup F)
rw [hcomap]
let eQ0 :
Quotient (QuotientGroup.rightRel L) ≃
Quotient (QuotientGroup.rightRel H0) := by
simpa [hcomapL] using eQ
letI : Finite (F ⧸ (H : Subgroup F)) :=
ProCGroups.openSubgroup_finiteQuotient (G := F) H
letI : Finite (Quotient (QuotientGroup.rightRel (H : Subgroup F))) := by
exact
Finite.of_equiv (F ⧸ (H : Subgroup F))
(QuotientGroup.quotientRightRelEquivQuotientLeftRel (H : Subgroup F)).symm
have hRightEq :
Quotient (QuotientGroup.rightRel (H : Subgroup F)) =
Quotient (QuotientGroup.rightRel H0) := by
simpa using
congrArg (fun S : Subgroup F => Quotient (QuotientGroup.rightRel S)) hH0.symm
letI : Finite (Quotient (QuotientGroup.rightRel H0)) := by
exact Eq.ndrec
(motive := fun T => Finite T)
(inferInstance : Finite (Quotient (QuotientGroup.rightRel (H : Subgroup F))))
hRightEq
letI : Finite (Quotient (QuotientGroup.rightRel L)) :=
Finite.of_equiv
(Quotient (QuotientGroup.rightRel H0)) eQ0.symm
letI : Finite (FreeGroup X ⧸ L) :=
Finite.of_equiv
(Quotient (QuotientGroup.rightRel L))
(QuotientGroup.quotientRightRelEquivQuotientLeftRel L)
have hquotCard :
Nat.card (FreeGroup X ⧸ L) = Nat.card (F ⧸ (H : Subgroup F)) := by
calc
Nat.card (FreeGroup X ⧸ L)
= Nat.card (Quotient (QuotientGroup.rightRel L)) :=
Nat.card_congr (QuotientGroup.quotientRightRelEquivQuotientLeftRel L).symm
_ = Nat.card (Quotient (QuotientGroup.rightRel H0)) :=
Nat.card_congr eQ0
_ = Nat.card (Quotient (QuotientGroup.rightRel (H : Subgroup F))) := by
simpa using congrArg Nat.card hRightEq.symm
_ = Nat.card (F ⧸ (H : Subgroup F)) :=
Nat.card_congr (QuotientGroup.quotientRightRelEquivQuotientLeftRel (H : Subgroup F))
obtain ⟨Y, hYfree, hYcard⟩ :=
exists_freeBasis_subgroupOfFreeGroup_of_rankTransform (X := X) (L := L)
refine ⟨Y, hYfree, ?_⟩
simpa [hquotCard] using hYcardProof. 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.
□