NYLL
Module

CanonicalAugmentation.lean

Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.CanonicalAugmentation
13 declarations indexed from sourceView source ↗

Module documentation

Completed Group Algebra / All Finite Augmentation / Canonical Augmentation

This module defines the all-finite canonical augmentation as the composition of a terminal finite-stage augmentation with the canonical bundled projection, and proves that it can be computed at every finite stage.

Imports1
Imported by2

Declarations

def

completedGroupAlgebraAugmentationAt

L35 ↗
CompletedGroupAlgebra.completedGroupAlgebraAugmentationAt
Documentation

The completed augmentation evaluated at a finite stage.

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
def completedGroupAlgebraAugmentationAt (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] (U : CompletedGroupAlgebraIndex G) :
    CompletedGroupAlgebraCarrier R G → R
theorem

completedGroupAlgebraAugmentationAt_eq_of_le

L46 ↗
CompletedGroupAlgebra.completedGroupAlgebraAugmentationAt_eq_of_le
Documentation

The coordinate defining the completed augmentation is independent of the chosen sufficiently terminal index.

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 completedGroupAlgebraAugmentationAt_eq_of_le
    {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraAugmentationAt R G U x =
      completedGroupAlgebraAugmentationAt R G V x
def

completedGroupAlgebraCanonicalAugmentation

L69 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation
Documentation

The canonical augmentation \(\varepsilon:\widehat{R[G]}\to R\) is the ring homomorphism obtained by applying the finite-stage augmentation to any sufficiently terminal coordinate.

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
def completedGroupAlgebraCanonicalAugmentation (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] :
    CompletedGroupAlgebraCarrier R G →+* R
theorem

completedGroupAlgebraCanonicalAugmentation_eq_at

L80 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_eq_at
Documentation

The canonical completed augmentation is computed at any finite stage.

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 completedGroupAlgebraCanonicalAugmentation_eq_at
    (U : CompletedGroupAlgebraIndex G) (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraCanonicalAugmentation R G x =
      completedGroupAlgebraAugmentationAt R G U x
theorem

completedGroupAlgebraStageAugmentation_comp_projection

L93 ↗
CompletedGroupAlgebra.completedGroupAlgebraStageAugmentation_comp_projection
Documentation

For every finite quotient stage \(U\), projecting \(\widehat{R[G]}\) to \(R[G/U]\) and then applying the finite-stage augmentation gives the canonical augmentation on \(\widehat{R[G]}\).

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 completedGroupAlgebraStageAugmentation_comp_projection
    (U : CompletedGroupAlgebraIndex G) :
    (completedGroupAlgebraStageAugmentation R G U).comp
        (completedGroupAlgebraProjection R G U) =
      completedGroupAlgebraCanonicalAugmentation R G
theorem

completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra

L107 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra
Documentation

The canonical augmentation extends the abstract group-algebra augmentation through the dense algebraic map.

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 completedGroupAlgebraCanonicalAugmentation_toCompletedGroupAlgebra
    (x : MonoidAlgebra R G) :
    completedGroupAlgebraCanonicalAugmentation R G (toCompletedGroupAlgebra R G x) =
      groupAlgebraAugmentation R G x
theorem

completedGroupAlgebraCanonicalAugmentation_comp_toCompletedGroupAlgebra

L123 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_comp_toCompletedGroupAlgebra
Documentation

Composing the canonical augmentation with the dense map gives the abstract 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 completedGroupAlgebraCanonicalAugmentation_comp_toCompletedGroupAlgebra :
    (completedGroupAlgebraCanonicalAugmentation R G).comp
        (toCompletedGroupAlgebraRingHom R G) =
      groupAlgebraAugmentation R G
theorem

completedGroupAlgebraCanonicalAugmentation_comp_coeffMap

L133 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_comp_coeffMap
Documentation

Canonical augmentation is natural in the coefficient ring.

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 completedGroupAlgebraCanonicalAugmentation_comp_coeffMap
    (S : Type w) [CommRing S] [TopologicalSpace S] [IsTopologicalRing S]
    (f : R →+* S) :
    (completedGroupAlgebraCanonicalAugmentation S G).comp
        (completedGroupAlgebraCoeffMap (R := R) (G := G) S f) =
      f.comp (completedGroupAlgebraCanonicalAugmentation R G)
theorem

completedGroupAlgebraCanonicalAugmentation_map

L156 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_map
Documentation

Canonical augmentation is natural with respect to functorial completed group-algebra maps.

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 completedGroupAlgebraCanonicalAugmentation_map
    (φ : G →* H) (hφ : Continuous φ)
    (x : CompletedGroupAlgebraCarrier R G) :
    completedGroupAlgebraCanonicalAugmentation R H
        (completedGroupAlgebraMap (G := G) (H := H) R φ hφ x) =
      completedGroupAlgebraCanonicalAugmentation R G x
theorem

completedGroupAlgebraCanonicalAugmentation_comp_map

L196 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_comp_map
Documentation

Canonical augmentation after the functorial completed map agrees with canonical 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 completedGroupAlgebraCanonicalAugmentation_comp_map
    (φ : G →* H) (hφ : Continuous φ) :
    (completedGroupAlgebraCanonicalAugmentation R H).comp
        (completedGroupAlgebraMap (G := G) (H := H) R φ hφ) =
      completedGroupAlgebraCanonicalAugmentation R G
theorem

completedGroupAlgebraCanonicalAugmentation_of

L207 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_of
Documentation

The canonical augmentation sends every completed group-like element to one.

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 completedGroupAlgebraCanonicalAugmentation_of (g : G) :
    completedGroupAlgebraCanonicalAugmentation R G (completedGroupAlgebraOf R G g) = 1
theorem

completedGroupAlgebraCanonicalAugmentation_surjective

L214 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_surjective
Documentation

The canonical augmentation \(\varepsilon:\widehat{R[G]}\to R\) is surjective.

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 completedGroupAlgebraCanonicalAugmentation_surjective :
    Function.Surjective (completedGroupAlgebraCanonicalAugmentation R G)
theorem

continuous_completedGroupAlgebraCanonicalAugmentation

L227 ↗
CompletedGroupAlgebra.continuous_completedGroupAlgebraCanonicalAugmentation
Documentation

The canonical augmentation \(\varepsilon:\widehat{R[G]}\to R\) is continuous for the inverse-limit topology on \(\widehat{R[G]}\).

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 continuous_completedGroupAlgebraCanonicalAugmentation :
    Continuous (completedGroupAlgebraCanonicalAugmentation R G)

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