ProCGroups.ProC.OpenNormalSubgroups.CountableChains
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.
def HasCountableOpenNormalBasisAtOne
(G : Type u) [Group G] [TopologicalSpace G] : Prop :=
∃ U : ℕ → OpenNormalSubgroup G,
Antitone (fun n => (U n : Subgroup G)) ∧
∀ W : Set G, IsOpen W → (1 : G) ∈ W →
∃ n : ℕ, (((U n : Subgroup G) : Set G)) ⊆ WPreparatory countable-chain layer for later use: \(1\) has a countable fundamental system of open normal subgroups. This isolates the part of the corollary that does not yet depend on the not-yet-formalized cardinal invariant \(w_0(G)\) or on the generator-counting statements from the later section on generators.
theorem exists_term_le_openSubgroup_of_iInf_le [CompactSpace G]
(H : ℕ → Subgroup G) (hmono : Antitone H)
(hclosed : ∀ n, IsClosed (((H n : Subgroup G) : Set G)))
(U : OpenSubgroup G) (hInf : iInf H ≤ (U : Subgroup G)) :
∃ n : ℕ, H n ≤ (U : Subgroup G)Compactness lemma for descending families of closed subgroups: if the total intersection lies inside an open subgroup, then one term already lies inside that open subgroup.
Show proof
by
let K : Set G := (((U : Subgroup G) : Set G))ᶜ
have hKclosed : IsClosed K := by
simpa [K] using (openSubgroup_isOpen (G := G) U).isClosed_compl
have hKcompact : IsCompact K := hKclosed.isCompact
have havoid : K ∩ ⋂ n, (((H n : Subgroup G) : Set G)) = ∅ := by
ext x
constructor
· intro hx
have hxInf : x ∈ iInf H := by
simpa using hx.2
exact False.elim (hx.1 (hInf hxInf))
· intro hx
simp only [Set.mem_empty_iff_false] at hx
have hdir : Directed (fun s t : Set G => s ⊇ t) (fun n => (((H n : Subgroup G) : Set G))) := by
intro i j
refine ⟨max i j, ?_, ?_⟩
· exact hmono (Nat.le_max_left i j)
· exact hmono (Nat.le_max_right i j)
rcases hKcompact.elim_directed_family_closed
(fun n => (((H n : Subgroup G) : Set G))) hclosed havoid hdir with ⟨n, hn⟩
refine ⟨n, ?_⟩
intro x hx
by_contra hxU
have hxK : x ∈ K := by
simpa [K] using hxU
have hmem : x ∈ K ∩ (((H n : Subgroup G) : Set G)) := by
exact ⟨hxK, hx⟩
have : x ∈ (∅ : Set G) := by
simp only [hn, Set.mem_empty_iff_false] at hmem
simp only [Set.mem_empty_iff_false] at thisProof. 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\). 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 hasCountableOpenNormalBasisAtOne_iff_exists_descending_openNormalChain
[IsTopologicalGroup G] [CompactSpace G] [T1Space G] [TotallyDisconnectedSpace G] :
HasCountableOpenNormalBasisAtOne G ↔
∃ U : ℕ → OpenNormalSubgroup G,
Antitone (fun n => (U n : Subgroup G)) ∧
iInf (fun n => (U n : Subgroup G)) = (⊥ : Subgroup G)Preparatory countable-chain / neighborhood-basis equivalence for profinite groups: for a profinite group, giving a countable descending chain of open normal subgroups with trivial intersection is equivalent to giving a countable neighborhood basis at \(1\) formed by a descending chain of open normal subgroups. This is exactly the chain-theoretic content of the corollary; the generator-cardinality half will be added later once the \(w_0(G)\) / convergent-generator formulation is in place.
Show proof
by
constructor
· rintro ⟨U, hmono, hbasis⟩
refine ⟨U, hmono, ?_⟩
apply le_antisymm
· intro x hx
change x = 1
by_contra hxne
let W : Set G := ({x} : Set G)ᶜ
have hW : IsOpen W := by
simp only [isOpen_compl_iff, Set.finite_singleton, Set.Finite.isClosed, W]
have h1W : (1 : G) ∈ W := by
have hx1 : (1 : G) ≠ x := by
intro h1x
exact hxne h1x.symm
simpa [W] using hx1
rcases hbasis W hW h1W with ⟨n, hnW⟩
have hxall : ∀ n : ℕ, x ∈ (((U n : Subgroup G) : Set G)) := by
simpa using hx
have hxW : x ∈ W := hnW (hxall n)
have : x ∉ ({x} : Set G) := by
simp only [Set.mem_compl_iff, Set.mem_singleton_iff, not_true_eq_false, W] at hxW
exact this (by simp only [Set.mem_singleton_iff])
· exact bot_le
· rintro ⟨U, hmono, hinf⟩
refine ⟨U, hmono, ?_⟩
intro W hW h1W
rcases ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
(G := G) hW h1W with ⟨N, hNW⟩
have hInfLe : iInf (fun n => (U n : Subgroup G)) ≤ (N : Subgroup G) := by
simp only [hinf, bot_le]
rcases exists_term_le_openSubgroup_of_iInf_le (G := G)
(fun n => (U n : Subgroup G)) hmono
(fun n => openNormalSubgroup_isClosed (G := G) (U n))
N.toOpenSubgroup hInfLe with ⟨n, hnN⟩
exact ⟨n, fun x hx => hNW (hnN 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. 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.
□theorem hasCountableOpenNormalBasisAtOne_iff_exists_descending_openNormalChain_of_isProfinite
[IsTopologicalGroup G]
(hprof : IsProfiniteGroup G) :
HasCountableOpenNormalBasisAtOne G ↔
∃ U : ℕ → OpenNormalSubgroup G,
Antitone (fun n => (U n : Subgroup G)) ∧
iInf (fun n => (U n : Subgroup G)) = (⊥ : Subgroup G)The same preparatory countable-chain equivalence, packaged with the working IsProfiniteGroup predicate used throughout this file.
Show proof
by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hprof
letI : T2Space G := IsProfiniteGroup.t2Space hprof
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hprof
simpa using
(hasCountableOpenNormalBasisAtOne_iff_exists_descending_openNormalChain (G := 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. 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.
□