NYLL
Module

UnitRepresentation.lean

Nyll.ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.UnitRepresentation
5 declarations indexed from sourceView source ↗

Module documentation

Unit representations in the in-class completion

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.

Imports1
Imported by2

Declarations

theorem

completedGroupAlgebraUnitRepresentationInClassConcrete_val

L41 ↗
CompletedGroupAlgebra.completedGroupAlgebraUnitRepresentationInClassConcrete_val
Documentation

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

Source context 12 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
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
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
theorem

continuous_completedGroupAlgebraUnitRepresentationInClassConcrete_val

L54 ↗
CompletedGroupAlgebra.continuous_completedGroupAlgebraUnitRepresentationInClassConcrete_val
Documentation

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

Source context 12 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
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · full declaration
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) := by
  apply (continuous_completedGroupAlgebraOfInClass (R := R) (G := G) C).congr
  intro g
  exact (completedGroupAlgebraUnitRepresentationInClassConcrete_val
    (R := R) (G := G) C g).symm
theorem

toCompletedGroupAlgebraInClassRingHom_mem_span_completedGroupAlgebraOfInClass

L66 ↗
CompletedGroupAlgebra.toCompletedGroupAlgebraInClassRingHom_mem_span_completedGroupAlgebraOfInClass
Documentation

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

Source context 12 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
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
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))
theorem

completedGroupAlgebraOfInClass_dense_span

L101 ↗
CompletedGroupAlgebra.completedGroupAlgebraOfInClass_dense_span
Documentation

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

Source context 12 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
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
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
theorem

completedGroupAlgebraInClass_module_induces_continuous_gmodule

L125 ↗
CompletedGroupAlgebra.completedGroupAlgebraInClass_module_induces_continuous_gmodule
Documentation

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

Source context 12 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
open ProCGroups.Completion
universe u v w
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · full declaration
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 := by
  let : DistribMulAction G A :=
    unitRepresentationDistribMulAction G (CompletedGroupAlgebraInClass C R G) A
      (completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C R G)
        (toCompletedGroupAlgebraInClassRingHom C R G))
  exact unitRepresentation_continuousSMul G (CompletedGroupAlgebraInClass C R G) A
    (completedGroupAlgebraUnitRepresentation R G (CompletedGroupAlgebraInClass C R G)
        (toCompletedGroupAlgebraInClassRingHom C R G))
    (continuous_completedGroupAlgebraUnitRepresentationInClassConcrete_val (R := R) (G := G) C )

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