ProCGroups.ProC.OpenNormalSubgroups.ClosedAndCosets
This module studies closed and cosets for pro cgroups. A closed subgroup of a profinite group is the intersection of all open subgroups containing it. If the intersection of a family of subgroups is trivial, every nonidentity element is omitted by at least one member of the family.
theorem closedSubgroup_eq_sInf_open [CompactSpace G] [TotallyDisconnectedSpace G]
(H : ClosedSubgroup G) :
(H : Subgroup G) = sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N}A closed subgroup of a profinite group is the intersection of all open subgroups containing it.
Show proof
by
ext x
constructor
· intro hx
simp only [Subgroup.mem_sInf, Set.mem_setOf_eq]
intro N hN
exact hN.2 hx
· intro hx
by_contra hxH
let W : Set G := { y : G | x * y⁻¹ ∉ (H : Set G) }
have hW : IsOpen W := by
change IsOpen ((fun y : G => x * y⁻¹) ⁻¹' ((H : Set G)ᶜ))
exact H.isClosed'.isOpen_compl.preimage (continuous_const.mul continuous_inv)
have h1W : (1 : G) ∈ W := by
simpa [W] using hxH
rcases ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
(G := G) hW h1W with ⟨N, hNW⟩
let K : OpenSubgroup G :=
⟨(H : Subgroup G) ⊔ (N : Subgroup G),
Subgroup.isOpen_of_openSubgroup ((H : Subgroup G) ⊔ (N : Subgroup G))
(show (N : Subgroup G) ≤ (H : Subgroup G) ⊔ (N : Subgroup G) from le_sup_right)⟩
have hHK : (H : Subgroup G) ≤ (K : Subgroup G) := by
intro y hy
exact Subgroup.mem_sup_left hy
have hxK : x ∈ (K : Subgroup G) := by
have hxall : ∀ N : Subgroup G, IsOpen (N : Set G) ∧ (H : Subgroup G) ≤ N → x ∈ N := by
simpa only [Subgroup.mem_sInf, Set.mem_setOf_eq] using hx
exact hxall (K : Subgroup G) ⟨openSubgroup_isOpen (G := G) K, hHK⟩
rcases
(Subgroup.mem_sup_of_normal_right (s := (H : Subgroup G)) (t := (N : Subgroup G))).1
hxK with
⟨h, hhH, n, hnN, hxn⟩
have hnW : n ∈ W := hNW hnN
have : h ∉ (H : Set G) := by
simpa [W, hxn.symm, mul_assoc] using hnW
exact this hhHProof. 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. One inclusion is immediate because every open subgroup in the intersection contains the closed subgroup. For the reverse inclusion, take a point outside the closed subgroup; compact Hausdorff total disconnectedness gives a clopen neighborhood separating that point from the subgroup, and the associated open subgroup contains the closed subgroup but not the point. 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. 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.
□theorem exists_not_mem_of_iInf_eq_bot {ι : Type v} (U : ι → Subgroup G)
(hU : iInf U = (⊥ : Subgroup G)) {x : G} (hx : x ≠ 1) :
∃ i : ι, x ∉ U iIf the intersection of a family of subgroups is trivial, every nonidentity element is omitted by at least one member of the family.
Show proof
by
by_contra h
have hxall : ∀ i : ι, x ∈ U i := by
intro i
by_contra hxi
exact h ⟨i, hxi⟩
have hxinf : x ∈ iInf U := by
simpa [Subgroup.mem_iInf] using hxall
have hxbot : x ∈ (⊥ : Subgroup G) := by
simpa [hU] using hxinf
exact hx (by simpa using hxbot)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. 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. 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 disjoint_leftCoset_of_not_mem (U : Subgroup G) {x y : G} (hxy : x⁻¹ * y ∉ U) :
Disjoint {g : G | x⁻¹ * g ∈ U} {g : G | y⁻¹ * g ∈ U}Distinct left cosets of a subgroup are disjoint.
Show proof
by
refine Set.disjoint_left.2 ?_
intro g hx hg
apply hxy
have hmul : (x⁻¹ * g) * (y⁻¹ * g)⁻¹ ∈ U := U.mul_mem hx (U.inv_mem hg)
simpa [mul_assoc] using hmulProof. 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. 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 isClopen_leftCoset_openSubgroup (U : OpenSubgroup G) (x : G) :
IsClopen {g : G | x⁻¹ * g ∈ (U : Subgroup G)}The left coset of an open subgroup is clopen.
Show proof
by
let f : G → G := fun g => x⁻¹ * g
have hf : Continuous f := continuous_const.mul continuous_id
refine ⟨?_, ?_⟩
· simpa [f] using (openSubgroup_isClosed (G := G) U).preimage hf
· simpa [f] using (openSubgroup_isOpen (G := G) U).preimage hfProof. 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. 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.
□