Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.CoeffMap
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Basic
2import Mathlib.Algebra.Algebra.ZMod
3import Mathlib.Algebra.MonoidAlgebra.Basic
5/-!
6# Fox differential: completed — coefficient rings — mod-\(n\) completed group algebra — coeff map
8The principal declarations in this module are:
10- `modNCompletedCoeffMap`
11 The coefficient reduction map \(\mathbb{Z}/m\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}\) attached to a
12 divisibility relation \(n \mid m\).
13- `modNCompletedGroupRingCoeffMap`
14 The coefficient reduction map on one residue-coefficient group ring.
15- `modNCompletedCoeffMap_rfl`
16 Coefficient reduction along reflexive divisibility is the identity map.
17- `modNCompletedCoeffMap_comp`
18 Coefficient change is performed stagewise: supports are unchanged and coefficients are transported
19 by the given ring homomorphism.
20-/
22namespace FoxDifferential
24noncomputable section
26open ProCGroups.InverseSystems
27open ProCGroups.ProC
29universe u
31variable {n m k : ℕ}
32variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]
34omit [Fact (0 < n)] [Fact (0 < m)] in
35/--
36The coefficient reduction map \(\mathbb{Z}/m\mathbb{Z} \to \mathbb{Z}/n\mathbb{Z}\) attached to
37a divisibility relation \(n \mid m\).
38-/
39def modNCompletedCoeffMap (hnm : n ∣ m) :
40 ModNCompletedCoeff m →+* ModNCompletedCoeff n :=
41 ZMod.castHom hnm (ModNCompletedCoeff n)
43omit [Fact (0 < n)] in
44/-- Coefficient reduction along reflexive divisibility is the identity map. -/
45@[simp]
46theorem modNCompletedCoeffMap_rfl :
47 modNCompletedCoeffMap (n := n) (m := n) dvd_rfl = RingHom.id _ := by
48 ext x
49 rcases ZMod.intCast_surjective x with ⟨t, rfl⟩
50 simp only [modNCompletedCoeffMap, ZMod.castHom_self, map_intCast]
52omit [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)] in
53/--
54Coefficient change is performed stagewise: supports are unchanged and coefficients are
55transported by the given ring homomorphism.
56-/
57@[simp]
58theorem modNCompletedCoeffMap_comp (hnm : n ∣ m) (hmk : m ∣ k) :
59 (modNCompletedCoeffMap (n := n) (m := m) hnm).comp
60 (modNCompletedCoeffMap (n := m) (m := k) hmk) =
61 modNCompletedCoeffMap (n := n) (m := k) (dvd_trans hnm hmk) := by
62 ext x
63 rcases ZMod.intCast_surjective x with ⟨t, rfl⟩
64 simp only [modNCompletedCoeffMap, ZMod.castHom_comp, map_intCast]
66omit [Fact (0 < n)] [Fact (0 < m)] in
67/-- The coefficient reduction map on one residue-coefficient group ring. -/
68def modNCompletedGroupRingCoeffMap (H : Type*) [Monoid H] (hnm : n ∣ m) :
69 ModNCompletedGroupRing m H →+* ModNCompletedGroupRing n H := by
70 letI : Algebra (ModNCompletedCoeff m) (ModNCompletedCoeff n) :=
71 ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := m) hnm
72 letI : Algebra (ModNCompletedCoeff m) (ModNCompletedGroupRing n H) := inferInstance
73 exact
74 (MonoidAlgebra.lift (ModNCompletedCoeff m) (ModNCompletedGroupRing n H) H
75 (MonoidAlgebra.of (ModNCompletedCoeff n) H)).toRingHom
77omit [Fact (0 < n)] [Fact (0 < m)] in
78/-- Evaluation of coefficient reduction on a group-like basis element. -/
79@[simp]
80theorem modNCompletedGroupRingCoeffMap_of
81 (H : Type*) [Monoid H] (hnm : n ∣ m) (h : H) :
82 modNCompletedGroupRingCoeffMap (n := n) (m := m) H hnm
83 (MonoidAlgebra.of (ModNCompletedCoeff m) H h) =
84 MonoidAlgebra.of (ModNCompletedCoeff n) H h := by
85 letI : Algebra (ModNCompletedCoeff m) (ModNCompletedCoeff n) :=
86 ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := m) hnm
87 letI : Algebra (ModNCompletedCoeff m) (ModNCompletedGroupRing n H) := inferInstance
88 change
89 MonoidAlgebra.lift (ModNCompletedCoeff m) (ModNCompletedGroupRing n H) H
90 (MonoidAlgebra.of (ModNCompletedCoeff n) H)
91 (MonoidAlgebra.of (ModNCompletedCoeff m) H h) =
92 MonoidAlgebra.of (ModNCompletedCoeff n) H h
93 exact MonoidAlgebra.lift_of
94 (R := ModNCompletedCoeff m) (A := ModNCompletedGroupRing n H)
95 (M := H) (MonoidAlgebra.of (ModNCompletedCoeff n) H) h
97end
99end FoxDifferential