Module

Projections.lean

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Projections

4 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Basic / All Finite / Projections

This module bundles the canonical all-finite stage projections and proves continuity of the coefficient map through the inverse-limit lifting property.

Imports1

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Ring

Imported by2

theorem

continuous_completedGroupAlgebra_algebraMap

L33 ↗

CompletedGroupAlgebra.continuous_completedGroupAlgebra_algebraMap

Documentation

The coefficient-ring map \(R \to \widehat{R[G]}\) is continuous.

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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

theorem continuous_completedGroupAlgebra_algebraMap :
    Continuous (algebraMap R (CompletedGroupAlgebraCarrier R G))

def

completedGroupAlgebraProjectionAlgHom

L54 ↗

CompletedGroupAlgebra.completedGroupAlgebraProjectionAlgHom

Documentation

The canonical projection to a finite stage is bundled as an \(R\)-algebra homomorphism.

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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · full declaration

def completedGroupAlgebraProjectionAlgHom (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraCarrier R G →ₐ[R] CompletedGroupAlgebraStage R G U where
  toRingHom := completedGroupAlgebraProjection R G U
  commutes' := by
    intro r
    rfl

def

completedGroupAlgebraProjectionLinearMap

L64 ↗

CompletedGroupAlgebra.completedGroupAlgebraProjectionLinearMap

Documentation

The canonical projection to a finite stage, viewed as an \(R\)-linear map.

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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · statement

def completedGroupAlgebraProjectionLinearMap (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraCarrier R G →ₗ[R] CompletedGroupAlgebraStage R G U

def

completedGroupAlgebraProjectionContinuousLinearMap

L71 ↗

CompletedGroupAlgebra.completedGroupAlgebraProjectionContinuousLinearMap

Documentation

The finite-stage projection, as a continuous \(R\)-linear map.

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
open ProCGroups.Completion
universe u v
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

Lean source · full declaration

def completedGroupAlgebraProjectionContinuousLinearMap (R : Type u) (G : Type v)
    [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
    letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
      (completedGroupAlgebraSystem R G).topologicalSpace U
    CompletedGroupAlgebraCarrier R G →L[R] CompletedGroupAlgebraStage R G U := by
  letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=
    (completedGroupAlgebraSystem R G).topologicalSpace U
  exact
    { toLinearMap := completedGroupAlgebraProjectionLinearMap R G U
      cont := (completedGroupAlgebraSystem R G).continuous_projection U }

Module documentation

Completed Group Algebra / Basic / All Finite / Projections

Declarations

continuous_completedGroupAlgebra_algebraMap

completedGroupAlgebraProjectionAlgHom

completedGroupAlgebraProjectionLinearMap

completedGroupAlgebraProjectionContinuousLinearMap