Module

Stage.lean

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.InClass.Stage

14 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / Basic / Within a Class / Stage

This module defines the \(C\)-indexed finite group-algebra stages, their transition and coefficient-change ring homomorphisms, and the compatibility identities used by the inverse system.

Imports1

Nyll.ProCGroups.CompletedGroupAlgebra.Basic.InClass.Index

Imported by2

abbrev

CompletedGroupAlgebraStageInClass

L35 ↗

CompletedGroupAlgebra.CompletedGroupAlgebraStageInClass

Documentation

A \(C\)-indexed quotient \(G/U\) determines the finite-stage group algebra \(R[G/U]\).

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

abbrev CompletedGroupAlgebraStageInClass (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndexInClass G C) :
    Type (max u v)

def

completedGroupAlgebraStageCoeffMapInClass

L45 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMapInClass

Documentation

The coefficient-change map on one \(C\)-indexed completed-group-algebra stage is defined by changing coefficients.

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

def completedGroupAlgebraStageCoeffMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S]
    (f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C) :
    CompletedGroupAlgebraStageInClass C R G U →+*
      CompletedGroupAlgebraStageInClass C S G U

theorem

completedGroupAlgebraStageCoeffMapInClass_single

L57 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMapInClass_single

Documentation

At a \(C\)-indexed stage, coefficient change sends the singleton at \(q\) with coefficient \(r\) to the singleton at \(q\) with coefficient \(f(r)\).

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

theorem completedGroupAlgebraStageCoeffMapInClass_single
    (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S]
    (f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C)
    (q : CompletedGroupAlgebraQuotientInClass G C U) (r : R) :
    completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U
        (MonoidAlgebra.single q r) =
      MonoidAlgebra.single q (f r)

theorem

completedGroupAlgebraStageCoeffMapInClass_comp

L71 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMapInClass_comp

Documentation

At a \(C\)-indexed stage \(U\), changing coefficients first along \(f\) and then along \(g\) equals changing coefficients along \(g\circ f\).

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

theorem completedGroupAlgebraStageCoeffMapInClass_comp
    (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) (T : Type*) [CommRing S]
    [CommRing T] (f : R →+* S) (g : S →+* T)
    (U : CompletedGroupAlgebraIndexInClass G C) :
    (completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp
        (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U) =
      completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C T (g.comp f) U

theorem

finite_completedGroupAlgebraStageInClass

L82 ↗

CompletedGroupAlgebra.finite_completedGroupAlgebraStageInClass

Documentation

A finite coefficient ring gives finite \(C\)-indexed completed-group-algebra stages.

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

theorem finite_completedGroupAlgebraStageInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [Finite R] (U : CompletedGroupAlgebraIndexInClass G C) :
    Finite (CompletedGroupAlgebraStageInClass C R G U)

def

completedGroupAlgebraTransitionInClass

L98 ↗

CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass

Documentation

The transition map \(R[G/V] \to R[G/U]\) in the \(C\)-indexed completed-group-algebra tower.

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

def completedGroupAlgebraTransitionInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    CompletedGroupAlgebraStageInClass C R G V →+*
      CompletedGroupAlgebraStageInClass C R G U

theorem

completedGroupAlgebraTransitionInClass_of

L110 ↗

CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_of

Documentation

The transition map sends group-like basis elements by quotient projection.

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

theorem completedGroupAlgebraTransitionInClass_of
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
    (g : CompletedGroupAlgebraQuotientInClass G C V) :
    completedGroupAlgebraTransitionInClass C R G hUV (MonoidAlgebra.of R _ g) =
      MonoidAlgebra.single ((OpenNormalSubgroupInClass.map
        (C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) g) 1

theorem

completedGroupAlgebraTransitionInClass_single

L136 ↗

CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_single

Documentation

The \(C\)-indexed transition map between finite stages sends a singleton supported at a class of the finer quotient to the singleton supported at its image in the coarser quotient, preserving the coefficient.

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

theorem completedGroupAlgebraTransitionInClass_single
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
    (q : CompletedGroupAlgebraQuotientInClass G C V) (r : R) :
    completedGroupAlgebraTransitionInClass C R G hUV (MonoidAlgebra.single q r) =
      MonoidAlgebra.single
        ((OpenNormalSubgroupInClass.map
          (C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV) q) r

theorem

completedGroupAlgebraTransitionInClass_id

L159 ↗

CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_id

Documentation

The identity transition map in the \(C\)-indexed tower is the identity ring 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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

theorem completedGroupAlgebraTransitionInClass_id
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
    completedGroupAlgebraTransitionInClass C R G (le_rfl : U ≤ U) = RingHom.id _

theorem

completedGroupAlgebraTransitionInClass_comp

L168 ↗

CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_comp

Documentation

Transition maps in the \(C\)-indexed tower compose as expected.

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

theorem completedGroupAlgebraTransitionInClass_comp
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
    (completedGroupAlgebraTransitionInClass C R G hUV).comp
        (completedGroupAlgebraTransitionInClass C R G hVW) =
      completedGroupAlgebraTransitionInClass C R G (hUV.trans hVW)

theorem

completedGroupAlgebraStageCoeffMapInClass_compatible

L191 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMapInClass_compatible

Documentation

\(C\)-indexed stage transitions commute with coefficient change.

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

theorem completedGroupAlgebraStageCoeffMapInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) [CommRing S] (f : R →+* S)
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U).comp
        (completedGroupAlgebraTransitionInClass C R G hUV) =
      (completedGroupAlgebraTransitionInClass C S G hUV).comp
        (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f V)

theorem

completedGroupAlgebraStageCoeffMapInClass_transition_comp

L208 ↗

CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMapInClass_transition_comp

Documentation

Two coefficient changes and two \(C\)-indexed group-quotient transitions compose as the combined change and combined transition.

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

theorem completedGroupAlgebraStageCoeffMapInClass_transition_comp
    (C : ProCGroups.FiniteGroupClass.{v}) (S : Type w) (T : Type*) [CommRing S]
    [CommRing T] (f : R →+* S) (g : S →+* T)
    {U V W : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (hVW : V ≤ W) :
    ((completedGroupAlgebraStageCoeffMapInClass (R := S) (G := G) C T g U).comp
        (completedGroupAlgebraTransitionInClass C S G hUV)).comp
        ((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f V).comp
          (completedGroupAlgebraTransitionInClass C R G hVW)) =
      (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C T (g.comp f) U).comp
        (completedGroupAlgebraTransitionInClass C R G (hUV.trans hVW))

theorem

completedGroupAlgebraTransitionInClass_smul

L257 ↗

CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_smul

Documentation

Transition maps commute with scalar multiplication by coefficients.

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

theorem completedGroupAlgebraTransitionInClass_smul
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V)
    (r : R) (x : CompletedGroupAlgebraStageInClass C R G V) :
    completedGroupAlgebraTransitionInClass C R G hUV (r • x) =
      r • completedGroupAlgebraTransitionInClass C R G hUV x

theorem

completedGroupAlgebraTransitionInClass_algebraMap

L275 ↗

CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_algebraMap

Documentation

Transition maps commute with the coefficient algebra maps.

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
universe u v w
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable (R : Type u) [CommRing R]
section InClass

Lean source · statement

theorem completedGroupAlgebraTransitionInClass_algebraMap
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) (r : R) :
    completedGroupAlgebraTransitionInClass C R G hUV
        (algebraMap R (CompletedGroupAlgebraStageInClass C R G V) r) =
      algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r

Module documentation

Completed Group Algebra / Basic / Within a Class / Stage

Declarations