Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.StageMaps
ProCGroups/CompletedGroupAlgebra/InClassFunctoriality/StageMaps

ProCGroups.CompletedGroupAlgebra.InClassFunctoriality.StageMaps

8 Theorems | 1 Definition

This file constructs the finite-stage group-algebra map induced by a continuous group homomorphism. It proves formulas on basis elements and scalars and compatibility with coefficient change, transitions, and the completed map.

imports
Imported by

Declarations

Definition CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMapInClass 
def completedGroupAlgebraFunctorialStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (R : Type u) [CommRing R] (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndexInClass H C) :
    CompletedGroupAlgebraStageInClass C R G
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V) →+*
      CompletedGroupAlgebraStageInClass C R H V :=
  MonoidAlgebra.mapDomainRingHom R
    (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H) C hHer φ hφ V)

The \(C\)-indexed finite-stage map \(R[G/\varphi^{-1}(V)]\to R[H/V]\) is induced by a continuous homomorphism \(\varphi : G \to H\).

Theorem CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMapInClass_surjective_of_surjective 
omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraFunctorialStageMapInClass_surjective_of_surjective
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ)
    (V : CompletedGroupAlgebraIndexInClass H C) :
    Function.Surjective
      (completedGroupAlgebraFunctorialStageMapInClass
        (G := G) (H := H) C hHer (R := R) φ hφ V)

A surjective group homomorphism induces a surjective finite-stage group-algebra map.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMapInClass_single 
omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraFunctorialStageMapInClass_single
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C)
    (q : CompletedGroupAlgebraQuotientInClass G C
      (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) (r : R) :
    completedGroupAlgebraFunctorialStageMapInClass
        (G := G) (H := H) C hHer (R := R) φ hφ V (MonoidAlgebra.single q r) =
      MonoidAlgebra.single
        (completedGroupAlgebraComapQuotientMapInClass (G := G) (H := H)
          C hHer φ hφ V q) r

The functorial finite-stage map sends singleton coefficients to singleton coefficients.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMapInClass_algebraMap 
omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraFunctorialStageMapInClass_algebraMap
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) (r : R) :
    completedGroupAlgebraFunctorialStageMapInClass
        (G := G) (H := H) C hHer (R := R) φ hφ V
        (algebraMap R
          (CompletedGroupAlgebraStageInClass C R G
            (completedGroupAlgebraComapIndexInClass
              (G := G) (H := H) C hHer φ hφ V)) r) =
      algebraMap R (CompletedGroupAlgebraStageInClass C R H V) r

The functorial finite-stage map preserves coefficient algebra-map elements.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraStageCoeffMapInClass_comp_functorialStageMapInClass 
omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraStageCoeffMapInClass_comp_functorialStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (S : Type w) [CommRing S] (f : R →+* S)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
    (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := H) C S f V).comp
        (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := R) φ hφ V) =
      (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := S) φ hφ V).comp
        (completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f
          (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V))

Functorial finite-stage maps commute with coefficient change.

Show Lean proof
Theorem CompletedGroupAlgebra.continuous_completedGroupAlgebraFunctorialStageMapInClass 
theorem continuous_completedGroupAlgebraFunctorialStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
    letI : TopologicalSpace
        (CompletedGroupAlgebraStageInClass C R G
          (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) :=
      (completedGroupAlgebraSystemInClass C R G).topologicalSpace
        (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)
    letI : TopologicalSpace (CompletedGroupAlgebraStageInClass C R H V) :=
      (completedGroupAlgebraSystemInClass C R H).topologicalSpace V
    Continuous (completedGroupAlgebraFunctorialStageMapInClass
      (G := G) (H := H) C hHer (R := R) φ hφ V)

The functorial finite-stage group-algebra map is continuous for the finite-stage topologies.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMapInClass_transition 
omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraFunctorialStageMapInClass_transition
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ)
    {V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
    (completedGroupAlgebraTransitionInClass C R H hVW).comp
        (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := R) φ hφ W) =
      (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := R) φ hφ V).comp
        (completedGroupAlgebraTransitionInClass C R G
          (completedGroupAlgebraComapIndexInClass_mono
            (G := G) (H := H) C hHer φ hφ hVW))

Functorial finite-stage maps commute with transition maps.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGAStageCoeffMapInClass_comp_transition_comp_functorialStageMapInClass 
omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGAStageCoeffMapInClass_comp_transition_comp_functorialStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (S : Type w) [CommRing S] (f : R →+* S)
    (φ : G →* H) (hφ : Continuous φ)
    {V W : CompletedGroupAlgebraIndexInClass H C} (hVW : V ≤ W) :
    ((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := H) C S f V).comp
        (completedGroupAlgebraTransitionInClass C R H hVW)).comp
        (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := R) φ hφ W) =
      (completedGroupAlgebraFunctorialStageMapInClass
          (G := G) (H := H) C hHer (R := S) φ hφ V).comp
        ((completedGroupAlgebraStageCoeffMapInClass (R := R) (G := G) C S f
          (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)).comp
          (completedGroupAlgebraTransitionInClass C R G
            (completedGroupAlgebraComapIndexInClass_mono
              (G := G) (H := H) C hHer φ hφ hVW)))

Functorial finite-stage maps commute with a group transition followed by coefficient change.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMapInClass_comp_stageMap 
omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraFunctorialStageMapInClass_comp_stageMap
    (C : ProCGroups.FiniteGroupClass.{v}) (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndexInClass H C) :
    (completedGroupAlgebraFunctorialStageMapInClass
        (G := G) (H := H) C hHer (R := R) φ hφ V).comp
        (completedGroupAlgebraStageMapInClass C R G
          (completedGroupAlgebraComapIndexInClass (G := G) (H := H) C hHer φ hφ V)) =
      (completedGroupAlgebraStageMapInClass C R H V).comp
        (MonoidAlgebra.mapDomainRingHom R φ)

The functorial finite-stage map agrees with the stage map after passing to the comap quotient.

Show Lean proof