ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods
This module studies closed subgroup neighborhoods for pro cgroups. Given an open subgroup of a closed subgroup of a profinite group, one can shrink it to the intersection with an ambient open normal subgroup. Class-restricted version of \(exists_openNormalSubgroup_inter_closedSubgroup_le\) for a closed subgroup of a pro-\(C\) group.
import
theorem exists_openNormalSubgroup_inter_closedSubgroup_le
(hG : IsProfiniteGroup G) (H : ClosedSubgroup G) (U : OpenSubgroup H) :
∃ V : OpenNormalSubgroup G,
(OpenNormalSubgroup.comap ((H : Subgroup G).subtype) continuous_subtype_val V : Subgroup H) ≤
(U : Subgroup H)Given an open subgroup of a closed subgroup of a profinite group, one can shrink it to the intersection with an ambient open normal subgroup.
Show proof
by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : T2Space G := IsProfiniteGroup.t2Space hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
have hU_nhds : (((U : Subgroup H) : Set H)) ∈ 𝓝 (1 : H) := by
exact U.isOpen'.mem_nhds U.one_mem'
rcases (mem_nhds_subtype (H : Set G) (1 : H) (((U : Subgroup H) : Set H))).1 hU_nhds with
⟨W, hW_nhds, hWU⟩
rcases mem_nhds_iff.mp hW_nhds with ⟨W', hW'W, hW'open, h1W'⟩
rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW'open h1W' with ⟨V, hVW'⟩
refine ⟨V, ?_⟩
intro x hx
exact hWU <| by
change x.1 ∈ W
exact hW'W (hVW' 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. 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 exists_openNormalSubgroupInClass_inter_closedSubgroup_le
{C : FiniteGroupClass.{u}} (hG : IsProCGroup C G)
(H : ClosedSubgroup G) (U : OpenSubgroup H) :
∃ V : OpenNormalSubgroupInClass C G,
(OpenNormalSubgroup.comap ((H : Subgroup G).subtype) continuous_subtype_val V.1 :
Subgroup H) ≤
(U : Subgroup H)Class-restricted version of \(exists_openNormalSubgroup_inter_closedSubgroup_le\) for a closed subgroup of a pro-\(C\) group.
Show proof
by
letI : CompactSpace G := IsProCGroup.compactSpace hG
letI : T2Space G := IsProCGroup.t2Space hG
letI : TotallyDisconnectedSpace G := IsProCGroup.totallyDisconnectedSpace hG
have hU_nhds : (((U : Subgroup H) : Set H)) ∈ 𝓝 (1 : H) := by
exact U.isOpen'.mem_nhds U.one_mem'
rcases (mem_nhds_subtype (H : Set G) (1 : H) (((U : Subgroup H) : Set H))).1
hU_nhds with
⟨W, hW_nhds, hWU⟩
rcases mem_nhds_iff.mp hW_nhds with ⟨W', hW'W, hW'open, h1W'⟩
rcases hG.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW'open h1W' with
⟨V, hVW'⟩
refine ⟨V, ?_⟩
intro x hx
exact hWU <| by
change x.1 ∈ W
exact hW'W (hVW' 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. 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. 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.
□