NYLL
Module

Stage.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Stage
12 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — coefficient rings — prime-power augmentation ideal — stage

The principal declarations in this module are:

  • primePowerCompletedGroupAlgebraStageAugmentationIdeal

The augmentation ideal on one prime-power finite stage.

  • primePowerCompletedGroupAlgebraAugmentationKernel

The kernel of the canonical prime-power augmentation.

  • mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff

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

  • mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff

Membership in the relevant augmentation kernel or augmentation ideal is equivalent to the corresponding vanishing condition.

Imports1
Imported by2

Declarations

def

primePowerCompletedGroupAlgebraStageAugmentationIdeal

L39 ↗
FoxDifferential.primePowerCompletedGroupAlgebraStageAugmentationIdeal
Documentation

The augmentation ideal on one prime-power finite stage.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def primePowerCompletedGroupAlgebraStageAugmentationIdeal
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    Ideal (PrimePowerCompletedGroupAlgebraStage ℓ G i)
instance

instFinitePrimePowerCompletedGroupAlgebraStageAugmentationIdeal

L46 ↗
FoxDifferential.instFinitePrimePowerCompletedGroupAlgebraStageAugmentationIdeal
Documentation

The prime-power completed group-algebra stage augmentation ideal is finite.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
instance instFinitePrimePowerCompletedGroupAlgebraStageAugmentationIdeal
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    Finite ↥(primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i)
def

primePowerCompletedGroupAlgebraAugmentationKernel

L57 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationKernel
Documentation

The kernel of the canonical prime-power augmentation.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def primePowerCompletedGroupAlgebraAugmentationKernel :
    Set (PrimePowerCompletedGroupAlgebra ℓ G)
abbrev

PrimePowerCompletedGroupAlgebraAugmentationKernel

L63 ↗
FoxDifferential.PrimePowerCompletedGroupAlgebraAugmentationKernel
Documentation

The kernel of the canonical prime-power augmentation is viewed as a subtype.

Source context 6 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
abbrev PrimePowerCompletedGroupAlgebraAugmentationKernel
theorem

mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff

L74 ↗
FoxDifferential.mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff
Documentation

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

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
Lean source · statement
theorem mem_primePowerCompletedGroupAlgebraStageAugmentationIdeal_iff
    {i : PrimePowerCompletedGroupAlgebraIndex G}
    {x : PrimePowerCompletedGroupAlgebraStage ℓ G i} :
    x ∈ primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i ↔
      modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2 x = 0
theorem

mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff

L88 ↗
FoxDifferential.mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff
Documentation

Membership in the relevant augmentation kernel or augmentation ideal is equivalent to the corresponding vanishing condition.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff
    {x : PrimePowerCompletedGroupAlgebra ℓ G} :
    x ∈ primePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) ↔
      primePowerCompletedGroupAlgebraAugmentation (ℓ := ℓ) (G := G) x =
        (Zero.zero : PrimePowerCompletedCoeff ℓ G)
theorem

mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff_forall

L101 ↗
FoxDifferential.mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff_forall
Documentation

Membership in the prime-power augmentation kernel is equivalent to vanishing after every finite-stage augmentation.

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem mem_primePowerCompletedGroupAlgebraAugmentationKernel_iff_forall
    {x : PrimePowerCompletedGroupAlgebra ℓ G} :
    x ∈ primePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) ↔
      ∀ i : PrimePowerCompletedGroupAlgebraIndex G,
        modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2
          (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x) = 0
def

primePowerCompletedGroupAlgebraStageAugmentationIdealTransition

L137 ↗
FoxDifferential.primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
Documentation

The transition maps on the prime-power 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
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
variable {ℓ G} in
Lean source · statement
def primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
    primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j →
      primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i
theorem

primePowerCompletedGroupAlgebraStageAugmentationIdealTransition_val

L162 ↗
FoxDifferential.primePowerCompletedGroupAlgebraStageAugmentationIdealTransition_val
Documentation

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

Source context 10 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
variable {ℓ G} in
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraStageAugmentationIdealTransition_val
    {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
    (x : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) :
    ((primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
        (ℓ := ℓ) (G := G) hij x :
          primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i) :
      PrimePowerCompletedGroupAlgebraStage ℓ G i) =
      primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij x.1
def

primePowerCompletedGroupAlgebraAugmentationIdealSystem

L172 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealSystem
Documentation

The inverse system of prime-power 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
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
variable {ℓ G} in
Lean source · full declaration
def primePowerCompletedGroupAlgebraAugmentationIdealSystem :
    InverseSystem (I := PrimePowerCompletedGroupAlgebraIndex G) where
  X := fun i => ↥(primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i)
  topologicalSpace := fun _ => ⊥
  map := fun {i j} hij =>
    primePowerCompletedGroupAlgebraStageAugmentationIdealTransition
      (ℓ := ℓ) (G := G) hij
  continuous_map := by
    intro i j hij
    let : TopologicalSpace
        (primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i) := ⊥
    let : TopologicalSpace
        (primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) := ⊥
    let : DiscreteTopology
        (primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro i
    funext x
    apply Subtype.ext
    exact congrFun
      (congrArg DFunLike.coe
        (primePowerCompletedGroupAlgebraTransition_id (ℓ := ℓ) (G := G) i)) x.1
  map_comp := by
    intro i j k hij hjk
    funext x
    apply Subtype.ext
    exact congrFun
      (congrArg DFunLike.coe
        (primePowerCompletedGroupAlgebraTransition_comp (ℓ := ℓ) (G := G) hij hjk))
      x.1
abbrev

PrimePowerCompletedGroupAlgebraAugmentationIdeal

L205 ↗
FoxDifferential.PrimePowerCompletedGroupAlgebraAugmentationIdeal
Documentation

The inverse-limit object of the prime-power augmentation-ideal system.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
variable {ℓ G} in
Lean source · statement
abbrev PrimePowerCompletedGroupAlgebraAugmentationIdeal
abbrev

primePowerCompletedGroupAlgebraAugmentationIdealProjection

L209 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationIdealProjection
Documentation

The projection from the prime-power augmentation-ideal inverse limit to one stage.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
variable {ℓ G} in
variable {ℓ G} in
variable {ℓ G} in
Lean source · statement
abbrev primePowerCompletedGroupAlgebraAugmentationIdealProjection
    (i : PrimePowerCompletedGroupAlgebraIndex G) :
    PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G →
      primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i

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