ProCGroups.Topologies.FullSubgroupTopology.QuotientFormation
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.Group.Basic
structure QuotientFormation where
contains : ∀ {G : Type u} [Group G], Subgroup G → Prop
top_mem : ∀ {G : Type u} [Group G], contains (G := G) (⊤ : Subgroup G)
normal_of_mem : ∀ {G : Type u} [Group G] {N : Subgroup G}, contains (G := G) N → N.Normal
upward_closed :
∀ {G : Type u} [Group G] {N K : Subgroup G},
contains (G := G) N → N ≤ K → K.Normal → contains (G := G) K
inf_closed :
∀ {G : Type u} [Group G] {N K : Subgroup G},
contains (G := G) N → contains (G := G) K → contains (G := G) (N ⊓ K)A quotient formation records which quotient subgroups belong to the chosen class and the closure properties needed for the pro-\(C\) topology.
def IsOpenSubgroup {G : Type u} [Group G] (H : Subgroup G) : Prop :=
∃ N : Subgroup G, C.contains N ∧ N ≤ HA subgroup is open in the pro-\(C\) topology if and only if it contains one of the basic kernels.
def proCClosure {G : Type u} [Group G] (H : Subgroup G) : Subgroup G :=
sInf {K : Subgroup G | C.IsOpenSubgroup K ∧ H ≤ K}Algebraic closure operator attached to the pro-\(C\) topology.
def IsClosedSubgroup {G : Type u} [Group G] (H : Subgroup G) : Prop :=
C.proCClosure H = HA subgroup is closed in the algebraic pro-\(C\) topology exactly when it equals its pro-\(C\) closure.
def IsResiduallyC {G : Type u} [Group G] : Prop :=
C.proCClosure (⊥ : Subgroup G) = ⊥Residuality for the pro-\(C\) topology: the identity is separated by the basic open kernels.
@[simp] theorem isOpenSubgroup_top (C : QuotientFormation) :
C.IsOpenSubgroup (⊤ : Subgroup G)The whole group is open for a quotient formation.
Show proof
by
exact ⟨⊤, C.top_mem, le_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. 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 isOpenSubgroup_sup_left (C : QuotientFormation) {H K : Subgroup G}
(hH : C.IsOpenSubgroup H) :
C.IsOpenSubgroup (H ⊔ K)A subgroup containing an open subgroup for a quotient formation is open in the left-hand quotient-formation topology.
Show proof
by
rcases hH with ⟨N, hN, hNH⟩
exact ⟨N, hN, le_trans hNH le_sup_left⟩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 isOpenSubgroup_sup_right (C : QuotientFormation) {H K : Subgroup G}
(hK : C.IsOpenSubgroup K) :
C.IsOpenSubgroup (H ⊔ K)A subgroup containing an open subgroup for a quotient formation is open in the right-hand quotient-formation topology.
Show proof
by
simpa [sup_comm] using
(C.isOpenSubgroup_sup_left (H := K) (K := H) hK)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 le_proCClosure (C : QuotientFormation) (H : Subgroup G) :
H ≤ C.proCClosure HA subgroup is contained in its pro-\(C\) closure.
Show proof
by
change H ≤ sInf {K : Subgroup G | C.IsOpenSubgroup K ∧ H ≤ K}
exact le_sInf fun K hK => hK.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. 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 proCClosure_mono (C : QuotientFormation) {H K : Subgroup G}
(hHK : H ≤ K) :
C.proCClosure H ≤ C.proCClosure KThe pro-\(C\) closure operation is monotone.
Show proof
by
change
sInf {L : Subgroup G | C.IsOpenSubgroup L ∧ H ≤ L} ≤
sInf {L : Subgroup G | C.IsOpenSubgroup L ∧ K ≤ L}
refine le_sInf ?_
intro L hL
exact sInf_le ⟨hL.1, hHK.trans hL.2⟩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 proCClosure_idem (C : QuotientFormation) (H : Subgroup G) :
C.proCClosure (C.proCClosure H) = C.proCClosure HThe pro-\(C\) closure operation is idempotent.
Show proof
by
refine le_antisymm ?_ (C.proCClosure_mono (C.le_proCClosure H))
change
sInf {L : Subgroup G | C.IsOpenSubgroup L ∧ C.proCClosure H ≤ L} ≤
sInf {L : Subgroup G | C.IsOpenSubgroup L ∧ H ≤ L}
refine le_sInf ?_
intro L hL
exact sInf_le ⟨hL.1, sInf_le hL⟩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 isClosedSubgroup_iff_proCClosure_le {C : QuotientFormation} {H : Subgroup G} :
C.IsClosedSubgroup H ↔ C.proCClosure H ≤ HClosed subgroups for the quotient formation are exactly those containing the pro-\(C\) closure of every smaller subgroup.
Show proof
by
constructor
· intro hH
rw [QuotientFormation.IsClosedSubgroup] at hH
rw [hH]
· intro hH
exact le_antisymm hH (C.le_proCClosure H)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. 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. 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.
□@[simp] theorem isResiduallyC_iff_proCClosure_bot_eq_bot {C : QuotientFormation} :
C.IsResiduallyC (G := G) ↔ C.proCClosure (⊥ : Subgroup G) = ⊥Residual \(C\)-ness is equivalent to the pro-\(C\) closure of the bottom subgroup being bottom.
Show proof
Iff.rflProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem exists_openSubgroup_not_mem_of_not_mem_proCClosure
(C : QuotientFormation) {H : Subgroup G} {x : G}
(hx : x ∉ C.proCClosure H) :
∃ K : Subgroup G, C.IsOpenSubgroup K ∧ H ≤ K ∧ x ∉ KAn element outside the pro-\(C\) closure is separated by an open subgroup in the quotient formation.
Show proof
by
rw [QuotientFormation.proCClosure, Subgroup.mem_sInf] at hx
push_neg at hx
rcases hx with ⟨K, hK, hxK⟩
exact ⟨K, hK.1, hK.2, hxK⟩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. 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. 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_openSubgroup_not_mem_of_isResiduallyC
(C : QuotientFormation) (hC : C.IsResiduallyC (G := G))
{x : G} (hx : x ≠ 1) :
∃ K : Subgroup G, C.IsOpenSubgroup K ∧ x ∉ KIn a residually \(C\) group, a nontrivial element is excluded by some open subgroup in the quotient formation.
Show proof
by
have hxbot : x ∉ C.proCClosure (⊥ : Subgroup G) := by
rw [hC]
simpa using hx
rcases C.exists_openSubgroup_not_mem_of_not_mem_proCClosure
(H := (⊥ : Subgroup G)) hxbot with ⟨K, hKopen, _hbotK, hxK⟩
exact ⟨K, hKopen, hxK⟩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. 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. 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 normalCore_mem_of_open (C : QuotientFormation) {H : Subgroup G}
(hH : C.IsOpenSubgroup H) :
C.contains H.normalCoreThe normal core of an open subgroup again defines a quotient in the formation.
Show proof
by
rcases hH with ⟨N, hN, hNH⟩
let _ : N.Normal := C.normal_of_mem hN
have hNcore : N ≤ H.normalCore := (Subgroup.normal_le_normalCore).2 hNH
exact C.upward_closed hN hNcore inferInstanceProof. 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 exists_openKernel_not_mem_of_isResiduallyC
(C : QuotientFormation) (hC : C.IsResiduallyC (G := G))
{x : G} (hx : x ≠ 1) :
∃ N : Subgroup G, C.contains N ∧ N.Normal ∧ x ∉ NIn a residually \(C\) group, a nontrivial element is excluded by an open normal kernel in the quotient formation.
Show proof
by
rcases C.exists_openSubgroup_not_mem_of_isResiduallyC (G := G) hC hx with
⟨K, hKopen, hxK⟩
refine ⟨K.normalCore, C.normalCore_mem_of_open hKopen, ?_, ?_⟩
· exact C.normal_of_mem (C.normalCore_mem_of_open hKopen)
· intro hxcore
exact hxK (Subgroup.normalCore_le K hxcore)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 isClosedSubgroup_iff_exists_sInf_openSubgroups
{C : QuotientFormation} {H : Subgroup G} :
C.IsClosedSubgroup H ↔
∃ S : Set (Subgroup G), (∀ K ∈ S, C.IsOpenSubgroup K) ∧ H = sInf SClosed subgroups are exactly intersections of open subgroups.
Show proof
by
constructor
· intro hH
refine ⟨{K : Subgroup G | C.IsOpenSubgroup K ∧ H ≤ K}, ?_, ?_⟩
· intro K hK
exact hK.1
· simpa [QuotientFormation.IsClosedSubgroup, QuotientFormation.proCClosure] using hH.symm
· rintro ⟨S, hSopen, hEq⟩
rw [QuotientFormation.IsClosedSubgroup]
refine le_antisymm ?_ (C.le_proCClosure H)
calc
C.proCClosure H ≤ sInf S := by
refine le_sInf ?_
intro K hK
have hHK : H ≤ K := by
rw [hEq]
exact sInf_le hK
exact sInf_le ⟨hSopen K hK, hHK⟩
_ = H := hEq.symmProof. 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. 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. 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.
□