Module

CompletedLeibniz.lean

Nyll.ProCGroups.ProP.Fox.CompletedLeibniz

3 declarations indexed from sourceView source ↗

Module documentation

Extending the Fox--Leibniz rule to completed group algebras

A continuous linear map out of a completed group algebra is determined by its values on completed group-like elements. Applying this uniqueness principle in each variable extends a crossed-product identity on the underlying group to the right Fox--Leibniz rule on the whole completed group algebra.

Imports2

Mathlib.Topology.Algebra.Algebra
Nyll.ProCGroups.CompletedGroupAlgebra.UniversalProperty.Basic

Imported by2

def

foxMulLeftContinuousLinearMap

L32 ↗

ClassFieldTower.ProP.foxMulLeftContinuousLinearMap

Documentation

Left multiplication in a topological algebra, as a continuous linear map.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u v w

Lean source · full declaration

def foxMulLeftContinuousLinearMap
    {R : Type u} [CommRing R]
    {A : Type w} [Ring A] [TopologicalSpace A] [IsTopologicalRing A]
    [Algebra R A] (a : A) : A →L[R] A where
  toLinearMap := LinearMap.mulLeft R a
  cont := continuous_const.mul continuous_id

def

foxMulRightContinuousLinearMap

L41 ↗

ClassFieldTower.ProP.foxMulRightContinuousLinearMap

Documentation

Right multiplication in a topological algebra, as a continuous linear map.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u v w

Lean source · full declaration

def foxMulRightContinuousLinearMap
    {R : Type u} [CommRing R]
    {A : Type w} [Ring A] [TopologicalSpace A] [IsTopologicalRing A]
    [Algebra R A] (a : A) : A →L[R] A where
  toLinearMap := LinearMap.mulRight R a
  cont := continuous_id.mul continuous_const

theorem

completedGroupAlgebra_rightFoxLeibniz_of_groupLike

L51 ↗

ClassFieldTower.ProP.completedGroupAlgebra_rightFoxLeibniz_of_groupLike

Documentation

A continuous linear extension of a crossed map on completed group-like elements satisfies the right Fox--Leibniz rule on the whole completed group algebra.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace ClassFieldTower.ProP
open CompletedGroupAlgebra
open ProCGroups
noncomputable section
universe u v w

Lean source · statement

theorem completedGroupAlgebra_rightFoxLeibniz_of_groupLike
    (R : ProfiniteCommRing.{u}) (G : ProfiniteGrp.{v})
    {B : Type w} [Ring B] [TopologicalSpace B] [IsTopologicalRing B]
    [Algebra R B] [ContinuousSMul R B] [T2Space B]
    (epsilon : CompletedGroupAlgebraCarrier R G →A[R] R)
    (phi : CompletedGroupAlgebraCarrier R G →A[R] B)
    (D : CompletedGroupAlgebraCarrier R G →L[R] B)
    (hepsilon : ∀ g : G,
      epsilon (completedGroupAlgebraOf R G g) = 1)
    (hcrossed : ∀ g h : G,
      D (completedGroupAlgebraOf R G (g * h)) =
        D (completedGroupAlgebraOf R G g) +
          phi (completedGroupAlgebraOf R G g) *
            D (completedGroupAlgebraOf R G h)) :
    ∀ x y : CompletedGroupAlgebraCarrier R G,
      D (x * y) =
        algebraMap R B (epsilon y) * D x + phi x * D y

Module documentation

Extending the Fox--Leibniz rule to completed group algebras

Declarations

foxMulLeftContinuousLinearMap

foxMulRightContinuousLinearMap

completedGroupAlgebra_rightFoxLeibniz_of_groupLike