FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.CoeffMap
Fox Differential / Completed / Coefficient Rings / Completed Group Algebra Mod N / Coefficient Map.
import
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Basic
- Mathlib.Algebra.Algebra.ZMod
- Mathlib.Algebra.MonoidAlgebra.Basic
Imported by
- FoxDifferential.Completed
- FoxDifferential.Completed.CoefficientRings
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap
- FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.Coeff
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 modNCompletedCoeffMap_rfl :
modNCompletedCoeffMap (n := n) (m := n) dvd_rfl = RingHom.id _Coefficient change is performed stagewise: each coefficient is transported by the given ring homomorphism while the finite quotient support is left unchanged.
Show proof
by
ext x
rcases ZMod.intCast_surjective x with ⟨t, rfl⟩
simp only [modNCompletedCoeffMap, ZMod.castHom_self, map_intCast]Proof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□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 proof
by
ext x
rcases ZMod.intCast_surjective x with ⟨t, rfl⟩
simp only [modNCompletedCoeffMap, ZMod.castHom_comp, map_intCast]Proof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□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)).toRingHomThe coefficient reduction map on one residue-coefficient group ring.
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 hEvaluation of coefficient reduction on a group-like basis element.
Show proof
by
classical
simp only [modNCompletedGroupRingCoeffMap, MonoidAlgebra.of, MonoidAlgebra.single, AlgHom.toRingHom_eq_coe,
MonoidHom.coe_mk, OneHom.coe_mk, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidAlgebra.smul_single, one_smul]Proof. Unfold the mod-\(n\) completed group algebra as the inverse limit over finite group quotients with fixed coefficient ring \(\mathbb{Z}/n\mathbb{Z}\). Projections, transitions, augmentation, coefficient reduction, and algebra operations are computed coordinatewise at finite group-algebra stages. Compatibility under quotient refinement and inverse-limit extensionality assemble the completed statements.
□