Yamaguchi Lean 4 Library
ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.StageMap
ProCGroups/CompletedGroupAlgebra/AllFiniteFunctoriality/StageMap

ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.StageMap

6 Theorems | 1 Definition

This module lifts the quotient homomorphism from Comap to finite group algebras and proves its continuity, transition compatibility, and compatibility with the canonical dense stage maps.

imports
Imported by

Declarations

Definition CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMap 
def completedGroupAlgebraFunctorialStageMap
    (R : Type u) [CommRing R]
    (φ : G →* H) (hφ : Continuous φ) (V : CompletedGroupAlgebraIndex H) :
    CompletedGroupAlgebraStage R G (completedGroupAlgebraComapIndex (G := G) φ hφ V) →+*
      CompletedGroupAlgebraStage R H V :=
  MonoidAlgebra.mapDomainRingHom R
    (completedGroupAlgebraComapQuotientMap (G := G) φ hφ V)

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

Theorem CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMap_surjective_of_surjective 
theorem completedGroupAlgebraFunctorialStageMap_surjective_of_surjective
    (φ : G →* H) (hφ : Continuous φ)
    (hφsurj : Function.Surjective φ) (V : CompletedGroupAlgebraIndex H) :
    Function.Surjective
      (completedGroupAlgebraFunctorialStageMap
        (G := G) (H := H) (R := R) φ hφ V)

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

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMap_single 
@[simp]
theorem completedGroupAlgebraFunctorialStageMap_single
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H)
    (q : CompletedGroupAlgebraQuotient G
      (completedGroupAlgebraComapIndex (G := G) φ hφ V)) (r : R) :
    completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ V
        (MonoidAlgebra.single q r) =
      MonoidAlgebra.single (completedGroupAlgebraComapQuotientMap (G := G) φ hφ V q) r

The finite-stage functorial map induced by \(\varphi : G \to H\) carries a singleton basis function on \(G/\varphi^{-1}(V)\) to the singleton basis function on \(H/V\) supported at the induced image, with unchanged coefficient.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMap_algebraMap 
theorem completedGroupAlgebraFunctorialStageMap_algebraMap
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) (r : R) :
    completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ V
        (algebraMap R
          (CompletedGroupAlgebraStage R G
            (completedGroupAlgebraComapIndex (G := G) φ hφ V)) r) =
      algebraMap R (CompletedGroupAlgebraStage R H V) r

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

Show Lean proof
Theorem CompletedGroupAlgebra.continuous_completedGroupAlgebraFunctorialStageMap 
theorem continuous_completedGroupAlgebraFunctorialStageMap
    [TopologicalSpace R] [IsTopologicalRing R]
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) :
    letI : TopologicalSpace
        (CompletedGroupAlgebraStage R G (completedGroupAlgebraComapIndex (G := G) φ hφ V)) :=
      (completedGroupAlgebraSystem R G).topologicalSpace
        (completedGroupAlgebraComapIndex (G := G) φ hφ V)
    letI : TopologicalSpace (CompletedGroupAlgebraStage R H V) :=
      (completedGroupAlgebraSystem R H).topologicalSpace V
    Continuous (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
      φ hφ V)

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

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMap_transition 
@[simp]
theorem completedGroupAlgebraFunctorialStageMap_transition
    (φ : G →* H) (hφ : Continuous φ)
    {V W : CompletedGroupAlgebraIndex H} (hVW : V ≤ W) :
    (completedGroupAlgebraTransition R H hVW).comp
        (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ W) =
      (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ V).comp
        (completedGroupAlgebraTransition R G
          (completedGroupAlgebraComapIndex_mono (G := G) φ hφ hVW))

Functorial finite-stage maps commute with the transition maps attached to refinements of finite quotients.

Show Lean proof
Theorem CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMap_comp_stageMap 
@[simp]
theorem completedGroupAlgebraFunctorialStageMap_comp_stageMap
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) :
    (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ V).comp
        (completedGroupAlgebraStageMap R G
          (completedGroupAlgebraComapIndex (G := G) φ hφ V)) =
      (completedGroupAlgebraStageMap R H V).comp
        (MonoidAlgebra.mapDomainRingHom R φ)

The finite-stage functorial map agrees with the dense stage map after applying \(\varphi\).

Show Lean proof