Module

DescendingClosedSubgroupQuotients.lean

Nyll.ProCGroups.ProC.Quotients.DescendingClosedSubgroupQuotients

4 declarations indexed from sourceView source ↗

Module documentation

Quotients along descending closed-subgroup systems

This file constructs the inverse system of left quotients associated with a directed descending family of closed subgroups and proves the existence of compatible continuous lifts into its limit.

Imports1

Nyll.ProCGroups.ProC.Quotients.OpenSubgroupSections

Imported by2

def

closedSubgroup_sInf

L31 ↗

ProCGroups.ProC.closedSubgroup_sInf

Documentation

The infimum of a family of closed subgroups, repackaged as a closed subgroup.

Source context 7 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
variable {I : Type v} [Preorder I] [Nonempty I]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · full declaration

def closedSubgroup_sInf (L : I → ClosedSubgroup G) : ClosedSubgroup G where
  toSubgroup := iInf fun i => (L i : Subgroup G)
  isClosed' := by
    convert isClosed_iInter fun i => (L i).isClosed' using 1
    ext x
    simp only [Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup, Subgroup.mem_toSubmonoid,
  Subgroup.mem_iInf, mem_iInter]

theorem

closedSubgroup_sInf_le

L40 ↗

ProCGroups.ProC.closedSubgroup_sInf_le

Documentation

The infimum subgroup is contained in each term of the family.

Source context 7 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
variable {I : Type v} [Preorder I] [Nonempty I]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · statement

theorem closedSubgroup_sInf_le {I : Type v} {G : Type u} [Group G] [TopologicalSpace G]
    (L : I → ClosedSubgroup G) (i : I) :
    (closedSubgroup_sInf L : Subgroup G) ≤ (L i : Subgroup G)

def

descendingClosedSubgroupSystem

L48 ↗

ProCGroups.ProC.descendingClosedSubgroupSystem

Documentation

The inverse system of left quotient spaces attached to a decreasing family of closed subgroups.

Source context 7 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
variable {I : Type v} [Preorder I] [Nonempty I]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

Lean source · full declaration

def descendingClosedSubgroupSystem (L : I → ClosedSubgroup G)
    (hL : ∀ {i j}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G)) :
    InverseSystems.InverseSystem (I := I) where
  X i := G ⧸ (L i : Subgroup G)
  topologicalSpace i := inferInstance
  map := fun {i j} hij =>
    leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij)
  continuous_map := by
    intro i j hij
    exact continuous_leftQuotientProjection
      (K := (L j : Subgroup G)) (H := (L i : Subgroup G)) (hL hij)
  map_id := by
    intro i
    exact leftQuotientProjection_id (K := (L i : Subgroup G))
  map_comp := by
    intro i j k hij hjk
    exact
      leftQuotientProjection_comp
        (K := (L k : Subgroup G)) (H := (L j : Subgroup G)) (L := (L i : Subgroup G))
        (hL hjk) (hL hij)

theorem

exists_continuous_leftQuotient_lift_of_directed

L74 ↗

ProCGroups.ProC.exists_continuous_leftQuotient_lift_of_directed

Documentation

A compatible family of maps into a decreasing family of left quotient spaces lifts uniquely to the quotient by the infimum subgroup.

Source context 8 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
variable {I : Type v} [Preorder I] [Nonempty I]
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
omit [T2Space G] [TotallyDisconnectedSpace G] in

Lean source · statement

theorem exists_continuous_leftQuotient_lift_of_directed
    (L : I → ClosedSubgroup G)
    (hL : ∀ {i j}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G))
    (hdir : Directed (· ≤ ·) (id : I → I))
    {Y : Type v} [TopologicalSpace Y]
    (η : ∀ i, Y → G ⧸ (L i : Subgroup G))
    (hηcont : ∀ i, Continuous (η i))
    (hηcompat : ∀ {i j} (hij : i ≤ j),
      leftQuotientProjection (L j : Subgroup G) (L i : Subgroup G) (hL hij) ∘ η j = η i)
    (y0 : Y)
    (hηone : ∀ i, η i y0 = QuotientGroup.mk (s := (L i : Subgroup G)) (1 : G)) :
    ∃ ηinf : Y → G ⧸ ((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G),
      Continuous ηinf ∧
        (∀ i,
          leftQuotientProjection
              (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G))
              (L i : Subgroup G)
              (closedSubgroup_sInf_le (L := L) i) ∘ ηinf = η i) ∧
        ηinf y0 =
          QuotientGroup.mk (s := (((closedSubgroup_sInf L : ClosedSubgroup G) : Subgroup G)))
            (1 : G)

Module documentation

Quotients along descending closed-subgroup systems

Declarations

closedSubgroup_sInf

closedSubgroup_sInf_le

descendingClosedSubgroupSystem

exists_continuous_leftQuotient_lift_of_directed