Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.CoeffMap
ProCGroups/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/CoeffMap

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.CoeffMap

3 Theorems | 2 Definitions

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.
imports
Imported by

Declarations

Definition FoxDifferential.modNCompletedCoeffMap 
omit [Fact (0 < n)] [Fact (0 < m)] in
def modNCompletedCoeffMap (hnm : n ∣ m) :
    ModNCompletedCoeff m →+* ModNCompletedCoeff n :=
  ZMod.castHom hnm (ModNCompletedCoeff n)

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

Theorem FoxDifferential.modNCompletedCoeffMap_rfl 
omit [Fact (0 < n)] in
@[simp]
theorem modNCompletedCoeffMap_rfl :
    modNCompletedCoeffMap (n := n) (m := n) dvd_rfl = RingHom.id _

Coefficient reduction along reflexive divisibility is the identity map.

Show Lean proof
Theorem FoxDifferential.modNCompletedCoeffMap_comp 
omit [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)] in
@[simp]
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)

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

Show Lean proof
Definition FoxDifferential.modNCompletedGroupRingCoeffMap 
omit [Fact (0 < n)] [Fact (0 < m)] in
def modNCompletedGroupRingCoeffMap (H : Type*) [Monoid H] (hnm : n ∣ m) :
    ModNCompletedGroupRing m H →+* ModNCompletedGroupRing n H := by
  letI : Algebra (ModNCompletedCoeff m) (ModNCompletedCoeff n) :=
    ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := m) hnm
  letI : Algebra (ModNCompletedCoeff m) (ModNCompletedGroupRing n H) := inferInstance
  exact
    (MonoidAlgebra.lift (ModNCompletedCoeff m) (ModNCompletedGroupRing n H) H
      (MonoidAlgebra.of (ModNCompletedCoeff n) H)).toRingHom

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

Theorem FoxDifferential.modNCompletedGroupRingCoeffMap_of 
omit [Fact (0 < n)] [Fact (0 < m)] in
@[simp]
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

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

Show Lean proof