ProCGroups.FiniteGeneration.Basic
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
import
- Mathlib.GroupTheory.FreeGroup.Basic
- ProCGroups.Generation.QuotientGeneratorConvergingPairs
def TopologicallyFinitelyGenerated
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop :=
∃ s : Finset G, TopologicallyGenerates (G := G) (↑s : Set G)Finitely generated as a topological group.
def IsTopologicallyCharacteristic
(G : Type u) [Group G] [TopologicalSpace G] (H : Subgroup G) : Prop :=
∀ φ : G ≃ₜ* G, ∀ g : G, φ g ∈ H ↔ g ∈ HA subgroup is topologically characteristic if every continuous automorphism preserves it.
theorem IsTopologicallyCharacteristic.apply_mem_iff {H : Subgroup G}
(hH : IsTopologicallyCharacteristic (G := G) H) (φ : G ≃ₜ* G) {g : G} :
φ g ∈ H ↔ g ∈ HMembership in a topologically characteristic subgroup is invariant under applying a continuous automorphism.
Show proof
hH φ gProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 IsTopologicallyCharacteristic.inf {H K : Subgroup G}
(hH : IsTopologicallyCharacteristic (G := G) H) (hK : IsTopologicallyCharacteristic (G := G) K) :
IsTopologicallyCharacteristic (G := G) (H ⊓ K)Intersections of topologically characteristic subgroups are topologically characteristic.
Show proof
by
intro φ g
simp only [Subgroup.mem_inf, hH φ g, hK φ g]Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 IsTopologicallyCharacteristic.sInf {S : Set (Subgroup G)}
(hS : ∀ H ∈ S, IsTopologicallyCharacteristic (G := G) H) :
IsTopologicallyCharacteristic (G := G) (sInf S)Arbitrary infima of topologically characteristic subgroups are topologically characteristic.
Show proof
by
intro φ g
simp only [Subgroup.mem_sInf]
constructor
· intro hg H hH
exact (hS H hH φ g).1 (hg H hH)
· intro hg H hH
exact (hS H hH φ g).2 (hg H hH)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 IsTopologicallyCharacteristic.iInf {ι : Sort*} {S : ι → Subgroup G}
(hS : ∀ i, IsTopologicallyCharacteristic (G := G) (S i)) :
IsTopologicallyCharacteristic (G := G) (iInf S)Indexed infima of topologically characteristic subgroups are topologically characteristic.
Show proof
by
intro φ g
simp only [Subgroup.mem_iInf]
constructor
· intro hg i
exact (hS i φ g).1 (hg i)
· intro hg i
exact (hS i φ g).2 (hg i)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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.
□@[simp] theorem IsTopologicallyCharacteristic.top :
IsTopologicallyCharacteristic (G := G) (⊤ : Subgroup G)The top subgroup is topologically characteristic, since every continuous automorphism preserves it.
Show proof
by
intro φ g
simp only [Subgroup.mem_top]Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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.
□def TopologicallyGeneratedByAtMost
(n : ℕ) (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
Prop :=
∃ s : Finset G, s.card ≤ n ∧ TopologicallyGenerates (G := G) (↑s : Set G)\(G\) can be topologically generated by at most \(n\) elements.
theorem TopologicallyGeneratedByAtMost.mono {m n : ℕ}
(hmn : m ≤ n)
(hG : TopologicallyGeneratedByAtMost (G := G) m) :
TopologicallyGeneratedByAtMost (G := G) nIncreasing the allowed number of generators preserves bounded topological generation.
Show proof
by
rcases hG with ⟨s, hs, hgen⟩
exact ⟨s, hs.trans hmn, hgen⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure.
□theorem topologicallyFinitelyGenerated_iff_exists_topologicallyGeneratedByAtMost :
TopologicallyFinitelyGenerated G ↔
∃ n, TopologicallyGeneratedByAtMost (G := G) nA group is topologically finitely generated if and only if it is generated by at most \(n\) elements for some natural number \(n\).
Show proof
by
constructor
· rintro ⟨s, hs⟩
exact ⟨s.card, s, le_rfl, hs⟩
· rintro ⟨_n, s, _hs, hgen⟩
exact ⟨s, hgen⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 finiteSet_convergesToOne (s : Finset G) :
ConvergesToOne (G := G) (↑s : Set G)A finite set of elements converges to \(1\) in the profinite generating-family sense.
Show proof
ConvergesToOne.of_finite s.finite_toSetProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem topologicalRank_le_of_topologicallyGeneratedByAtMost {n : ℕ}
(h : TopologicallyGeneratedByAtMost (G := G) n) :
topologicalRank G ≤ nIf \(G\) is topologically generated by at most \(n\) elements, its topological rank is at most \(n\).
Show proof
by
rcases h with ⟨s, hs, hgen⟩
have hconv : ConvergesToOne (G := G) (↑s : Set G) :=
finiteSet_convergesToOne (G := G) s
calc
topologicalRank G ≤ Cardinal.mk (↑s : Set G) :=
topologicalRank_le_mk_of_generatesAndConvergesToOne (G := G) ⟨hgen, hconv⟩
_ = (s.card : Cardinal) := by
exact Cardinal.mk_coe_finset (s := s)
_ ≤ n := by
exact_mod_cast hsProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 density or closed-generation statements, the calculation is first made on the algebraic span of the group-like generators. The image of this span is dense in the completed target, and closedness of the kernel, image, or generated submodule allows the containment obtained on generators to pass to the completed closure.
□theorem topologicallyGenerates_range_comp_of_surjective
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(φ : G →ₜ* H) (hφ : Function.Surjective φ)
{ι : Sort w} (g : ι → G)
(hg : TopologicallyGenerates (G := G) (Set.range g)) :
TopologicallyGenerates (G := H) (Set.range (φ ∘ g))The image of a topological generating family under a continuous surjective homomorphism topologically generates the codomain.
Show proof
by
simpa [Set.range_comp, Function.comp] using
topologicallyGenerates_image_of_continuousMonoidHom_surjective
(G := G) (H := H) φ hφ hgProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 TopologicallyGeneratedByAtMost.of_surjective
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(φ : G →ₜ* H) (hφ : Function.Surjective φ) {n : ℕ}
(hG : TopologicallyGeneratedByAtMost (G := G) n) :
TopologicallyGeneratedByAtMost (G := H) nBounded topological generation descends along continuous surjective homomorphisms.
Show proof
by
classical
rcases hG with ⟨s, hs, hgen⟩
refine ⟨s.image φ, (Finset.card_image_le).trans hs, ?_⟩
simpa [Finset.coe_image] using
topologicallyGenerates_image_of_continuousMonoidHom_surjective
(G := G) (H := H) φ hφ hgenProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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.
□theorem topologicallyFinitelyGenerated_of_continuousSurjective
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(φ : G →ₜ* H) (hφ : Function.Surjective φ)
(hG : TopologicallyFinitelyGenerated G) :
TopologicallyFinitelyGenerated HTopological finite generation descends along continuous surjective homomorphisms.
Show proof
by
rw [topologicallyFinitelyGenerated_iff_exists_topologicallyGeneratedByAtMost] at hG ⊢
rcases hG with ⟨n, hn⟩
exact ⟨n, TopologicallyGeneratedByAtMost.of_surjective (G := G) (H := H) φ hφ hn⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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.
□theorem topologicallyGenerates_iff_subgroupClosure_eq_top_of_discrete
[DiscreteTopology G] {X : Set G} :
TopologicallyGenerates (G := G) X ↔ Subgroup.closure X = ⊤In the discrete case, topological generation is abstract subgroup generation.
Show proof
by
have htc : (Subgroup.closure X).topologicalClosure = Subgroup.closure X := by
apply SetLike.ext'
rw [Subgroup.topologicalClosure_coe]
exact closure_discrete ((Subgroup.closure X : Subgroup G) : Set G)
rw [TopologicallyGenerates, htc]Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 freeGroup_lift_surjective_of_topologicallyGenerates_discrete
{X : Type v} [DiscreteTopology G] (g : X → G)
(hg : TopologicallyGenerates (G := G) (Set.range g)) :
Function.Surjective (FreeGroup.lift g)A map from a free group onto a discrete topologically generated group is surjective. This is the finite-stage bridge used by Magnus arguments: after passing to a discrete quotient, topological generation of the images of the chosen generators is exactly abstract generation.
Show proof
by
rw [topologicallyGenerates_iff_subgroupClosure_eq_top_of_discrete] at hg
have hclosure_le_range :
Subgroup.closure (Set.range g) ≤ (FreeGroup.lift g).range := by
refine (Subgroup.closure_le (K := (FreeGroup.lift g).range)).2 ?_
rintro y ⟨x, rfl⟩
exact ⟨FreeGroup.of x, by simp only [FreeGroup.lift_apply_of]⟩
intro y
have hy : y ∈ Subgroup.closure (Set.range g) := by
rw [hg]
trivial
exact hclosure_le_range hyProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□theorem topologicallyFinitelyGenerated_of_finite [Finite G] [DiscreteTopology G] :
TopologicallyFinitelyGenerated GA finite discrete group is topologically finitely generated.
Show proof
by
classical
letI : Fintype G := Fintype.ofFinite G
refine ⟨Finset.univ, ?_⟩
rw [topologicallyGenerates_iff_subgroupClosure_eq_top_of_discrete]
simp only [Finset.coe_univ, Subgroup.closure_univ]Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 topologicallyGeneratedByAtMost_of_topologicalRank_eq_nat
(hG : ProCGroups.IsProfiniteGroup G) {n : ℕ}
(hd : topologicalRank G = n) :
TopologicallyGeneratedByAtMost (G := G) nIf the topological rank of a profinite group is the natural number \(n\), then the group is topologically generated by at most \(n\) elements.
Show proof
by
classical
let C : Set Cardinal := {κ : Cardinal |
∃ X : Set G,
GeneratesAndConvergesToOne (G := G) X ∧ Cardinal.mk X = κ}
have hCne : C.Nonempty := by
rcases exists_generatorsConvergingToOne (G := G) hG with ⟨X, hX⟩
exact ⟨Cardinal.mk X, X, hX, rfl⟩
have hdmem : topologicalRank G ∈ C := by
simpa [topologicalRank, C] using (csInf_mem hCne)
rcases hdmem with ⟨X, hX, hXcard⟩
have hXlt : Cardinal.mk X < Cardinal.aleph0 := by
calc
Cardinal.mk X = topologicalRank G := hXcard
_ = n := hd
_ < Cardinal.aleph0 := Cardinal.natCast_lt_aleph0 (n := n)
letI : Finite X := (Cardinal.lt_aleph0_iff_finite (α := X)).mp hXlt
have hXfin : X.Finite := Set.toFinite X
let s : Finset G := hXfin.toFinset
have hs_card : s.card = n := by
have hs_mk : (s.card : Cardinal) = Cardinal.mk X := by
simpa [s] using (Cardinal.mk_coe_finset (s := hXfin.toFinset)).symm
exact_mod_cast (hs_mk.trans (hXcard.trans hd))
refine ⟨s, hs_card.le, ?_⟩
simpa [s] using hX.1Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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_generatingTuple_of_topologicalRank_le_of_finite
(hG : TopologicallyFinitelyGenerated G) {n : ℕ} (hd : topologicalRank G ≤ n) :
∃ g : Fin n → G, TopologicallyGenerates (G := G) (Set.range g)A finite upper bound on the topological rank gives an explicit generating tuple of that length.
Show proof
by
classical
have hdfin : topologicalRank G < Cardinal.aleph0 := by
rcases hG with ⟨s, hs⟩
have hconv : ConvergesToOne (G := G) (↑s : Set G) :=
finiteSet_convergesToOne (G := G) s
have hdle : topologicalRank G ≤ Cardinal.mk (↑s : Set G) :=
topologicalRank_le_mk_of_generatesAndConvergesToOne (G := G) ⟨hs, hconv⟩
exact hdle.trans_lt <| by
have hsMk : Cardinal.mk (↑s : Set G) = (s.card : Cardinal) :=
Cardinal.mk_coe_finset (s := s)
rw [hsMk]
exact Cardinal.natCast_lt_aleph0 (n := s.card)
let m := Cardinal.toNat (topologicalRank G)
have hm : topologicalRank G = m := by
symm
exact Cardinal.cast_toNat_of_lt_aleph0 hdfin
have hExists : ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X := by
rcases hG with ⟨s, hs⟩
exact ⟨(↑s : Set G), ⟨hs, finiteSet_convergesToOne (G := G) s⟩⟩
rcases exists_generatesAndConvergesToOne_card_eq_topologicalRank (G := G) hExists with
⟨X, hX, hXcard⟩
have hXfin : X.Finite := by
have hXlt : Cardinal.mk X < Cardinal.aleph0 := by
calc
Cardinal.mk X = topologicalRank G := hXcard
_ = m := hm
_ < Cardinal.aleph0 := Cardinal.natCast_lt_aleph0 (n := m)
letI : Finite X := (Cardinal.lt_aleph0_iff_finite (α := X)).mp <| by
simpa using hXlt
exact Set.toFinite X
let s : Finset G := hXfin.toFinset
have hs_gen : TopologicallyGenerates (G := G) (↑s : Set G) := by
simpa [s] using hX.1
have hs_card : s.card = m := by
have hs_mk : (s.card : Cardinal) = Cardinal.mk X := by
simpa [s] using (Cardinal.mk_coe_finset (s := hXfin.toFinset)).symm
exact_mod_cast (hs_mk.trans (hXcard.trans hm))
have hmle : m ≤ n := by
simpa [m] using
(Cardinal.toNat_le_toNat hd (Cardinal.natCast_lt_aleph0 (n := n)))
have hs_le : s.card ≤ n := by
simpa [hs_card] using hmle
let e : Fin s.card ≃ s := by
simpa using (Fintype.equivFin s).symm
let g0 : Fin s.card → G := fun i => (e i : G)
have hs_subset_range : (↑s : Set G) ⊆ Set.range g0 := by
intro x hx
refine ⟨e.symm ⟨x, hx⟩, ?_⟩
simp only [Equiv.apply_symm_apply, g0]
have hg0 : TopologicallyGenerates (G := G) (Set.range g0) :=
topologicallyGenerates_mono hs_gen hs_subset_range
let g : Fin n → G := fun i =>
if hi : i.1 < s.card then g0 ⟨i.1, hi⟩ else 1
have hg0_subset : Set.range g0 ⊆ Set.range g := by
intro x hx
rcases hx with ⟨i, rfl⟩
refine ⟨Fin.castLE hs_le i, ?_⟩
have hi : (Fin.castLE hs_le i).1 < s.card := i.2
simp only [Fin.val_castLE, Fin.is_lt, ↓reduceDIte, Fin.eta, g]
exact ⟨g, topologicallyGenerates_mono hg0 hg0_subset⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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 topologicalRank_inverseLimit_le_of_componentBound
{I : Type v} [Preorder I]
(S : ProCGroups.InverseSystems.InverseSystem (I := I))
[Nonempty I] [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
[∀ i, IsTopologicalGroup (S.X i)] [∀ i, Finite (S.X i)]
[∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
(hdir : Directed (· ≤ ·) (id : I → I))
(hsurj : ∀ {i j : I} (hij : i ≤ j), Function.Surjective (S.map hij))
{n : ℕ} (hbound : ∀ i, topologicalRank (S.X i) ≤ n) :
topologicalRank S.inverseLimit ≤ nIf every finite stage of a surjective inverse system has topological rank at most \(n\), then so does the inverse limit.
Show proof
by
classical
letI : ∀ i, DiscreteTopology (S.X i) := fun _ => by infer_instance
let T : ProCGroups.InverseSystems.InverseSystem (I := I) := {
X := fun i => { g : Fin n → S.X i // TopologicallyGenerates (G := S.X i) (Set.range g) }
topologicalSpace := fun _ => inferInstance
map := fun {i j} hij g =>
⟨fun a => S.map hij (g.1 a), by
let φij : ContinuousMonoidHom (S.X j) (S.X i) :=
{ toMonoidHom :=
{ toFun := S.map hij
map_one' := ProCGroups.InverseSystems.IsGroupSystem.map_one (S := S) hij
map_mul' := ProCGroups.InverseSystems.IsGroupSystem.map_mul (S := S) hij }
continuous_toFun := S.continuous_map hij }
simpa [Function.comp] using
topologicallyGenerates_range_comp_of_surjective
(G := S.X j) (H := S.X i) φij (hsurj hij) g.1 g.2⟩
continuous_map := fun {_i _j} _hij => by
exact continuous_of_discreteTopology
map_id := fun i => by
ext g a
simp only [InverseSystems.InverseSystem.map_id_apply, id_eq]
map_comp := fun hij hjk => by
ext g a
simp only [Function.comp_apply, InverseSystems.InverseSystem.map_comp_apply]}
have hTnonempty : ∀ i, Nonempty (T.X i) := by
intro i
have hfg : TopologicallyFinitelyGenerated (S.X i) :=
topologicallyFinitelyGenerated_of_finite (G := S.X i)
rcases exists_generatingTuple_of_topologicalRank_le_of_finite
(G := S.X i) hfg (hbound i) with ⟨g, hg⟩
exact ⟨⟨g, hg⟩⟩
letI : ∀ i, Nonempty (T.X i) := hTnonempty
letI : ∀ i, Finite (T.X i) := fun _ => inferInstance
rcases ProCGroups.InverseSystems.InverseSystem.nonempty_inverseLimit_of_finite
(S := T) hdir with ⟨x⟩
let g : Fin n → S.inverseLimit := fun a =>
⟨fun i => (x.1 i).1 a, by
intro i j hij
have hcompat := congrArg Subtype.val (x.2 i j hij)
exact congrArg (fun f => f a) hcompat⟩
have hgproj : ∀ i, TopologicallyGenerates (G := S.X i) (S.projection i '' Set.range g) := by
intro i
rw [← Set.range_comp (S.projection i) g]
simpa [g, Function.comp] using (x.1 i).2
have hggen : TopologicallyGenerates (G := S.inverseLimit) (Set.range g) := by
exact
(topologicallyGenerates_iff_forall_projection_inverseLimit
(S := S) hdir hsurj (X := Set.range g)).2 hgproj
let s : Finset S.inverseLimit := Finset.univ.image g
have hs_card : s.card ≤ n := by
simpa [s] using (Finset.card_image_le (f := g) (s := (Finset.univ : Finset (Fin n))))
have hsgen : TopologicallyGenerates (G := S.inverseLimit) (↑s : Set S.inverseLimit) := by
simpa [s, Finset.coe_image] using hggen
exact topologicalRank_le_of_topologicallyGeneratedByAtMost (G := S.inverseLimit)
⟨s, hs_card, hsgen⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. 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.
□