Module

InClassComparison.lean

Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.InClassComparison

2 declarations indexed from sourceView source ↗

Module documentation

Comparing all-finite and in-class augmentations

The canonical comparison maps between the all-finite and in-class completions commute with their augmentations. This file records both directions of that compatibility.

Imports2

Imported by3

theorem

completedGroupAlgebraCanonicalAugmentationInClass_comp_toInClass

L39 ↗

CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_comp_toInClass

Documentation

Composing the class-indexed canonical augmentation with the comparison map gives the all-finite augmentation.

Source context 11 commands

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

open scoped Topology
namespace CompletedGroupAlgebra
noncomputable section
open ProCGroups
open ProCGroups.ProC
open ProCGroups.InverseSystems
open ProCGroups.Completion
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 completedGroupAlgebraCanonicalAugmentationInClass_comp_toInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C ).comp
        (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C ) =
      completedGroupAlgebraCanonicalAugmentation R G

theorem

completedGroupAlgebraCanonicalAugmentation_fromInClass

L74 ↗

CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_fromInClass