NYLL
Module

LimitAlgebra.lean

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.InClass.LimitAlgebra
14 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Basic / Within a Class / Limit Algebra

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.

Imports1
Imported by2

Declarations

def

CompletedGroupAlgebraInClass

L35 ↗
CompletedGroupAlgebra.CompletedGroupAlgebraInClass
Documentation

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

Source context 9 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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
Lean source · statement
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)
instance

instTopologicalSpaceCompletedGroupAlgebraInClass

L43 ↗
CompletedGroupAlgebra.instTopologicalSpaceCompletedGroupAlgebraInClass
Documentation

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

Source context 9 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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
Lean source · statement
instance instTopologicalSpaceCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    TopologicalSpace (CompletedGroupAlgebraInClass C R G)
def

completedGroupAlgebraInClassCompatibleFamilyEquiv

L51 ↗
CompletedGroupAlgebra.completedGroupAlgebraInClassCompatibleFamilyEquiv
Documentation

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

Source context 9 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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
Lean source · statement
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
instance

instRingCompletedGroupAlgebraSystemInClassStage

L59 ↗
CompletedGroupAlgebra.instRingCompletedGroupAlgebraSystemInClassStage
Source context 9 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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
Lean source · statement
instance instRingCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U)
instance

instModuleCompletedGroupAlgebraSystemInClassStage

L66 ↗
CompletedGroupAlgebra.instModuleCompletedGroupAlgebraSystemInClassStage
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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
Lean source · statement
instance instModuleCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U)
instance

instRingCompletedGroupAlgebraInClass

L74 ↗
CompletedGroupAlgebra.instRingCompletedGroupAlgebraInClass
Documentation

The \(C\)-indexed ring structure is inherited from the generic ring 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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
Lean source · statement
instance instRingCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    Ring (CompletedGroupAlgebraInClass C R G)
def

completedGroupAlgebraProjectionInClass

L81 ↗
CompletedGroupAlgebra.completedGroupAlgebraProjectionInClass
Documentation

The canonical \(C\)-indexed finite-stage projection, 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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
Lean source · statement
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
theorem

completedGroupAlgebraProjectionInClass_compatible

L91 ↗
CompletedGroupAlgebra.completedGroupAlgebraProjectionInClass_compatible
Documentation

The \(C\)-indexed bundled projections satisfy the transition compatibility 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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
Lean source · statement
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
theorem

completedGroupAlgebraInClass_ext

L104 ↗
CompletedGroupAlgebra.completedGroupAlgebraInClass_ext
Documentation

\(C\)-indexed completed elements are equal when all bundled stage projections 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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
Lean source · statement
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
instance

instIsModuleSystemCompletedGroupAlgebraSystemInClass

L116 ↗
CompletedGroupAlgebra.instIsModuleSystemCompletedGroupAlgebraSystemInClass
Documentation

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

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
Lean source · full declaration
instance instIsModuleSystemCompletedGroupAlgebraSystemInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    @IsModuleSystem _ _ R _ (completedGroupAlgebraSystemInClass C R G)
      (fun U => @Ring.toAddCommGroup _
        (instRingCompletedGroupAlgebraSystemInClassStage
          (G := G) (R := R) C U))
      (fun U => instModuleCompletedGroupAlgebraSystemInClassStage
        (G := G) (R := R) C U) :=
  @IsModuleSystem.mk _ _ R _ (completedGroupAlgebraSystemInClass C R G)
    (fun U => @Ring.toAddCommGroup _
      (instRingCompletedGroupAlgebraSystemInClassStage
        (G := G) (R := R) C U))
    (fun U => instModuleCompletedGroupAlgebraSystemInClassStage
      (G := G) (R := R) C U)
    (completedGroupAlgebraTransitionInClass_smul (R := R) (G := G) C)
instance

instModuleCoeffCompletedGroupAlgebraInClass

L133 ↗
CompletedGroupAlgebra.instModuleCoeffCompletedGroupAlgebraInClass
Documentation

The \(C\)-indexed module structure is inherited from the generic module 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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
Lean source · statement
instance instModuleCoeffCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v}) :
    Module R (CompletedGroupAlgebraInClass C R G)
def

completedGroupAlgebraCoeffMapInClass

L158 ↗
CompletedGroupAlgebra.completedGroupAlgebraCoeffMapInClass
Documentation

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

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
Lean source · full declaration
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)
def

completedGroupAlgebraAlgebraMapInClass

L222 ↗
CompletedGroupAlgebra.completedGroupAlgebraAlgebraMapInClass
Documentation

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

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
Lean source · full declaration
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
instance

instAlgebraCompletedGroupAlgebraInClass

L255 ↗
CompletedGroupAlgebra.instAlgebraCompletedGroupAlgebraInClass
Documentation

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

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
local instance instRingCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Ring ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Ring (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
local instance instModuleCompletedGroupAlgebraSystemInClassStage
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    Module R ((completedGroupAlgebraSystemInClass C R G).X U) := by
  change Module R (CompletedGroupAlgebraStageInClass C R G U)
  infer_instance
Lean source · full declaration
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
    have hproj :
        completedGroupAlgebraProjectionInClass C R G U (r • x) =
          r • completedGroupAlgebraProjectionInClass C R G U x := by
      let _ : Module R
          (completedGroupAlgebraSystemInClass C R G).inverseLimit :=
        instModuleCoeffCompletedGroupAlgebraInClass (G := G) (R := R) C
      change
        (completedGroupAlgebraSystemInClass C R G).projection U
            (r • completedGroupAlgebraInClassCompatibleFamilyEquiv
              (R := R) (G := G) C x) =
          r • (completedGroupAlgebraSystemInClass C R G).projection U
            (completedGroupAlgebraInClassCompatibleFamilyEquiv
              (R := R) (G := G) C x)
      rfl
    calc
      completedGroupAlgebraProjectionInClass C R G U (r • x) =
          r • completedGroupAlgebraProjectionInClass C R G U x := hproj
      _ = algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r *
          completedGroupAlgebraProjectionInClass C R G U x :=
        Algebra.smul_def r (completedGroupAlgebraProjectionInClass C R G U x)
      _ = completedGroupAlgebraProjectionInClass C R G U
          (completedGroupAlgebraAlgebraMapInClass (R := R) (G := G) C r) *
            completedGroupAlgebraProjectionInClass C R G U x := by rfl
      _ = completedGroupAlgebraProjectionInClass C R G U
          (completedGroupAlgebraAlgebraMapInClass (R := R) (G := G) C r * x) :=
        (map_mul (completedGroupAlgebraProjectionInClass C R G U)
          (completedGroupAlgebraAlgebraMapInClass (R := R) (G := G) C r) x).symm

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