ProCGroups.CompletedGroupAlgebra.Basic.InClass.LimitAlgebra

2 Theorems | 5 Definitions | 5 Instances

This module gives the \(C\)-indexed completion the same opaque-carrier API as the all-finite completion. Its inverse-limit representation is exchanged explicitly, while projections, compatibility, and extensionality are the ordinary public interface. Algebraic structures are inherited from the generic ring and module inverse limits.

import

ProCGroups.CompletedGroupAlgebra.Basic.InClass.System

Imported by

ProCGroups.CompletedGroupAlgebra.Basic.InClass.Projection

Definition CompletedGroupAlgebra.CompletedGroupAlgebraInClass

def CompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    Type (max u v) :=
  (completedGroupAlgebraSystemInClass C R G).inverseLimit

The \(C\)-indexed completed group algebra, kept opaque from its compatible-family inverse-limit realization.

Instance CompletedGroupAlgebra.instTopologicalSpaceCompletedGroupAlgebraInClass

instance instTopologicalSpaceCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    TopologicalSpace (CompletedGroupAlgebraInClass C R G) :=
  inferInstanceAs
    (TopologicalSpace (completedGroupAlgebraSystemInClass C R G).inverseLimit)

The \(C\)-indexed completion carries its inverse-limit topology.

Definition CompletedGroupAlgebra.completedGroupAlgebraInClassCompatibleFamilyEquiv

def completedGroupAlgebraInClassCompatibleFamilyEquiv
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    CompletedGroupAlgebraInClass C R G ≃
      (completedGroupAlgebraSystemInClass C R G).inverseLimit :=
  Equiv.refl _

Explicit exchange between the named \(C\)-indexed carrier and its concrete compatible-family realization. Ordinary code should use finite-stage projections instead.

Instance CompletedGroupAlgebra.instRingCompletedGroupAlgebraInClass

instance instRingCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    Ring (CompletedGroupAlgebraInClass C R G) :=
  inferInstanceAs (Ring (completedGroupAlgebraSystemInClass C R G).inverseLimit)

The \(C\)-indexed ring structure is inherited from the generic ring inverse limit.

Definition CompletedGroupAlgebra.completedGroupAlgebraProjectionInClass

def completedGroupAlgebraProjectionInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    CompletedGroupAlgebraInClass C R G →+*
      CompletedGroupAlgebraStageInClass C R G U :=
  projectionRingHom (S := completedGroupAlgebraSystemInClass C R G) U

The canonical \(C\)-indexed finite-stage projection, bundled at its source as a ring homomorphism.

Theorem CompletedGroupAlgebra.completedGroupAlgebraProjectionInClass_compatible

theorem completedGroupAlgebraProjectionInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
    (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraTransitionInClass C R G hUV
        (completedGroupAlgebraProjectionInClass C R G V x) =
      completedGroupAlgebraProjectionInClass C R G U x

The \(C\)-indexed bundled projections satisfy the transition compatibility equations.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraInClass_ext

@[ext]
theorem completedGroupAlgebraInClass_ext
    (C : ProCGroups.FiniteGroupClass.{v})
    {x y : CompletedGroupAlgebraInClass C R G}
    (h : ∀ U, completedGroupAlgebraProjectionInClass C R G U x =
      completedGroupAlgebraProjectionInClass C R G U y) :
    x = y

\(C\)-indexed completed elements are equal when all bundled stage projections agree.

Show Lean proof

Instance CompletedGroupAlgebra.instIsModuleSystemCompletedGroupAlgebraSystemInClass

instance instIsModuleSystemCompletedGroupAlgebraSystemInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    IsModuleSystem R (completedGroupAlgebraSystemInClass C R G) where
  map_smul := completedGroupAlgebraTransitionInClass_smul
    (R := R) (G := G) C

The \(C\)-indexed tower is a module-valued inverse system over the coefficient ring.

Instance CompletedGroupAlgebra.instModuleCoeffCompletedGroupAlgebraInClass

instance instModuleCoeffCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    Module R (CompletedGroupAlgebraInClass C R G) :=
  inferInstanceAs
    (Module R (completedGroupAlgebraSystemInClass C R G).inverseLimit)

The \(C\)-indexed module structure is inherited from the generic module inverse limit.

Definition CompletedGroupAlgebra.completedGroupAlgebraCoeffMapInClass

def completedGroupAlgebraCoeffMapInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
    (f : R →+* S) :
    CompletedGroupAlgebraInClass C R G →+*
      CompletedGroupAlgebraInClass C S G where
  toFun x :=
    (completedGroupAlgebraInClassCompatibleFamilyEquiv
      (R := S) (G := G) C).symm
      ((completedGroupAlgebraSystemInClass C S G).inverseLimitLift
        (fun U x =>
          completedGroupAlgebraStageCoeffMapInClass
            (R := R) (G := G) C S f U
            (completedGroupAlgebraProjectionInClass C R G U x))
        (by
          intro U V hUV
          funext x
          have hcompat := congrFun
            (congrArg DFunLike.coe
              (completedGroupAlgebraStageCoeffMapInClass_compatible
                (R := R) (G := G) C S f hUV))
            (completedGroupAlgebraProjectionInClass C R G V x)
          calc
            completedGroupAlgebraTransitionInClass C S G hUV
                (completedGroupAlgebraStageCoeffMapInClass
                  (R := R) (G := G) C S f V
                  (completedGroupAlgebraProjectionInClass C R G V x))
                =
              completedGroupAlgebraStageCoeffMapInClass
                (R := R) (G := G) C S f U
                (completedGroupAlgebraTransitionInClass C R G hUV
                  (completedGroupAlgebraProjectionInClass C R G V x)) :=
                    hcompat.symm
            _ =
              completedGroupAlgebraStageCoeffMapInClass
                (R := R) (G := G) C S f U
                (completedGroupAlgebraProjectionInClass C R G U x) := by
                  rw [completedGroupAlgebraProjectionInClass_compatible]) x)
  map_zero' := by
    apply completedGroupAlgebraInClass_ext (R := S) (G := G) C
    intro U
    exact map_zero
      (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)
  map_one' := by
    apply completedGroupAlgebraInClass_ext (R := S) (G := G) C
    intro U
    exact map_one
      (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)
  map_add' x y := by
    apply completedGroupAlgebraInClass_ext (R := S) (G := G) C
    intro U
    exact map_add
      (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)
      (completedGroupAlgebraProjectionInClass C R G U x)
      (completedGroupAlgebraProjectionInClass C R G U y)
  map_mul' x y := by
    apply completedGroupAlgebraInClass_ext (R := S) (G := G) C
    intro U
    exact map_mul
      (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U)
      (completedGroupAlgebraProjectionInClass C R G U x)
      (completedGroupAlgebraProjectionInClass C R G U y)

Stagewise coefficient change on the \(C\)-indexed completion.

Definition CompletedGroupAlgebra.completedGroupAlgebraAlgebraMapInClass

def completedGroupAlgebraAlgebraMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    R →+* CompletedGroupAlgebraInClass C R G where
  toFun r :=
    (completedGroupAlgebraInClassCompatibleFamilyEquiv
      (R := R) (G := G) C).symm
      ((completedGroupAlgebraSystemInClass C R G).inverseLimitLift
        (fun U r => algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r)
        (by
          intro U V hUV
          funext r
          exact completedGroupAlgebraTransitionInClass_algebraMap
            (R := R) (G := G) C hUV r) r)
  map_zero' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact map_zero (algebraMap R (CompletedGroupAlgebraStageInClass C R G U))
  map_one' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact map_one (algebraMap R (CompletedGroupAlgebraStageInClass C R G U))
  map_add' r s := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact map_add
      (algebraMap R (CompletedGroupAlgebraStageInClass C R G U)) r s
  map_mul' r s := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact map_mul
      (algebraMap R (CompletedGroupAlgebraStageInClass C R G U)) r s

The coefficient-ring map is the inverse-limit lift of the \(C\)-indexed stage algebra maps.

Instance CompletedGroupAlgebra.instAlgebraCompletedGroupAlgebraInClass

instance instAlgebraCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    Algebra R (CompletedGroupAlgebraInClass C R G) where
  algebraMap := completedGroupAlgebraAlgebraMapInClass
    (R := R) (G := G) C
  commutes' := by
    intro r x
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact Algebra.commutes r
      (completedGroupAlgebraProjectionInClass C R G U x)
  smul_def' := by
    intro r x
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    change r • completedGroupAlgebraProjectionInClass C R G U x =
      algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r *
        completedGroupAlgebraProjectionInClass C R G U x
    rw [Algebra.smul_def]

The \(C\)-indexed completed group algebra is an algebra over its coefficient ring.

ProCGroups.CompletedGroupAlgebra.Basic.InClass.LimitAlgebra

Declarations