FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/CoeffMap.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Basic
2import Mathlib.Algebra.Algebra.ZMod
3import Mathlib.Algebra.MonoidAlgebra.Basic
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/CoeffMap.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Completed coefficient algebras
16Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.
17-/
18namespace FoxDifferential
20noncomputable section
22open ProCGroups.InverseSystems
23open ProCGroups.ProC
25universe u
27variable {n m k : ℕ}
28variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
30omit [Fact (0 < n)] [Fact (0 < m)] in
31/-- The coefficient reduction map `ZMod m -> ZMod n` attached to a divisibility relation `n ∣ m`.
32-/
33def modNCompletedCoeffMap (hnm : n ∣ m) :
34 ModNCompletedCoeff m →+* ModNCompletedCoeff n :=
35 ZMod.castHom hnm (ModNCompletedCoeff n)
37omit [Fact (0 < n)] in
38/-- Identity case for `modNCompletedCoeffMap`. -/
39@[simp]
40theorem modNCompletedCoeffMap_rfl :
41 modNCompletedCoeffMap (n := n) (m := n) dvd_rfl = RingHom.id _ := by
42 ext x
43 rcases ZMod.intCast_surjective x with ⟨t, rfl⟩
44 simp only [modNCompletedCoeffMap, ZMod.castHom_self, map_intCast]
46omit [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)] in
47/-- Composition of coefficient reduction maps. -/
48@[simp]
49theorem modNCompletedCoeffMap_comp (hnm : n ∣ m) (hmk : m ∣ k) :
50 (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
51 (modNCompletedCoeffMap (n := m) (m := k) hmk) =
52 modNCompletedCoeffMap (n := n) (m := k) (dvd_trans hnm hmk) := by
53 ext x
54 rcases ZMod.intCast_surjective x with ⟨t, rfl⟩
55 simp only [modNCompletedCoeffMap, ZMod.castHom_comp, map_intCast]
57omit [Fact (0 < n)] [Fact (0 < m)] in
58/-- The coefficient reduction map on one residue-coefficient group ring. -/
59def modNCompletedGroupRingCoeffMap (H : Type*) [Monoid H] (hnm : n ∣ m) :
60 ModNCompletedGroupRing m H →+* ModNCompletedGroupRing n H := by
61 letI : Algebra (ModNCompletedCoeff m) (ModNCompletedCoeff n) :=
62 ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := m) hnm
63 letI : Algebra (ModNCompletedCoeff m) (ModNCompletedGroupRing n H) := inferInstance
64 exact
65 (MonoidAlgebra.lift (ModNCompletedCoeff m) (ModNCompletedGroupRing n H) H
66 (MonoidAlgebra.of (ModNCompletedCoeff n) H)).toRingHom
68omit [Fact (0 < n)] [Fact (0 < m)] in
69/-- Evaluation of coefficient reduction on a group-like basis element. -/
70@[simp]
72 (H : Type*) [Monoid H] (hnm : n ∣ m) (h : H) :
73 modNCompletedGroupRingCoeffMap (n := n) (m := m) H hnm
74 (MonoidAlgebra.of (ModNCompletedCoeff m) H h) =
75 MonoidAlgebra.of (ModNCompletedCoeff n) H h := by
76 classical
77 simp only [modNCompletedGroupRingCoeffMap, MonoidAlgebra.of, MonoidAlgebra.single, AlgHom.toRingHom_eq_coe,
78 MonoidHom.coe_mk, OneHom.coe_mk, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidAlgebra.smul_single, one_smul]
80end
82end FoxDifferential