NYLL
Module

StagewiseIso.lean

Nyll.ProCGroups.InverseSystems.StagewiseIso
8 declarations indexed from sourceView source ↗

Module documentation

Stagewise isomorphisms and inverse-limit equivalences

A compatible family of continuous group isomorphisms defines morphisms in both directions between two inverse systems. The induced maps on their inverse limits are assembled into a canonical continuous multiplicative equivalence.

Imports2
Imported by5

Declarations

structure

InverseSystemIso

L37 ↗
ProCGroups.InverseSystems.InverseSystem.InverseSystemIso
Documentation

A compatible family of stagewise continuous group isomorphisms between two concrete inverse systems.

Source context 10 commands

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

open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v
namespace InverseSystem
variable {I : Type u} [Preorder I]
variable (S T : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [∀ i, Group (T.X i)]
variable [IsGroupSystem S] [IsGroupSystem T]
variable [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)]
Lean source · full declaration
structure InverseSystemIso where
  /-- A continuous group isomorphism between the source and target objects at each index. -/
  stageEquiv : ∀ i, S.X i ≃ₜ* T.X i
  /-- The stagewise isomorphisms intertwine the transition maps of the two systems. -/
  comm : ∀ {i j : I} (hij : i ≤ j) (x : S.X j),
    stageEquiv i (S.map hij x) = T.map hij (stageEquiv j x)
def

toMorphism

L49 ↗
ProCGroups.InverseSystems.InverseSystem.InverseSystemIso.toMorphism
Documentation

A stagewise isomorphism determines the forward morphism of inverse systems.

Source context 12 commands

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

open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v
namespace InverseSystem
variable {I : Type u} [Preorder I]
variable (S T : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [∀ i, Group (T.X i)]
variable [IsGroupSystem S] [IsGroupSystem T]
variable [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)]
namespace InverseSystemIso
variable {S T}
Lean source · full declaration
def toMorphism (E : InverseSystemIso S T) : S.Morphism T where
  map i := E.stageEquiv i
  continuous_map i := (E.stageEquiv i).continuous_toFun
  comm := by
    intro i j hij
    funext x
    exact (E.comm hij x).symm
def

invMorphism

L58 ↗
ProCGroups.InverseSystems.InverseSystem.InverseSystemIso.invMorphism
Documentation

A stagewise isomorphism determines the inverse morphism of inverse systems.

Source context 12 commands

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

open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v
namespace InverseSystem
variable {I : Type u} [Preorder I]
variable (S T : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [∀ i, Group (T.X i)]
variable [IsGroupSystem S] [IsGroupSystem T]
variable [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)]
namespace InverseSystemIso
variable {S T}
Lean source · full declaration
def invMorphism (E : InverseSystemIso S T) : T.Morphism S where
  map i := (E.stageEquiv i).symm
  continuous_map i := (E.stageEquiv i).continuous_invFun
  comm := by
    intro i j hij
    funext x
    apply (E.stageEquiv i).injective
    simpa using E.comm hij ((E.stageEquiv j).symm x)
def

toContinuousMonoidHom

L68 ↗
ProCGroups.InverseSystems.InverseSystem.InverseSystemIso.toContinuousMonoidHom
Documentation

The forward continuous homomorphism on inverse limits induced by a stagewise isomorphism.

Source context 12 commands

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

open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v
namespace InverseSystem
variable {I : Type u} [Preorder I]
variable (S T : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [∀ i, Group (T.X i)]
variable [IsGroupSystem S] [IsGroupSystem T]
variable [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)]
namespace InverseSystemIso
variable {S T}
Lean source · full declaration
def toContinuousMonoidHom (E : InverseSystemIso S T) :
    S.inverseLimit →ₜ* T.inverseLimit where
  toMonoidHom :=
    { toFun := S.limMap E.toMorphism
      map_one' := by
        apply T.ext
        intro i
        change T.projection i (S.limMap E.toMorphism 1) = T.projection i 1
        rw [S.π_limMap_apply (Θ := E.toMorphism)]
        change (E.stageEquiv i) (1 : S.X i) = (1 : T.X i)
        exact (E.stageEquiv i).toMulEquiv.map_one
      map_mul' := by
        intro x y
        apply T.ext
        intro i
        change T.projection i (S.limMap E.toMorphism (x * y)) =
          T.projection i (S.limMap E.toMorphism x * S.limMap E.toMorphism y)
        rw [S.π_limMap_apply (Θ := E.toMorphism)]
        rw [projection_mul (S := T), S.π_limMap_apply (Θ := E.toMorphism),
          S.π_limMap_apply (Θ := E.toMorphism)]
        change (E.stageEquiv i) (S.projection i x * S.projection i y) =
          (E.stageEquiv i) (S.projection i x) * (E.stageEquiv i) (S.projection i y)
        exact (E.stageEquiv i).toMulEquiv.map_mul (S.projection i x) (S.projection i y) }
  continuous_toFun := S.continuous_limMap E.toMorphism
def

invContinuousMonoidHom

L94 ↗
ProCGroups.InverseSystems.InverseSystem.InverseSystemIso.invContinuousMonoidHom
Documentation

The inverse continuous homomorphism on inverse limits induced by a stagewise isomorphism.

Source context 12 commands

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

open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v
namespace InverseSystem
variable {I : Type u} [Preorder I]
variable (S T : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [∀ i, Group (T.X i)]
variable [IsGroupSystem S] [IsGroupSystem T]
variable [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)]
namespace InverseSystemIso
variable {S T}
Lean source · full declaration
def invContinuousMonoidHom (E : InverseSystemIso S T) :
    T.inverseLimit →ₜ* S.inverseLimit where
  toMonoidHom :=
    { toFun := T.limMap E.invMorphism
      map_one' := by
        apply S.ext
        intro i
        change S.projection i (T.limMap E.invMorphism 1) = S.projection i 1
        rw [T.π_limMap_apply (Θ := E.invMorphism)]
        change (E.stageEquiv i).symm (1 : T.X i) = (1 : S.X i)
        exact (E.stageEquiv i).symm.toMulEquiv.map_one
      map_mul' := by
        intro x y
        apply S.ext
        intro i
        change S.projection i (T.limMap E.invMorphism (x * y)) =
          S.projection i (T.limMap E.invMorphism x * T.limMap E.invMorphism y)
        rw [T.π_limMap_apply (Θ := E.invMorphism)]
        rw [projection_mul (S := S), T.π_limMap_apply (Θ := E.invMorphism),
          T.π_limMap_apply (Θ := E.invMorphism)]
        change (E.stageEquiv i).symm (T.projection i x * T.projection i y) =
          (E.stageEquiv i).symm (T.projection i x) * (E.stageEquiv i).symm (T.projection i y)
        exact (E.stageEquiv i).symm.toMulEquiv.map_mul (T.projection i x) (T.projection i y) }
  continuous_toFun := T.continuous_limMap E.invMorphism
def

inverseLimitContinuousMulEquiv

L123 ↗
ProCGroups.InverseSystems.InverseSystem.InverseSystemIso.inverseLimitContinuousMulEquiv
Documentation

Compatible stagewise continuous group isomorphisms induce a continuous multiplicative equivalence on concrete inverse limits.

Source context 12 commands

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

open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v
namespace InverseSystem
variable {I : Type u} [Preorder I]
variable (S T : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [∀ i, Group (T.X i)]
variable [IsGroupSystem S] [IsGroupSystem T]
variable [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)]
namespace InverseSystemIso
variable {S T}
Lean source · statement
def inverseLimitContinuousMulEquiv (E : InverseSystemIso S T) :
    S.inverseLimit ≃ₜ* T.inverseLimit
theorem

projection_inverseLimitContinuousMulEquiv

L153 ↗
ProCGroups.InverseSystems.InverseSystem.InverseSystemIso.projection_inverseLimitContinuousMulEquiv
Documentation

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

Source context 13 commands

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

open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v
namespace InverseSystem
variable {I : Type u} [Preorder I]
variable (S T : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [∀ i, Group (T.X i)]
variable [IsGroupSystem S] [IsGroupSystem T]
variable [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)]
namespace InverseSystemIso
variable {S T}
omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)] in
Lean source · statement
theorem projection_inverseLimitContinuousMulEquiv
    (E : InverseSystemIso S T) (i : I) (x : S.inverseLimit) :
    T.projection i (E.inverseLimitContinuousMulEquiv x) =
      E.stageEquiv i (S.projection i x)
theorem

projection_inverseLimitContinuousMulEquiv_symm

L167 ↗
ProCGroups.InverseSystems.InverseSystem.InverseSystemIso.projection_inverseLimitContinuousMulEquiv_symm
Documentation

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

Source context 13 commands

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

open scoped Topology
namespace ProCGroups
namespace InverseSystems
universe u v
namespace InverseSystem
variable {I : Type u} [Preorder I]
variable (S T : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [∀ i, Group (T.X i)]
variable [IsGroupSystem S] [IsGroupSystem T]
variable [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)]
namespace InverseSystemIso
variable {S T}
omit [∀ i, IsTopologicalGroup (S.X i)] [∀ i, IsTopologicalGroup (T.X i)] in
Lean source · statement
theorem projection_inverseLimitContinuousMulEquiv_symm
    (E : InverseSystemIso S T) (i : I) (x : T.inverseLimit) :
    S.projection i (E.inverseLimitContinuousMulEquiv.symm x) =
      (E.stageEquiv i).symm (T.projection i x)

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