Module

Closure.lean

Nyll.ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Closure

2 declarations indexed from sourceView source ↗

Module documentation

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

The principal declarations in this module are:

zcCompletedGroupAlgebraStageAugmentationIdeal_mem_projection_standard

Every finite-stage augmentation-ideal element is the projection of an element of the algebraic standard augmentation ideal.

closure_zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_augmentationIdeal

The completed augmentation ideal is the closure of the algebraic standard-generator ideal.

Imports3

Imported by3

theorem

zcCompletedGroupAlgebraStageAugmentationIdeal_mem_projection_standard

L46 ↗

FoxDifferential.zcCompletedGroupAlgebraStageAugmentationIdeal_mem_projection_standard

Documentation

Every finite-stage augmentation-ideal element is the projection of an element of the algebraic standard augmentation ideal.

Source context 12 commands

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

namespace FoxDifferential
noncomputable section
open scoped Topology
open ProCGroups.Completion
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
section Closure
variable (C : ProCGroups.FiniteGroupClass.{u})
variable [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C]
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
omit
  [ProCGroups.FiniteGroupClass.ContainsTrivialQuotients C] in

Lean source · statement

theorem zcCompletedGroupAlgebraStageAugmentationIdeal_mem_projection_standard
    (i : ZCCompletedGroupAlgebraIndex C H)
    (x : zcCompletedGroupAlgebraStageAugmentationIdeal C H i) :
    ∃ y ∈ zcCompletedGroupAlgebraStandardAugmentationIdeal C H,
      zcCompletedGroupAlgebraProjection C H i y = (x : ZCCompletedGroupAlgebraStage C H i)

theorem

closure_zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_augmentationIdeal

L90 ↗

FoxDifferential.closure_zcCompletedGroupAlgebraStandardAugmentationIdeal_eq_augmentationIdeal