NYLL
Module

Functoriality.lean

Nyll.ProCGroups.CompletedGroupAlgebra.Augmentation.Functoriality
5 declarations indexed from sourceView source ↗

Module documentation

Functoriality of augmentation

Maps of in-class completed group algebras commute with canonical augmentation. This file derives the corresponding comap and image formulas for augmentation ideals, including the surjective case.

Imports1
Imported by3

Declarations

theorem

completedGroupAlgebraCanonicalAugmentationInClass_map

L36 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_map
Documentation

The in-class canonical augmentation is natural under functorial completed 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 completedGroupAlgebraCanonicalAugmentationInClass_map
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) (x : CompletedGroupAlgebraInClass C R G) :
    completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := H) C
        (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x) =
      completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C x
theorem

completedGroupAlgebraCanonicalAugmentationInClass_comp_map

L83 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationInClass_comp_map
Documentation

Composing an in-class completed map with augmentation gives the source 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_map
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) :
    (completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := H) C ).comp
        (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ) =
      completedGroupAlgebraCanonicalAugmentationInClass (R := R) (G := G) C
theorem

completedGroupAlgebraMapInClass_mem_canonicalAugmentationIdeal_iff

L101 ↗
CompletedGroupAlgebra.completedGroupAlgebraMapInClass_mem_canonicalAugmentationIdeal_iff
Documentation

A functorial in-class completed group-algebra map preserves and reflects membership in the canonical augmentation ideal.

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 completedGroupAlgebraMapInClass_mem_canonicalAugmentationIdeal_iff
    {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {C : ProCGroups.FiniteGroupClass.{v}}
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ)
    {x : CompletedGroupAlgebraInClass C R G} :
    completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ x ∈
        completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C ↔
      x ∈ completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C
theorem

completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_map

L118 ↗
CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_map
Documentation

The \(C\)-indexed canonical augmentation ideal is pulled back to itself by functorial 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 completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_map
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) :
    Ideal.comap (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ)
        (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C ) =
      completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C
theorem

completedGACanonicalAugmentationIdealInClass_map_functorial_of_surj

L134 ↗
CompletedGroupAlgebra.completedGACanonicalAugmentationIdealInClass_map_functorial_of_surj
Documentation

A surjective functorial map sends the \(C\)-indexed canonical augmentation ideal onto the target canonical augmentation ideal.

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 completedGACanonicalAugmentationIdealInClass_map_functorial_of_surj
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    (hHer : ProCGroups.FiniteGroupClass.Hereditary C)
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (hH : HasOpenNormalBasisInClass C H)
    (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ) :
    Ideal.map (completedGroupAlgebraMapInClass (G := G) (H := H) C hHer R φ hφ)
        (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ) =
      completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := H) C

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