Module

ProfiniteLimits.lean

Nyll.ProCGroups.InverseSystems.ProfiniteLimits

5 declarations indexed from sourceView source ↗

Module documentation

Projection kernels in profinite inverse limits

For inverse systems of finite discrete groups, the canonical projections are bundled as group homomorphisms. Their kernels are open normal subgroups, and under the usual directedness and surjectivity assumptions these kernels form a fundamental system of neighborhoods of one in the inverse limit.

Imports2

Imported by1

Nyll.ProCGroups.InverseSystems.All

def

inverseLimitProjectionHom

L32 ↗

ProCGroups.inverseLimitProjectionHom

Documentation

The projection from a group-valued inverse limit to one component is viewed as a homomorphism.

Source context 5 commands

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

open scoped Topology Pointwise
namespace ProCGroups
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · full declaration

def inverseLimitProjectionHom {I : Type v} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S] (i : I) :
    S.inverseLimit →* S.X i where
  toFun := S.projection i
  map_one' := rfl
  map_mul' := by
    intro x y
    rfl

def

inverseLimitProjectionKer

L43 ↗

ProCGroups.inverseLimitProjectionKer

Documentation

The kernel of a projection from an inverse limit of discrete groups is open normal.

Source context 5 commands

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

open scoped Topology Pointwise
namespace ProCGroups
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · full declaration

def inverseLimitProjectionKer {I : Type v} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, DiscreteTopology (S.X i)] (i : I) :
    OpenNormalSubgroup S.inverseLimit where
  toOpenSubgroup :=
    { toSubgroup := (inverseLimitProjectionHom S i).ker
      isOpen' := by
        change IsOpen (S.projection i ⁻¹' ({1} : Set (S.X i)))
        exact
          (isOpen_discrete ({1} : Set (S.X i))).preimage
            (S.continuous_projection i) }
  isNormal' := by
    change ((inverseLimitProjectionHom S i).ker).Normal
    infer_instance

theorem

mem_inverseLimitProjectionKer

L63 ↗

ProCGroups.mem_inverseLimitProjectionKer

Documentation

Membership in the kernel of an inverse-limit projection is membership in the kernel at that finite stage.

Source context 5 commands

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

open scoped Topology Pointwise
namespace ProCGroups
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem mem_inverseLimitProjectionKer {I : Type v} [Preorder I]
    {S : InverseSystems.InverseSystem (I := I)}
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, DiscreteTopology (S.X i)]
    {i : I} {x : S.inverseLimit} :
    x ∈ inverseLimitProjectionKer S i ↔ S.projection i x = 1

theorem

exists_inverseLimitProjectionKer_sub_open_nhds_of_one

L75 ↗

ProCGroups.exists_inverseLimitProjectionKer_sub_open_nhds_of_one

Documentation

In an inverse limit of discrete groups, every open neighborhood of \(1\) contains the kernel of one projection map.

Source context 5 commands

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

open scoped Topology Pointwise
namespace ProCGroups
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem exists_inverseLimitProjectionKer_sub_open_nhds_of_one
    {I : Type v} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I)) [Nonempty I]
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, DiscreteTopology (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I))
    {W : Set S.inverseLimit} (hW : IsOpen W) (h1W : (1 : S.inverseLimit) ∈ W) :
    ∃ i : I,
      (((inverseLimitProjectionKer S i : OpenNormalSubgroup S.inverseLimit) :
        Subgroup S.inverseLimit) : Set S.inverseLimit) ⊆ W

theorem

inverseLimitProjectionKer_fundamentalSystemAtOne

L100 ↗

ProCGroups.inverseLimitProjectionKer_fundamentalSystemAtOne

Documentation

The projection kernels form a fundamental system of open neighborhoods of 1 in the inverse limit.

Source context 5 commands

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

open scoped Topology Pointwise
namespace ProCGroups
universe u v
section
variable {G : Type u} [Group G] [TopologicalSpace G]

Lean source · statement

theorem inverseLimitProjectionKer_fundamentalSystemAtOne
    {I : Type v} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I)) [Nonempty I]
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, DiscreteTopology (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I)) :
    (∀ i : I,
      IsOpen ((((inverseLimitProjectionKer S i : OpenNormalSubgroup S.inverseLimit) :
        Subgroup S.inverseLimit) : Set S.inverseLimit)) ∧
      (1 : S.inverseLimit) ∈ (((inverseLimitProjectionKer S i :
        OpenNormalSubgroup S.inverseLimit) : Subgroup S.inverseLimit) : Set S.inverseLimit)) ∧
    ∀ W : Set S.inverseLimit, IsOpen W → (1 : S.inverseLimit) ∈ W →
      ∃ i : I,
        ((((inverseLimitProjectionKer S i : OpenNormalSubgroup S.inverseLimit) :
          Subgroup S.inverseLimit) : Set S.inverseLimit)) ⊆ W

Module documentation

Projection kernels in profinite inverse limits

Declarations

inverseLimitProjectionHom

inverseLimitProjectionKer

mem_inverseLimitProjectionKer

exists_inverseLimitProjectionKer_sub_open_nhds_of_one

inverseLimitProjectionKer_fundamentalSystemAtOne