ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps

27 Theorems | 10 Definitions

This module constructs the canonical dense maps from the abstract group algebra to the \(C\)-indexed and all-finite named completions, together with their bundled ring, algebra, and linear forms and finite-stage characterizations.

import

ProCGroups.CompletedGroupAlgebra.Basic.ClassComparison

Imported by

Definition CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass

def completedGroupAlgebraStageMapInClass
    (C : ProCGroups.FiniteGroupClass.{v}) (R : Type u) (G : Type v) [CommRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (U : CompletedGroupAlgebraIndexInClass G C) :
    MonoidAlgebra R G →+* CompletedGroupAlgebraStageInClass C R G U :=
  MonoidAlgebra.mapDomainRingHom R
    (openNormalSubgroupInClassProj (C := C) (G := G) U)

The quotient map from the abstract group algebra \(R[G]\) to one \(C\)-indexed finite stage.

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_of

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraStageMapInClass_of
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (g : G) :
    completedGroupAlgebraStageMapInClass C R G U (MonoidAlgebra.of R G g) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) 1

At a \(C\)-indexed stage \(U\), the quotient map sends the group-like element of \(g\) to the singleton at the image of \(g\) in \(G/U\), with coefficient \(1\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_single

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraStageMapInClass_single
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (g : G) (r : R) :
    completedGroupAlgebraStageMapInClass C R G U (MonoidAlgebra.single g r) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj (C := C) (G := G) U g) r

At a \(C\)-indexed stage \(U\), the quotient map sends the singleton at \(g\) with coefficient \(r\) to the singleton at the image of \(g\) in \(G/U\), with coefficient \(r\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_smul

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraStageMapInClass_smul
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (r : R) (x : MonoidAlgebra R G) :
    completedGroupAlgebraStageMapInClass C R G U (r • x) =
      r • completedGroupAlgebraStageMapInClass C R G U x

The \(C\)-indexed quotient-stage map preserves scalar multiplication by elements of \(R\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_algebraMap

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraStageMapInClass_algebraMap
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C)
    (r : R) :
    completedGroupAlgebraStageMapInClass C R G U (algebraMap R (MonoidAlgebra R G) r) =
      algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r

The \(C\)-indexed quotient-stage map commutes with the canonical embeddings of scalars from \(R\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_surjective

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraStageMapInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{v}) (U : CompletedGroupAlgebraIndexInClass G C) :
    Function.Surjective (completedGroupAlgebraStageMapInClass C R G U)

The quotient map \(R[G]\to R[G/U]\) is surjective for every \(C\)-indexed stage \(U\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_compatible

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraStageMapInClass_compatible
    (C : ProCGroups.FiniteGroupClass.{v})
    {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
    (completedGroupAlgebraTransitionInClass C R G hUV).comp
        (completedGroupAlgebraStageMapInClass C R G V) =
      completedGroupAlgebraStageMapInClass C R G U

The class-restricted completed group-algebra stage map is compatible with transition maps and coordinate projections for the completed group algebra.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMapInClass_compatibleMaps

theorem completedGroupAlgebraStageMapInClass_compatibleMaps
    (C : ProCGroups.FiniteGroupClass.{v}) :
    (completedGroupAlgebraSystemInClass C R G).CompatibleMaps
      (fun U => completedGroupAlgebraStageMapInClass C R G U)

The \(C\)-indexed finite-stage quotient maps form a compatible family.

Show Lean proof

Definition CompletedGroupAlgebra.toCompletedGroupAlgebraInClass

def toCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (x : MonoidAlgebra R G) : CompletedGroupAlgebraInClass C R G :=
  (completedGroupAlgebraInClassCompatibleFamilyEquiv
    (R := R) (G := G) C).symm
    ((completedGroupAlgebraSystemInClass C R G).inverseLimitLift
      (fun U => completedGroupAlgebraStageMapInClass C R G U)
      (completedGroupAlgebraStageMapInClass_compatibleMaps
        (R := R) (G := G) C) x)

The canonical map \(R[G] \to \widehat{R[G]}_C\), obtained from all \(C\)-indexed quotient maps.

Theorem CompletedGroupAlgebra.completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass

@[simp]
theorem completedGroupAlgebraProjectionInClass_toCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) (x : MonoidAlgebra R G) :
    completedGroupAlgebraProjectionInClass C R G U
        (toCompletedGroupAlgebraInClass C R G x) =
      completedGroupAlgebraStageMapInClass C R G U x

The \(U\)-coordinate of the canonical dense element in the \(C\)-indexed completion is the \(C\)-indexed stage map at \(U\).

Show Lean proof

Theorem CompletedGroupAlgebra.toCompletedGroupAlgebraInClass_smul

@[simp]
theorem toCompletedGroupAlgebraInClass_smul
    (C : ProCGroups.FiniteGroupClass.{v})
    (r : R) (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraInClass C R G (r • x) =
      r • toCompletedGroupAlgebraInClass C R G x

The canonical map from \(R[G]\) into the \(C\)-indexed completed group algebra preserves scalar multiplication by \(R\).

Show Lean proof

Definition CompletedGroupAlgebra.toCompletedGroupAlgebraInClassRingHom

def toCompletedGroupAlgebraInClassRingHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    MonoidAlgebra R G →+* CompletedGroupAlgebraInClass C R G where
  toFun := toCompletedGroupAlgebraInClass C R G
  map_zero' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact map_zero (completedGroupAlgebraStageMapInClass C R G U)
  map_one' := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact map_one (completedGroupAlgebraStageMapInClass C R G U)
  map_add' x y := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact map_add (completedGroupAlgebraStageMapInClass C R G U) x y
  map_mul' x y := by
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    exact map_mul (completedGroupAlgebraStageMapInClass C R G U) x y

The canonical map \(R[G] \to \widehat{R[G]}_C\) is bundled as a ring homomorphism.

Theorem CompletedGroupAlgebra.toCompletedGroupAlgebraInClassRingHom_apply

@[simp]
theorem toCompletedGroupAlgebraInClassRingHom_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraInClassRingHom C R G x =
      toCompletedGroupAlgebraInClass C R G x

The bundled ring homomorphism has the same underlying function as the coordinatewise construction.

Show Lean proof

Definition CompletedGroupAlgebra.toCompletedGroupAlgebraInClassAlgHom

def toCompletedGroupAlgebraInClassAlgHom
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    MonoidAlgebra R G →ₐ[R] CompletedGroupAlgebraInClass C R G where
  toRingHom := toCompletedGroupAlgebraInClassRingHom C R G
  commutes' := by
    intro r
    apply completedGroupAlgebraInClass_ext (R := R) (G := G) C
    intro U
    change completedGroupAlgebraStageMapInClass C R G U
        (algebraMap R (MonoidAlgebra R G) r) =
      algebraMap R (CompletedGroupAlgebraStageInClass C R G U) r
    exact completedGroupAlgebraStageMapInClass_algebraMap (R := R) (G := G) C U r

The canonical map \(R[G] \to \widehat{R[G]}_C\), as an algebra homomorphism.

Theorem CompletedGroupAlgebra.toCompletedGroupAlgebraInClassAlgHom_apply

@[simp]
theorem toCompletedGroupAlgebraInClassAlgHom_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraInClassAlgHom C R G x =
      toCompletedGroupAlgebraInClass C R G x

Evaluating the canonical \(C\)-indexed algebra homomorphism gives the coordinatewise dense map toCompletedGroupAlgebraInClass.

Show Lean proof

Definition CompletedGroupAlgebra.toCompletedGroupAlgebraInClassLinearMap

def toCompletedGroupAlgebraInClassLinearMap
    (C : ProCGroups.FiniteGroupClass.{v})
    (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
    MonoidAlgebra R G →ₗ[R] CompletedGroupAlgebraInClass C R G where
  toFun := toCompletedGroupAlgebraInClass C R G
  map_add' := by
    intro x y
    exact map_add (toCompletedGroupAlgebraInClassRingHom C R G) x y
  map_smul' := toCompletedGroupAlgebraInClass_smul (R := R) (G := G) C

The canonical map \(R[G] \to \widehat{R[G]}_C\), as a linear map.

Theorem CompletedGroupAlgebra.toCompletedGroupAlgebraInClassLinearMap_apply

@[simp]
theorem toCompletedGroupAlgebraInClassLinearMap_apply
    (C : ProCGroups.FiniteGroupClass.{v})
    (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebraInClassLinearMap C R G x =
      toCompletedGroupAlgebraInClass C R G x

The bundled linear map has the same underlying function as the coordinatewise construction.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGAProjectionInClass_comp_toCompletedGAInClass

@[simp]
theorem completedGAProjectionInClass_comp_toCompletedGAInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (U : CompletedGroupAlgebraIndexInClass G C) :
    (completedGroupAlgebraProjectionInClass C R G U).comp
        (toCompletedGroupAlgebraInClassRingHom C R G) =
      completedGroupAlgebraStageMapInClass C R G U

Composing the \(U\)-coordinate projection from the \(C\)-indexed completion with its canonical dense ring homomorphism gives the \(C\)-indexed stage map at \(U\).

Show Lean proof

Theorem CompletedGroupAlgebra.denseRange_toCompletedGroupAlgebraInClass

theorem denseRange_toCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    DenseRange (toCompletedGroupAlgebraInClass C R G)

The abstract group algebra is dense in the \(C\)-indexed completed group algebra when \(G\) is pro-\(C\) and \(C\) is a formation.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraTransition_comp_projection

@[simp]
theorem completedGroupAlgebraTransition_comp_projection
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (completedGroupAlgebraTransition R G hUV).comp
        (completedGroupAlgebraProjection R G V) =
      completedGroupAlgebraProjection R G U

Projecting to a finer stage \(V\) and then applying the transition to \(U\) agrees with projecting directly to \(U\).

Show Lean proof

Definition CompletedGroupAlgebra.completedGroupAlgebraStageMap

def completedGroupAlgebraStageMap (R : Type u) (G : Type v) [CommRing R] [Group G]
    [TopologicalSpace G] [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
    MonoidAlgebra R G →+* CompletedGroupAlgebraStage R G U :=
  MonoidAlgebra.mapDomainRingHom R
    (openNormalSubgroupInClassProj
      (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U)

The quotient map from the abstract group algebra \(R[G]\) to one finite stage \(R[G/U]\).

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMap_of

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraStageMap_of
    (U : CompletedGroupAlgebraIndex G) (g : G) :
    completedGroupAlgebraStageMap R G U (MonoidAlgebra.of R G g) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) 1

At an all-finite stage \(U\), the quotient map sends the group-like element of \(g\) to the singleton at the image of \(g\) in \(G/U\), with coefficient \(1\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMap_single

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraStageMap_single
    (U : CompletedGroupAlgebraIndex G) (g : G) (r : R) :
    completedGroupAlgebraStageMap R G U (MonoidAlgebra.single g r) =
      MonoidAlgebra.single (openNormalSubgroupInClassProj
        (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) r

At an all-finite stage \(U\), the quotient map sends the singleton at \(g\) with coefficient \(r\) to the singleton at the image of \(g\) in \(G/U\), with coefficient \(r\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMap_smul

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraStageMap_smul
    (U : CompletedGroupAlgebraIndex G) (r : R) (x : MonoidAlgebra R G) :
    completedGroupAlgebraStageMap R G U (r • x) =
      r • completedGroupAlgebraStageMap R G U x

The all-finite quotient-stage map preserves scalar multiplication by elements of \(R\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMap_algebraMap

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraStageMap_algebraMap
    (U : CompletedGroupAlgebraIndex G) (r : R) :
    completedGroupAlgebraStageMap R G U (algebraMap R (MonoidAlgebra R G) r) =
      algebraMap R (CompletedGroupAlgebraStage R G U) r

The all-finite quotient-stage map commutes with the canonical embeddings of scalars from \(R\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMap_surjective

omit [TopologicalSpace R] [IsTopologicalRing R] in
theorem completedGroupAlgebraStageMap_surjective (U : CompletedGroupAlgebraIndex G) :
    Function.Surjective (completedGroupAlgebraStageMap R G U)

The quotient map \(R[G]\to R[G/U]\) is surjective for every all-finite stage \(U\).

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMap_compatible

omit [TopologicalSpace R] [IsTopologicalRing R] in
@[simp]
theorem completedGroupAlgebraStageMap_compatible
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
    (completedGroupAlgebraTransition R G hUV).comp (completedGroupAlgebraStageMap R G V) =
      completedGroupAlgebraStageMap R G U

The completed group-algebra stage map is compatible with transition maps and coordinate projections for the completed group algebra.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraStageMap_compatibleMaps

theorem completedGroupAlgebraStageMap_compatibleMaps :
    (completedGroupAlgebraSystem R G).CompatibleMaps
      (fun U => completedGroupAlgebraStageMap R G U)

The finite-stage quotient maps form a compatible family into the completed group algebra system.

Show Lean proof

Definition CompletedGroupAlgebra.toCompletedGroupAlgebra

def toCompletedGroupAlgebra (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (x : MonoidAlgebra R G) : CompletedGroupAlgebraCarrier R G :=
  (completedGroupAlgebraCompatibleFamilyEquiv (R := R) (G := G)).symm
    ((completedGroupAlgebraSystem R G).inverseLimitLift
      (fun U => completedGroupAlgebraStageMap R G U)
      (completedGroupAlgebraStageMap_compatibleMaps (R := R) (G := G)) x)

The canonical map \(R[G] \to \widehat{R[G]}\), obtained from all quotient maps \(R[G]\to R[G/U]\).

Theorem CompletedGroupAlgebra.completedGroupAlgebraProjection_toCompletedGroupAlgebra

@[simp]
theorem completedGroupAlgebraProjection_toCompletedGroupAlgebra
    (U : CompletedGroupAlgebraIndex G) (x : MonoidAlgebra R G) :
    completedGroupAlgebraProjection R G U (toCompletedGroupAlgebra R G x) =
      completedGroupAlgebraStageMap R G U x

The \(U\)-coordinate of the canonical dense element in the all-finite completion is the all-finite stage map at \(U\).

Show Lean proof

Theorem CompletedGroupAlgebra.toCompletedGroupAlgebra_smul

@[simp]
theorem toCompletedGroupAlgebra_smul (r : R) (x : MonoidAlgebra R G) :
    toCompletedGroupAlgebra R G (r • x) =
      r • toCompletedGroupAlgebra R G x

The canonical map from \(R[G]\) into the all-finite completed group algebra preserves scalar multiplication by \(R\).

Show Lean proof

Definition CompletedGroupAlgebra.toCompletedGroupAlgebraRingHom

def toCompletedGroupAlgebraRingHom (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] :
    MonoidAlgebra R G →+* CompletedGroupAlgebraCarrier R G where
  toFun := toCompletedGroupAlgebra R G
  map_zero' := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    exact map_zero (completedGroupAlgebraStageMap R G U)
  map_one' := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    exact map_one (completedGroupAlgebraStageMap R G U)
  map_add' x y := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    exact map_add (completedGroupAlgebraStageMap R G U) x y
  map_mul' x y := by
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    exact map_mul (completedGroupAlgebraStageMap R G U) x y

The canonical map \(R[G] \to \widehat{R[G]}\) is bundled as a ring homomorphism.

Theorem CompletedGroupAlgebra.completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra

@[simp]
theorem completedGroupAlgebraToInClass_comp_toCompletedGroupAlgebra
    (C : ProCGroups.FiniteGroupClass.{v}) :
    (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ).comp
        (toCompletedGroupAlgebraRingHom R G) =
      toCompletedGroupAlgebraInClassRingHom C R G

Restricting the all-finite completion to its \(C\)-indexed coordinates after applying the all-finite dense map agrees with the canonical \(C\)-indexed dense map.

Show Lean proof

Theorem CompletedGroupAlgebra.completedGroupAlgebraFromInClassRingHom_comp_toCompletedGroupAlgebraInClass

@[simp]
theorem completedGroupAlgebraFromInClassRingHom_comp_toCompletedGroupAlgebraInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG).comp
        (toCompletedGroupAlgebraInClassRingHom C R G) =
      toCompletedGroupAlgebraRingHom R G

Under the formation and pro-\(C\) hypotheses, transporting the \(C\)-indexed dense map back to the all-finite completion recovers the all-finite dense map.

Show Lean proof

Definition CompletedGroupAlgebra.toCompletedGroupAlgebraAlgHom

def toCompletedGroupAlgebraAlgHom (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] :
    MonoidAlgebra R G →ₐ[R] CompletedGroupAlgebraCarrier R G where
  toRingHom := toCompletedGroupAlgebraRingHom R G
  commutes' := by
    intro r
    apply completedGroupAlgebra_ext (R := R) (G := G)
    intro U
    change completedGroupAlgebraStageMap R G U (algebraMap R (MonoidAlgebra R G) r) =
      algebraMap R (CompletedGroupAlgebraStage R G U) r
    exact completedGroupAlgebraStageMap_algebraMap (R := R) (G := G) U r

The canonical map \(R[G] \to \widehat{R[G]}\) as an \(R\)-algebra homomorphism.

Definition CompletedGroupAlgebra.toCompletedGroupAlgebraLinearMap

def toCompletedGroupAlgebraLinearMap (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] :
    MonoidAlgebra R G →ₗ[R] CompletedGroupAlgebraCarrier R G where
  toFun := toCompletedGroupAlgebra R G
  map_add' := by
    intro x y
    exact map_add (toCompletedGroupAlgebraRingHom R G) x y
  map_smul' := toCompletedGroupAlgebra_smul (R := R) (G := G)

The canonical map \(R[G] \to \widehat{R[G]}\) as an \(R\)-linear map.

Theorem CompletedGroupAlgebra.completedGroupAlgebraProjection_comp_toCompletedGroupAlgebra

@[simp]
theorem completedGroupAlgebraProjection_comp_toCompletedGroupAlgebra
    (U : CompletedGroupAlgebraIndex G) :
    (completedGroupAlgebraProjection R G U).comp
        (toCompletedGroupAlgebraRingHom R G) =
      completedGroupAlgebraStageMap R G U

Composing the \(U\)-coordinate projection from the all-finite completion with its canonical dense ring homomorphism gives the all-finite stage map at \(U\).

Show Lean proof

ProCGroups.CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps

Declarations