ResidueQuotient.lean

1 import PaperICompletion3
2 import Mathlib.Algebra.Module.Torsion.Basic
3 import Mathlib.RingTheory.Artinian.Module
4 
5 /-! # Exact residue quotients of primary products
6 The kernel is identified with the actual scalar image, and the resulting
7 quotient equivalences are linear over the residue ring, not only the base ring.
8 -/
9 set_option autoImplicit false
10 noncomputable section
11 open scoped Pointwise
12 namespace Komorebi.PaperICompletion4.ResidueQuotient
13 open Komorebi.PaperICompletion3.PrimarySeedFormula
14 universe u v w
15 variable {R : Type u} [CommRing R]
16 
17 /-- A quotient factor vanishes precisely on multiples of its generator. -/
18 theorem factor_eq_zero_iff_smul (I : Ideal R) (p : R)
19     (hI : I ≤ Ideal.span {p}) (x : R ⧸ I) :
20     Ideal.Quotient.factor hI x = 0 ↔ ∃ y : R ⧸ I, p • y = x := by
21   obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
22   constructor
23   · intro h
24     have hd : p ∣ r := Ideal.mem_span_singleton.mp
25       (Ideal.Quotient.eq_zero_iff_mem.mp h)
26     obtain ⟨s, rfl⟩ := hd
27     exact ⟨Ideal.Quotient.mk I s, by simp [Algebra.smul_def]⟩
28   · rintro ⟨y, hy⟩
29     obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
30     rw [← hy]
31     simp only [Algebra.smul_def]
32     exact Ideal.Quotient.eq_zero_iff_mem.mpr
33       (Ideal.mem_span_singleton.mpr (dvd_mul_right p s))
34 
35 /-- Multiplication by a coprime element is onto the quotient. -/
36 theorem smul_surjective_of_coprime (p q : R) (h : IsCoprime p q) :
37     Function.Surjective (fun x : R ⧸ Ideal.span {q} ↦ p • x) := by
38   obtain ⟨a, b, hab⟩ := h
39   intro x
40   refine ⟨a • x, ?_⟩
41   have hq : (Ideal.Quotient.mk (Ideal.span {q})) q = 0 :=
42     Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.subset_span (Set.mem_singleton q))
43   have hid := congrArg (Ideal.Quotient.mk (Ideal.span {q})) hab
44   simp only [map_add, map_mul, map_one, hq, mul_zero, add_zero] at hid
45   simp only [Algebra.smul_def]
46   rw [← mul_assoc, mul_comm ((algebraMap R (R ⧸ Ideal.span {q})) p)]
47   change ((Ideal.Quotient.mk (Ideal.span {q})) a *
48     (Ideal.Quotient.mk (Ideal.span {q})) p) * x = x
49   rw [hid, one_mul]
50 
51 /-- The scalar-image quotient carries its canonical residue-ring action. -/
52 abbrev ScalarQuotient (M : Type v) [AddCommGroup M] [Module R M] (p : R) :=
53   M ⧸ (p • (⊤ : Submodule R M))
54 
55 /-- Literal membership in the scalar image, including zero modules. -/
56 theorem mem_scalarImage_iff {M : Type v} [AddCommGroup M] [Module R M]
57     (p : R) (x : M) : x ∈ p • (⊤ : Submodule R M) ↔ ∃ y, p • y = x := by
58   simp only [Submodule.mem_smul_pointwise_iff_exists, Submodule.mem_top, true_and]
59 
60 
61 section QuotientEquivalence
62 variable {M : Type v} [AddCommGroup M] [Module R M]
63 variable {N : Type w} [AddCommGroup N] [Module R N]
64 variable (p : R) [Module (R ⧸ Ideal.span {p}) N]
65   [IsScalarTower R (R ⧸ Ideal.span {p}) N]
66 
67 /-- Exact kernel and surjectivity induce an equivalence over the residue ring.
68 The action on the source is the canonical action on the literal quotient by pM. -/
69 def scalarQuotientEquiv (f : M →ₗ[R] N) (hf : Function.Surjective f)
70     (hker : f.ker = p • (⊤ : Submodule R M)) :
71     ScalarQuotient M p ≃ₗ[R ⧸ Ideal.span {p}] N := by
72   let e : ScalarQuotient M p ≃ₗ[R] N :=
73     (Submodule.quotEquivOfEq _ _ hker.symm).trans (f.quotKerEquivOfSurjective hf)
74   exact
75     { e.toAddEquiv with
76       map_smul' := by
77         intro a x
78         obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective a
79         change e (r • x) = (Ideal.Quotient.mk (Ideal.span {p}) r) • e x
80         rw [e.map_smul]
81         exact (IsScalarTower.algebraMap_smul (R ⧸ Ideal.span {p}) r (e x)).symm }
82 
83 /-- The induced map takes a quotient class to the original residue map. -/
84 theorem scalarQuotientEquiv_mk (f : M →ₗ[R] N) (hf : Function.Surjective f)
85     (hker : f.ker = p • (⊤ : Submodule R M)) (x : M) :
86     scalarQuotientEquiv p f hf hker (Submodule.Quotient.mk x) = f x := by
87   simp [scalarQuotientEquiv]
88 end QuotientEquivalence
89 
90 section PrimaryProduct
91 variable [IsDomain R] [IsPrincipalIdealRing R]
92 variable {ι : Type v} [Fintype ι]
93 variable (q : ι → R) (hq : ∀ i, Irreducible (q i))
94   (e : ι → ℕ) (he : ∀ i, 0 < e i)
95 
96 /-- The canonical map from each prime-power quotient to its residue field. -/
97 def primaryResidueMap (p : R) :
98     ((i : ι) → R ⧸ Ideal.span {q i ^ e i}) →ₗ[R]
99       ({i : ι // Ideal.span {q i} = Ideal.span {p}} → R ⧸ Ideal.span {p}) :=
100   residueFiberMap (fun i ↦ Ideal.span {q i ^ e i}) (fun i ↦ Ideal.span {q i})
101     (fun i ↦ Ideal.span_singleton_le_span_singleton.mpr
102       (dvd_pow_self _ (Nat.ne_of_gt (he i)))) (Ideal.span {p})
103 
104 omit [Fintype ι] in
105 include hq in
106 /-- The full residue map, including all off-primary coordinates, has kernel pM. -/
107 theorem primaryResidueMap_ker (p : R) (hp : Irreducible p) :
108     (primaryResidueMap q e he p).ker =
109       p • (⊤ : Submodule R ((i : ι) → R ⧸ Ideal.span {q i ^ e i})) := by
110   classical
111   ext x
112   rw [LinearMap.mem_ker, mem_scalarImage_iff]
113   constructor
114   · intro hx
115     have hcoord : ∀ i, ∃ y : R ⧸ Ideal.span {q i ^ e i}, p • y = x i := by
116       intro i
117       by_cases hi : Ideal.span {q i} = Ideal.span {p}
118       · have hz := congrFun hx ⟨i, hi⟩
119         exact (factor_eq_zero_iff_smul _ p
120           ((Ideal.span_singleton_le_span_singleton.mpr
121             (dvd_pow_self _ (Nat.ne_of_gt (he i)))).trans_eq hi) (x i)).mp hz
122       · have hc : IsCoprime p (q i ^ e i) := by
123           have h := coprime_primePower_ideals p (q i) hp (hq i)
124             (Ne.symm hi) 1 (e i)
125           simpa only [pow_one] using (Ideal.isCoprime_span_singleton_iff _ _).mp h
126         exact smul_surjective_of_coprime p (q i ^ e i) hc (x i)
127     choose y hy using hcoord
128     exact ⟨y, funext hy⟩
129   · rintro ⟨y, rfl⟩
130     ext i
131     exact (factor_eq_zero_iff_smul _ p
132       ((Ideal.span_singleton_le_span_singleton.mpr
133         (dvd_pow_self _ (Nat.ne_of_gt (he i)))).trans_eq i.property) (p • y i)).mpr
134       ⟨y i, rfl⟩
135 
136 omit [IsDomain R] [IsPrincipalIdealRing R] [Fintype ι] in
137 /-- The full primary residue map is onto even for an absent label. -/
138 theorem primaryResidueMap_surjective (p : R) :
139     Function.Surjective (primaryResidueMap q e he p) :=
140   residueFiberMap_surjective _ _ _ _
141 
142 /-- The literal quotient by p is the selected residue-field fibre. -/
143 def primaryProductQuotientEquiv (p : R) (hp : Irreducible p) :
144     ScalarQuotient ((i : ι) → R ⧸ Ideal.span {q i ^ e i}) p ≃ₗ[R ⧸ Ideal.span {p}]
145       ({i : ι // Ideal.span {q i} = Ideal.span {p}} → R ⧸ Ideal.span {p}) :=
146   scalarQuotientEquiv p (primaryResidueMap q e he p)
147     (primaryResidueMap_surjective q e he p) (primaryResidueMap_ker q hq e he p hp)
148 
149 end PrimaryProduct
150 
151 section Transport
152 variable {M : Type v} [AddCommGroup M] [Module R M]
153 variable {N : Type w} [AddCommGroup N] [Module R N]
154 
155 /-- The exact scalar image is preserved by an actual module equivalence. -/
156 theorem quotientAfterEquiv_ker (p : R) (f : M ≃ₗ[R] N) :
157     ((p • (⊤ : Submodule R N)).mkQ.comp f.toLinearMap).ker =
158       p • (⊤ : Submodule R M) := by
159   ext x
160   change Submodule.Quotient.mk (f x) = (0 : ScalarQuotient N p) ↔ _
161   rw [Submodule.Quotient.mk_eq_zero, mem_scalarImage_iff, mem_scalarImage_iff]
162   constructor
163   · rintro ⟨y, hy⟩
164     refine ⟨f.symm y, ?_⟩
165     apply f.injective
166     simpa only [map_smul, f.apply_symm_apply] using hy
167   · rintro ⟨y, rfl⟩
168     exact ⟨f y, (f.map_smul p y).symm⟩
169 
170 /-- Quotients by scalar images transport linearly over the residue ring. -/
171 def scalarQuotientCongr (p : R) (f : M ≃ₗ[R] N) :
172     ScalarQuotient M p ≃ₗ[R ⧸ Ideal.span {p}] ScalarQuotient N p :=
173   scalarQuotientEquiv p ((p • (⊤ : Submodule R N)).mkQ.comp f.toLinearMap)
174     ((p • (⊤ : Submodule R N)).mkQ_surjective.comp f.surjective)
175     (quotientAfterEquiv_ker p f)
176 
177 /-- Transport is the natural map on representatives. -/
178 theorem scalarQuotientCongr_mk (p : R) (f : M ≃ₗ[R] N) (x : M) :
179     scalarQuotientCongr p f (Submodule.Quotient.mk x) =
180       Submodule.Quotient.mk (f x) :=
181   scalarQuotientEquiv_mk p _ _ _ x
182 end Transport
183 end Komorebi.PaperICompletion4.ResidueQuotient

Back to source controls