Module

Map.lean

Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.Map

6 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / All Finite Functoriality / Map

This module lifts the functorial finite-stage maps to the named all-finite completed carrier and proves their algebraic, topological, and dense-subalgebra characterizations.

Imports1

Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteFunctoriality.StageMap

Imported by4

def

completedGroupAlgebraMap

L35 ↗

CompletedGroupAlgebra.completedGroupAlgebraMap

Documentation

In Lemma 5.3.5(e), map construction, a continuous homomorphism of profinite groups \(\varphi : G \to H\) induces a continuous ring homomorphism \(\widehat{R[G]} \to \widehat{R[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] [TopologicalSpace R] [IsTopologicalRing 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

def completedGroupAlgebraMap
    (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    (φ : G →* H) (hφ : Continuous φ) :
    CompletedGroupAlgebraCarrier R G →+* CompletedGroupAlgebraCarrier R H where
  toFun x :=
    (completedGroupAlgebraCompatibleFamilyEquiv (R := R) (G := H)).symm
      ((completedGroupAlgebraSystem R H).inverseLimitLift
        (fun V x =>
          completedGroupAlgebraFunctorialStageMap
            (G := G) (H := H) (R := R) φ hφ V
            (completedGroupAlgebraProjection R G
              (completedGroupAlgebraComapIndex (G := G) φ hφ V) x))
        (by
          intro V W hVW
          funext x
          have hcomp := congrFun
            (congrArg DFunLike.coe
              (completedGroupAlgebraFunctorialStageMap_transition
                (R := R) (G := G) (H := H) φ hφ hVW))
              (completedGroupAlgebraProjection R G
              (completedGroupAlgebraComapIndex (G := G) φ hφ W) x)
          rw [RingHom.comp_apply, RingHom.comp_apply] at hcomp
          simp only
          rw [← completedGroupAlgebraProjection_compatible
            (R := R) (G := G) x
            (completedGroupAlgebraComapIndex_mono
              (G := G) φ hφ hVW)]
          exact hcomp) x)
  map_zero' := by
    apply completedGroupAlgebra_ext (R := R) (G := H)
    intro V
    exact map_zero (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
      φ hφ V)
  map_one' := by
    apply completedGroupAlgebra_ext (R := R) (G := H)
    intro V
    exact map_one (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
      φ hφ V)
  map_add' x y := by
    apply completedGroupAlgebra_ext (R := R) (G := H)
    intro V
    exact map_add (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
      φ hφ V)
      (completedGroupAlgebraProjection R G
        (completedGroupAlgebraComapIndex (G := G) φ hφ V) x)
      (completedGroupAlgebraProjection R G
        (completedGroupAlgebraComapIndex (G := G) φ hφ V) y)
  map_mul' x y := by
    apply completedGroupAlgebra_ext (R := R) (G := H)
    intro V
    exact map_mul (completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R)
      φ hφ V)
      (completedGroupAlgebraProjection R G
        (completedGroupAlgebraComapIndex (G := G) φ hφ V) x)
      (completedGroupAlgebraProjection R G
        (completedGroupAlgebraComapIndex (G := G) φ hφ V) y)

theorem

completedGroupAlgebraProjection_map

L94 ↗

CompletedGroupAlgebra.completedGroupAlgebraProjection_map

Documentation

Projection of the completed functorial map is computed by the corresponding stage 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] [TopologicalSpace R] [IsTopologicalRing 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 completedGroupAlgebraProjection_map
    (φ : G →* H) (hφ : Continuous φ)
    (V : CompletedGroupAlgebraIndex H) (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraProjection R H V
        (completedGroupAlgebraMap (G := G) (H := H) R φ hφ x) =
      completedGroupAlgebraFunctorialStageMap (G := G) (H := H) (R := R) φ hφ V
        (completedGroupAlgebraProjection R G
          (completedGroupAlgebraComapIndex (G := G) φ hφ V) x)

def

completedGroupAlgebraMapAlgHom

L108 ↗

CompletedGroupAlgebra.completedGroupAlgebraMapAlgHom

Documentation

In Lemma 5.3.5(e), algebra form, a continuous homomorphism of profinite groups induces an \(R\)-algebra homomorphism on completed group algebras.

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] [TopologicalSpace R] [IsTopologicalRing 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

def completedGroupAlgebraMapAlgHom
    (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    (φ : G →* H) (hφ : Continuous φ) :
    CompletedGroupAlgebraCarrier R G →ₐ[R] CompletedGroupAlgebraCarrier R H where
  toRingHom := completedGroupAlgebraMap (G := G) (H := H) R φ hφ
  commutes' := by
    intro r
    apply completedGroupAlgebra_ext (R := R) (G := H)
    intro V
    change 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
    exact completedGroupAlgebraFunctorialStageMap_algebraMap
      (R := R) (G := G) (H := H) φ hφ V r

theorem

completedGroupAlgebraMapAlgHom_apply

L130 ↗

CompletedGroupAlgebra.completedGroupAlgebraMapAlgHom_apply

Documentation

The algebra homomorphism form of the completed functorial map has the same underlying function as the corresponding completed ring homomorphism.

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] [TopologicalSpace R] [IsTopologicalRing 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 completedGroupAlgebraMapAlgHom_apply
    (φ : G →* H) (hφ : Continuous φ)
    (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraMapAlgHom (G := G) (H := H) R φ hφ x =
      completedGroupAlgebraMap (G := G) (H := H) R φ hφ x

theorem

continuous_completedGroupAlgebraMap

L138 ↗

CompletedGroupAlgebra.continuous_completedGroupAlgebraMap

Documentation

The completed group-algebra map induced by a continuous group homomorphism is continuous.

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] [TopologicalSpace R] [IsTopologicalRing 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 continuous_completedGroupAlgebraMap
    (φ : G →* H) (hφ : Continuous φ) :
    Continuous (completedGroupAlgebraMap (G := G) (H := H) R φ hφ)

theorem

completedGroupAlgebraMap_comp_toCompletedGroupAlgebra

L183 ↗

CompletedGroupAlgebra.completedGroupAlgebraMap_comp_toCompletedGroupAlgebra

Documentation

The completed functorial map agrees on the dense abstract group algebra with the ordinary group-algebra map induced by the group homomorphism.

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] [TopologicalSpace R] [IsTopologicalRing 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 completedGroupAlgebraMap_comp_toCompletedGroupAlgebra
    (φ : G →* H) (hφ : Continuous φ) :
    (completedGroupAlgebraMap (G := G) (H := H) R φ hφ).comp
        (toCompletedGroupAlgebraRingHom R G) =
      (toCompletedGroupAlgebraRingHom R H).comp (MonoidAlgebra.mapDomainRingHom R φ)

Module documentation

Completed Group Algebra / All Finite Functoriality / Map

Declarations

completedGroupAlgebraMap

completedGroupAlgebraProjection_map

completedGroupAlgebraMapAlgHom

completedGroupAlgebraMapAlgHom_apply

continuous_completedGroupAlgebraMap

completedGroupAlgebraMap_comp_toCompletedGroupAlgebra