Module

FiniteStage.lean

Nyll.ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.FiniteStage

20 declarations indexed from sourceView source ↗

Module documentation

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

The principal declarations in this module are:

zcCompletedGroupAlgebraStageAugmentationIdeal

The augmentation ideal in one finite stage of \(\mathbb{Z}_C\llbracket H\rrbracket\).

zcCompletedGroupAlgebraStageAugmentationGenerator

The standard generator \([q]-1\) in one finite stage of \(\mathbb{Z}_C\llbracket H\rrbracket\).

mem_zcCompletedGroupAlgebraStageAugmentationIdeal_iff

Membership in a finite-stage completed augmentation ideal is equivalent to vanishing under the corresponding stage augmentation map.

zcCompletedGroupAlgebraStageAugmentationGenerator_mem

A finite-stage standard generator lies in the finite-stage augmentation ideal.

Imports2

Imported by2

def

zcCompletedGroupAlgebraStageAugmentationIdeal

L42 ↗

FoxDifferential.zcCompletedGroupAlgebraStageAugmentationIdeal

Documentation

The augmentation ideal in one finite stage of \(\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.InverseSystems
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section FiniteStageAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def zcCompletedGroupAlgebraStageAugmentationIdeal
    (i : ZCCompletedGroupAlgebraIndex C H) :
    Ideal (ZCCompletedGroupAlgebraStage C H i)

theorem

mem_zcCompletedGroupAlgebraStageAugmentationIdeal_iff

L54 ↗

FoxDifferential.mem_zcCompletedGroupAlgebraStageAugmentationIdeal_iff

Documentation

Membership in a finite-stage completed augmentation ideal is equivalent to vanishing under the corresponding stage augmentation map.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section FiniteStageAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem mem_zcCompletedGroupAlgebraStageAugmentationIdeal_iff
    {C : ProCGroups.FiniteGroupClass.{u}}
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
    {i : ZCCompletedGroupAlgebraIndex C H}
    {x : ZCCompletedGroupAlgebraStage C H i} :
    x ∈ zcCompletedGroupAlgebraStageAugmentationIdeal C H i ↔
      modNCompletedGroupAlgebraStageAugmentationInClass i.1.modulus H C i.2 x = 0

def

zcCompletedGroupAlgebraStageAugmentationGenerator

L67 ↗

FoxDifferential.zcCompletedGroupAlgebraStageAugmentationGenerator

Documentation

The standard generator \([q]-1\) in one finite stage of \(\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.InverseSystems
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section FiniteStageAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def zcCompletedGroupAlgebraStageAugmentationGenerator
    (i : ZCCompletedGroupAlgebraIndex C H)
    (q : CompletedGroupAlgebraQuotientInClass H C i.2) :
    ZCCompletedGroupAlgebraStage C H i

theorem

zcCompletedGroupAlgebraStageAugmentationGenerator_mem

L76 ↗

FoxDifferential.zcCompletedGroupAlgebraStageAugmentationGenerator_mem

Documentation

A finite-stage standard generator lies in the finite-stage augmentation ideal.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section FiniteStageAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcCompletedGroupAlgebraStageAugmentationGenerator_mem
    (i : ZCCompletedGroupAlgebraIndex C H)
    (q : CompletedGroupAlgebraQuotientInClass H C i.2) :
    zcCompletedGroupAlgebraStageAugmentationGenerator C H i q ∈
      zcCompletedGroupAlgebraStageAugmentationIdeal C H i

def

zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype

L87 ↗

FoxDifferential.zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype

Documentation

The standard generators \([q]-1\), viewed inside the finite-stage augmentation ideal.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section FiniteStageAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype
    (i : ZCCompletedGroupAlgebraIndex C H)
    (q : CompletedGroupAlgebraQuotientInClass H C i.2) :
    zcCompletedGroupAlgebraStageAugmentationIdeal C H i

theorem

zcCompletedGroupAlgebraStageAugmentationIdeal_span_standardGenerators_eq_top

L95 ↗

FoxDifferential.zcCompletedGroupAlgebraStageAugmentationIdeal_span_standardGenerators_eq_top

Documentation

In each finite stage, the augmentation ideal is spanned by the standard generators [q]-1.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section FiniteStageAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcCompletedGroupAlgebraStageAugmentationIdeal_span_standardGenerators_eq_top
    (i : ZCCompletedGroupAlgebraIndex C H) :
    Submodule.span (ZCCompletedGroupAlgebraStage C H i)
      (Set.range (zcCompletedGroupAlgebraStageAugmentationGeneratorSubtype C H i)) = ⊤

def

zcCompletedGroupAlgebraStageAugmentationIdealTransition

L121 ↗

FoxDifferential.zcCompletedGroupAlgebraStageAugmentationIdealTransition

Documentation

Transition maps preserve the finite-stage augmentation ideals.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section FiniteStageAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

def zcCompletedGroupAlgebraStageAugmentationIdealTransition
    {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j) :
    zcCompletedGroupAlgebraStageAugmentationIdeal C H j →
      zcCompletedGroupAlgebraStageAugmentationIdeal C H i

theorem

zcCompletedGroupAlgebraStageAugmentationIdealTransition_val

L172 ↗

FoxDifferential.zcCompletedGroupAlgebraStageAugmentationIdealTransition_val

Documentation

The transition map between finite-stage augmentation ideals is evaluated by the corresponding stage transition.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section FiniteStageAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

theorem zcCompletedGroupAlgebraStageAugmentationIdealTransition_val
    {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
    (x : zcCompletedGroupAlgebraStageAugmentationIdeal C H j) :
    ((zcCompletedGroupAlgebraStageAugmentationIdealTransition
        (C := C) (H := H) hij x :
      ZCCompletedGroupAlgebraStage C H i)) =
      zcCompletedGroupAlgebraTransition C H hij x.1

def

zcCompletedGroupAlgebraAugmentationIdealStageSystem

L185 ↗

FoxDifferential.zcCompletedGroupAlgebraAugmentationIdealStageSystem

Documentation

The inverse system of finite-stage augmentation ideals of \(\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.InverseSystems
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section FiniteStageAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · full declaration

def zcCompletedGroupAlgebraAugmentationIdealStageSystem :
    InverseSystem (I := ZCCompletedGroupAlgebraIndex C H) where
  X := fun i => zcCompletedGroupAlgebraStageAugmentationIdeal C H i
  topologicalSpace := fun _ => ⊥
  map := fun {i j} hij =>
    zcCompletedGroupAlgebraStageAugmentationIdealTransition (C := C) (H := H) hij
  continuous_map := by
    intro i j hij
    let : TopologicalSpace (zcCompletedGroupAlgebraStageAugmentationIdeal C H i) := ⊥
    let : TopologicalSpace (zcCompletedGroupAlgebraStageAugmentationIdeal C H j) := ⊥
    let : DiscreteTopology (zcCompletedGroupAlgebraStageAugmentationIdeal C H j) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro i
    funext x
    apply Subtype.ext
    exact congrFun
      (congrArg DFunLike.coe
        (zcCompletedGroupAlgebraTransition_id C H i)) x.1
  map_comp := by
    intro i j k hij hjk
    funext x
    apply Subtype.ext
    exact congrFun
      (congrArg DFunLike.coe
        (zcCompletedGroupAlgebraTransition_comp C H hij hjk)) x.1

abbrev

ZCCompletedGroupAlgebraAugmentationIdealStageFamily

L213 ↗

FoxDifferential.ZCCompletedGroupAlgebraAugmentationIdealStageFamily

Documentation

Compatible inverse-limit families of finite-stage augmentation-ideal elements.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.Completion
open ProCGroups.ProC
universe u
section FiniteStageAugmentationIdeal
variable (C : ProCGroups.FiniteGroupClass.{u})
variable (H : Type u) [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

Lean source · statement

abbrev ZCCompletedGroupAlgebraAugmentationIdealStageFamily : Type u

def

zcCompletedGroupAlgebraAugmentationIdealProjection

L219 ↗

FoxDifferential.zcCompletedGroupAlgebraAugmentationIdealProjection

Documentation

A completed augmentation-ideal element projects to a finite-stage augmentation ideal.

Source context 10 commands

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

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

Lean source · statement

def zcCompletedGroupAlgebraAugmentationIdealProjection
    (i : ZCCompletedGroupAlgebraIndex C H) :
    ZCCompletedGroupAlgebraAugmentationIdeal C H →
      zcCompletedGroupAlgebraStageAugmentationIdeal C H i

theorem

zcCompletedGroupAlgebraAugmentationIdealProjection_val

L237 ↗

FoxDifferential.zcCompletedGroupAlgebraAugmentationIdealProjection_val

Documentation

The value of the augmentation-ideal projection is the value of the corresponding finite-stage projection.

Source context 10 commands

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

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

Lean source · statement

theorem zcCompletedGroupAlgebraAugmentationIdealProjection_val
    (i : ZCCompletedGroupAlgebraIndex C H)
    (x : ZCCompletedGroupAlgebraAugmentationIdeal C H) :
    ((zcCompletedGroupAlgebraAugmentationIdealProjection C H i x :
      ZCCompletedGroupAlgebraStage C H i)) =
      zcCompletedGroupAlgebraProjection C H i x.1

theorem

zcCompletedGroupAlgebraAugmentationIdealProjection_transition

L246 ↗

FoxDifferential.zcCompletedGroupAlgebraAugmentationIdealProjection_transition

Documentation

Finite-stage projections of a completed augmentation-ideal point are compatible.

Source context 10 commands

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

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

Lean source · statement

theorem zcCompletedGroupAlgebraAugmentationIdealProjection_transition
    {i j : ZCCompletedGroupAlgebraIndex C H} (hij : i ≤ j)
    (x : ZCCompletedGroupAlgebraAugmentationIdeal C H) :
    zcCompletedGroupAlgebraStageAugmentationIdealTransition C H hij
        (zcCompletedGroupAlgebraAugmentationIdealProjection C H j x) =
      zcCompletedGroupAlgebraAugmentationIdealProjection C H i x

def

zcCompletedGroupAlgebraAugmentationIdealToStageFamily

L256 ↗

FoxDifferential.zcCompletedGroupAlgebraAugmentationIdealToStageFamily

Documentation

A completed augmentation-ideal point determines its compatible finite-stage family.

Source context 10 commands

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

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

Lean source · statement

def zcCompletedGroupAlgebraAugmentationIdealToStageFamily :
    ZCCompletedGroupAlgebraAugmentationIdeal C H →
      ZCCompletedGroupAlgebraAugmentationIdealStageFamily C H

theorem

zcCompletedGroupAlgebraAugmentationIdealToStageFamily_apply

L269 ↗

FoxDifferential.zcCompletedGroupAlgebraAugmentationIdealToStageFamily_apply

Documentation

The stage family associated to a completed augmentation-ideal element evaluates at i as its augmentation-ideal projection at i.

Source context 10 commands

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

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

Lean source · statement

theorem zcCompletedGroupAlgebraAugmentationIdealToStageFamily_apply
    (x : ZCCompletedGroupAlgebraAugmentationIdeal C H)
    (i : ZCCompletedGroupAlgebraIndex C H) :
    (zcCompletedGroupAlgebraAugmentationIdealToStageFamily C H x).1 i =
      zcCompletedGroupAlgebraAugmentationIdealProjection C H i x

def

zcCompletedGroupAlgebraAugmentationIdealOfStageFamily

L280 ↗

FoxDifferential.zcCompletedGroupAlgebraAugmentationIdealOfStageFamily

Documentation

A compatible family of finite-stage augmentation-ideal points determines a completed augmentation-ideal point.

Source context 10 commands

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

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

Lean source · statement

def zcCompletedGroupAlgebraAugmentationIdealOfStageFamily :
    ZCCompletedGroupAlgebraAugmentationIdealStageFamily C H →
      ZCCompletedGroupAlgebraAugmentationIdeal C H

theorem

zcCompletedGroupAlgebraAugmentationIdealProjection_ofStageFamily

L304 ↗

FoxDifferential.zcCompletedGroupAlgebraAugmentationIdealProjection_ofStageFamily

Documentation

The augmentation-ideal projection of a stage-family element is the corresponding finite-stage coordinate.

Source context 10 commands

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

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

Lean source · statement

theorem zcCompletedGroupAlgebraAugmentationIdealProjection_ofStageFamily
    (x : ZCCompletedGroupAlgebraAugmentationIdealStageFamily C H)
    (i : ZCCompletedGroupAlgebraIndex C H) :
    zcCompletedGroupAlgebraAugmentationIdealProjection C H i
        (zcCompletedGroupAlgebraAugmentationIdealOfStageFamily C H x) =
      x.1 i

theorem

zcCompletedGroupAlgebraAugmentationIdealOfStageFamily_toStageFamily

L318 ↗

FoxDifferential.zcCompletedGroupAlgebraAugmentationIdealOfStageFamily_toStageFamily

Documentation

Converting an augmentation-ideal stage family to its underlying stage family recovers the same compatible coordinates.

Source context 10 commands

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

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

Lean source · statement

theorem zcCompletedGroupAlgebraAugmentationIdealOfStageFamily_toStageFamily
    (x : ZCCompletedGroupAlgebraAugmentationIdeal C H) :
    zcCompletedGroupAlgebraAugmentationIdealOfStageFamily C H
        (zcCompletedGroupAlgebraAugmentationIdealToStageFamily C H x) = x

theorem

zcCompletedGroupAlgebraAugmentationIdealToStageFamily_ofStageFamily

L332 ↗

FoxDifferential.zcCompletedGroupAlgebraAugmentationIdealToStageFamily_ofStageFamily

Documentation

Converting a stage-family element to the completed augmentation ideal and back preserves its finite-stage coordinates.

Source context 10 commands

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

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

Lean source · statement

theorem zcCompletedGroupAlgebraAugmentationIdealToStageFamily_ofStageFamily
    (x : ZCCompletedGroupAlgebraAugmentationIdealStageFamily C H) :
    zcCompletedGroupAlgebraAugmentationIdealToStageFamily C H
        (zcCompletedGroupAlgebraAugmentationIdealOfStageFamily C H x) = x

def

zcCompletedGroupAlgebraAugmentationIdealStageFamilyEquiv

L344 ↗

FoxDifferential.zcCompletedGroupAlgebraAugmentationIdealStageFamilyEquiv

Documentation

The completed augmentation ideal is the inverse limit of its finite-stage augmentation ideals.

Source context 10 commands

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

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

Lean source · full declaration

def zcCompletedGroupAlgebraAugmentationIdealStageFamilyEquiv :
    ZCCompletedGroupAlgebraAugmentationIdeal C H ≃
      ZCCompletedGroupAlgebraAugmentationIdealStageFamily C H where
  toFun := zcCompletedGroupAlgebraAugmentationIdealToStageFamily C H
  invFun := zcCompletedGroupAlgebraAugmentationIdealOfStageFamily C H
  left_inv := zcCompletedGroupAlgebraAugmentationIdealOfStageFamily_toStageFamily C H
  right_inv := zcCompletedGroupAlgebraAugmentationIdealToStageFamily_ofStageFamily C H

Module documentation

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

Declarations