Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.Basic.InClass.Projection
ProCGroups/CompletedGroupAlgebra/Basic/InClass/Projection

ProCGroups.CompletedGroupAlgebra.Basic.InClass.Projection

4 Theorems | 3 Definitions

This module bundles the canonical \(C\)-indexed finite-stage projection as ring, algebra, linear, and continuous linear maps. The underlying projection and compatibility theorem are defined with the opaque carrier in LimitAlgebra.

import
Imported by

Declarations

Theorem CompletedGroupAlgebra.completedGroupAlgebraProjectionInClass_algebraMap 
@[simp]
theorem completedGroupAlgebraProjectionInClass_algebraMap
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) (r : R) :
    completedGroupAlgebraProjectionInClass C R G U
        (completedGroupAlgebraAlgebraMapInClass (R := R) (G := G) C r) =
      algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r

Projection of a coefficient element to a finite stage is the stage algebra map.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraProjectionInClass_coeffMap 
@[simp]
theorem completedGroupAlgebraProjectionInClass_coeffMap
    (C : ProCGroups.FiniteGroupClass.{v})
    (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
    (f : R →+* S) (U : CompletedGroupAlgebraIndexInClass G C)
    (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraProjectionInClass C S G U
        (completedGroupAlgebraCoeffMapInClass (R := R) (G := G) C S f x) =
      completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f U
        (completedGroupAlgebraProjectionInClass C R G U x)

Projection of a coefficient-changed element is coefficient change of the projection.

Show Lean proof
Definition CompletedGroupAlgebra.completedGroupAlgebraProjectionAlgHomInClass 
def completedGroupAlgebraProjectionAlgHomInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    CompletedGroupAlgebraInClass C R G →ₐ[R] CompletedGroupAlgebraStageInClass C R G U where
  toRingHom := completedGroupAlgebraProjectionInClass C R G U
  commutes' := by
    intro r
    rfl

The projection from a \(C\)-indexed completed group algebra to a finite stage is bundled as an algebra homomorphism.

Definition CompletedGroupAlgebra.completedGroupAlgebraProjectionLinearMapInClass 
def completedGroupAlgebraProjectionLinearMapInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    CompletedGroupAlgebraInClass C R G →ₗ[R] CompletedGroupAlgebraStageInClass C R G U :=
  (completedGroupAlgebraProjectionAlgHomInClass C R G U).toLinearMap

The projection from a \(C\)-indexed completed group algebra to a finite stage, viewed as an \(R\)-linear map.

Theorem CompletedGroupAlgebra.completedGroupAlgebraTransitionInClass_comp_projection 
@[simp]
theorem completedGroupAlgebraTransitionInClass_comp_projection
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    (completedGroupAlgebraTransitionInClass C R G hUV).comp
        (completedGroupAlgebraProjectionInClass C R G V) =
      completedGroupAlgebraProjectionInClass C R G U

Composing a stage projection with a transition map gives the coarser stage projection.

Show Lean proof
Theorem CompletedGroupAlgebra.continuous_completedGroupAlgebraProjectionInClass 
theorem continuous_completedGroupAlgebraProjectionInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
      (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
    Continuous (completedGroupAlgebraProjectionInClass C R G U)

Continuity of the projection from the \(C\)-indexed completed group algebra to a stage.

Show Lean proof
Definition CompletedGroupAlgebra.completedGroupAlgebraProjectionContinuousLinearMapInClass 
def completedGroupAlgebraProjectionContinuousLinearMapInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
      (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
    CompletedGroupAlgebraInClass C R G →L[R] CompletedGroupAlgebraStageInClass C R G U := by
  letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R G U) :=
    (completedGroupAlgebraSystemInClass C R G).topologicalSpace U
  exact
    { toLinearMap := completedGroupAlgebraProjectionLinearMapInClass C R G U
      cont := (completedGroupAlgebraSystemInClass C R G).continuous_projection U }

The projection from a \(C\)-indexed completed group algebra to a finite stage is bundled as a continuous \(R\)-linear map.