ProCGroups.Generation.QuotientCriteria
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
import
theorem topologicallyGenerates_iff_forall_projection_inverseLimit
{I : Type v} [Preorder I] {S : InverseSystem (I := I)} [Nonempty I]
[∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
[∀ i, IsTopologicalGroup (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))
{X : Set S.inverseLimit} :
TopologicallyGenerates (G := S.inverseLimit) X ↔
∀ i, TopologicallyGenerates (G := S.X i) (S.projection i '' X)Topological generation in a surjective inverse system can be checked after every projection.
Show proof
by
classical
constructor
· intro hX i
let πi : S.inverseLimit →* S.X i := {
toFun := fun x => S.projection i x
map_one' := rfl
map_mul' := by
intro x y
rfl
}
have hπsurj : Function.Surjective πi := S.surjective_π hdir hsurj i
have hmap :
(Subgroup.closure X).map πi = Subgroup.closure (S.projection i '' X) := by
simpa [πi] using (MonoidHom.map_closure πi X)
have htop :
((Subgroup.closure X).map πi).topologicalClosure = ⊤ := by
have hX' : (Subgroup.closure X).topologicalClosure = ⊤ := by
simpa [TopologicallyGenerates] using hX
exact DenseRange.topologicalClosure_map_subgroup
(f := πi) (hf := S.continuous_projection i) (hf' := hπsurj.denseRange) hX'
simpa [TopologicallyGenerates, hmap] using htop
· intro hproj
let Y : Set S.inverseLimit :=
(((Subgroup.closure X).topologicalClosure : Subgroup S.inverseLimit) : Set S.inverseLimit)
have hYclosed : IsClosed Y := Subgroup.isClosed_topologicalClosure _
have hprojY : ∀ i, S.projection i '' Y = (Set.univ : Set (S.X i)) := by
intro i
let πi : S.inverseLimit →* S.X i := {
toFun := fun x => S.projection i x
map_one' := rfl
map_mul' := by
intro x y
rfl
}
have hmap :
(Subgroup.closure X).map πi = Subgroup.closure (S.projection i '' X) := by
simpa [πi] using (MonoidHom.map_closure πi X)
have hsubset :
((Subgroup.closure (S.projection i '' X) : Subgroup (S.X i)) : Set (S.X i)) ⊆ S.projection i '' Y := by
intro y hy
have hy' : y ∈ (Subgroup.closure X).map πi := by
simpa [hmap] using hy
rcases hy' with ⟨z, hz, rfl⟩
exact ⟨z, Subgroup.le_topologicalClosure _ hz, rfl⟩
have hclosedImg : IsClosed (S.projection i '' Y) := by
exact (hYclosed.isCompact.image (S.continuous_projection i)).isClosed
have hdense :
Dense (((Subgroup.closure (S.projection i '' X) : Subgroup (S.X i)) : Set (S.X i))) :=
(topologicallyGenerates_iff_dense (G := S.X i) (X := S.projection i '' X)).1 (hproj i)
apply Set.eq_univ_iff_forall.2
intro y
have hy' :
y ∈ closure (((Subgroup.closure (S.projection i '' X) : Subgroup (S.X i)) : Set (S.X i))) := by
rw [hdense.closure_eq]
simp only [mem_univ]
exact closure_minimal hsubset hclosedImg hy'
have hYuniv : Y = (Set.univ : Set S.inverseLimit) := by
ext x
constructor
· intro hx
simp only [mem_univ]
· intro _
rw [S.mem_isClosed_iff_forall_projection_mem hdir hYclosed]
intro i
rw [hprojY i]
simp only [InverseSystem.projection_apply, mem_univ]
rw [TopologicallyGenerates]
exact SetLike.ext' hYunivProof. 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_union_subgroup_iff_forall_openNormalQuotient
(hG : IsProfiniteGroup G) {N : Subgroup G} [N.Normal]
{X : Set G} :
TopologicallyGenerates (G := G) (X ∪ (N : Set G)) ↔
∀ U : OpenNormalSubgroup G, N ≤ (U : Subgroup G) →
TopologicallyGenerates (G := G ⧸ (U : Subgroup G))
((QuotientGroup.mk' (U : Subgroup G)) '' X)A closed-normal quotient version of topological generation: \(X \cup N\) generates if and only if the image of \(X\) generates modulo every open normal subgroup containing \(N\).
Show proof
by
classical
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : TotallyDisconnectedSpace G :=
IsProfiniteGroup.totallyDisconnectedSpace hG
letI : T2Space G := IsProfiniteGroup.t2Space hG
constructor
· intro hX U hNU
have hmap :
TopologicallyGenerates (G := G ⧸ (U : Subgroup G))
((QuotientGroup.mk' (U : Subgroup G)) '' (X ∪ (N : Set G))) :=
topologicallyGenerates_quotient_image (G := G) (N := (U : Subgroup G)) hX
have himg :
(QuotientGroup.mk' (U : Subgroup G) '' (X ∪ (N : Set G))) =
((QuotientGroup.mk' (U : Subgroup G)) '' X) ∪
({1} : Set (G ⧸ (U : Subgroup G))) := by
ext y
constructor
· intro hy
rcases hy with ⟨x, hx, rfl⟩
rcases hx with hxX | hxN
· exact Or.inl ⟨x, hxX, rfl⟩
· exact Or.inr (by
simp only [QuotientGroup.mk'_apply, mem_singleton_iff, QuotientGroup.eq_one_iff, hNU hxN])
· intro hy
rcases hy with hyX | hy1
· rcases hyX with ⟨x, hxX, rfl⟩
exact ⟨x, Or.inl hxX, rfl⟩
· refine ⟨1, Or.inr N.one_mem, ?_⟩
simpa using hy1.symm
have hmap' :
TopologicallyGenerates (G := G ⧸ (U : Subgroup G))
((((QuotientGroup.mk' (U : Subgroup G)) '' X) ∪
({1} : Set (G ⧸ (U : Subgroup G))))) := by
rwa [← himg]
exact
(topologicallyGenerates_union_one_iff
(G := G ⧸ (U : Subgroup G))
(X := ((QuotientGroup.mk' (U : Subgroup G)) '' X))).1 hmap'
· intro hquot
let H : ClosedSubgroup G :=
{ toSubgroup := (Subgroup.closure (X ∪ (N : Set G))).topologicalClosure
isClosed' := Subgroup.isClosed_topologicalClosure _ }
have hXleH : X ⊆ (H : Subgroup G) := by
intro x hx
exact Subgroup.le_topologicalClosure _
(Subgroup.subset_closure (Or.inl hx))
have hNleH : N ≤ (H : Subgroup G) := by
intro n hn
exact Subgroup.le_topologicalClosure _
(Subgroup.subset_closure (Or.inr hn))
by_contra hH
change ¬ ((Subgroup.closure (X ∪ (N : Set G))).topologicalClosure = ⊤) at hH
have hHproper :
((H : Subgroup G) : Set G) ≠ (Set.univ : Set G) := by
intro hEq
apply hH
change (H : Subgroup G) = ⊤
ext x
constructor
· intro _
simp only [Subgroup.mem_top]
· intro _
have hx' : x ∈ (Set.univ : Set G) := by simp only [mem_univ]
rwa [← hEq] at hx'
have hxNotAll : ¬ ∀ x : G, x ∈ ((H : Subgroup G) : Set G) := by
simpa [Set.eq_univ_iff_forall] using hHproper
push_neg at hxNotAll
rcases hxNotAll with ⟨x, hxH⟩
have hxNotAll :
¬ ∀ V : Subgroup G, IsOpen (V : Set G) → (H : Subgroup G) ≤ V → x ∈ V := by
intro hxAll
apply hxH
change x ∈ (H : Subgroup G)
rw [closedSubgroup_eq_sInf_open (G := G) H]
rw [Subgroup.mem_sInf]
intro V hV
exact hxAll V hV.1 hV.2
push_neg at hxNotAll
rcases hxNotAll with ⟨V, hVopen, hHV, hxV⟩
have hVfin : Subgroup.FiniteIndex V := by
letI : Finite (G ⧸ V) := Subgroup.quotient_finite_of_isOpen V hVopen
exact Subgroup.finiteIndex_of_finite_quotient
letI : Subgroup.FiniteIndex V := hVfin
let U : OpenNormalSubgroup G :=
{ toSubgroup := Subgroup.normalCore V
isOpen' := Subgroup.isOpen_of_isClosed_of_finiteIndex _ (V.normalCore_isClosed
(Subgroup.isClosed_of_isOpen V hVopen)) }
letI : (U : Subgroup G).Normal := U.isNormal'
have hNU : N ≤ (U : Subgroup G) :=
(Subgroup.normal_le_normalCore).2 (hNleH.trans hHV)
have hUV : (U : Subgroup G) ≤ V := by
change Subgroup.normalCore V ≤ V
exact Subgroup.normalCore_le V
have hxU : x ∉ (U : Set G) := by
intro hxU
exact hxV (hUV hxU)
have hgen := hquot U hNU
let qH : Subgroup (G ⧸ (U : Subgroup G)) :=
(H : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G))
have himage_le_qH :
((QuotientGroup.mk' (U : Subgroup G)) '' X) ⊆
(qH : Set (G ⧸ (U : Subgroup G))) := by
intro y hy
rcases hy with ⟨z, hzX, rfl⟩
exact ⟨z, hXleH hzX, rfl⟩
have hcl_le_qH :
Subgroup.closure (((QuotientGroup.mk' (U : Subgroup G)) '' X)) ≤ qH :=
(Subgroup.closure_le (K := qH)).2 himage_le_qH
have hclosure_le_qH :
(Subgroup.closure (((QuotientGroup.mk' (U : Subgroup G)) '' X))).topologicalClosure ≤
qH := by
letI : DiscreteTopology (G ⧸ (U : Subgroup G)) :=
QuotientGroup.discreteTopology U.toOpenSubgroup.isOpen'
have hqHclosed : IsClosed (qH : Set (G ⧸ (U : Subgroup G))) := by
exact isClosed_discrete (qH : Set (G ⧸ (U : Subgroup G)))
exact Subgroup.topologicalClosure_minimal _ hcl_le_qH hqHclosed
let qx : G ⧸ (U : Subgroup G) := QuotientGroup.mk' (U : Subgroup G) x
have hx_not_qH : qx ∉ (qH : Set (G ⧸ (U : Subgroup G))) := by
intro hxq
rcases hxq with ⟨z, hzH, hzx⟩
have hzV : z ∈ V := hHV hzH
have hdiv : z⁻¹ * x ∈ (U : Subgroup G) := by
exact (QuotientGroup.eq).1 hzx
have hdivV : z⁻¹ * x ∈ V := hUV hdiv
have hxV' : x ∈ V := by
simpa [mul_assoc] using V.mul_mem hzV hdivV
exact hxV hxV'
have hxtop : qx ∈ (((⊤ : Subgroup (G ⧸ (U : Subgroup G))) :
Set (G ⧸ (U : Subgroup G)))) := by
simp only [Subgroup.coe_top, mem_univ]
have htop :
(⊤ : Subgroup (G ⧸ (U : Subgroup G))) ≤
(Subgroup.closure (((QuotientGroup.mk' (U : Subgroup G)) '' X))).topologicalClosure := by
simpa [TopologicallyGenerates] using hgen
exact hx_not_qH (hclosure_le_qH (htop hxtop))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\). 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem topologicallyGenerates_iff_forall_quotientProj_image
(hG : IsProfiniteGroup G) {X : Set G} :
TopologicallyGenerates (G := G) X ↔
∀ U : OpenNormalSubgroup G,
TopologicallyGenerates (G := G ⧸ (U : Subgroup G))
(OpenNormalSubgroup.quotientProj U '' X)This is the direct finite-quotient test for topological generation, phrased with the bundled quotient projections.
Show proof
by
letI : T2Space G := IsProfiniteGroup.t2Space hG
have h :=
topologicallyGenerates_union_subgroup_iff_forall_openNormalQuotient
(G := G) hG (N := (⊥ : Subgroup G)) (X := X)
constructor
· intro hX U
have hUnion :
TopologicallyGenerates (G := G) (X ∪ (((⊥ : Subgroup G) : Set G))) := by
rw [show X ∪ (((⊥ : Subgroup G) : Set G)) = X ∪ ({1} : Set G) by
ext x
simp only [Subgroup.coe_bot, union_singleton, mem_insert_iff]]
exact (topologicallyGenerates_union_one_iff (G := G) (X := X)).2 hX
simpa [OpenNormalSubgroup.quotientProj] using h.1 hUnion U bot_le
· intro hquot
have hUnion :
TopologicallyGenerates (G := G) (X ∪ (((⊥ : Subgroup G) : Set G))) :=
h.2 (fun U _hU => by
simpa [OpenNormalSubgroup.quotientProj] using hquot U)
have hUnionOne : TopologicallyGenerates (G := G) (X ∪ ({1} : Set G)) := by
rw [show X ∪ ({1} : Set G) = X ∪ (((⊥ : Subgroup G) : Set G)) by
ext x
simp only [union_singleton, mem_insert_iff, Subgroup.coe_bot]]
exact hUnion
exact (topologicallyGenerates_union_one_iff (G := G) (X := X)).1 hUnionOneProof. 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.
□