Module

AugmentationIdeal.lean

Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.AugmentationIdeal

14 declarations indexed from sourceView source ↗

Module documentation

The canonical augmentation ideal

This file defines the kernel of the canonical augmentation on the all-finite completed group algebra, packages its short exact sequence, and proves comparison and functoriality formulas for the ideal.

Imports3

Imported by1

Nyll.ProCGroups.CompletedGroupAlgebra.AllFiniteAugmentation.All

def

completedGroupAlgebraCanonicalAugmentationIdeal

L40 ↗

CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdeal

Documentation

The canonical augmentation ideal \(I_G\subseteq \widehat{R[G]}\) is the kernel of the completed augmentation \(\varepsilon:\widehat{R[G]}\to R\).

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 completedGroupAlgebraCanonicalAugmentationIdeal (R : Type u) (G : Type v) [CommRing R]
    [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] : Ideal (CompletedGroupAlgebraCarrier R G)

theorem

mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff

L50 ↗

CompletedGroupAlgebra.mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff

Documentation

An all-finite completed group-algebra element lies in the canonical augmentation ideal iff the canonical augmentation sends it to zero.

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 mem_completedGroupAlgebraCanonicalAugmentationIdeal_iff
    {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    {x : CompletedGroupAlgebraCarrier R G} :
    x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R G ↔
      completedGroupAlgebraCanonicalAugmentation R G x = 0

theorem

completedGroupAlgebraCanonicalAugmentationIdeal_subtype_injective

L59 ↗

CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdeal_subtype_injective

Documentation

The inclusion of the canonical completed augmentation ideal is injective.

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 · full declaration

theorem completedGroupAlgebraCanonicalAugmentationIdeal_subtype_injective :
    Function.Injective
      (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
        (x : CompletedGroupAlgebraCarrier R G)) := by
  intro x y hxy
  exact Subtype.ext hxy

theorem

exact_completedGroupAlgebraCanonicalAugmentationIdeal_subtype

L69 ↗

CompletedGroupAlgebra.exact_completedGroupAlgebraCanonicalAugmentationIdeal_subtype

Documentation

The canonical completed augmentation ideal is exactly the kernel of the 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 · full declaration

theorem exact_completedGroupAlgebraCanonicalAugmentationIdeal_subtype :
    Function.Exact
      (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
        (x : CompletedGroupAlgebraCarrier R G))
      (completedGroupAlgebraCanonicalAugmentation R G) := by
  intro x
  constructor
  · intro hx
    exact ⟨⟨x, hx⟩, rfl⟩
  · rintro ⟨y, rfl⟩
    exact y.2

theorem

completedGroupAlgebraCanonicalAugmentation_shortExact

L86 ↗

CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentation_shortExact

Documentation

The canonical augmentation sequence with augmentation ideal as kernel is short exact: the inclusion is injective, its image is the kernel of augmentation, and the augmentation 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 · full declaration

theorem completedGroupAlgebraCanonicalAugmentation_shortExact :
    Function.Injective
        (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
          (x : CompletedGroupAlgebraCarrier R G)) ∧
      Function.Exact
        (fun x : completedGroupAlgebraCanonicalAugmentationIdeal R G =>
          (x : CompletedGroupAlgebraCarrier R G))
        (completedGroupAlgebraCanonicalAugmentation R G) ∧
      Function.Surjective (completedGroupAlgebraCanonicalAugmentation R G) := by
  exact ⟨completedGroupAlgebraCanonicalAugmentationIdeal_subtype_injective (R := R) (G := G),
    exact_completedGroupAlgebraCanonicalAugmentationIdeal_subtype (R := R) (G := G),
    completedGroupAlgebraCanonicalAugmentation_surjective (R := R) (G := G)⟩

theorem

completedGroupAlgebraCanonicalAugmentationIdeal_comap_fromInClass

L104 ↗

CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdeal_comap_fromInClass

Documentation

The all-finite augmentation ideal pulls back along the from-in-class comparison map to the class-indexed 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 completedGroupAlgebraCanonicalAugmentationIdeal_comap_fromInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Ideal.comap (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)
        (completedGroupAlgebraCanonicalAugmentationIdeal R G) =
      completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C

theorem

completedGroupAlgebraCanonicalAugmentationIdealInClass_map_fromInClass

L122 ↗

CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdealInClass_map_fromInClass

Documentation

The from-in-class comparison map sends the class-indexed augmentation ideal into the all-finite 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 completedGroupAlgebraCanonicalAugmentationIdealInClass_map_fromInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Ideal.map (completedGroupAlgebraFromInClassRingHom (R := R) (G := G) C hForm hG)
        (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ) =
      completedGroupAlgebraCanonicalAugmentationIdeal R G

theorem

completedGroupAlgebraToInClass_mem_canonicalAugmentationIdeal_iff

L141 ↗

CompletedGroupAlgebra.completedGroupAlgebraToInClass_mem_canonicalAugmentationIdeal_iff

Documentation

The all-finite-to-in-class comparison 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 completedGroupAlgebraToInClass_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]
    {x : CompletedGroupAlgebraCarrier R G} :
    completedGroupAlgebraToInClassRingHom (R := R) (G := G) C x ∈
        completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ↔
      x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R G

theorem

completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_toInClass

L167 ↗

CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_toInClass

Documentation

The class-indexed augmentation ideal pulls back along the to-in-class comparison map to the all-finite 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 completedGroupAlgebraCanonicalAugmentationIdealInClass_comap_toInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] :
    Ideal.comap (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )
        (completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C ) =
      completedGroupAlgebraCanonicalAugmentationIdeal R G

theorem

completedGroupAlgebraCanonicalAugmentationIdeal_map_toInClass

L182 ↗

CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdeal_map_toInClass

Documentation

The to-in-class comparison map sends the all-finite augmentation ideal into the class-indexed 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 completedGroupAlgebraCanonicalAugmentationIdeal_map_toInClass
    (C : ProCGroups.FiniteGroupClass.{v})
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G) :
    Ideal.map (completedGroupAlgebraToInClassRingHom (R := R) (G := G) C )
        (completedGroupAlgebraCanonicalAugmentationIdeal R G) =
      completedGroupAlgebraCanonicalAugmentationIdealInClass (R := R) (G := G) C

theorem

completedGroupAlgebraMap_sub_one_of

L201 ↗

CompletedGroupAlgebra.completedGroupAlgebraMap_sub_one_of

Documentation

A functorial all-finite completed group-algebra map sends augmentation generators to their images.

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 completedGroupAlgebraMap_sub_one_of
    (φ : G →* H) (hφ : Continuous φ) (g : G) :
    completedGroupAlgebraMap (G := G) (H := H) R φ hφ
        (completedGroupAlgebraOf R G g - 1) =
      completedGroupAlgebraOf R H (φ g) - 1

theorem

completedGroupAlgebraMap_mem_canonicalAugmentationIdeal_iff

L213 ↗

CompletedGroupAlgebra.completedGroupAlgebraMap_mem_canonicalAugmentationIdeal_iff

Documentation

A functorial all-finite 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 completedGroupAlgebraMap_mem_canonicalAugmentationIdeal_iff
    {R : Type u} {G : Type v} [CommRing R] [TopologicalSpace R]
    [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (φ : G →* H) (hφ : Continuous φ)
    {x : CompletedGroupAlgebraCarrier R G} :
    completedGroupAlgebraMap (G := G) (H := H) R φ hφ x ∈
        completedGroupAlgebraCanonicalAugmentationIdeal R H ↔
      x ∈ completedGroupAlgebraCanonicalAugmentationIdeal R G

theorem

completedGroupAlgebraCanonicalAugmentationIdeal_comap_map

L230 ↗

CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdeal_comap_map

Documentation

Pulling back the target canonical augmentation ideal along a completed group-algebra map gives the source 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 completedGroupAlgebraCanonicalAugmentationIdeal_comap_map
    (φ : G →* H) (hφ : Continuous φ) :
    Ideal.comap (completedGroupAlgebraMap (G := G) (H := H) R φ hφ)
        (completedGroupAlgebraCanonicalAugmentationIdeal R H) =
      completedGroupAlgebraCanonicalAugmentationIdeal R G

theorem

completedGroupAlgebraCanonicalAugmentationIdeal_map_functorial_of_surjective

L243 ↗

CompletedGroupAlgebra.completedGroupAlgebraCanonicalAugmentationIdeal_map_functorial_of_surjective

Documentation

A surjective functorial map sends the canonical completed 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 completedGroupAlgebraCanonicalAugmentationIdeal_map_functorial_of_surjective
    [CompactSpace R] [T2Space R] [TotallyDisconnectedSpace R]
    (φ : G →* H) (hφ : Continuous φ)
    (hφsurj : Function.Surjective φ) :
    Ideal.map (completedGroupAlgebraMap (G := G) (H := H) R φ hφ)
        (completedGroupAlgebraCanonicalAugmentationIdeal R G) =
      completedGroupAlgebraCanonicalAugmentationIdeal R H

Module documentation

The canonical augmentation ideal

Declarations