NYLL
Module

StageMap.lean

Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.StageMap
7 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / All Finite Functoriality / Stage Map

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.

Imports2
Imported by2

Declarations

def

completedGroupAlgebraFunctorialStageMap

L36 ↗
CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMap
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
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
theorem

completedGroupAlgebraFunctorialStageMap_surjective_of_surjective

L45 ↗
CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMap_surjective_of_surjective
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
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)
theorem

completedGroupAlgebraFunctorialStageMap_single

L66 ↗
CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMap_single
Documentation

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.

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
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
theorem

completedGroupAlgebraFunctorialStageMap_algebraMap

L83 ↗
CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMap_algebraMap
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
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
theorem

continuous_completedGroupAlgebraFunctorialStageMap

L100 ↗
CompletedGroupAlgebra.continuous_completedGroupAlgebraFunctorialStageMap
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · full declaration
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) := by
  let : TopologicalSpace
      (CompletedGroupAlgebraStage R G (completedGroupAlgebraComapIndex (G := G) φ hφ V)) :=
    (completedGroupAlgebraSystem R G).topologicalSpace
      (completedGroupAlgebraComapIndex (G := G) φ hφ V)
  let : TopologicalSpace (CompletedGroupAlgebraStage R H V) :=
    (completedGroupAlgebraSystem R H).topologicalSpace V
  exact finiteGroupAlgebra_mapDomainRingHom_continuous R
    (CompletedGroupAlgebraQuotient G (completedGroupAlgebraComapIndex (G := G) φ hφ V))
    (CompletedGroupAlgebraQuotient H V)
    (completedGroupAlgebraComapQuotientMap (G := G) φ hφ V)
theorem

completedGroupAlgebraFunctorialStageMap_transition

L128 ↗
CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMap_transition
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
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))
theorem

completedGroupAlgebraFunctorialStageMap_comp_stageMap

L184 ↗
CompletedGroupAlgebra.completedGroupAlgebraFunctorialStageMap_comp_stageMap
Documentation

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

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
universe u v w
variable (R : Type u) [CommRing R]
variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
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 φ)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.