Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.UnitRepresentation
ProCGroups/CompletedGroupAlgebra/InClassFunctoriality/UnitRepresentation

ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.UnitRepresentation

5 Theorems

This file studies the continuous group-like unit representation in an in-class completed group algebra. Its image spans densely, and scalar restriction along it equips profinite modules with a continuous group action.

import
Imported by

Declarations

Theorem CompletedGroupAlgebra.completedGroupAlgebraUnitRepresentationInClassConcrete_val 
@[simp]
theorem completedGroupAlgebraUnitRepresentationInClassConcrete_val
    (C : ProCGroups.FiniteGroupClass.{v})
    (g : G) :
    ((completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C R G)
        (toCompletedGroupAlgebraInClassRingHom C R G) g :
        (CompletedGroupAlgebraInClass C R G)ˣ) : CompletedGroupAlgebraInClass C R G) =
      completedGroupAlgebraOfInClass C R G g

The concrete class-indexed unit representation evaluates to the corresponding completed group-like element.

Show Lean proof
Theorem CompletedGroupAlgebra.continuous_completedGroupAlgebraUnitRepresentationInClassConcrete_val 
theorem continuous_completedGroupAlgebraUnitRepresentationInClassConcrete_val
    (C : ProCGroups.FiniteGroupClass.{v}) :
    Continuous fun g : G =>
      ((completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C R G)
        (toCompletedGroupAlgebraInClassRingHom C R G) g :
        (CompletedGroupAlgebraInClass C R G)ˣ) : CompletedGroupAlgebraInClass C R G)

The \(C\)-indexed canonical unit representation is continuous after forgetting to \(\widehat{R[G]}_{C}\).

Show Lean proof
Theorem CompletedGroupAlgebra.toCompletedGroupAlgebraInClassRingHom_mem_span_completedGroupAlgebraOfInClass 
theorem toCompletedGroupAlgebraInClassRingHom_mem_span_completedGroupAlgebraOfInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraInClassRingHom C R G x ∈
      Submodule.span R (Set.range (completedGroupAlgebraOfInClass C R G))

The dense abstract map lands in the span of class-indexed completed group-like elements.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraOfInClass_dense_span 
theorem completedGroupAlgebraOfInClass_dense_span
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    closure (Submodule.span R (Set.range (completedGroupAlgebraOfInClass C R G)) :
      Set (CompletedGroupAlgebraInClass C R G)) = Set.univ

The \(C\)-indexed completed group-like elements topologically generate \(\widehat{R[G]}_{C}\) as an \(R\)-module, for pro-\(C\) groups and formation classes.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraInClass_module_induces_continuous_gmodule 
theorem completedGroupAlgebraInClass_module_induces_continuous_gmodule
    (C : ProCGroups.FiniteGroupClass.{v})
    (A : Type (max u v)) [AddCommGroup A] [TopologicalSpace A]
    [Module (CompletedGroupAlgebraInClass C R G) A]
    [ContinuousSMul (CompletedGroupAlgebraInClass C R G) A] :
    letI : DistribMulAction G A :=
      unitRepresentationDistribMulAction G (CompletedGroupAlgebraInClass C R G) A
        (completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C R G)
            (toCompletedGroupAlgebraInClassRingHom C R G))
    ContinuousSMul G A

A continuous module over the \(C\)-indexed completed group algebra inherits the natural continuous \(G\)-module structure via the group-like units.

Show Lean proof