NYLL
Module

CountableChains.lean

Nyll.ProCGroups.ProC.OpenNormalSubgroups.CountableChains
3 declarations indexed from sourceView source ↗

Module documentation

Countable descending open-normal chains

This file defines countable open-normal bases at the identity and characterizes them by descending chains with trivial intersection. It also supplies the refinement property needed to use such chains as neighborhood bases.

Imports1
Imported by2

Declarations

def

HasCountableOpenNormalBasisAtOne

L31 ↗
ProCGroups.ProC.HasCountableOpenNormalBasisAtOne
Documentation

Preparatory 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.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.ProC
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
def HasCountableOpenNormalBasisAtOne
    (G : Type u) [Group G] [TopologicalSpace G] : Prop
theorem

exists_term_le_openSubgroup_of_iInf_le

L42 ↗
ProCGroups.ProC.exists_term_le_openSubgroup_of_iInf_le
Documentation

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.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.ProC
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · statement
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)
theorem

hasCountableOpenNormalBasisAtOne_iff_exists_descending_openNormalChain

L89 ↗
ProCGroups.ProC.hasCountableOpenNormalBasisAtOne_iff_exists_descending_openNormalChain
Documentation

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.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ProCGroups.ProC
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G]
Lean source · full declaration
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) := 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)⟩

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.