NYLL
Module

System.lean

Nyll.ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.System
10 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Open Finite Quotient Topology / Open Finite Limit / System

This module defines the two-parameter open-finite quotient system and its named inverse-limit carrier. The compatible-family representation is exposed only by an explicit equivalence and the canonical projection/compatibility/extensionality API.

Imports1
Imported by2

Declarations

def

completedGroupAlgebraOpenFiniteQuotientSystem

L37 ↗
CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientSystem
Documentation

The two-parameter inverse system \(K = (I, U) \mapsto (R/I)[G/U]\) for the kernel-neighborhood topology.

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def completedGroupAlgebraOpenFiniteQuotientSystem
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] :
    ProCGroups.InverseSystems.InverseSystem
      (I := CompletedGroupAlgebraOpenQuotientIndex R G) where
  X := CompletedGroupAlgebraOpenQuotientStage R G
  topologicalSpace := completedGroupAlgebraOpenFiniteQuotientStageTopology R G
  map := fun {K L} hKL => completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
  continuous_map := by
    intro K L hKL
    let : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G K) :=
      completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
    let : TopologicalSpace (CompletedGroupAlgebraOpenQuotientStage R G L) :=
      completedGroupAlgebraOpenFiniteQuotientStageTopology R G L
    have : DiscreteTopology (CompletedGroupAlgebraOpenQuotientStage R G L) :=
      completedGroupAlgebraOpenFiniteQuotientStage_discrete R G L
    exact continuous_of_discreteTopology
  map_id := by
    intro K
    exact congrArg DFunLike.coe
      (completedGroupAlgebraOpenFiniteQuotientTransition_id R G K)
  map_comp := by
    intro K L M hKL hLM
    exact congrArg DFunLike.coe
      (completedGroupAlgebraOpenFiniteQuotientTransition_comp R G hKL hLM)
def

CompletedGroupAlgebraOpenFiniteQuotientLimit

L65 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraOpenFiniteQuotientLimit
Documentation

The two-parameter inverse limit \(\varprojlim_{I,U}(R/I)[G/U]\), kept opaque from its concrete compatible-family realization.

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def CompletedGroupAlgebraOpenFiniteQuotientLimit
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] :
    Type (max u v)
instance

instTopologicalSpaceCompletedGroupAlgebraOpenFiniteQuotientLimit

L72 ↗
CompletedGroupAlgebra.instTopologicalSpaceCompletedGroupAlgebraOpenFiniteQuotientLimit
Documentation

The two-parameter completion carries its inverse-limit topology.

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
instance instTopologicalSpaceCompletedGroupAlgebraOpenFiniteQuotientLimit :
    TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G)
def

completedGroupAlgebraOpenFiniteQuotientCompatibleFamilyEquiv

L79 ↗
CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientCompatibleFamilyEquiv
Documentation

Explicit exchange between the named two-parameter carrier and its compatible-family model.

Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def completedGroupAlgebraOpenFiniteQuotientCompatibleFamilyEquiv :
    CompletedGroupAlgebraOpenFiniteQuotientLimit R G ≃
      (completedGroupAlgebraOpenFiniteQuotientSystem R G).inverseLimit
instance

(anonymous instance)

L84 ↗
Source context 10 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K)
instance

instIsRingSystemCompletedGroupAlgebraOpenFiniteQuotientSystem

L90 ↗
CompletedGroupAlgebra.instIsRingSystemCompletedGroupAlgebraOpenFiniteQuotientSystem
Documentation

The open-finite quotient tower is a ring-valued inverse system.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
  change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
  infer_instance
Lean source · full declaration
instance instIsRingSystemCompletedGroupAlgebraOpenFiniteQuotientSystem :
    IsRingSystem (completedGroupAlgebraOpenFiniteQuotientSystem R G) where
  map_zero := by
    intro K L hKL
    exact map_zero (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL)
  map_one := by
    intro K L hKL
    exact map_one (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL)
  map_add := by
    intro K L hKL x y
    exact map_add (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL) x y
  map_mul := by
    intro K L hKL x y
    exact map_mul (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL) x y
instance

instRingCompletedGroupAlgebraOpenFiniteQuotientLimit

L106 ↗
CompletedGroupAlgebra.instRingCompletedGroupAlgebraOpenFiniteQuotientLimit
Documentation

The two-parameter completion inherits its ring structure from the generic inverse limit.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
  change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
  infer_instance
Lean source · statement
instance instRingCompletedGroupAlgebraOpenFiniteQuotientLimit :
    Ring (CompletedGroupAlgebraOpenFiniteQuotientLimit R G)
def

completedGroupAlgebraOpenFiniteQuotientLimitProjection

L113 ↗
CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitProjection
Documentation

The canonical projection to one quotient \((R/I)[G/U]\), bundled at its source as a ring homomorphism.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
  change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
  infer_instance
Lean source · statement
def completedGroupAlgebraOpenFiniteQuotientLimitProjection
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G]
    (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    CompletedGroupAlgebraOpenFiniteQuotientLimit R G →+*
      CompletedGroupAlgebraOpenQuotientStage R G K
theorem

completedGroupAlgebraOpenFiniteQuotientLimitProjection_compatible

L125 ↗
CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimitProjection_compatible
Documentation

The open-finite quotient projections satisfy the two-parameter transition equations.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
  change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
  infer_instance
Lean source · statement
theorem completedGroupAlgebraOpenFiniteQuotientLimitProjection_compatible
    {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L)
    (x : CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :
    completedGroupAlgebraOpenFiniteQuotientTransition R G hKL
        (completedGroupAlgebraOpenFiniteQuotientLimitProjection R G L x) =
      completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K x
theorem

completedGroupAlgebraOpenFiniteQuotientLimit_ext

L139 ↗
CompletedGroupAlgebra.completedGroupAlgebraOpenFiniteQuotientLimit_ext
Documentation

Two open-finite quotient completed elements are equal when all bundled coordinates agree.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
universe u v
variable (R : Type u) [CommRing R] [TopologicalSpace R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
local instance (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
    Ring ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by
  change Ring (CompletedGroupAlgebraOpenQuotientStage R G K)
  infer_instance
Lean source · statement
theorem completedGroupAlgebraOpenFiniteQuotientLimit_ext
    {x y : CompletedGroupAlgebraOpenFiniteQuotientLimit R G}
    (h : ∀ K, completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K x =
      completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K y) :
    x = y

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