ProCGroups.CompletedGroupAlgebra.Basic.InClass.Stage

11 Theorems | 2 Definitions | 1 Abbreviation

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.

import

ProCGroups.CompletedGroupAlgebra.Basic.InClass.Index

Imported by

ProCGroups.CompletedGroupAlgebra.Basic.InClass.System

Abbreviation CompletedGroupAlgebra.CompletedGroupAlgebraStageInClass

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) :=
  MonoidAlgebra R (CompletedGroupAlgebraQuotientInClass G C U)

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

Definition CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMapInClass

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 :=
  MonoidAlgebra.mapRingHom (CompletedGroupAlgebraQuotientInClass G C U) f

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

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMapInClass_single

@[simp]
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)

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

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMapInClass_comp

@[simp]
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

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

Show Lean proof

Theorem CompletedGroupAlgebra.finite_completedGroupAlgebraStageInClass

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

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

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass

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 :=
  MonoidAlgebra.mapDomainRingHom R
    (OpenNormalSubgroupInClass.map
      (C := C) (G := G) (U := OrderDual.ofDual U) (V := OrderDual.ofDual V) hUV)

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

Theorem CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_of

@[simp]
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

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

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_single

@[simp]
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

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.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_id

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

The identity transition map in the \(C\)-indexed tower is the identity ring homomorphism.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_comp

@[simp]
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)

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

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMapInClass_compatible

@[simp]
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)

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

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMapInClass_transition_comp

@[simp 900]
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))

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

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_smul

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

Transition maps commute with scalar multiplication by coefficients.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_algebraMap

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

Transition maps commute with the coefficient algebra maps.

Show Lean proof

ProCGroups.CompletedGroupAlgebra.Basic.InClass.Stage

Declarations