Module

Limits.lean

Nyll.ProCGroups.ProC.InverseLimits.Limits

3 declarations indexed from sourceView source ↗

Module documentation

Inverse limits and closed-normal quotients

This file equips inverse limits of finite topological group systems with their canonical topology and proves the pro-\(C\) basis property for the resulting limits and for quotients by closed normal subgroups.

Imports4

Imported by4

instance

instTopologicalSpaceX

L37 ↗

ProCGroups.ProC.instTopologicalSpaceX

Documentation

The constructed object carries the topological space structure inherited from its construction.

Source context 9 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
section
variable {C : FiniteGroupClass.{u}}
variable {I : Type u} [Preorder I] [Nonempty I]
variable (S : InverseSystems.InverseSystem (I := I))

Lean source · statement

instance instTopologicalSpaceX (i : I) : TopologicalSpace (S.X i)

theorem

inverseLimit

L43 ↗

ProCGroups.ProC.inverseLimit

Documentation

A directed inverse limit of pro-\(C\) groups is pro-\(C\).

Source context 12 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
section
variable {C : FiniteGroupClass.{u}}
variable {I : Type u} [Preorder I] [Nonempty I]
variable (S : InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [InverseSystems.IsGroupSystem S]

Lean source · statement

theorem inverseLimit
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hIso : FiniteGroupClass.IsomClosed C)
    (hQuot : FiniteGroupClass.QuotientClosed C)
    (hdir : Directed (· ≤ ·) (id : I → I))
    (hX : ∀ i, HasOpenNormalBasisInClass C (S.X i)) :
    HasOpenNormalBasisInClass C S.inverseLimit

theorem

quotient_closedNormalSubgroup

L89 ↗

ProCGroups.ProC.quotient_closedNormalSubgroup

Documentation

If \(G\) is pro-\(C\) and \(C\) is closed under quotients, then every quotient of \(G\) by a closed normal subgroup is again pro-\(C\).

Source context 13 commands

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

open Set
open scoped Topology Pointwise
namespace ProCGroups.ProC
universe u v
open InverseSystems
section
variable {C : FiniteGroupClass.{u}}
variable {I : Type u} [Preorder I] [Nonempty I]
variable (S : InverseSystems.InverseSystem (I := I))
variable [∀ i, Group (S.X i)]
variable [∀ i, IsTopologicalGroup (S.X i)]
variable [InverseSystems.IsGroupSystem S]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

Lean source · statement

theorem quotient_closedNormalSubgroup
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hIso : FiniteGroupClass.IsomClosed C)
    (hQuot : FiniteGroupClass.QuotientClosed C)
    (hG : HasOpenNormalBasisInClass C G)
    (K : Subgroup G) [K.Normal] (hK : IsClosed (K : Set G)) :
    HasOpenNormalBasisInClass C (G ⧸ K)

Module documentation

Inverse limits and closed-normal quotients

Declarations

instTopologicalSpaceX

inverseLimit

quotient_closedNormalSubgroup