NYLL
Module

Augmentation.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Augmentation
15 declarations indexed from sourceView source ↗

Module documentation

Fox differential: coefficient rings — prime-power completed group algebra — in class —

augmentation

The principal declarations in this module are:

  • primePowerCompletedCoeffSystemInClass

The class-restricted coefficient inverse system indexed by \(i = (a,U)\), whose coefficient stage is \(\mathrm{ZMod}\,(\ell^a)\).

  • PrimePowerCompletedCoeffCompatibleInClass

Compatibility for the class-indexed coefficient tower; the finite quotient component is retained only to match the surrounding pro-\(C\) index shape.

  • primePowerCompletedCoeffProjectionInClass_zero

The finite-stage projection sends \(0\) to \(0\).

  • primePowerCompletedCoeffProjectionInClass_add

The class-indexed prime-power coefficient projection preserves addition.

Imports1
Imported by1

Declarations

def

primePowerCompletedCoeffSystemInClass

L43 ↗
FoxDifferential.primePowerCompletedCoeffSystemInClass
Documentation

The class-restricted coefficient inverse system indexed by \(i = (a,U)\), whose coefficient stage is \(\mathrm{ZMod}\,(\ell^a)\).

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
def primePowerCompletedCoeffSystemInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    InverseSystem (I := PrimePowerCompletedGroupAlgebraIndexInClass G C) where
  X := fun i => ModNCompletedCoeff (ℓ ^ i.1)
  topologicalSpace := fun _ => ⊥
  map := fun {i j} hij =>
    modNCompletedCoeffMap
      (n := ℓ ^ i.1) (m := ℓ ^ j.1)
      (primePow_dvd_primePow (ℓ := ℓ) hij.1)
  continuous_map := by
    intro i j hij
    let : TopologicalSpace (ModNCompletedCoeff (ℓ ^ i.1)) := ⊥
    let : TopologicalSpace (ModNCompletedCoeff (ℓ ^ j.1)) := ⊥
    let : DiscreteTopology (ModNCompletedCoeff (ℓ ^ j.1)) := ⟨rfl⟩
    exact continuous_of_discreteTopology
  map_id := by
    intro i
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (modNCompletedCoeffMap_rfl (n := ℓ ^ i.1))) x
  map_comp := by
    intro i j k hij hjk
    funext x
    exact congrFun
      (congrArg DFunLike.coe
        (modNCompletedCoeffMap_comp
          (n := ℓ ^ i.1) (m := ℓ ^ j.1) (k := ℓ ^ k.1)
          (primePow_dvd_primePow (ℓ := ℓ) hij.1)
          (primePow_dvd_primePow (ℓ := ℓ) hjk.1))) x
def

PrimePowerCompletedCoeffCompatibleInClass

L78 ↗
FoxDifferential.PrimePowerCompletedCoeffCompatibleInClass
Documentation

Compatibility for the class-indexed coefficient tower; the finite quotient component is retained only to match the surrounding pro-\(C\) index shape.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def PrimePowerCompletedCoeffCompatibleInClass
    (C : ProCGroups.FiniteGroupClass.{u})
    (x : ∀ i : PrimePowerCompletedGroupAlgebraIndexInClass G C,
      ModNCompletedCoeff (ℓ ^ i.1)) : Prop
abbrev

PrimePowerCompletedCoeffInClass

L85 ↗
FoxDifferential.PrimePowerCompletedCoeffInClass
Documentation

The pro-\(C\)-indexed prime-power completed coefficient inverse limit.

Source context 7 commands

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

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

primePowerCompletedCoeffProjectionInClass

L91 ↗
FoxDifferential.primePowerCompletedCoeffProjectionInClass
Documentation

The projection from the pro-\(C\)-indexed coefficient limit to one finite stage.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def primePowerCompletedCoeffProjectionInClass
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    PrimePowerCompletedCoeffInClass ℓ G C → ModNCompletedCoeff (ℓ ^ i.1)
instance

instZeroPrimePowerCompletedCoeffInClass

L100 ↗
FoxDifferential.instZeroPrimePowerCompletedCoeffInClass
Documentation

The zero element of the class-indexed prime-power completed coefficient ring is the compatible family of finite-stage zero elements.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instZeroPrimePowerCompletedCoeffInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Zero (PrimePowerCompletedCoeffInClass ℓ G C) where
  zero := ⟨fun _ => 0, by
    dsimp [PrimePowerCompletedCoeffCompatibleInClass]
    intro i j hij
    exact map_zero
      (modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1))⟩
instance

instAddPrimePowerCompletedCoeffInClass

L115 ↗
FoxDifferential.instAddPrimePowerCompletedCoeffInClass
Documentation

Addition in the prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient additions.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instAddPrimePowerCompletedCoeffInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Add (PrimePowerCompletedCoeffInClass ℓ G C) where
  add x y := ⟨fun i =>
      (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i), by
    dsimp [PrimePowerCompletedCoeffCompatibleInClass]
    intro i j hij
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        ((show ZMod (ℓ ^ j.1) from x.1 j) + (show ZMod (ℓ ^ j.1) from y.1 j)) =
      (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i)
    rw [map_add]
    exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩
instance

instNegPrimePowerCompletedCoeffInClass

L134 ↗
FoxDifferential.instNegPrimePowerCompletedCoeffInClass
Documentation

Negation on the class-indexed prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient negations.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instNegPrimePowerCompletedCoeffInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Neg (PrimePowerCompletedCoeffInClass ℓ G C) where
  neg x := ⟨fun i => -(show ZMod (ℓ ^ i.1) from x.1 i), by
    dsimp [PrimePowerCompletedCoeffCompatibleInClass]
    intro i j hij
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        (-(show ZMod (ℓ ^ j.1) from x.1 j)) =
      -(show ZMod (ℓ ^ i.1) from x.1 i)
    rw [map_neg]
    exact congrArg Neg.neg (x.2 i j hij)⟩
instance

instSubPrimePowerCompletedCoeffInClass

L152 ↗
FoxDifferential.instSubPrimePowerCompletedCoeffInClass
Documentation

Subtraction in the class-indexed prime-power completed coefficient ring is defined coordinatewise through finite-stage coefficient-ring subtractions.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · full declaration
instance instSubPrimePowerCompletedCoeffInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Sub (PrimePowerCompletedCoeffInClass ℓ G C) where
  sub x y := ⟨fun i =>
      (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i), by
    dsimp [PrimePowerCompletedCoeffCompatibleInClass]
    intro i j hij
    change modNCompletedCoeffMap
        (n := ℓ ^ i.1) (m := ℓ ^ j.1)
        (primePow_dvd_primePow (ℓ := ℓ) hij.1)
        ((show ZMod (ℓ ^ j.1) from x.1 j) - (show ZMod (ℓ ^ j.1) from y.1 j)) =
      (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i)
    rw [map_sub]
    exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩
theorem

primePowerCompletedCoeffProjectionInClass_zero

L170 ↗
FoxDifferential.primePowerCompletedCoeffProjectionInClass_zero
Documentation

The finite-stage projection sends \(0\) to \(0\).

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjectionInClass_zero
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C) :
    primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i
        (0 : PrimePowerCompletedCoeffInClass ℓ G C) = 0
theorem

primePowerCompletedCoeffProjectionInClass_add

L179 ↗
FoxDifferential.primePowerCompletedCoeffProjectionInClass_add
Documentation

The class-indexed prime-power coefficient projection preserves addition.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjectionInClass_add
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (x y : PrimePowerCompletedCoeffInClass ℓ G C) :
    primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i (x + y) =
      primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i x +
        primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i y
theorem

primePowerCompletedCoeffProjectionInClass_neg

L190 ↗
FoxDifferential.primePowerCompletedCoeffProjectionInClass_neg
Documentation

The class-indexed prime-power coefficient projection preserves negation.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjectionInClass_neg
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (x : PrimePowerCompletedCoeffInClass ℓ G C) :
    primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i (-x) =
      -primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i x
theorem

primePowerCompletedCoeffProjectionInClass_sub

L200 ↗
FoxDifferential.primePowerCompletedCoeffProjectionInClass_sub
Documentation

The class-indexed prime-power coefficient projection preserves subtraction.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
Lean source · statement
theorem primePowerCompletedCoeffProjectionInClass_sub
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (x y : PrimePowerCompletedCoeffInClass ℓ G C) :
    primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i (x - y) =
      primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i x -
        primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i y
def

primePowerCompletedGroupAlgebraAugmentationInClass

L212 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationInClass
Documentation

The class-restricted prime-power completed group algebra carries a canonical augmentation to the pro-\(C\)-indexed coefficient limit.

Source context 7 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def primePowerCompletedGroupAlgebraAugmentationInClass
    (C : ProCGroups.FiniteGroupClass.{u}) :
    PrimePowerCompletedGroupAlgebraInClass ℓ G C →
      PrimePowerCompletedCoeffInClass ℓ G C
theorem

primePowerCompletedCoeffProjectionInClass_augmentation

L250 ↗
FoxDifferential.primePowerCompletedCoeffProjectionInClass_augmentation
Documentation

Projecting the class-indexed prime-power completed augmentation to a coefficient stage agrees with the corresponding finite-stage augmentation.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedCoeffProjectionInClass_augmentation
    (C : ProCGroups.FiniteGroupClass.{u}) (i : PrimePowerCompletedGroupAlgebraIndexInClass G C)
    (x : PrimePowerCompletedGroupAlgebraInClass ℓ G C) :
    primePowerCompletedCoeffProjectionInClass (ℓ := ℓ) (G := G) C i
        (primePowerCompletedGroupAlgebraAugmentationInClass (ℓ := ℓ) (G := G) C x) =
      modNCompletedGroupAlgebraStageAugmentationInClass (ℓ ^ i.1) G C i.2
        (primePowerCompletedGroupAlgebraProjectionInClass (ℓ := ℓ) (G := G) C i x)
theorem

primePowerCompletedGroupAlgebraAugmentationInClass_surjective

L263 ↗
FoxDifferential.primePowerCompletedGroupAlgebraAugmentationInClass_surjective
Documentation

The class-indexed completed group-algebra augmentation has a canonical section, obtained by placing each compatible coefficient system on the identity monomial at every finite stage.

Source context 8 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable (ℓ : ℕ) [Fact (0 < ℓ)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < ℓ)] in
Lean source · statement
theorem primePowerCompletedGroupAlgebraAugmentationInClass_surjective
    (C : ProCGroups.FiniteGroupClass.{u}) :
    Function.Surjective
      (primePowerCompletedGroupAlgebraAugmentationInClass (ℓ := ℓ) (G := G) C)

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