ProCGroups.Generation.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.Topology.Algebra.ClopenNhdofOne
- Mathlib.Topology.Algebra.ContinuousMonoidHom
def TopologicallyGenerates (X : Set G) : Prop :=
(Subgroup.closure X).topologicalClosure = ⊤X topologically generates G if the abstract subgroup generated by X is dense in G.
def ConvergesToOne (X : Set G) : Prop :=
∀ U : OpenSubgroup G, (X \ (U : Set G)).FiniteA family \(X\) converges to \(1\) if every open subgroup contains all but finitely many elements of \(X\).
theorem ConvergesToOne.of_finite {X : Set G} (hX : X.Finite) :
ConvergesToOne (G := G) XA finite set converges to \(1\) in the coarse sense used for profinite generating families.
Show proof
by
intro U
exact hX.subset (by
intro x hx
exact hx.1)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. 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.
□def GeneratesAndConvergesToOne (X : Set G) : Prop :=
TopologicallyGenerates (G := G) X ∧ ConvergesToOne (G := G) XThis structure records a generating set that converges to \(1\).
noncomputable def topologicalRank
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
Cardinal :=
sInf {κ : Cardinal | ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X ∧ Cardinal.mk X = κ}The minimal cardinality of a generating set converging to \(1\). This is the topological rank usually denoted \(d(G)\) in the profinite-group literature.
theorem topologicalRank_le_mk_of_generatesAndConvergesToOne {X : Set G}
(hX : GeneratesAndConvergesToOne (G := G) X) :
topologicalRank G ≤ Cardinal.mk XThe topological rank is bounded by the cardinality of any generating set converging to \(1\).
Show proof
by
change sInf {κ : Cardinal |
∃ X : Set G, GeneratesAndConvergesToOne (G := G) X ∧ Cardinal.mk X = κ} ≤
Cardinal.mk X
exact csInf_le' ⟨X, hX, rfl⟩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 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 exists_generatesAndConvergesToOne_card_eq_topologicalRank
(h : ∃ X : Set G, GeneratesAndConvergesToOne (G := G) X) :
∃ X : Set G, GeneratesAndConvergesToOne (G := G) X ∧
Cardinal.mk X = topologicalRank GShow proof
by
let C : Set Cardinal := {κ : Cardinal |
∃ X : Set G, GeneratesAndConvergesToOne (G := G) X ∧ Cardinal.mk X = κ}
have hC : C.Nonempty := by
rcases h with ⟨X, hX⟩
exact ⟨Cardinal.mk X, X, hX, rfl⟩
simpa [topologicalRank, C] using (csInf_mem hC)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. 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.
□def wordProducts (X : Set G) : ℕ → Set G
| 0 => {1}
| n + 1 => wordProducts X n * XIterated products of words in \(X\), with \(\mathrm{wordProducts}(X,0)=\{1\}\) and \(\mathrm{wordProducts}(X,n+1)=\mathrm{wordProducts}(X,n)\cdot X\).
theorem topologicallyGenerates_iff_dense {X : Set G} :
TopologicallyGenerates (G := G) X ↔ Dense ((Subgroup.closure X : Subgroup G) : Set G)Topological generation is equivalently density of the abstract subgroup generated by the set.
Show proof
by
rw [TopologicallyGenerates, SetLike.ext'_iff, Subgroup.topologicalClosure_coe, Subgroup.coe_top,
dense_iff_closure_eq]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 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 continuousMonoidHom_ext_of_topologicallyGenerates
{R : Type v} [Group R] [TopologicalSpace R] [T2Space R]
{X : Set G} (hX : TopologicallyGenerates (G := G) X)
{f g : ContinuousMonoidHom G R} (hfg : ∀ x ∈ X, f x = g x) :
f = gContinuous homomorphisms out of a topologically generated group are determined by their values on the generating set.
Show proof
by
let K : Subgroup G := {
carrier := { x | f x = g x }
one_mem' := by simp only [mem_setOf_eq, map_one]
mul_mem' := by
intro a b ha hb
change f (a * b) = g (a * b)
rw [map_mul, map_mul, ha, hb]
inv_mem' := by
intro a ha
simpa using congrArg Inv.inv ha
}
have hKclosed : IsClosed ((K : Subgroup G) : Set G) := by
change IsClosed { x | f x = g x }
exact isClosed_eq f.continuous_toFun g.continuous_toFun
have hsub : Subgroup.closure X ≤ K := by
rw [Subgroup.closure_le]
intro x hx
exact hfg x hx
have htop : (⊤ : Subgroup G) ≤ K := by
have hcl : (Subgroup.closure X).topologicalClosure ≤ K :=
Subgroup.topologicalClosure_minimal _ hsub hKclosed
rw [TopologicallyGenerates] at hX
simpa [hX] using hcl
ext x
simpa [K] using htop (show x ∈ (⊤ : Subgroup G) from by 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. 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.
□def closedSubgroupGenerated (X : Set G) : ClosedSubgroup G where
toSubgroup := (Subgroup.closure X).topologicalClosure
isClosed' := Subgroup.isClosed_topologicalClosure _The closed subgroup topologically generated by a set.
def closedSubgroupGeneratedMap {A : Type v} (φ : A → G) :
A → (closedSubgroupGenerated (G := G) (Set.range φ) : Subgroup G) :=
fun a =>
⟨φ a, Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨a, rfl⟩)⟩The canonical map from an indexed family into the closed subgroup it topologically generates.
theorem closedSubgroupGeneratedMap_topologicallyGenerates {A : Type v} (φ : A → G) :
TopologicallyGenerates
(G := (closedSubgroupGenerated (G := G) (Set.range φ) : Subgroup G))
(Set.range (closedSubgroupGeneratedMap (G := G) φ))The canonical indexed family topologically generates its closed generated subgroup.
Show proof
by
let K : ClosedSubgroup G := closedSubgroupGenerated (G := G) (Set.range φ)
let φK : A → (K : Subgroup G) := closedSubgroupGeneratedMap (G := G) φ
let L : Subgroup (K : Subgroup G) := Subgroup.closure (Set.range φK)
have hmap :
Subgroup.map (K : Subgroup G).subtype L = Subgroup.closure (Set.range φ) := by
refine le_antisymm ?_ ?_
· rw [Subgroup.map_le_iff_le_comap, Subgroup.closure_le]
rintro y ⟨a, rfl⟩
exact Subgroup.subset_closure ⟨a, rfl⟩
· rw [Subgroup.closure_le]
rintro y ⟨a, rfl⟩
change φ a ∈ Subgroup.map (K : Subgroup G).subtype L
exact ⟨φK a, Subgroup.subset_closure ⟨a, rfl⟩, rfl⟩
have himage :
((Subtype.val : ↥(K : Subgroup G) → G) ''
((L : Subgroup ↥(K : Subgroup G)) : Set ↥(K : Subgroup G))) =
((Subgroup.map (K : Subgroup G).subtype L : Subgroup G) : Set G) := by
ext y
constructor
· rintro ⟨z, hz, rfl⟩
exact ⟨z, hz, rfl⟩
· rintro ⟨z, hz, hzy⟩
exact ⟨z, hz, hzy⟩
rw [topologicallyGenerates_iff_dense, dense_iff_closure_eq]
ext y
constructor
· intro _
simp only [mem_univ]
· intro _
change y ∈ closure ((L : Subgroup K) : Set K)
rw [closure_subtype]
change (y : G) ∈
closure
(((Subtype.val : ↥(K : Subgroup G) → G) ''
((L : Subgroup ↥(K : Subgroup G)) : Set ↥(K : Subgroup G))))
rw [himage, hmap]
change (y : G) ∈ ((Subgroup.closure (Set.range φ)).topologicalClosure : Set G)
exact y.2Proof. 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 map_mem_closedSubgroupGenerated_image
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(φ : G →ₜ* H) {X : Set G} {y : G}
(hy : y ∈ (closedSubgroupGenerated (G := G) X : Subgroup G)) :
φ y ∈ (closedSubgroupGenerated (G := H) (φ '' X) : Subgroup H)Membership in a closed generated subgroup is preserved by continuous homomorphisms, after mapping the generating set.
Show proof
by
let K : Subgroup G :=
(closedSubgroupGenerated (G := H) (φ '' X) : Subgroup H).comap (φ : G →* H)
have hX : X ⊆ K := by
intro x hx
exact Subgroup.le_topologicalClosure _ (Subgroup.subset_closure ⟨x, hx, rfl⟩)
have hKclosed : IsClosed (K : Set G) := by
change IsClosed {x : G | φ x ∈
(closedSubgroupGenerated (G := H) (φ '' X) : Subgroup H)}
exact (closedSubgroupGenerated (G := H) (φ '' X)).isClosed'.preimage φ.continuous
exact
(Subgroup.topologicalClosure_minimal _
((Subgroup.closure_le (K := K)).2 hX) hKclosed) 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. 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. 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 map_mem_closedSubgroupGenerated_singleton
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(φ : G →ₜ* H) (x : G) {y : G}
(hy : y ∈ (closedSubgroupGenerated (G := G) ({x} : Set G) : Subgroup G)) :
φ y ∈ (closedSubgroupGenerated (G := H) ({φ x} : Set H) : Subgroup H)Membership in a topologically generated cyclic closed subgroup is preserved by continuous homomorphisms.
Show proof
by
simpa using
(map_mem_closedSubgroupGenerated_image (G := G) (H := H) φ
(X := ({x} : Set G)) hy)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. 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 zpowers_subtype_topologically_generated_by_generator
{G₀ : Type*} [Group G₀] (g : G₀) :
let cyc : Subgroup G₀The distinguished element g algebraically generates its subgroup of powers.
Show proof
Subgroup.zpowers g
let gcyc : cyc := ⟨g, Subgroup.mem_zpowers_iff.mpr ⟨1, by simp only [zpow_one]⟩⟩
∀ z : cyc, z ∈ Subgroup.zpowers gcyc := by
intro cyc gcyc z
rcases Subgroup.mem_zpowers_iff.mp z.2 with ⟨k, hk⟩
refine Subgroup.mem_zpowers_iff.mpr ⟨k, ?_⟩
apply Subtype.ext
simpa [gcyc] using hkProof. 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 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 map_mem_zpowers_of_topologicallyGenerates_singleton
{A : Type u} [TopologicalSpace A] [Group A] [IsTopologicalGroup A]
{B : Type v} [TopologicalSpace B] [Group B] [IsTopologicalGroup B]
[DiscreteTopology B]
(f : A →ₜ* B) {x a : A}
(hxgen : TopologicallyGenerates (G := A) ({x} : Set A)) :
f a ∈ Subgroup.zpowers (f x)Show proof
by
have ha_closed :
a ∈ (closedSubgroupGenerated ({x} : Set A) : Subgroup A) := by
have htop :
(closedSubgroupGenerated ({x} : Set A) : Subgroup A) = ⊤ := by
simpa [closedSubgroupGenerated] using hxgen
rw [htop]
simp only [Subgroup.mem_top]
have hfa_closed :
f a ∈ (closedSubgroupGenerated ({f x} : Set B) : Subgroup B) :=
map_mem_closedSubgroupGenerated_singleton f x ha_closed
have hclosure_eq :
(Subgroup.closure ({f x} : Set B)).topologicalClosure =
Subgroup.closure ({f x} : Set B) := by
ext y
change y ∈ closure (((Subgroup.closure ({f x} : Set B) : Subgroup B) : Set B)) ↔
y ∈ ((Subgroup.closure ({f x} : Set B) : Subgroup B) : Set B)
rw [closure_discrete]
have hfa_closure :
f a ∈ Subgroup.closure ({f x} : Set B) := by
simpa [closedSubgroupGenerated, hclosure_eq] using hfa_closed
simpa [Subgroup.zpowers_eq_closure] using hfa_closureProof. 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 monoidHom_map_mem_zpowers_of_topologicallyGenerates_singleton
{A : Type u} [TopologicalSpace A] [Group A] [IsTopologicalGroup A]
{B : Type v} [TopologicalSpace B] [Group B] [IsTopologicalGroup B]
[DiscreteTopology B]
(f : A →* B) (hf : Continuous f) {x a : A}
(hxgen : TopologicallyGenerates (G := A) ({x} : Set A)) :
f a ∈ Subgroup.zpowers (f x)MonoidHom version of map_mem_zpowers_of_topologicallyGenerates_singleton.
Show proof
by
let fcont : A →ₜ* B :=
{ toMonoidHom := f
continuous_toFun := hf }
simpa [fcont] using
map_mem_zpowers_of_topologicallyGenerates_singleton
(A := A) fcont hxgen (a := a)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. 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 zpowers_image_le_closedSubgroupGenerated_map
{Q : Type u} [TopologicalSpace Q] [Group Q] [IsTopologicalGroup Q]
{B : Type v} [Group B]
(q : Q →* B) (x : Q) :
Subgroup.zpowers (q x) ≤
((closedSubgroupGenerated ({x} : Set Q) : ClosedSubgroup Q) :
Subgroup Q).map qAlgebraic powers of the image of \(x\) lie in the image of the closed subgroup generated by \(x\).
Show proof
by
intro b hb
rcases (Subgroup.mem_zpowers_iff.mp hb) with ⟨k, rfl⟩
refine ⟨x ^ k, ?_, by simp only [map_zpow]⟩
have hxmem :
x ∈ ((closedSubgroupGenerated ({x} : Set Q) : ClosedSubgroup Q) :
Subgroup Q) := by
change x ∈ (Subgroup.closure ({x} : Set Q)).topologicalClosure
exact Subgroup.le_topologicalClosure _
(Subgroup.subset_closure (by simp only [Set.mem_singleton_iff]))
exact
((closedSubgroupGenerated ({x} : Set Q) : ClosedSubgroup Q) :
Subgroup Q).zpow_mem hxmem kProof. 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. 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_singleton_of_denseRange_mint
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(f : Multiplicative ℤ →* H) (hf : DenseRange f) :
TopologicallyGenerates (G := H) ({f (Multiplicative.ofAdd 1)} : Set H)A dense homomorphic image of the infinite cyclic group is topologically generated by the image of \(1\).
Show proof
by
let g : H := f (Multiplicative.ofAdd 1)
have hsubset :
Set.range f ⊆
(((Subgroup.closure ({g} : Set H)).topologicalClosure : Subgroup H) : Set H) := by
intro y hy
rcases hy with ⟨n, rfl⟩
have hz : f n ∈ Subgroup.zpowers g := by
have hEq : f n = g ^ n.toAdd := by
simpa [g] using (MonoidHom.apply_mint (f := f) (n := n))
rw [hEq]
exact (Subgroup.zpowers g).zpow_mem (Subgroup.mem_zpowers g) n.toAdd
exact Subgroup.le_topologicalClosure _
(by simpa [g, Subgroup.zpowers_eq_closure] using hz)
have hclosure :
closure (Set.range f) ⊆
(((Subgroup.closure ({g} : Set H)).topologicalClosure : Subgroup H) : Set H) :=
closure_minimal hsubset (Subgroup.isClosed_topologicalClosure _)
rw [TopologicallyGenerates]
apply top_unique
intro x _hx
have hx' : x ∈ closure (Set.range f) := by
rw [hf.closure_range]
simp only [mem_univ]
exact hclosure hx'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 topologicallyGenerates_closure_iff {X : Set G} :
TopologicallyGenerates (G := G) X ↔ TopologicallyGenerates (G := G) (closure X)Topological generation is unchanged by closing the generating set.
Show proof
by
constructor
· intro hX
have hsub :
Subgroup.closure X ≤ (Subgroup.closure (closure X)).topologicalClosure := by
exact (Subgroup.closure_mono subset_closure).trans (Subgroup.le_topologicalClosure _)
have hle :
(Subgroup.closure X).topologicalClosure ≤
(Subgroup.closure (closure X)).topologicalClosure := by
exact Subgroup.topologicalClosure_minimal _ hsub (Subgroup.isClosed_topologicalClosure _)
have htop : (⊤ : Subgroup G) ≤ (Subgroup.closure X).topologicalClosure := by
rw [hX]
exact top_unique (htop.trans hle)
· intro hX
have hsubset : closure X ⊆ ((Subgroup.closure X).topologicalClosure : Set G) := by
refine closure_minimal ?_ (Subgroup.isClosed_topologicalClosure _)
intro x hx
exact (Subgroup.le_topologicalClosure (Subgroup.closure X)) (Subgroup.subset_closure hx)
have hsub : Subgroup.closure (closure X) ≤ (Subgroup.closure X).topologicalClosure := by
exact (Subgroup.closure_le (K := (Subgroup.closure X).topologicalClosure)).2 hsubset
have hle :
(Subgroup.closure (closure X)).topologicalClosure ≤
(Subgroup.closure X).topologicalClosure := by
exact Subgroup.topologicalClosure_minimal _ hsub (Subgroup.isClosed_topologicalClosure _)
have htop : (⊤ : Subgroup G) ≤ (Subgroup.closure (closure X)).topologicalClosure := by
rw [hX]
exact top_unique (htop.trans hle)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 topologicallyGenerates_insert_one_iff {X : Set G} :
TopologicallyGenerates (G := G) (insert (1 : G) X) ↔ TopologicallyGenerates (G := G) XAdding \(1\) to a topological generating set does not change generation.
Show proof
by
simp only [TopologicallyGenerates, Subgroup.closure_insert_one]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 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 topologicallyGenerates_union_one_iff {X : Set G} :
TopologicallyGenerates (G := G) (X ∪ ({1} : Set G)) ↔ TopologicallyGenerates (G := G) XUnion with \(\{1\}\) does not change topological generation.
Show proof
by
simpa [Set.union_singleton] using topologicallyGenerates_insert_one_iff (G := G) (X := X)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 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 closure_nontrivial_range_eq_closure_range
{α : Type v} (f : α → G) :
Subgroup.closure ({g | ∃ a, g = f a ∧ g ≠ 1} : Set G) =
Subgroup.closure (Set.range f)Removing occurrences of 1 from a parametrized generating range does not change its abstract subgroup closure.
Show proof
by
apply le_antisymm
· exact Subgroup.closure_mono (by
rintro g ⟨a, rfl, _⟩
exact ⟨a, rfl⟩)
· have hrange :
Set.range f ⊆ insert (1 : G) ({g | ∃ a, g = f a ∧ g ≠ 1} : Set G) := by
rintro g ⟨a, rfl⟩
by_cases h : f a = 1
· exact Or.inl h
· exact Or.inr ⟨a, rfl, h⟩
refine (Subgroup.closure_mono hrange).trans ?_
exact le_of_eq (Subgroup.closure_insert_one ({g | ∃ a, g = f a ∧ g ≠ 1} : Set 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. 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 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. 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_mono {X Y : Set G}
(hX : TopologicallyGenerates (G := G) X) (hXY : X ⊆ Y) :
TopologicallyGenerates (G := G) YTopological generation is monotone in the generating set.
Show proof
by
have hle :
(Subgroup.closure X).topologicalClosure ≤ (Subgroup.closure Y).topologicalClosure := by
exact Subgroup.topologicalClosure_minimal _
((Subgroup.closure_mono hXY).trans (Subgroup.le_topologicalClosure _))
(Subgroup.isClosed_topologicalClosure _)
have htop : (⊤ : Subgroup G) ≤ (Subgroup.closure X).topologicalClosure := by
simpa [TopologicallyGenerates] using (show TopologicallyGenerates (G := G) X from hX)
exact top_unique (htop.trans hle)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 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 topologicallyGenerates_of_subset_closure {X Y : Set G}
(hX : TopologicallyGenerates (G := G) X)
(hXY : X ⊆ ((Subgroup.closure Y : Subgroup G) : Set G)) :
TopologicallyGenerates (G := G) YA topological generating set may be replaced by any set whose abstract closure contains it.
Show proof
by
have hle : Subgroup.closure X ≤ Subgroup.closure Y :=
(Subgroup.closure_le (K := Subgroup.closure Y)).2 hXY
have hle' :
(Subgroup.closure X).topologicalClosure ≤ (Subgroup.closure Y).topologicalClosure := by
exact Subgroup.topologicalClosure_minimal _
(hle.trans (Subgroup.le_topologicalClosure _))
(Subgroup.isClosed_topologicalClosure _)
have htop : (⊤ : Subgroup G) ≤ (Subgroup.closure X).topologicalClosure := by
simpa [TopologicallyGenerates] using (show TopologicallyGenerates (G := G) X from hX)
exact top_unique (htop.trans hle')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 topologicallyGenerates_image_of_continuousSurjective
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(f : G →* H) (hf : Continuous f) (hfsurj : Function.Surjective f)
{X : Set G} (hX : TopologicallyGenerates (G := G) X) :
TopologicallyGenerates (G := H) (f '' X)Topological generation pushes forward along continuous surjective homomorphisms.
Show proof
by
have hmap :
(Subgroup.closure X).map f = Subgroup.closure (f '' X) := by
simpa using MonoidHom.map_closure f X
have htop :
((Subgroup.closure X).map f).topologicalClosure = ⊤ := by
exact DenseRange.topologicalClosure_map_subgroup
(f := f)
(hf := hf)
(hf' := hfsurj.denseRange)
(by simpa [TopologicallyGenerates] using hX)
rw [TopologicallyGenerates, ← hmap]
exact htopProof. 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 topologicallyGenerates_image_of_continuousMonoidHom_surjective
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(f : G →ₜ* H) (hfsurj : Function.Surjective f)
{X : Set G} (hX : TopologicallyGenerates (G := G) X) :
TopologicallyGenerates (G := H) (f '' X)Continuous-homomorphism form of push-forward for topological generation.
Show proof
topologicallyGenerates_image_of_continuousSurjective
(G := G) (H := H) f.toMonoidHom f.continuous_toFun hfsurj hXProof. 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 continuousMonoidHom_surjective_of_topologicallyGenerates_subset_range
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
[CompactSpace G] [T2Space H]
(f : G →ₜ* H) {X : Set H} (hX : TopologicallyGenerates (G := H) X)
(hXrange : X ⊆ ((f.toMonoidHom.range : Subgroup H) : Set H)) :
Function.Surjective fA continuous homomorphism from a compact group onto a Hausdorff target is surjective as soon as its closed range contains a topological generating set of the target.
Show proof
by
have hrangeClosed : IsClosed (((f.toMonoidHom.range : Subgroup H) : Set H)) := by
have himage : IsCompact (f '' (Set.univ : Set G)) :=
isCompact_univ.image f.continuous_toFun
have hEq :
f '' (Set.univ : Set G) =
((f.toMonoidHom.range : Subgroup H) : Set H) := by
ext y
constructor
· rintro ⟨x, _hx, rfl⟩
exact ⟨x, rfl⟩
· rintro ⟨x, rfl⟩
exact ⟨x, trivial, rfl⟩
exact (hEq ▸ himage).isClosed
have hclosure_le :
(Subgroup.closure X).topologicalClosure ≤ f.toMonoidHom.range :=
Subgroup.topologicalClosure_minimal _
((Subgroup.closure_le (K := f.toMonoidHom.range)).2 hXrange) hrangeClosed
have htop : (⊤ : Subgroup H) ≤ f.toMonoidHom.range := by
rw [← hX]
exact hclosure_le
intro y
exact htop trivialProof. 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 topologicallyGenerates_quotient_image
(N : Subgroup G) [N.Normal]
{X : Set G} (hX : TopologicallyGenerates (G := G) X) :
TopologicallyGenerates (G := G ⧸ N) ((QuotientGroup.mk' N) '' X)Topological generation descends to every quotient by a normal subgroup.
Show proof
topologicallyGenerates_image_of_continuousSurjective
(G := G)
(H := G ⧸ N)
(QuotientGroup.mk' N)
continuous_quotient_mk'
(QuotientGroup.mk'_surjective N)
hXProof. 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 topologicallyGenerates_continuousMulEquiv_image
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(e : G ≃ₜ* H) {X : Set G} (hX : TopologicallyGenerates (G := G) X) :
TopologicallyGenerates (G := H) (e '' X)Topological generation is preserved by continuous multiplicative equivalences.
Show proof
topologicallyGenerates_image_of_continuousSurjective
(G := G) (H := H) e.toMonoidHom e.continuous e.surjective hXProof. 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. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums.
□theorem topologicallyGenerates_continuousMulEquiv_image_iff
{H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
(e : G ≃ₜ* H) {X : Set G} :
TopologicallyGenerates (G := H) (e '' X) ↔ TopologicallyGenerates (G := G) XTopological generation is transported across a continuous multiplicative equivalence.
Show proof
by
constructor
· intro h
have hpre :=
topologicallyGenerates_continuousMulEquiv_image
(G := H) (H := G) e.symm (X := e '' X) h
have hset : e.symm '' (e '' X) = X := by
ext x
constructor
· rintro ⟨y, ⟨z, hz, rfl⟩, rfl⟩
simpa using hz
· intro hx
exact ⟨e x, ⟨x, hx, rfl⟩, by simp only [ContinuousMulEquiv.symm_apply_apply]⟩
simpa [hset] using hpre
· exact topologicallyGenerates_continuousMulEquiv_image (G := G) (H := H) eProof. 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. Coefficient and scalar compatibility is verified without changing the support in the finite quotient: only coefficients are transported by the given ring homomorphism or scalar action. Linearity, multiplicativity, and the algebra-map identities then extend the singleton computation to arbitrary finite sums.
□