NYLL
Module

CoeffMap.lean

Nyll.ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.CoeffMap
5 declarations indexed from sourceView source ↗

Module documentation

Fox differential: completed — coefficient rings — mod-\(n\) completed group algebra — coeff map

The principal declarations in this module are:

  • modNCompletedCoeffMap

The coefficient reduction map \(\mathbb{Z}/m\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}\) attached to a divisibility relation \(n \mid m\).

  • modNCompletedGroupRingCoeffMap

The coefficient reduction map on one residue-coefficient group ring.

  • modNCompletedCoeffMap_rfl

Coefficient reduction along reflexive divisibility is the identity map.

  • modNCompletedCoeffMap_comp

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

Imports3
Imported by3

Declarations

def

modNCompletedCoeffMap

L45 ↗
FoxDifferential.modNCompletedCoeffMap
Documentation

The coefficient reduction map \(\mathbb{Z}/m\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}\) attached to a divisibility relation \(n \mid m\).

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)]
omit [Fact (0 < n)] [Fact (0 < m)] in
Lean source · statement
def modNCompletedCoeffMap (hnm : n ∣ m) :
    ModNCompletedCoeff m →+* ModNCompletedCoeff n
theorem

modNCompletedCoeffMap_rfl

L52 ↗
FoxDifferential.modNCompletedCoeffMap_rfl
Documentation

Coefficient reduction along reflexive divisibility is the identity map.

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)]
omit [Fact (0 < n)] in
Lean source · statement
theorem modNCompletedCoeffMap_rfl :
    modNCompletedCoeffMap (n := n) (m := n) dvd_rfl = RingHom.id _
theorem

modNCompletedCoeffMap_comp

L64 ↗
FoxDifferential.modNCompletedCoeffMap_comp
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)]
omit [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)] in
Lean source · statement
theorem modNCompletedCoeffMap_comp (hnm : n ∣ m) (hmk : m ∣ k) :
    (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
        (modNCompletedCoeffMap (n := m) (m := k) hmk) =
      modNCompletedCoeffMap (n := n) (m := k) (dvd_trans hnm hmk)
def

modNCompletedGroupRingCoeffMap

L74 ↗
FoxDifferential.modNCompletedGroupRingCoeffMap
Documentation

The coefficient reduction map on one residue-coefficient group ring.

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)]
omit [Fact (0 < n)] [Fact (0 < m)] in
Lean source · statement
def modNCompletedGroupRingCoeffMap (H : Type*) [Monoid H] (hnm : n ∣ m) :
    ModNCompletedGroupRing m H →+* ModNCompletedGroupRing n H
theorem

modNCompletedGroupRingCoeffMap_of

L86 ↗
FoxDifferential.modNCompletedGroupRingCoeffMap_of
Documentation

Evaluation of coefficient reduction on a group-like basis element.

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)]
omit [Fact (0 < n)] [Fact (0 < m)] in
Lean source · statement
theorem modNCompletedGroupRingCoeffMap_of
    (H : Type*) [Monoid H] (hnm : n ∣ m) (h : H) :
    modNCompletedGroupRingCoeffMap (n := n) (m := m) H hnm
        (MonoidAlgebra.of (ModNCompletedCoeff m) H h) =
      MonoidAlgebra.of (ModNCompletedCoeff n) H h

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