ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Carrier

3 Theorems | 3 Definitions | 5 Instances

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.

import

ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Stage

Imported by

ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Ring

Definition CompletedGroupAlgebra.CompletedGroupAlgebraCarrier

def CompletedGroupAlgebraCarrier (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] : Type (max u v) :=
  (completedGroupAlgebraSystem R G).inverseLimit

The all-finite completed group algebra \(\widehat{R[G]}=\varprojlim_U R[G/U]\), kept opaque from its compatible-family model.

Instance CompletedGroupAlgebra.instTopologicalSpaceCompletedGroupAlgebraCarrier

instance instTopologicalSpaceCompletedGroupAlgebraCarrier :
    TopologicalSpace (CompletedGroupAlgebraCarrier R G) :=
  inferInstanceAs (TopologicalSpace (completedGroupAlgebraSystem R G).inverseLimit)

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

Definition CompletedGroupAlgebra.completedGroupAlgebraCompatibleFamilyEquiv

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 :=
  Equiv.refl _

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

Instance CompletedGroupAlgebra.instIsRingSystemCompletedGroupAlgebraSystem

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

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

Instance CompletedGroupAlgebra.instRingCompletedGroupAlgebra

instance instRingCompletedGroupAlgebra :
    Ring (CompletedGroupAlgebraCarrier R G) := by
  change Ring (completedGroupAlgebraSystem R G).inverseLimit
  infer_instance

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

Definition CompletedGroupAlgebra.completedGroupAlgebraProjection

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 := by
  change (completedGroupAlgebraSystem R G).inverseLimit →+*
    (completedGroupAlgebraSystem R G).X U
  exact projectionRingHom (S := completedGroupAlgebraSystem R G) U

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

Theorem CompletedGroupAlgebra.completedGroupAlgebraProjection_compatible

@[simp]
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

The canonical projections satisfy the inverse-system compatibility equations.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebra_ext

@[ext]
theorem completedGroupAlgebra_ext {x y : CompletedGroupAlgebraCarrier R G}
    (h : ∀ U, completedGroupAlgebraProjection R G U x =
      completedGroupAlgebraProjection R G U y) :
    x = y

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

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraTransition_smul

omit [TopologicalSpace R] [IsTopologicalRing R] in
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

Transition maps commute with coefficient scalar multiplication.

Show Lean proof

Instance CompletedGroupAlgebra.instIsModuleSystemCompletedGroupAlgebra

instance instIsModuleSystemCompletedGroupAlgebra :
    IsModuleSystem R (completedGroupAlgebraSystem R G) where
  map_smul := completedGroupAlgebraTransition_smul (R := R) (G := G)

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

Instance CompletedGroupAlgebra.instModuleCoeffCompletedGroupAlgebra

instance instModuleCoeffCompletedGroupAlgebra :
    Module R (CompletedGroupAlgebraCarrier R G) := by
  change Module R (completedGroupAlgebraSystem R G).inverseLimit
  infer_instance

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

ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Carrier

Declarations