NYLL
Module

Quotients.lean

Nyll.ProCGroups.InverseSystems.Quotients
25 declarations indexed from sourceView source ↗

Module documentation

Quotients of group-valued inverse systems

A compatible family of closed normal stage subgroups induces an inverse system of quotient groups and a canonical map from the original limit. This module identifies its kernel and, under compact Hausdorff directed-surjective hypotheses, proves that quotienting the inverse limit agrees topologically and algebraically with taking the inverse limit of the stage quotients.

Imports3
Imported by2

Declarations

def

transitionHom

L35 ↗
ProCGroups.InverseSystems.InverseSystem.transitionHom
Documentation

The transition map of a group-valued inverse system is bundled as a homomorphism.

Source context 9 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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
Lean source · full declaration
def transitionHom {i j : I} (hij : i ≤ j) : S.X j →* S.X i where
  toFun := S.map hij
  map_one' := IsGroupSystem.map_one (S := S) hij
  map_mul' := IsGroupSystem.map_mul (S := S) hij
theorem

transitionHom_apply

L42 ↗
ProCGroups.InverseSystems.InverseSystem.transitionHom_apply
Documentation

The bundled transition homomorphism evaluates to the underlying transition map of S.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem transitionHom_apply {i j : I} (hij : i ≤ j) (x : S.X j) :
    S.transitionHom hij x = S.map hij x
theorem

continuous_transitionHom

L47 ↗
ProCGroups.InverseSystems.InverseSystem.continuous_transitionHom
Documentation

The bundled transition homomorphism of an inverse system is continuous.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem continuous_transitionHom {i j : I} (hij : i ≤ j) :
    Continuous (S.transitionHom hij)
structure

CompatibleClosedNormalSubgroups

L52 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups
Documentation

Closed normal subgroups of the stages, compatible with transition maps.

Source context 9 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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
Lean source · full declaration
structure CompatibleClosedNormalSubgroups where
  /-- The subgroup by which the stage at index `i` will be quotiented. -/
  N : ∀ i, Subgroup (S.X i)
  /-- Every selected stage subgroup is normal, so its group quotient is defined. -/
  normal : ∀ i, (N i).Normal
  /-- Every selected stage subgroup is closed in the topology of that stage. -/
  closed : ∀ i, IsClosed ((N i : Subgroup (S.X i)) : Set (S.X i))
  /--
  A transition homomorphism sends the subgroup at the later stage into the subgroup at the
  earlier stage, and hence descends to the corresponding quotients.
  -/
  map_le :
    ∀ {i j : I} (hij : i ≤ j), N j ≤ (N i).comap (S.transitionHom hij)
instance

instNormalN

L72 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.instNormalN
Documentation

The chosen subgroup is normal.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
Lean source · statement
instance instNormalN (i : I) : (Q.N i).Normal
def

quotientMap

L75 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.quotientMap
Documentation

The transition map induced on stage quotients.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
Lean source · statement
def quotientMap {i j : I} (hij : i ≤ j) :
    S.X j ⧸ Q.N j →* S.X i ⧸ Q.N i
theorem

quotientMap_mk

L84 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.quotientMap_mk
Documentation

The induced quotient transition sends the class of x modulo N j to the class of its transition image modulo N i.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem quotientMap_mk {i j : I} (hij : i ≤ j) (x : S.X j) :
    Q.quotientMap hij (QuotientGroup.mk' (Q.N j) x) =
      QuotientGroup.mk' (Q.N i) (S.map hij x)
theorem

continuous_quotientMap

L92 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.continuous_quotientMap
Documentation

The induced map on stage quotients is continuous.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem continuous_quotientMap {i j : I} (hij : i ≤ j) :
    Continuous (Q.quotientMap hij)
def

quotientInverseSystem

L99 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.quotientInverseSystem
Documentation

The inverse system obtained by quotienting each stage by a compatible closed normal subgroup.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
Lean source · full declaration
def quotientInverseSystem : InverseSystem (I := I) where
  X := fun i => S.X i ⧸ Q.N i
  topologicalSpace := fun i => inferInstance
  map := fun {_i _j} hij => Q.quotientMap hij
  continuous_map := fun {_i _j} hij => Q.continuous_quotientMap hij
  map_id := by
    intro i
    funext x
    refine Quotient.inductionOn' x ?_
    intro a
    change QuotientGroup.mk' (Q.N i) (S.map (le_rfl : i ≤ i) a) =
      QuotientGroup.mk' (Q.N i) a
    exact congrArg (QuotientGroup.mk' (Q.N 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' (Q.N i) (S.map hij (S.map hjk a)) =
      QuotientGroup.mk' (Q.N i) (S.map (hij.trans hjk) a)
    exact congrArg (QuotientGroup.mk' (Q.N i)) (S.map_comp_apply hij hjk a)
instance

quotientInverseSystem_stageGroup

L122 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.quotientInverseSystem_stageGroup
Documentation

The quotient inverse system has the expected finite-stage quotient groups.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
Lean source · statement
instance quotientInverseSystem_stageGroup (i : I) :
    Group (Q.quotientInverseSystem.X i)
instance

quotientInverseSystem_stageTopologicalGroup

L129 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.quotientInverseSystem_stageTopologicalGroup
Documentation

Each stage quotient carries the quotient topology and its induced topological-group structure.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
Lean source · statement
instance quotientInverseSystem_stageTopologicalGroup (i : I) :
    IsTopologicalGroup (Q.quotientInverseSystem.X i)
theorem

quotientInverseSystem_stageT2Space

L135 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.quotientInverseSystem_stageT2Space
Documentation

Fix the closed-subgroup boundary before using the quotient's canonical topology.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
Lean source · statement
theorem quotientInverseSystem_stageT2Space (i : I) :
    T2Space (Q.quotientInverseSystem.X i)
instance

quotientInverseSystem_isGroupSystem

L142 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.quotientInverseSystem_isGroupSystem
Documentation

The induced quotient transitions preserve the group operations at every stage.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
Lean source · full declaration
instance quotientInverseSystem_isGroupSystem :
    IsGroupSystem Q.quotientInverseSystem where
  map_one := by
    intro i j hij
    exact (Q.quotientMap hij).map_one
  map_mul := by
    intro i j hij x y
    exact (Q.quotientMap hij).map_mul x y
  map_inv := by
    intro i j hij x
    exact (Q.quotientMap hij).map_inv x
def

toQuotientInverseSystem

L155 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.toQuotientInverseSystem
Documentation

The stagewise quotient maps form a morphism from the original system to the quotient system.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
Lean source · full declaration
def toQuotientInverseSystem : S.Morphism Q.quotientInverseSystem where
  map := fun i => QuotientGroup.mk' (Q.N i)
  continuous_map := fun _ => QuotientGroup.continuous_mk
  comm := by
    intro i j hij
    funext x
    exact (Q.quotientMap_mk hij x).symm
def

inverseLimitKernel

L164 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.inverseLimitKernel
Documentation

Kernel of the map from the inverse limit to the inverse limit of stage quotients.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
Lean source · statement
def inverseLimitKernel : Subgroup S.inverseLimit
instance

inverseLimitKernel_normal

L171 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.inverseLimitKernel_normal
Documentation

The intersection of the pullbacks of the normal subgroups N i along all limit projections is a normal subgroup of the inverse limit.

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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
Lean source · full declaration
instance inverseLimitKernel_normal : Q.inverseLimitKernel.Normal where
  conj_mem x hx g := by
    rw [inverseLimitKernel] at hx ⊢
    simp only [projectionHom, Subgroup.mem_iInf, Subgroup.mem_comap, MonoidHom.coe_mk,
        OneHom.coe_mk,
  projection_apply] at hx ⊢
    intro i
    change
      S.projection i g * S.projection i x * (S.projection i g)⁻¹ ∈ Q.N i
    exact (Q.normal i).conj_mem (S.projection i x) (hx i) (S.projection i g)
theorem

mem_inverseLimitKernel_iff

L189 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.mem_inverseLimitKernel_iff
Documentation

Membership in the named kernel is equivalent to vanishing under its defining quotient or augmentation map.

Source context 14 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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
variable {Q}
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem mem_inverseLimitKernel_iff {x : S.inverseLimit} :
    x ∈ Q.inverseLimitKernel ↔ ∀ i, S.projection i x ∈ Q.N i
def

quotientInverseLimitComparison

L201 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.quotientInverseLimitComparison
Documentation

The canonical comparison from the quotient of the inverse limit to the inverse limit of the stage quotients.

Source context 14 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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
variable {Q}
variable (Q)
Lean source · statement
def quotientInverseLimitComparison :
    S.inverseLimit ⧸ Q.inverseLimitKernel →ₜ* Q.quotientInverseSystem.inverseLimit
theorem

quotientInverseLimitComparison_mk

L253 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.quotientInverseLimitComparison_mk
Documentation

The quotient inverse-limit comparison sends a representative to its compatible family of quotient coordinates.

Source context 15 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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
variable {Q}
variable (Q)
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem quotientInverseLimitComparison_mk (x : S.inverseLimit) :
    Q.quotientInverseLimitComparison (QuotientGroup.mk' Q.inverseLimitKernel x) =
      S.limMap Q.toQuotientInverseSystem x
theorem

projection_quotientInverseLimitComparison_mk

L265 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.projection_quotientInverseLimitComparison_mk
Documentation

Projecting the quotient inverse-limit comparison gives the corresponding stage quotient representative.

Source context 15 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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
variable {Q}
variable (Q)
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem projection_quotientInverseLimitComparison_mk
    (i : I) (x : S.inverseLimit) :
    Q.quotientInverseSystem.projection i
        (Q.quotientInverseLimitComparison (QuotientGroup.mk' Q.inverseLimitKernel x)) =
      QuotientGroup.mk' (Q.N i) (S.projection i x)
theorem

ker_quotientInverseLimitComparison

L275 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.ker_quotientInverseLimitComparison
Documentation

The comparison map has trivial kernel.

Source context 15 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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
variable {Q}
variable (Q)
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem ker_quotientInverseLimitComparison :
    Q.quotientInverseLimitComparison.toMonoidHom.ker = ⊥
theorem

injective_quotientInverseLimitComparison

L298 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.injective_quotientInverseLimitComparison
Documentation

The comparison map is injective: its kernel is exactly the subgroup used in the quotient.

Source context 15 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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
variable {Q}
variable (Q)
omit [∀ i, IsTopologicalGroup (S.X i)] in
Lean source · statement
theorem injective_quotientInverseLimitComparison :
    Function.Injective Q.quotientInverseLimitComparison
theorem

surjective_quotientInverseLimitComparison

L304 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.surjective_quotientInverseLimitComparison
Documentation

The comparison map is surjective for compact Hausdorff systems over a directed index.

Source context 14 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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
variable {Q}
variable (Q)
Lean source · statement
theorem surjective_quotientInverseLimitComparison
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I)) :
    Function.Surjective Q.quotientInverseLimitComparison
theorem

bijective_quotientInverseLimitComparison

L320 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.bijective_quotientInverseLimitComparison
Documentation

The comparison map is bijective for compact Hausdorff systems over a directed index.

Source context 14 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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
variable {Q}
variable (Q)
Lean source · statement
theorem bijective_quotientInverseLimitComparison
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I)) :
    Function.Bijective Q.quotientInverseLimitComparison
def

quotientInverseLimitContinuousMulEquiv

L331 ↗
ProCGroups.InverseSystems.InverseSystem.CompatibleClosedNormalSubgroups.quotientInverseLimitContinuousMulEquiv
Documentation

The quotient of an inverse limit by a compatible closed normal family is the inverse limit of the stage quotients.

Source context 14 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 : InverseSystem.{u, v} (I := I))
variable [∀ i, Group (S.X i)] [IsGroupSystem S]
variable [∀ i, IsTopologicalGroup (S.X i)]
namespace CompatibleClosedNormalSubgroups
variable {S}
variable (Q : S.CompatibleClosedNormalSubgroups)
variable {Q}
variable (Q)
Lean source · statement
def quotientInverseLimitContinuousMulEquiv
    [∀ i, CompactSpace (S.X i)] [∀ i, T2Space (S.X i)]
    (hdir : Directed (· ≤ ·) (id : I → I)) :
    S.inverseLimit ⧸ Q.inverseLimitKernel ≃ₜ* Q.quotientInverseSystem.inverseLimit

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