NYLL
Module

Augmentation.lean

Nyll.ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.Augmentation
17 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — \(\mathbb{Z}_C\) coefficients — augmentation

The principal declarations in this module are:

  • zcCompletedGroupAlgebraTopIndex

The canonical trivial group quotient used to read the completed augmentation.

  • zcCompletedGroupAlgebraAugmentationFamily

The finite coefficient coordinate of the completed augmentation \(\mathbb{Z}_C\llbracket H\rrbracket \to \mathbb{Z}_C\).

  • zcCompletedGroupAlgebraTopIndex_le

The canonical trivial quotient is below every finite quotient index.

  • zcCompletedGroupAlgebraAugmentationFamily_compatible

The finite coefficient coordinates of the completed augmentation are compatible.

Imports4
Imported by4

Declarations

abbrev

zcCompletedGroupAlgebraTopIndex

L44 ↗
FoxDifferential.zcCompletedGroupAlgebraTopIndex
Documentation

The canonical trivial group quotient used to read the completed augmentation.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
abbrev zcCompletedGroupAlgebraTopIndex : CompletedGroupAlgebraIndexInClass H C
theorem

zcCompletedGroupAlgebraTopIndex_le

L49 ↗
FoxDifferential.zcCompletedGroupAlgebraTopIndex_le
Documentation

The canonical trivial quotient is below every finite quotient index.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit [IsTopologicalGroup H] in
Lean source · statement
theorem zcCompletedGroupAlgebraTopIndex_le
    (U : CompletedGroupAlgebraIndexInClass H C) :
    zcCompletedGroupAlgebraTopIndex C H ≤ U
def

zcCompletedGroupAlgebraAugmentationFamily

L59 ↗
FoxDifferential.zcCompletedGroupAlgebraAugmentationFamily
Documentation

The finite coefficient coordinate of the completed augmentation \(\mathbb{Z}_C\llbracket H\rrbracket \to \mathbb{Z}_C\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def zcCompletedGroupAlgebraAugmentationFamily
    (x : ZCCompletedGroupAlgebra C H) (i : ProCIntegerIndex C) :
    ProCIntegerStage C i
theorem

zcCompletedGroupAlgebraAugmentationFamily_compatible

L70 ↗
FoxDifferential.zcCompletedGroupAlgebraAugmentationFamily_compatible
Documentation

The finite coefficient coordinates of the completed augmentation are compatible.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem zcCompletedGroupAlgebraAugmentationFamily_compatible
    (x : ZCCompletedGroupAlgebra C H) {i j : ProCIntegerIndex C} (hij : i ≤ j) :
    proCIntegerTransition (C := C) hij
        (zcCompletedGroupAlgebraAugmentationFamily C H x j) =
      zcCompletedGroupAlgebraAugmentationFamily C H x i
def

zcCompletedGroupAlgebraAugmentation

L109 ↗
FoxDifferential.zcCompletedGroupAlgebraAugmentation
Documentation

The completed augmentation \(\mathbb{Z}_C\llbracket H\rrbracket \to \mathbb{Z}_C\), obtained by augmenting every finite stage \((\mathbb{Z}/n\mathbb{Z})[H/U]\) at the canonical trivial quotient of \(H\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · full declaration
def zcCompletedGroupAlgebraAugmentation :
    ZCCompletedGroupAlgebra C H →+* ZCCoeff C where
  toFun x :=
    Subtype.mk
      (zcCompletedGroupAlgebraAugmentationFamily C H x)
      (by
        intro i j hij
        exact zcCompletedGroupAlgebraAugmentationFamily_compatible C H x hij)
  map_zero' := by
    ext i
    change zcCompletedGroupAlgebraAugmentationFamily C H
        (0 : ZCCompletedGroupAlgebra C H) i = 0
    simp only [zcCompletedGroupAlgebraAugmentationFamily,
        zcCompletedGroupAlgebraProjection_zero, map_zero]
  map_one' := by
    ext i
    change zcCompletedGroupAlgebraAugmentationFamily C H
        (1 : ZCCompletedGroupAlgebra C H) i = 1
    simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_one,
        map_one]
  map_add' x y := by
    ext i
    change zcCompletedGroupAlgebraAugmentationFamily C H (x + y) i =
      zcCompletedGroupAlgebraAugmentationFamily C H x i +
        zcCompletedGroupAlgebraAugmentationFamily C H y i
    simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_add,
        map_add]
  map_mul' x y := by
    ext i
    change zcCompletedGroupAlgebraAugmentationFamily C H (x * y) i =
      zcCompletedGroupAlgebraAugmentationFamily C H x i *
        zcCompletedGroupAlgebraAugmentationFamily C H y i
    simp only [zcCompletedGroupAlgebraAugmentationFamily, zcCompletedGroupAlgebraProjection_mul,
        map_mul]
theorem

proCIntegerProj_zcCompletedGroupAlgebraAugmentation

L146 ↗
FoxDifferential.proCIntegerProj_zcCompletedGroupAlgebraAugmentation
Documentation

Projecting the completed augmentation gives the corresponding finite-stage augmentation.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem proCIntegerProj_zcCompletedGroupAlgebraAugmentation
    (i : ProCIntegerIndex C) (x : ZCCompletedGroupAlgebra C H) :
    proCIntegerProj (C := C) i (zcCompletedGroupAlgebraAugmentation C H x) =
      zcCompletedGroupAlgebraAugmentationFamily C H x i
theorem

proCIntegerProj_zcCompletedGroupAlgebraAugmentation_eq_stage

L156 ↗
FoxDifferential.proCIntegerProj_zcCompletedGroupAlgebraAugmentation_eq_stage
Documentation

The completed augmentation can be read after projecting to any finite group quotient stage, not only the canonical trivial quotient used in its definition.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem proCIntegerProj_zcCompletedGroupAlgebraAugmentation_eq_stage
    (i : ZCCompletedGroupAlgebraIndex C H) (x : ZCCompletedGroupAlgebra C H) :
    proCIntegerProj (C := C) i.1 (zcCompletedGroupAlgebraAugmentation C H x) =
      modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C i.2
        (zcCompletedGroupAlgebraProjection C H i x)
theorem

zcCompletedGroupAlgebraAugmentation_groupLike

L179 ↗
FoxDifferential.zcCompletedGroupAlgebraAugmentation_groupLike
Documentation

The completed augmentation sends every group-like element to \(1\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem zcCompletedGroupAlgebraAugmentation_groupLike (h : H) :
    zcCompletedGroupAlgebraAugmentation C H (zcGroupLike C H h) = 1
theorem

zcCompletedGroupAlgebraAugmentation_boundary

L192 ↗
FoxDifferential.zcCompletedGroupAlgebraAugmentation_boundary
Documentation

The completed Fox boundary has augmentation zero.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem zcCompletedGroupAlgebraAugmentation_boundary
    {G : Type u} [Group G] (ψ : G →* H) (g : G) :
    zcCompletedGroupAlgebraAugmentation C H
        (zcCompletedGroupAlgebraBoundary C ψ g) = 0
def

zcCompletedGroupAlgebraAugmentationIdeal

L204 ↗
FoxDifferential.zcCompletedGroupAlgebraAugmentationIdeal
Documentation

The completed augmentation ideal, defined as the kernel of \(\mathbb{Z}_C\llbracket H\rrbracket \to \mathbb{Z}_C\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
def zcCompletedGroupAlgebraAugmentationIdeal :
    Ideal (ZCCompletedGroupAlgebra C H)
abbrev

ZCCompletedGroupAlgebraAugmentationIdeal

L209 ↗
FoxDifferential.ZCCompletedGroupAlgebraAugmentationIdeal
Documentation

The completed augmentation ideal is bundled as a subtype.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
abbrev ZCCompletedGroupAlgebraAugmentationIdeal : Type u
theorem

mem_zcCompletedGroupAlgebraAugmentationIdeal_iff

L217 ↗
FoxDifferential.mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
Documentation

A completed integer group-algebra element lies in the completed augmentation ideal iff the completed augmentation sends it to zero.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem mem_zcCompletedGroupAlgebraAugmentationIdeal_iff
    {C : ProCGroups.FiniteGroupClass.{u}}
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    {x : ZCCompletedGroupAlgebra C H} :
    x ∈ zcCompletedGroupAlgebraAugmentationIdeal C H ↔
      zcCompletedGroupAlgebraAugmentation C H x = 0
theorem

zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal

L227 ↗
FoxDifferential.zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal
Documentation

The algebraic standard-generator ideal is contained in the completed augmentation ideal.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem zcCompletedGroupAlgebraStandardAugmentationIdeal_le_augmentationIdeal :
    zcCompletedGroupAlgebraStandardAugmentationIdeal C H ≤
      zcCompletedGroupAlgebraAugmentationIdeal C H
theorem

zcCompletedGroupAlgebraBoundary_mem_augmentationIdeal

L238 ↗
FoxDifferential.zcCompletedGroupAlgebraBoundary_mem_augmentationIdeal
Documentation

The completed Fox boundary lies in the completed augmentation ideal.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem zcCompletedGroupAlgebraBoundary_mem_augmentationIdeal
    {G : Type u} [Group G] (ψ : G →* H) (g : G) :
    zcCompletedGroupAlgebraBoundary C ψ g ∈
      zcCompletedGroupAlgebraAugmentationIdeal C H
theorem

exact_zcToCompletedGA_of_surj_of_standardAugmentationIdeal_eq_augmentationIdeal

L249 ↗
FoxDifferential.exact_zcToCompletedGA_of_surj_of_standardAugmentationIdeal_eq_augmentationIdeal
Documentation

If the completed augmentation kernel is the algebraic standard-generator ideal, then a surjective completed Fox boundary gives exactness at \(\mathbb{Z}_C\llbracket H\rrbracket\).

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem exact_zcToCompletedGA_of_surj_of_standardAugmentationIdeal_eq_augmentationIdeal
    {G : Type u} [Group G] (ψ : G →* H) (hψ : Function.Surjective ψ)
    (hstandard :
      zcCompletedGroupAlgebraStandardAugmentationIdeal C H =
        zcCompletedGroupAlgebraAugmentationIdeal C H) :
    Function.Exact
      (zcToCompletedGroupAlgebra C ψ :
        ZCCompletedDifferentialModule C ψ → ZCCompletedGroupAlgebra C H)
      (zcCompletedGroupAlgebraAugmentation C H :
        ZCCompletedGroupAlgebra C H → ZCCoeff C)
theorem

exact_zcToCompletedGA_iff_standardAugmentationIdeal_eq_augmentationIdeal_of_surj

L287 ↗
FoxDifferential.exact_zcToCompletedGA_iff_standardAugmentationIdeal_eq_augmentationIdeal_of_surj
Documentation

For a surjective coefficient group map, exactness of the algebraic completed Fox tail is equivalent to the algebraic standard-generator ideal already being the completed augmentation ideal. This isolates the closed-range obstruction for infinite completed group algebras.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem exact_zcToCompletedGA_iff_standardAugmentationIdeal_eq_augmentationIdeal_of_surj
    {C : ProCGroups.FiniteGroupClass.{u}}
    [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    {G : Type u} [Group G] (ψ : G →* H) (hψ : Function.Surjective ψ) :
    Function.Exact
        (zcToCompletedGroupAlgebra C ψ :
          ZCCompletedDifferentialModule C ψ → ZCCompletedGroupAlgebra C H)
        (zcCompletedGroupAlgebraAugmentation C H :
          ZCCompletedGroupAlgebra C H → ZCCoeff C) ↔
      zcCompletedGroupAlgebraStandardAugmentationIdeal C H =
        zcCompletedGroupAlgebraAugmentationIdeal C H
theorem

zcCompletedGroupAlgebraAugmentation_surjective

L322 ↗
FoxDifferential.zcCompletedGroupAlgebraAugmentation_surjective
Documentation

The completed augmentation \(\mathbb{Z}_C\llbracket H\rrbracket \to \mathbb{Z}_C\) is surjective.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section Augmentation
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
Lean source · statement
theorem zcCompletedGroupAlgebraAugmentation_surjective :
    Function.Surjective (zcCompletedGroupAlgebraAugmentation C H)

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