Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.UniversalProperty.ProfiniteModule
ProCGroups/CompletedGroupAlgebra/UniversalProperty/ProfiniteModule

ProCGroups.CompletedGroupAlgebra.UniversalProperty.ProfiniteModule

2 Theorems | 1 Definition

Compatible lifts to all open-submodule quotients are assembled by compactness into a continuous linear map to a profinite module. This file proves existence and uniqueness and applies it to the free profinite-module property of completed group algebras.

import
Imported by

Declarations

Definition CompletedGroupAlgebra.completedGroupAlgebraProfiniteModule 
def completedGroupAlgebraProfiniteModule
    (Λ : ProfiniteCommRing.{u}) (P : ProfiniteGrp.{v}) :
    ProfiniteModule Λ.toProfiniteRing := by
  letI : CompactSpace (CompletedGroupAlgebraCarrier Λ P) :=
    completedGroupAlgebra_compactSpace (R := Λ) (G := P)
  letI : T2Space (CompletedGroupAlgebraCarrier Λ P) :=
    completedGroupAlgebra_t2Space (R := Λ) (G := P)
  letI : TotallyDisconnectedSpace (CompletedGroupAlgebraCarrier Λ P) :=
    completedGroupAlgebra_totallyDisconnectedSpace (R := Λ) (G := P)
  letI : Module Λ.toProfiniteRing (CompletedGroupAlgebraCarrier Λ P) :=
    instModuleCoeffCompletedGroupAlgebra (R := Λ) (G := P)
  letI : ContinuousSMul Λ.toProfiniteRing (CompletedGroupAlgebraCarrier Λ P) :=
    instContinuousSMulCompletedGroupAlgebra (R := Λ) (G := P)
  exact
    { toProfinite := Profinite.of (CompletedGroupAlgebraCarrier Λ P)
      addCommGroup := inferInstance
      module := inferInstance
      isTopologicalAddGroup := inferInstance
      continuousSMul := inferInstance }

The completed group algebra as an object in profinite modules over a bundled profinite coefficient ring.

Theorem CompletedGroupAlgebra.completedGroupAlgebraOf_hasFreeLiftTo 
theorem completedGroupAlgebraOf_hasFreeLiftTo
    (Λ : ProfiniteCommRing.{u}) (P : ProfiniteGrp.{v})
    (N : ProfiniteModule.{u, w} Λ.toProfiniteRing) :
    ProfiniteModule.HasFreeLiftTo
      (completedGroupAlgebraProfiniteModule Λ P)
      P.toProfinite (fun g => by
        change CompletedGroupAlgebraCarrier Λ P
        exact completedGroupAlgebraOf Λ P g) N

Cross-universe extension property for the bundled completed group algebra.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraOf_freeProfiniteModule 
theorem completedGroupAlgebraOf_freeProfiniteModule
    (Λ : ProfiniteCommRing.{u}) (P : ProfiniteGrp.{v}) :
    (completedGroupAlgebraProfiniteModule Λ P).IsFreeOn
      P.toProfinite (fun g => by
        change CompletedGroupAlgebraCarrier Λ P
        exact completedGroupAlgebraOf Λ P g)

Ribes--Zalesskii Lemma 5.3.5(d): \(\widehat{R[G]}\) is the free profinite \(R\)-module on the profinite space G, with basis map \(g\mapsto [g]\) inside the completed group algebra.

Show Lean proof