NYLL
Module

TopologicalAbelianizationLimits.lean

Nyll.ProCGroups.Abelian.TopologicalAbelianizationLimits
19 declarations indexed from sourceView source ↗

Module documentation

Topological abelianization and inverse limits

This module applies topological abelianization stagewise to inverse systems and compares the resulting limit with the abelianization of the original limit.

Imports4
Imported by2

Declarations

def

abelianizationInverseSystem

L27 ↗
ProCGroups.Abelian.abelianizationInverseSystem
Documentation

The stagewise inverse system obtained by applying topological abelianization.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · full declaration
def abelianizationInverseSystem
    {I : Type u} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)] :
    InverseSystems.InverseSystem (I := I) where
  X := fun i => TopologicalAbelianization (S.X i)
  topologicalSpace := fun i => inferInstance
  map := fun {i j} hij =>
    TopologicalAbelianization.map
      { toMonoidHom :=
          { toFun := S.map hij
            map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij
            map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }
        continuous_toFun := S.continuous_map hij }
  continuous_map := by
    intro i j hij
    exact (TopologicalAbelianization.map
      { toMonoidHom :=
          { toFun := S.map hij
            map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij
            map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }
        continuous_toFun := S.continuous_map hij }).continuous_toFun
  map_id := by
    intro i
    funext x
    refine Quotient.inductionOn' x ?_
    intro a
    change
      QuotientGroup.mk'
          (Subgroup.topologicalClosure (commutator (S.X i)))
          (S.map (le_rfl : i ≤ i) a) =
        QuotientGroup.mk'
          (Subgroup.topologicalClosure (commutator (S.X i)))
          a
    exact congrArg
      (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))))
      (S.map_id_apply i a)
  map_comp := by
    intro i j k hij hjk
    funext x
    refine Quotient.inductionOn' x ?_
    intro a
    change
      QuotientGroup.mk'
          (Subgroup.topologicalClosure (commutator (S.X i)))
          (S.map hij (S.map hjk a)) =
        QuotientGroup.mk'
          (Subgroup.topologicalClosure (commutator (S.X i)))
          (S.map (hij.trans hjk) a)
    exact congrArg
      (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))))
      (S.map_comp_apply hij hjk a)
instance

abelianizationInverseSystem_stageGroup

L82 ↗
ProCGroups.Abelian.abelianizationInverseSystem_stageGroup
Documentation

Each stage of the abelianization inverse system inherits its quotient group structure.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
instance abelianizationInverseSystem_stageGroup
    {I : Type u} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)] (i : I) :
    Group ((abelianizationInverseSystem S).X i)
instance

abelianizationInverseSystem_isGroupSystem

L92 ↗
ProCGroups.Abelian.abelianizationInverseSystem_isGroupSystem
Documentation

The abelianization inverse system is a group-valued inverse system.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · full declaration
instance abelianizationInverseSystem_isGroupSystem
    {I : Type u} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)] :
    InverseSystems.IsGroupSystem (abelianizationInverseSystem S) where
  map_one := by
    intro i j hij
    exact (TopologicalAbelianization.map
      { toMonoidHom :=
          { toFun := S.map hij
            map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij
            map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }
        continuous_toFun := S.continuous_map hij }).map_one
  map_mul := by
    intro i j hij x y
    exact (TopologicalAbelianization.map
      { toMonoidHom :=
          { toFun := S.map hij
            map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij
            map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }
        continuous_toFun := S.continuous_map hij }).map_mul x y
  map_inv := by
    intro i j hij x
    exact (TopologicalAbelianization.map
      { toMonoidHom :=
          { toFun := S.map hij
            map_one' := InverseSystems.IsGroupSystem.map_one (S := S) hij
            map_mul' := InverseSystems.IsGroupSystem.map_mul (S := S) hij }
        continuous_toFun := S.continuous_map hij }).map_inv x
def

toAbelianizationInverseSystem

L127 ↗
ProCGroups.Abelian.toAbelianizationInverseSystem
Documentation

The stagewise quotient maps assemble into a morphism from an inverse system to its stagewise topological abelianization.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · full declaration
def toAbelianizationInverseSystem
    {I : Type u} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)] :
    S.Morphism (abelianizationInverseSystem S) where
  map := fun i => TopologicalAbelianization.mk (S.X i)
  continuous_map := fun _ => continuous_quotient_mk'
  comm := by
    intro i j hij
    funext x
    rfl
def

closedCommutatorCompatibleClosedNormalSubgroups

L144 ↗
ProCGroups.Abelian.closedCommutatorCompatibleClosedNormalSubgroups
Documentation

The stagewise closed commutator subgroups form a compatible closed-normal family in any group-valued inverse system of topological groups.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · full declaration
def closedCommutatorCompatibleClosedNormalSubgroups
    {I : Type u} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)] :
    S.CompatibleClosedNormalSubgroups where
  N := fun i => Subgroup.closedCommutator (S.X i)
  normal := fun i => by infer_instance
  closed := fun i => Subgroup.isClosed_closedCommutator (S.X i)
  map_le := by
    intro i j hij x hx
    let f : S.X j →ₜ* S.X i :=
      { toMonoidHom := S.transitionHom hij
        continuous_toFun :=
          InverseSystems.InverseSystem.continuous_transitionHom (S := S) hij }
    have hxmap :
        S.transitionHom hij x ∈
          (Subgroup.closedCommutator (S.X j)).map f.toMonoidHom :=
      Subgroup.mem_map_of_mem f.toMonoidHom hx
    exact Subgroup.closedCommutator_map_le f hxmap
def

topologicalAbelianizationInverseLimitComparison

L169 ↗
ProCGroups.Abelian.topologicalAbelianizationInverseLimitComparison
Documentation

The canonical comparison map from the abelianization of an inverse limit to the inverse limit of the stagewise abelianizations.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
def topologicalAbelianizationInverseLimitComparison
    {I : Type u} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)] :
    TopologicalAbelianization S.inverseLimit →ₜ*
      (abelianizationInverseSystem S).inverseLimit
theorem

π_topologicalAbelianizationInverseLimitComparison

L219 ↗
ProCGroups.Abelian.π_topologicalAbelianizationInverseLimitComparison
Documentation

The projection from the topological abelianization inverse-limit comparison to a finite stage.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · full declaration
theorem π_topologicalAbelianizationInverseLimitComparison
    {I : Type u} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)]
    (i : I) :
    (abelianizationInverseSystem S).projection i ∘
        topologicalAbelianizationInverseLimitComparison S =
      TopologicalAbelianization.map
        { toMonoidHom :=
            { toFun := S.projection i
              map_one' := rfl
              map_mul' := by intro x y; rfl }
          continuous_toFun := S.continuous_projection i } := by
  let T : InverseSystems.InverseSystem (I := I) := abelianizationInverseSystem S
  let ψ : ∀ i, TopologicalAbelianization S.inverseLimit →ₜ* T.X i := fun i =>
    TopologicalAbelianization.map
      { toMonoidHom := InverseSystems.projectionHom (S := S) i
        continuous_toFun := S.continuous_projection i }
  let ψFun : ∀ i, TopologicalAbelianization S.inverseLimit → T.X i := fun i => ψ i
  have hcompat : T.CompatibleMaps ψFun := by
    intro i j hij
    funext x
    refine Quotient.inductionOn' x ?_
    intro a
    change
      QuotientGroup.mk'
          (Subgroup.topologicalClosure (commutator (S.X i)))
          (S.map hij (S.projection j a)) =
        QuotientGroup.mk'
          (Subgroup.topologicalClosure (commutator (S.X i)))
          (S.projection i a)
    exact congrArg
      (QuotientGroup.mk' (Subgroup.topologicalClosure (commutator (S.X i))))
      (S.projection_compatible a i j hij)
  funext x
  change T.projection i (T.inverseLimitLift ψFun hcompat x) = ψFun i x
  exact T.projection_inverseLimitLift_apply ψFun hcompat i x
theorem

π_topologicalAbelianizationInverseLimitComparison_mk

L262 ↗
ProCGroups.Abelian.π_topologicalAbelianizationInverseLimitComparison_mk
Documentation

The finite-stage projection of the topological abelianization comparison has the stated value on representatives.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
theorem π_topologicalAbelianizationInverseLimitComparison_mk
    {I : Type u} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)]
    (i : I) (x : S.inverseLimit) :
    (abelianizationInverseSystem S).projection i
        (topologicalAbelianizationInverseLimitComparison S
          (QuotientGroup.mk' (Subgroup.closedCommutator S.inverseLimit) x)) =
      QuotientGroup.mk' (Subgroup.closedCommutator (S.X i)) (S.projection i x)
theorem

limMap_toAbelianizationInverseSystem_apply

L278 ↗
ProCGroups.Abelian.limMap_toAbelianizationInverseSystem_apply
Documentation

The inverse-limit map induced by stagewise abelianization factors as the limit quotient map followed by the abelianization comparison map.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
theorem limMap_toAbelianizationInverseSystem_apply
    {I : Type u} [Preorder I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)]
    (x : S.inverseLimit) :
    S.limMap (toAbelianizationInverseSystem S) x =
      topologicalAbelianizationInverseLimitComparison S
        (TopologicalAbelianization.mk S.inverseLimit x)
theorem

inj_topologicalAbelianizationInverseLimitComparison_of_profinite_inverse_system

L299 ↗
ProCGroups.Abelian.inj_topologicalAbelianizationInverseLimitComparison_of_profinite_inverse_system
Documentation

Auxiliary injectivity of the canonical comparison map used to build the continuous equivalence; the main formulation is \(injective_topologicalAbelianizationInverseLimitComparison\).

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
theorem inj_topologicalAbelianizationInverseLimitComparison_of_profinite_inverse_system
    {I : Type u} [Preorder I] [Nonempty I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)]
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I)) :
    Function.Injective (topologicalAbelianizationInverseLimitComparison S)
theorem

mem_closedCommutator_inverseLimit_iff

L385 ↗
ProCGroups.Abelian.mem_closedCommutator_inverseLimit_iff
Documentation

Membership in the inverse-limit closed commutator subgroup is equivalent to the displayed coordinate condition.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
theorem mem_closedCommutator_inverseLimit_iff
      {I : Type u} [Preorder I] [Nonempty I]
      {S : InverseSystems.InverseSystem (I := I)}
      [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
      [∀ i, IsTopologicalGroup (S.X i)]
      [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
      [∀ i, TotallyDisconnectedSpace (S.X i)]
      (hdir : Directed (· ≤ ·) (id : I → I)) {x : S.inverseLimit} :
      x ∈ Subgroup.closedCommutator S.inverseLimit ↔
        ∀ i, S.projection i x ∈ Subgroup.closedCommutator (S.X i)
theorem

closedCommutator_inverseLimit_eq_iInf_comap

L443 ↗
ProCGroups.Abelian.closedCommutator_inverseLimit_eq_iInf_comap
Documentation

The closed commutator subgroup of a profinite inverse limit is the infimum of the pullbacks of the stagewise closed commutator subgroups.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · full declaration
theorem closedCommutator_inverseLimit_eq_iInf_comap
      {I : Type u} [Preorder I] [Nonempty I]
      (S : InverseSystems.InverseSystem (I := I))
      [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
      [∀ i, IsTopologicalGroup (S.X i)]
      [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
      [∀ i, TotallyDisconnectedSpace (S.X i)]
      (hdir : Directed (· ≤ ·) (id : I → I)) :
      Subgroup.closedCommutator S.inverseLimit =
        ⨅ i, (Subgroup.closedCommutator (S.X i)).comap
          ({ toFun := S.projection i
             map_one' := rfl
             map_mul' := by intro x y; rfl } : S.inverseLimit →* S.X i) := by
    change Subgroup.closedCommutator S.inverseLimit =
      ⨅ i, (Subgroup.closedCommutator (S.X i)).comap
        (InverseSystems.projectionHom (S := S) i)
    ext x
    simp only [Subgroup.mem_iInf, Subgroup.mem_comap, InverseSystems.projectionHom_apply]
    exact mem_closedCommutator_inverseLimit_iff (S := S) hdir (x := x)
theorem

closedCommutatorCompatibleClosedNormalSubgroups_inverseLimitKernel

L467 ↗
ProCGroups.Abelian.closedCommutatorCompatibleClosedNormalSubgroups_inverseLimitKernel
Documentation

For the closed-commutator compatible family, the generic quotient-limit kernel is the closed commutator subgroup of the inverse limit.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
theorem closedCommutatorCompatibleClosedNormalSubgroups_inverseLimitKernel
      {I : Type u} [Preorder I] [Nonempty I]
      (S : InverseSystems.InverseSystem (I := I))
      [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
      [∀ i, IsTopologicalGroup (S.X i)]
      [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
      [∀ i, TotallyDisconnectedSpace (S.X i)]
      (hdir : Directed (· ≤ ·) (id : I → I)) :
      (closedCommutatorCompatibleClosedNormalSubgroups S).inverseLimitKernel =
        Subgroup.closedCommutator S.inverseLimit
def

closedCommutatorQuotientInverseLimitContinuousMulEquiv

L484 ↗
ProCGroups.Abelian.closedCommutatorQuotientInverseLimitContinuousMulEquiv
Documentation

The generic quotient inverse-limit theorem specialized to the closed commutator family.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
def closedCommutatorQuotientInverseLimitContinuousMulEquiv
    {I : Type u} [Preorder I] [Nonempty I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)]
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I)) :
    TopologicalAbelianization S.inverseLimit ≃ₜ*
      (closedCommutatorCompatibleClosedNormalSubgroups S).quotientInverseSystem.inverseLimit
theorem

projection_closedCommutatorQuotientInverseLimitContinuousMulEquiv_mk

L517 ↗
ProCGroups.Abelian.projection_closedCommutatorQuotientInverseLimitContinuousMulEquiv_mk
Documentation

The projection closed commutator quotient inverse limit continuous multiplicative equivalence mk is compatible with the profinite topology and gives the continuous map or equivalence determined by the finite-quotient data.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
theorem projection_closedCommutatorQuotientInverseLimitContinuousMulEquiv_mk
    {I : Type u} [Preorder I] [Nonempty I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)]
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I))
    (i : I) (x : S.inverseLimit) :
    (closedCommutatorCompatibleClosedNormalSubgroups S).quotientInverseSystem.projection i
        (closedCommutatorQuotientInverseLimitContinuousMulEquiv (S := S) hdir
          (QuotientGroup.mk' (Subgroup.closedCommutator S.inverseLimit) x)) =
      QuotientGroup.mk'
        ((closedCommutatorCompatibleClosedNormalSubgroups S).N i)
        (S.projection i x)
def

topologicalAbelianizationInverseLimitContinuousMulEquiv

L549 ↗
ProCGroups.Abelian.topologicalAbelianizationInverseLimitContinuousMulEquiv
Documentation

Topological abelianization commutes with profinite inverse limits as a topological-group isomorphism.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
def topologicalAbelianizationInverseLimitContinuousMulEquiv
    {I : Type u} [Preorder I] [Nonempty I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)]
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I)) :
    TopologicalAbelianization S.inverseLimit ≃ₜ*
      (abelianizationInverseSystem S).inverseLimit
theorem

topologicalAbelianizationInverseLimitContinuousMulEquiv_apply

L568 ↗
ProCGroups.Abelian.topologicalAbelianizationInverseLimitContinuousMulEquiv_apply
Documentation

The inverse-limit comparison for topological abelianization evaluates coordinatewise.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
theorem topologicalAbelianizationInverseLimitContinuousMulEquiv_apply
    {I : Type u} [Preorder I] [Nonempty I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)]
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I))
    (x : TopologicalAbelianization S.inverseLimit) :
    topologicalAbelianizationInverseLimitContinuousMulEquiv (S := S) hdir x =
      topologicalAbelianizationInverseLimitComparison S x
theorem

injective_topologicalAbelianizationInverseLimitComparison

L620 ↗
ProCGroups.Abelian.injective_topologicalAbelianizationInverseLimitComparison
Documentation

The inverse-limit comparison is injective, as a corollary of the continuous equivalence.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
theorem injective_topologicalAbelianizationInverseLimitComparison
    {I : Type u} [Preorder I] [Nonempty I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)]
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I)) :
    Function.Injective (topologicalAbelianizationInverseLimitComparison S)
theorem

surjective_topologicalAbelianizationInverseLimitComparison

L635 ↗
ProCGroups.Abelian.surjective_topologicalAbelianizationInverseLimitComparison
Documentation

The inverse-limit comparison is surjective, as a corollary of the continuous equivalence.

Source context 4 commands

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

open scoped Topology
namespace ProCGroups.Abelian
open InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
universe u v
Lean source · statement
theorem surjective_topologicalAbelianizationInverseLimitComparison
    {I : Type u} [Preorder I] [Nonempty I]
    (S : InverseSystems.InverseSystem (I := I))
    [∀ i, Group (S.X i)] [InverseSystems.IsGroupSystem S]
    [∀ i, IsTopologicalGroup (S.X i)]
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    [∀ i, TotallyDisconnectedSpace (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I)) :
    Function.Surjective (topologicalAbelianizationInverseLimitComparison S)

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