NYLL
Module

Carrier.lean

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Carrier
13 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Basic / All Finite / Carrier

This module defines the all-finite completed group algebra as a named inverse-limit carrier. Its compatible-family realization is available only through the explicit equivalence, coordinate projection, compatibility, and extensionality API below. Ring and module structures are inherited once from the generic inverse-limit construction.

Imports1
Imported by2

Declarations

def

CompletedGroupAlgebraCarrier

L36 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraCarrier
Documentation

The all-finite completed group algebra \(\widehat{R[G]}=\varprojlim_U R[G/U]\), kept opaque from 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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
Lean source · statement
def CompletedGroupAlgebraCarrier (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] : Type (max u v)
instance

instTopologicalSpaceCompletedGroupAlgebraCarrier

L42 ↗
CompletedGroupAlgebra.instTopologicalSpaceCompletedGroupAlgebraCarrier
Documentation

The completed group algebra carries the inverse-limit topology of its finite stages.

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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
Lean source · statement
instance instTopologicalSpaceCompletedGroupAlgebraCarrier :
    TopologicalSpace (CompletedGroupAlgebraCarrier R G)
def

completedGroupAlgebraCompatibleFamilyEquiv

L48 ↗
CompletedGroupAlgebra.completedGroupAlgebraCompatibleFamilyEquiv
Documentation

Explicit exchange between the named completed carrier and the concrete compatible-family realization. Ordinary code should use finite-stage projections instead.

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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
Lean source · statement
def completedGroupAlgebraCompatibleFamilyEquiv
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    CompletedGroupAlgebraCarrier R G ≃
      (completedGroupAlgebraSystem R G).inverseLimit
instance

instRingCompletedGroupAlgebraSystemStage

L55 ↗
CompletedGroupAlgebra.instRingCompletedGroupAlgebraSystemStage
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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
Lean source · statement
instance instRingCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U)
instance

instModuleCompletedGroupAlgebraSystemStage

L61 ↗
CompletedGroupAlgebra.instModuleCompletedGroupAlgebraSystemStage
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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
Lean source · statement
instance instModuleCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U)
instance

instIsRingSystemCompletedGroupAlgebraSystem

L68 ↗
CompletedGroupAlgebra.instIsRingSystemCompletedGroupAlgebraSystem
Documentation

The all-finite tower is a ring-valued inverse system.

Source context 12 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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance
Lean source · full declaration
instance instIsRingSystemCompletedGroupAlgebraSystem :
    IsRingSystem (completedGroupAlgebraSystem R G) where
  map_zero := by
    intro U V hUV
    exact map_zero (completedGroupAlgebraTransition R G hUV)
  map_one := by
    intro U V hUV
    exact map_one (completedGroupAlgebraTransition R G hUV)
  map_add := by
    intro U V hUV x y
    exact map_add (completedGroupAlgebraTransition R G hUV) x y
  map_mul := by
    intro U V hUV x y
    exact map_mul (completedGroupAlgebraTransition R G hUV) x y
instance

instRingCompletedGroupAlgebra

L84 ↗
CompletedGroupAlgebra.instRingCompletedGroupAlgebra
Documentation

The ring structure is inherited once from the generic ring inverse limit.

Source context 12 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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance
Lean source · statement
instance instRingCompletedGroupAlgebra :
    Ring (CompletedGroupAlgebraCarrier R G)
def

completedGroupAlgebraProjection

L90 ↗
CompletedGroupAlgebra.completedGroupAlgebraProjection
Documentation

The canonical finite-stage projection, bundled at its source as a ring homomorphism.

Source context 12 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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance
Lean source · statement
def completedGroupAlgebraProjection
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraStage R G U
theorem

completedGroupAlgebraProjection_compatible

L101 ↗
CompletedGroupAlgebra.completedGroupAlgebraProjection_compatible
Documentation

The canonical projections satisfy the inverse-system compatibility equations.

Source context 12 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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance
Lean source · statement
theorem completedGroupAlgebraProjection_compatible
    (x : CompletedGroupAlgebraCarrier R G)
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    completedGroupAlgebraTransition R G hUV
        (completedGroupAlgebraProjection R G V x) =
      completedGroupAlgebraProjection R G U x
theorem

completedGroupAlgebra_ext

L115 ↗
CompletedGroupAlgebra.completedGroupAlgebra_ext
Documentation

Completed elements are equal when all bundled finite-stage projections agree.

Source context 12 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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance
Lean source · statement
theorem completedGroupAlgebra_ext {x y : CompletedGroupAlgebraCarrier R G}
    (h : ∀ U, completedGroupAlgebraProjection R G U x =
      completedGroupAlgebraProjection R G U y) :
    x = y
theorem

completedGroupAlgebraTransition_smul

L125 ↗
CompletedGroupAlgebra.completedGroupAlgebraTransition_smul
Documentation

Transition maps commute with coefficient scalar multiplication.

Source context 13 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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance
omit [TopologicalSpace R] [IsTopologicalRing R] in
Lean source · statement
theorem completedGroupAlgebraTransition_smul
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V)
    (r : R) (x : CompletedGroupAlgebraStage R G V) :
    completedGroupAlgebraTransition R G hUV (r • x) =
      r • completedGroupAlgebraTransition R G hUV x
instance

instIsModuleSystemCompletedGroupAlgebra

L142 ↗
CompletedGroupAlgebra.instIsModuleSystemCompletedGroupAlgebra
Documentation

The all-finite tower is a module-valued inverse system over its coefficient ring.

Source context 12 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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance
Lean source · full declaration
instance instIsModuleSystemCompletedGroupAlgebra :
    @IsModuleSystem _ _ R _ (completedGroupAlgebraSystem R G)
      (fun U => @Ring.toAddCommGroup _
        (instRingCompletedGroupAlgebraSystemStage (G := G) (R := R) U))
      (fun U => instModuleCompletedGroupAlgebraSystemStage (G := G) (R := R) U) :=
  @IsModuleSystem.mk _ _ R _ (completedGroupAlgebraSystem R G)
    (fun U => @Ring.toAddCommGroup _
      (instRingCompletedGroupAlgebraSystemStage (G := G) (R := R) U))
    (fun U => instModuleCompletedGroupAlgebraSystemStage (G := G) (R := R) U)
    (completedGroupAlgebraTransition_smul (R := R) (G := G))
instance

instModuleCoeffCompletedGroupAlgebra

L154 ↗
CompletedGroupAlgebra.instModuleCoeffCompletedGroupAlgebra
Documentation

The module structure is inherited once from the generic module inverse limit.

Source context 12 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 (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Ring ((completedGroupAlgebraSystem R G).X U) := by
  change Ring (CompletedGroupAlgebraStage R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemStage
    (U : CompletedGroupAlgebraIndex G) :
    Module R ((completedGroupAlgebraSystem R G).X U) := by
  change Module R (CompletedGroupAlgebraStage R G U)
  infer_instance
Lean source · statement
instance instModuleCoeffCompletedGroupAlgebra :
    Module R (CompletedGroupAlgebraCarrier R G)

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