NYLL
Module

Augmentation.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation
11 declarations indexed from sourceView source ↗

Module documentation

Fox differential: coefficient rings — prime-power completed group algebra — basic — augmentation

The principal declarations in this module are:

  • modNCompletedGroupAlgebraCoeffMap

The modulus-direction map on residue-coefficient completed group algebras.

  • modNCompletedGroupAlgebraAugmentationKernelCoeffMap

Coefficient change is performed stagewise: supports are unchanged and coefficients are transported by the given ring homomorphism.

  • modNCompletedGroupAlgebraProjection_coeffMap

The mod-\(n\) completed group-algebra projection commutes with the coefficient map.

  • modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap

Finite-stage augmentation commutes with coefficient reduction.

Imports2
Imported by3

Declarations

def

modNCompletedGroupAlgebraCoeffMap

L41 ↗
FoxDifferential.modNCompletedGroupAlgebraCoeffMap
Documentation

The modulus-direction map on residue-coefficient completed group algebras.

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 {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def modNCompletedGroupAlgebraCoeffMap (hnm : n ∣ m) :
    ModNCompletedGroupAlgebra m G → ModNCompletedGroupAlgebra n G
theorem

modNCompletedGroupAlgebraProjection_coeffMap

L67 ↗
FoxDifferential.modNCompletedGroupAlgebraProjection_coeffMap
Documentation

The mod-\(n\) completed group-algebra projection commutes with the coefficient map.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] [Fact (0 < m)] in
Lean source · statement
theorem modNCompletedGroupAlgebraProjection_coeffMap
    (hnm : n ∣ m) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
    (x : ModNCompletedGroupAlgebra m G) :
    modNCompletedGroupAlgebraProjection n G U
        (modNCompletedGroupAlgebraCoeffMap (n := n) (m := m) (G := G) hnm x) =
      modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm
        (modNCompletedGroupAlgebraProjection m G U x)
theorem

modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap

L80 ↗
FoxDifferential.modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap
Documentation

Finite-stage augmentation commutes with coefficient reduction.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] [Fact (0 < m)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap
    (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (hnm : n ∣ m) :
    (modNCompletedGroupAlgebraStageAugmentation n G U).comp
        (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm) =
      (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
        (modNCompletedGroupAlgebraStageAugmentation m G U)
theorem

modNCompletedGroupAlgebraStageAugmentationInClass_comp_coeffMap

L144 ↗
FoxDifferential.modNCompletedGroupAlgebraStageAugmentationInClass_comp_coeffMap
Documentation

Class-indexed finite-stage augmentation commutes with coefficient reduction.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] [Fact (0 < m)] in
Lean source · statement
theorem modNCompletedGroupAlgebraStageAugmentationInClass_comp_coeffMap
    (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (hnm : n ∣
        m) :
    (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp
        (modNCompletedGroupAlgebraStageCoeffMapInClass
          (n := n) (m := m) (G := G) C U hnm) =
      (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
        (modNCompletedGroupAlgebraStageAugmentationInClass m G C U)
theorem

modNCompletedGroupAlgebraAugmentation_coeffMap

L216 ↗
FoxDifferential.modNCompletedGroupAlgebraAugmentation_coeffMap
Documentation

Completed augmentation commutes with the coefficient-reduction map between moduli.

Source context 9 commands

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

namespace FoxDifferential
noncomputable section
open ProCGroups.InverseSystems
open ProCGroups.ProC
universe u
variable {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
omit [Fact (0 < n)] [Fact (0 < m)] in
Lean source · statement
theorem modNCompletedGroupAlgebraAugmentation_coeffMap
    (hnm : n ∣ m) (x : ModNCompletedGroupAlgebra m G) :
    modNCompletedGroupAlgebraAugmentation n G
        (modNCompletedGroupAlgebraCoeffMap (n := n) (m := m) (G := G) hnm x) =
      modNCompletedCoeffMap (n := n) (m := m) hnm
        (modNCompletedGroupAlgebraAugmentation m G x)
def

modNCompletedGroupAlgebraAugmentationKernelCoeffMap

L236 ↗
FoxDifferential.modNCompletedGroupAlgebraAugmentationKernelCoeffMap
Documentation

Coefficient change is performed stagewise: supports are unchanged and coefficients are transported by the given ring homomorphism.

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 {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def modNCompletedGroupAlgebraAugmentationKernelCoeffMap
    (hnm : n ∣ m) :
    ModNCompletedGroupAlgebraAugmentationKernel m G →
      ModNCompletedGroupAlgebraAugmentationKernel n G
theorem

primePow_dvd_primePow

L248 ↗
FoxDifferential.primePow_dvd_primePow
Documentation

The standard divisibility relation between prime powers with the same base.

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 {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
theorem primePow_dvd_primePow
    (ℓ : ℕ) {a b : ℕ} (hab : a ≤ b) :
    ℓ ^ a ∣ ℓ ^ b
def

primePowCompletedGroupAlgebraCoeffMap

L254 ↗
FoxDifferential.primePowCompletedGroupAlgebraCoeffMap
Documentation

The modulus-direction completed map specialized to prime-power stages.

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 {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def primePowCompletedGroupAlgebraCoeffMap
    (ℓ : ℕ) {a b : ℕ}
    (hab : a ≤ b) :
    ModNCompletedGroupAlgebra (ℓ ^ b) G → ModNCompletedGroupAlgebra (ℓ ^ a) G
def

primePowCompletedGroupAlgebraAugmentationKernelCoeffMap

L262 ↗
FoxDifferential.primePowCompletedGroupAlgebraAugmentationKernelCoeffMap
Documentation

The coefficient map between prime-power stages restricts to a map on augmentation kernels.

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 {n m k : ℕ}
variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
Lean source · statement
def primePowCompletedGroupAlgebraAugmentationKernelCoeffMap
    (ℓ : ℕ) {a b : ℕ}
    (hab : a ≤ b) :
    ModNCompletedGroupAlgebraAugmentationKernel (ℓ ^ b) G →
      ModNCompletedGroupAlgebraAugmentationKernel (ℓ ^ a) G
abbrev

PrimePowerCompletedGroupAlgebraIndex

L276 ↗
FoxDifferential.PrimePowerCompletedGroupAlgebraIndex
Documentation

The two-parameter index \((a,U)\) for the prime-power residue-coefficient stages.

Source context 10 commands

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

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

PrimePowerCompletedGroupAlgebraIndexInClass

L280 ↗
FoxDifferential.PrimePowerCompletedGroupAlgebraIndexInClass
Documentation

The two-parameter index \((a,U)\) for prime-power stages over a quotient class \(C\).

Source context 10 commands

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

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

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