NYLL
Module

Basic.lean

Nyll.ProCGroups.Order.Basic
37 declarations indexed from sourceView source ↗

Module documentation

The order structure on closed subgroups

This module equips closed subgroups with basic lattice operations, develops continuous images and preimages, and relates order-theoretic constructions to finite quotients of profinite groups.

Imports4
Imported by2

Declarations

instance

instTopClosedSubgroup

L35 ↗
ProCGroups.Order.ClosedSubgroup.instTopClosedSubgroup
Documentation

Closed subgroups have a top element: the whole group.

Source context 9 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
namespace ClosedSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
Lean source · statement
instance instTopClosedSubgroup : Top (ClosedSubgroup G)
instance

instBotClosedSubgroup

L42 ↗
ProCGroups.Order.ClosedSubgroup.instBotClosedSubgroup
Documentation

Closed subgroups have a bottom element: the trivial subgroup, closed in a \(T_1\) topological group.

Source context 9 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
namespace ClosedSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
Lean source · statement
instance instBotClosedSubgroup [T1Space G] : Bot (ClosedSubgroup G)
def

map

L52 ↗
ProCGroups.Order.ClosedSubgroup.map
Documentation

The image of a closed subgroup under a continuous homomorphism from a compact domain into a Hausdorff codomain.

Source context 9 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
namespace ClosedSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
Lean source · full declaration
def map [CompactSpace G] [T2Space K] (H : ClosedSubgroup G)
    (φ : G →* K) (hφ : Continuous φ) : ClosedSubgroup K where
  toSubgroup := (H : Subgroup G).map φ
  isClosed' := by
    let f : H → K := fun x => φ x
    have hcont : Continuous f := hφ.comp continuous_subtype_val
    have hcompact : IsCompact (Set.range f) := isCompact_range hcont
    have hEq : Set.range f = ((H : Subgroup G).map φ : Set K) := by
      ext y
      constructor
      · rintro ⟨x, rfl⟩
        exact (Subgroup.mem_map).2 ⟨x.1, x.2, rfl⟩
      · intro hy
        rcases (Subgroup.mem_map).1 hy with ⟨x, hx, rfl⟩
        exact ⟨⟨x, hx⟩, rfl⟩
    change IsClosed (((H : Subgroup G).map φ : Subgroup K) : Set K)
    rw [← hEq]
    exact hcompact.isClosed
theorem

toSubgroup_map

L74 ↗
ProCGroups.Order.ClosedSubgroup.toSubgroup_map
Documentation

The underlying subgroup of the image closed subgroup is the image of the underlying subgroup.

Source context 10 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
namespace ClosedSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
omit [IsTopologicalGroup K] in
Lean source · statement
theorem toSubgroup_map [CompactSpace G] [T2Space K] (H : ClosedSubgroup G)
    (φ : G →* K) (hφ : Continuous φ) :
    ((map H φ hφ : ClosedSubgroup K) : Subgroup K) = (H : Subgroup G).map φ
theorem

mem_map

L81 ↗
ProCGroups.Order.ClosedSubgroup.mem_map
Documentation

Membership in the image closed subgroup is membership in the subgroup map.

Source context 10 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
namespace ClosedSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
omit [IsTopologicalGroup K] in
Lean source · statement
theorem mem_map [CompactSpace G] [T2Space K] {H : ClosedSubgroup G}
    {φ : G →* K} (hφ : Continuous φ) {y : K} :
    y ∈ map H φ hφ ↔ ∃ x ∈ (H : Subgroup G), φ x = y
theorem

map_id

L88 ↗
ProCGroups.Order.ClosedSubgroup.map_id
Documentation

Mapping a closed subgroup along the identity homomorphism gives the same closed subgroup.

Source context 9 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
namespace ClosedSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
Lean source · statement
theorem map_id [CompactSpace G] [T2Space G] (H : ClosedSubgroup G) :
    map H (MonoidHom.id G) continuous_id = H
theorem

map_comp

L100 ↗
ProCGroups.Order.ClosedSubgroup.map_comp
Documentation

Images of closed subgroups compose under composition of continuous homomorphisms.

Source context 10 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
namespace ClosedSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
omit [IsTopologicalGroup K] in
Lean source · statement
theorem map_comp
    {L : Type w} [Group L] [TopologicalSpace L]
    [CompactSpace G] [T2Space K] [CompactSpace K] [T2Space L]
    (H : ClosedSubgroup G) (φ : G →* K) (hφ : Continuous φ)
    (ψ : K →* L) (hψ : Continuous ψ) :
    map (map H φ hφ) ψ hψ = map H (ψ.comp φ) (hψ.comp hφ)
theorem

map_mono

L117 ↗
ProCGroups.Order.ClosedSubgroup.map_mono
Documentation

The image construction on closed subgroups is monotone.

Source context 10 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
namespace ClosedSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
omit [IsTopologicalGroup K] in
Lean source · statement
theorem map_mono [CompactSpace G] [T2Space K] {H H' : ClosedSubgroup G}
    (hHH' : (H : Subgroup G) ≤ (H' : Subgroup G))
    (φ : G →* K) (hφ : Continuous φ) :
    ((map H φ hφ : ClosedSubgroup K) : Subgroup K) ≤
      ((map H' φ hφ : ClosedSubgroup K) : Subgroup K)
theorem

map_bot

L127 ↗
ProCGroups.Order.ClosedSubgroup.map_bot
Documentation

The image of the bottom closed subgroup is the bottom closed subgroup.

Source context 10 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
namespace ClosedSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
omit [IsTopologicalGroup K] in
Lean source · statement
theorem map_bot [CompactSpace G] [T1Space G] [T2Space K]
    (φ : G →* K) (hφ : Continuous φ) :
    map (⊥ : ClosedSubgroup G) φ hφ = (⊥ : ClosedSubgroup K)
theorem

map_eq_top_of_surjective

L146 ↗
ProCGroups.Order.ClosedSubgroup.map_eq_top_of_surjective
Documentation

The image of the top closed subgroup under a surjective homomorphism is top.

Source context 10 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
namespace ClosedSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
omit [IsTopologicalGroup K] in
Lean source · statement
theorem map_eq_top_of_surjective [CompactSpace G] [T2Space K] (H : ClosedSubgroup G)
    (φ : G →* K) (hφ : Continuous φ)
    (hφH : ∀ y : K, ∃ x ∈ (H : Subgroup G), φ x = y) :
    map H φ hφ = (⊤ : ClosedSubgroup K)
theorem

map_le_iff_le_comap

L160 ↗
ProCGroups.Order.ClosedSubgroup.map_le_iff_le_comap
Documentation

Image containment for closed subgroups is equivalent to containment in the comap.

Source context 10 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
namespace ClosedSubgroup
variable {G : Type u} [Group G] [TopologicalSpace G]
variable {K : Type v} [Group K] [TopologicalSpace K] [IsTopologicalGroup K]
omit [IsTopologicalGroup K] in
Lean source · statement
theorem map_le_iff_le_comap [CompactSpace G] [T2Space K]
    {H : ClosedSubgroup G} {L : ClosedSubgroup K}
    {φ : G →* K} (hφ : Continuous φ) :
    ((map H φ hφ : ClosedSubgroup K) : Subgroup K) ≤ (L : Subgroup K) ↔
      (H : Subgroup G) ≤ Subgroup.comap φ (L : Subgroup K)
def

IsSurjectiveInverseSystem

L175 ↗
ProCGroups.Order.IsSurjectiveInverseSystem
Documentation

The surjectivity hypothesis for transition maps in a group-valued inverse system.

Source context 6 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
Lean source · statement
def IsSurjectiveInverseSystem {I : Type v} [Preorder I]
    (S : ProCGroups.InverseSystems.InverseSystem (I := I)) : Prop
def

inverseLimitProjectionImage

L180 ↗
ProCGroups.Order.inverseLimitProjectionImage
Documentation

The image of a closed subgroup under a projection from a group-valued inverse limit.

Source context 6 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
Lean source · statement
def inverseLimitProjectionImage
    {I : Type v} [Preorder I]
    (S : ProCGroups.InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
    [∀ i, TopologicalSpace (S.X i)] [∀ i, T2Space (S.X i)]
    [CompactSpace S.inverseLimit]
    (H : ClosedSubgroup S.inverseLimit) (i : I) : ClosedSubgroup (S.X i)
def

quotientImage

L203 ↗
ProCGroups.Order.quotientImage
Documentation

The image of a closed subgroup in an open-normal finite quotient.

Source context 8 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
section FiniteQuotientImages
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def quotientImage [CompactSpace G] (H : ClosedSubgroup G)
    (U : OpenNormalSubgroup G) : ClosedSubgroup (G ⧸ (U : Subgroup G))
theorem

toSubgroup_quotientImage

L209 ↗
ProCGroups.Order.toSubgroup_quotientImage
Documentation

The subgroup underlying a quotient image is the image of the closed subgroup in the quotient.

Source context 8 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
section FiniteQuotientImages
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem toSubgroup_quotientImage [CompactSpace G] (H : ClosedSubgroup G)
    (U : OpenNormalSubgroup G) :
    ((quotientImage (G := G) H U : ClosedSubgroup (G ⧸ (U : Subgroup G))) :
      Subgroup (G ⧸ (U : Subgroup G))) =
        (H : Subgroup G).map (QuotientGroup.mk' (U : Subgroup G))
theorem

mem_quotientImage

L218 ↗
ProCGroups.Order.mem_quotientImage
Documentation

Membership in a quotient image is membership in the image of the underlying closed subgroup.

Source context 8 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
section FiniteQuotientImages
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem mem_quotientImage [CompactSpace G] {H : ClosedSubgroup G}
    {U : OpenNormalSubgroup G} {y : G ⧸ (U : Subgroup G)} :
    y ∈ quotientImage (G := G) H U ↔
      ∃ x ∈ (H : Subgroup G), QuotientGroup.mk' (U : Subgroup G) x = y
theorem

mem_closedSubgroup_iff_forall_quotientImage_mem

L228 ↗
ProCGroups.Order.mem_closedSubgroup_iff_forall_quotientImage_mem
Documentation

Membership in a closed subgroup of a profinite group can be checked after all open-normal finite quotients.

Source context 8 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
section FiniteQuotientImages
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem mem_closedSubgroup_iff_forall_quotientImage_mem
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {H : ClosedSubgroup G} {x : G} :
    x ∈ H ↔
      ∀ U : OpenNormalSubgroup G,
        OpenNormalSubgroup.quotientProj U x ∈
          (quotientImage (G := G) H U : Subgroup (G ⧸ (U : Subgroup G)))
theorem

closedSubgroup_le_iff_forall_quotientImages_le

L293 ↗
ProCGroups.Order.closedSubgroup_le_iff_forall_quotientImages_le
Documentation

Inclusion of closed subgroups of a profinite group can be checked on all open-normal finite quotients.

Source context 8 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
section FiniteQuotientImages
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem closedSubgroup_le_iff_forall_quotientImages_le
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {H K : ClosedSubgroup G} :
    (H : Subgroup G) ≤ (K : Subgroup G) ↔
      ∀ U : OpenNormalSubgroup G,
        (quotientImage (G := G) H U : Subgroup (G ⧸ (U : Subgroup G))) ≤
          (quotientImage (G := G) K U : Subgroup (G ⧸ (U : Subgroup G)))
theorem

closedSubgroup_eq_of_quotientImages_eq

L310 ↗
ProCGroups.Order.closedSubgroup_eq_of_quotientImages_eq
Documentation

Two closed subgroups are equal if their images agree in every finite quotient.

Source context 8 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
section FiniteQuotientImages
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem closedSubgroup_eq_of_quotientImages_eq
    [CompactSpace G] [TotallyDisconnectedSpace G]
    {H K : ClosedSubgroup G}
    (hHK : ∀ U : OpenNormalSubgroup G,
      quotientImage (G := G) H U = quotientImage (G := G) K U) :
    H = K
def

inverseSystemStageHom

L386 ↗
ProCGroups.Order.inverseSystemStageHom
Documentation

The transition map of a group-valued inverse system, viewed as a homomorphism.

Source context 13 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
Lean source · full declaration
def inverseSystemStageHom {i j : I} (hij : i ≤ j) : S.X j →* S.X i where
  toFun := S.map hij
  map_one' := ProCGroups.InverseSystems.IsGroupSystem.map_one (S := S) hij
  map_mul' := ProCGroups.InverseSystems.IsGroupSystem.map_mul (S := S) hij
theorem

inverseSystemStageHom_continuous

L394 ↗
ProCGroups.Order.inverseSystemStageHom_continuous
Documentation

The stage homomorphism associated to a group-valued inverse system is continuous.

Source context 14 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, CompactSpace (S.X i)]
  [∀ i, T2Space (S.X i)] in
Lean source · statement
theorem inverseSystemStageHom_continuous {i j : I} (hij : i ≤ j) :
    Continuous (inverseSystemStageHom (S := S) hij)
def

compatibleClosedSubgroupSystem

L403 ↗
ProCGroups.Order.compatibleClosedSubgroupSystem
Documentation

The inverse system obtained by restricting an ambient inverse system to a compatible family of closed subgroups.

Source context 13 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
Lean source · full declaration
def compatibleClosedSubgroupSystem
    (L : ∀ i, ClosedSubgroup (S.X i))
    (hcompat : ∀ {i j : I} (hij : i ≤ j),
      ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
          (inverseSystemStageHom_continuous (S := S) hij) :
          ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
        (L i : Subgroup (S.X i))) :
    ProCGroups.InverseSystems.InverseSystem (I := I) where
  X := fun i => L i
  topologicalSpace := fun i => inferInstance
  map := fun {i j} hij x =>
    ⟨S.map hij x.1, by
      have hx :
          S.map hij x.1 ∈
            ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
                (inverseSystemStageHom_continuous (S := S) hij) :
                  ClosedSubgroup (S.X i)) : Subgroup (S.X i)) := by
        exact (Subgroup.mem_map).2 ⟨x.1, x.2, rfl⟩
      rw [hcompat hij] at hx
      exact hx⟩
  continuous_map := fun {i j} hij =>
    Continuous.subtype_mk
      ((inverseSystemStageHom_continuous (S := S) hij).comp continuous_subtype_val) (fun x => by
      have hx :
          S.map hij x.1 ∈
            ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
                (inverseSystemStageHom_continuous (S := S) hij) :
                  ClosedSubgroup (S.X i)) : Subgroup (S.X i)) := by
        exact (Subgroup.mem_map).2 ⟨x.1, x.2, rfl⟩
      rw [hcompat hij] at hx
      exact hx)
  map_id := fun i => by
    funext x
    apply Subtype.ext
    simp only [InverseSystem.map_id_apply, id_eq]
  map_comp := fun {i j k} hij hjk => by
    funext x
    apply Subtype.ext
    simp only [Function.comp_apply, InverseSystem.map_comp_apply]
instance

compatibleClosedSubgroupSystem_group

L444 ↗
ProCGroups.Order.compatibleClosedSubgroupSystem_group
Documentation

Each stage of a compatible closed-subgroup system is a group.

Source context 13 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
Lean source · statement
instance compatibleClosedSubgroupSystem_group
    (L : ∀ i, ClosedSubgroup (S.X i))
    (hcompat : ∀ {i j : I} (hij : i ≤ j),
      ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
          (inverseSystemStageHom_continuous (S := S) hij) :
          ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
        (L i : Subgroup (S.X i)))
    (i : I) :
    Group ((compatibleClosedSubgroupSystem (S := S) L hcompat).X i)
instance

compatibleClosedSubgroupSystem_isGroupSystem

L457 ↗
ProCGroups.Order.compatibleClosedSubgroupSystem_isGroupSystem
Documentation

A compatible closed-subgroup system is a group-valued inverse system.

Source context 13 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
Lean source · full declaration
instance compatibleClosedSubgroupSystem_isGroupSystem
    (L : ∀ i, ClosedSubgroup (S.X i))
    (hcompat : ∀ {i j : I} (hij : i ≤ j),
      ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
          (inverseSystemStageHom_continuous (S := S) hij) :
          ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
        (L i : Subgroup (S.X i))) :
    ProCGroups.InverseSystems.IsGroupSystem (compatibleClosedSubgroupSystem (S := S) L hcompat)
        where
  map_one := by
    intro i j hij
    apply Subtype.ext
    change S.map hij (1 : S.X j) = 1
    exact ProCGroups.InverseSystems.IsGroupSystem.map_one (S := S) hij
  map_mul := by
    intro i j hij x y
    apply Subtype.ext
    change S.map hij (x.1 * y.1) = S.map hij x.1 * S.map hij y.1
    exact ProCGroups.InverseSystems.IsGroupSystem.map_mul (S := S) hij x.1 y.1
  map_inv := by
    intro i j hij x
    apply Subtype.ext
    change S.map hij x.1⁻¹ = (S.map hij x.1)⁻¹
    exact ProCGroups.InverseSystems.IsGroupSystem.map_inv (S := S) hij x.1
def

compatibleClosedSubgroupInclusion

L485 ↗
ProCGroups.Order.compatibleClosedSubgroupInclusion
Documentation

The canonical coordinatewise inclusion of a compatible subgroup system into the ambient system.

Source context 13 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
Lean source · full declaration
def compatibleClosedSubgroupInclusion
    (L : ∀ i, ClosedSubgroup (S.X i))
    (hcompat : ∀ {i j : I} (hij : i ≤ j),
      ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
          (inverseSystemStageHom_continuous (S := S) hij) :
          ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
        (L i : Subgroup (S.X i))) :
    (compatibleClosedSubgroupSystem (S := S) L hcompat).Morphism S where
  map := fun i => Subtype.val
  continuous_map := fun i => by
    dsimp [compatibleClosedSubgroupSystem]
    exact continuous_subtype_val
  comm := fun {i j} hij => by
    funext x
    rfl
def

compatibleClosedSubgroupLimHom

L505 ↗
ProCGroups.Order.compatibleClosedSubgroupLimHom
Documentation

The induced homomorphism from the inverse limit of a compatible subgroup family into the ambient inverse limit.

Source context 13 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
Lean source · full declaration
def compatibleClosedSubgroupLimHom
    (L : ∀ i, ClosedSubgroup (S.X i))
    (hcompat : ∀ {i j : I} (hij : i ≤ j),
      ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
          (inverseSystemStageHom_continuous (S := S) hij) :
          ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
        (L i : Subgroup (S.X i))) :
    (compatibleClosedSubgroupSystem (S := S) L hcompat).inverseLimit →* S.inverseLimit where
  toFun :=
    (compatibleClosedSubgroupSystem (S := S) L hcompat).limMap
      (compatibleClosedSubgroupInclusion (S := S) L hcompat)
  map_one' := by
    apply S.ext
    intro i
    rfl
  map_mul' := by
    intro x y
    apply S.ext
    intro i
    rfl
def

closedSubgroupFromCompatibleFamily

L530 ↗
ProCGroups.Order.closedSubgroupFromCompatibleFamily
Documentation

Closed subgroup of the ambient inverse limit obtained from a compatible family of closed subgroups with surjective transition maps.

Source context 13 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
Lean source · full declaration
def closedSubgroupFromCompatibleFamily
    (L : ∀ i, ClosedSubgroup (S.X i))
    (hcompat : ∀ {i j : I} (hij : i ≤ j),
      ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
          (inverseSystemStageHom_continuous (S := S) hij) :
          ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
        (L i : Subgroup (S.X i))) :
    ClosedSubgroup S.inverseLimit where
  toSubgroup := (compatibleClosedSubgroupLimHom (S := S) L hcompat).range
  isClosed' := by
    let T : InverseSystem (I := I) := compatibleClosedSubgroupSystem (S := S) L hcompat
    let : ∀ i, CompactSpace (T.X i) := fun i =>
      (inferInstance : CompactSpace (L i))
    let : ∀ i, T2Space (T.X i) := fun i =>
      (inferInstance : T2Space (L i))
    let φ : T.inverseLimit →* S.inverseLimit :=
      compatibleClosedSubgroupLimHom (S := S) L hcompat
    have hφcont :
        Continuous (φ : T.inverseLimit → S.inverseLimit) := by
      change Continuous (T.limMap (compatibleClosedSubgroupInclusion (S := S) L hcompat))
      exact T.continuous_limMap (compatibleClosedSubgroupInclusion (S := S) L hcompat)
    change IsClosed (Set.range (φ : T.inverseLimit → S.inverseLimit))
    exact (isCompact_range hφcont).isClosed
theorem

inverseLimitProjectionImage_closedSubgroupFromCompatibleFamily

L559 ↗
ProCGroups.Order.inverseLimitProjectionImage_closedSubgroupFromCompatibleFamily
Documentation

Projection images of a closed subgroup recovered from a compatible family match the given family.

Source context 14 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem inverseLimitProjectionImage_closedSubgroupFromCompatibleFamily
    [CompactSpace S.inverseLimit]
    (hdir : Directed (· ≤ ·) (id : I → I))
    (L : ∀ i, ClosedSubgroup (S.X i))
    (hcompat : ∀ {i j : I} (hij : i ≤ j),
      ((ClosedSubgroup.map (L j) (inverseSystemStageHom (S := S) hij)
          (inverseSystemStageHom_continuous (S := S) hij) :
          ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
        (L i : Subgroup (S.X i))) (i : I) :
    inverseLimitProjectionImage S (closedSubgroupFromCompatibleFamily (S := S) L hcompat) i =
      L i
theorem

map_inverseLimitProjectionImage

L624 ↗
ProCGroups.Order.map_inverseLimitProjectionImage
Documentation

Projection images commute with mapping a closed subgroup along a compatible inverse-limit morphism.

Source context 14 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem map_inverseLimitProjectionImage
    [CompactSpace S.inverseLimit]
    (H : ClosedSubgroup S.inverseLimit) {i j : I} (hij : i ≤ j) :
    ((ClosedSubgroup.map (inverseLimitProjectionImage S H j) (inverseSystemStageHom (S := S) hij)
        (inverseSystemStageHom_continuous (S := S) hij) :
        ClosedSubgroup (S.X i)) : Subgroup (S.X i)) =
      (inverseLimitProjectionImage S H i : Subgroup (S.X i))
theorem

map_inverseLimitProjectionImage_closed

L657 ↗
ProCGroups.Order.map_inverseLimitProjectionImage_closed
Documentation

The stage-transition compatibility of projection images, repackaged as an equality of closed subgroups.

Source context 14 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem map_inverseLimitProjectionImage_closed
    [CompactSpace S.inverseLimit]
    (H : ClosedSubgroup S.inverseLimit) {i j : I} (hij : i ≤ j) :
    ClosedSubgroup.map (inverseLimitProjectionImage S H j)
        (inverseSystemStageHom (S := S) hij)
        (inverseSystemStageHom_continuous (S := S) hij) =
      inverseLimitProjectionImage S H i
theorem

inverseLimitProjectionImage_bot

L670 ↗
ProCGroups.Order.inverseLimitProjectionImage_bot
Documentation

The projection image of the trivial closed subgroup is trivial.

Source context 14 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, CompactSpace (S.X i)] in
Lean source · statement
theorem inverseLimitProjectionImage_bot
    [CompactSpace S.inverseLimit] (i : I) :
    inverseLimitProjectionImage S (⊥ : ClosedSubgroup S.inverseLimit) i = ⊥
theorem

inverseLimitProjectionImage_top

L697 ↗
ProCGroups.Order.inverseLimitProjectionImage_top
Documentation

Under surjective transition maps, the projection image of the whole inverse limit is the whole stage group.

Source context 14 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem inverseLimitProjectionImage_top
    [CompactSpace S.inverseLimit]
    (hdir : Directed (· ≤ ·) (id : I → I))
    (hsurj : IsSurjectiveInverseSystem S) (i : I) :
    inverseLimitProjectionImage S (⊤ : ClosedSubgroup S.inverseLimit) i = ⊤
theorem

inverseLimitProjectionImage_mono

L717 ↗
ProCGroups.Order.inverseLimitProjectionImage_mono
Documentation

Projection images are monotone in the closed subgroup argument.

Source context 14 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, CompactSpace (S.X i)] in
Lean source · statement
theorem inverseLimitProjectionImage_mono
    [CompactSpace S.inverseLimit]
    {H K : ClosedSubgroup S.inverseLimit}
    (hHK : (H : Subgroup S.inverseLimit) ≤ K) (i : I) :
    (inverseLimitProjectionImage S H i : Subgroup (S.X i)) ≤
      (inverseLimitProjectionImage S K i : Subgroup (S.X i))
theorem

closedSubgroup_le_of_projectionImages_le

L728 ↗
ProCGroups.Order.closedSubgroup_le_of_projectionImages_le
Documentation

Closed subgroups of an inverse limit are determined by their stagewise projection images.

Source context 13 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
Lean source · statement
theorem closedSubgroup_le_of_projectionImages_le
    [Nonempty I] [CompactSpace S.inverseLimit]
    [TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I))
    (H K : ClosedSubgroup S.inverseLimit)
    (hproj : ∀ i,
      (inverseLimitProjectionImage S H i : Subgroup (S.X i)) ≤
        (inverseLimitProjectionImage S K i : Subgroup (S.X i))) :
    (H : Subgroup S.inverseLimit) ≤ (K : Subgroup S.inverseLimit)
theorem

closedSubgroup_eq_of_projectionImages_eq

L783 ↗
ProCGroups.Order.closedSubgroup_eq_of_projectionImages_eq
Documentation

Stagewise equality of projection images determines a closed subgroup of an inverse limit.

Source context 13 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
Lean source · statement
theorem closedSubgroup_eq_of_projectionImages_eq
    [Nonempty I] [CompactSpace S.inverseLimit]
    [TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I))
    (H K : ClosedSubgroup S.inverseLimit)
    (hproj : ∀ i, inverseLimitProjectionImage S H i = inverseLimitProjectionImage S K i) :
    H = K
theorem

closedSubgroup_eq_bot_of_projectionImages_eq_bot

L805 ↗
ProCGroups.Order.closedSubgroup_eq_bot_of_projectionImages_eq_bot
Documentation

If every stagewise projection image is trivial, then the closed subgroup itself is trivial.

Source context 13 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
Lean source · statement
theorem closedSubgroup_eq_bot_of_projectionImages_eq_bot
    [Nonempty I] [CompactSpace S.inverseLimit]
    [TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I))
    (H : ClosedSubgroup S.inverseLimit)
    (hproj : ∀ i, inverseLimitProjectionImage S H i = ⊥) :
    H = ⊥
theorem

closedSubgroup_eq_top_of_projectionImages_eq_top

L821 ↗
ProCGroups.Order.closedSubgroup_eq_top_of_projectionImages_eq_top
Documentation

If every stagewise projection image is the whole stage group, then the closed subgroup itself is the whole inverse limit.

Source context 13 commands

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

open Set
open scoped Topology Pointwise BigOperators
namespace ProCGroups.Order
universe u v w
open ProCGroups.InverseSystems
open ProCGroups.ProC
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
section CompatibleClosedSubgroupFamilies
variable {I : Type v} [Preorder I]
variable (S : ProCGroups.InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)] [ProCGroups.InverseSystems.IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
Lean source · statement
theorem closedSubgroup_eq_top_of_projectionImages_eq_top
    [Nonempty I] [CompactSpace S.inverseLimit]
    [TotallyDisconnectedSpace S.inverseLimit] [IsTopologicalGroup S.inverseLimit]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I))
    (hsurj : IsSurjectiveInverseSystem S)
    (H : ClosedSubgroup S.inverseLimit)
    (hproj : ∀ i, inverseLimitProjectionImage S H i = ⊤) :
    H = ⊤

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