ArtinModules.lean

1 import PaperXII.ArtinData
2 import PaperXII.PacketTrace
3 import Mathlib.RingTheory.Idempotents
4 import Mathlib.Algebra.DirectSum.Module
5 import Mathlib.RingTheory.Support
6 
7 set_option autoImplicit false
8 
9 open scoped DirectSum
10 
11 /-! Paper XII, Theorem 8.2: actual scalar-action packets, their direct sum,
12 and their canonical identification with localized modules. -/
13 namespace PaperXII.ArtinModules
14 
15 variable {R V I : Type*} [CommRing R] [AddCommGroup V] [Module R V]
16 
17 /-- The actual submodule fixed by an idempotent, equal to its scalar-action image. -/
18 def packet (e : R) : Submodule R V where
19   carrier := {v | e • v = v}
20   zero_mem' := smul_zero e
21   add_mem' hv hw := by simp only [Set.mem_ofPred_eq] at *; rw [smul_add, hv, hw]
22   smul_mem' r v hv := by
23     simp only [Set.mem_ofPred_eq] at *
24     rw [smul_comm e r, hv]
25 
26 theorem mem_packet_iff (e : R) (v : V) : v ∈ packet e ↔ e • v = v := Iff.rfl
27 
28 theorem mem_packet_iff_image {e : R} (he : IsIdempotentElem e) (v : V) :
29     v ∈ packet e ↔ ∃ w : V, e • w = v := by
30   constructor
31   · intro hv
32     exact ⟨v, hv⟩
33   · rintro ⟨w, rfl⟩
34     change e • (e • w) = e • w
35     rw [← mul_smul, he]
36 
37 /-- Projection to the packet is multiplication by the idempotent itself. -/
38 def projection (e : R) (he : IsIdempotentElem e) : V →ₗ[R] packet (V := V) e where
39   toFun v := ⟨e • v, by change e • (e • v) = e • v; rw [← mul_smul, he]⟩
40   map_add' v w := Subtype.ext (smul_add e v w)
41   map_smul' r v := Subtype.ext (smul_comm e r v)
42 
43 theorem projection_apply (e : R) (he : IsIdempotentElem e) (v : V) :
44     (projection e he v : V) = e • v := rfl
45 
46 theorem projection_packet (e : R) (he : IsIdempotentElem e) (v : packet (V := V) e) :
47     projection e he (v : V) = v := Subtype.ext v.property
48 
49 variable [Fintype I] (e : I → R) (he : CompleteOrthogonalIdempotents e)
50 
51 /-- The product of packet projections. -/
52 def toPackets : V →ₗ[R] ∀ i, packet (V := V) (e i) :=
53   LinearMap.pi fun i => projection (e i) (he.idem i)
54 
55 /-- Packet assembly adds their vectors in the original module. -/
56 def fromPackets : (∀ i, packet (V := V) (e i)) →ₗ[R] V where
57   toFun v := ∑ i, (v i : V)
58   map_add' v w := by simp [Finset.sum_add_distrib]
59   map_smul' r v := by simp [Finset.smul_sum]
60 
61 theorem from_to_packets (v : V) : fromPackets e (toPackets e he v) = v := by
62   change ∑ i, e i • v = v
63   rw [← Finset.sum_smul, he.complete, one_smul]
64 
65 theorem to_from_packets (v : ∀ i, packet (V := V) (e i)) :
66     toPackets e he (fromPackets e v) = v := by
67   classical
68   funext i
69   apply Subtype.ext
70   change e i • ∑ j, (v j : V) = (v i : V)
71   rw [Finset.smul_sum, Finset.sum_eq_single i]
72   · exact (v i).property
73   · intro j _ hji
74     calc
75       e i • (v j : V) = e i • (e j • (v j : V)) := congrArg (e i • ·) (v j).property.symm
76       _ = 0 := by rw [← mul_smul, he.ortho (Ne.symm hji), zero_smul]
77   · simp
78 
79 /-- The equivalence has the canonical projections and sum as its two maps. -/
80 def productEquiv : V ≃ₗ[R] ∀ i, packet (V := V) (e i) :=
81   LinearEquiv.ofLinearMap (toPackets e he) (fromPackets e)
82     (LinearMap.ext (to_from_packets e he)) (LinearMap.ext (from_to_packets e he))
83 
84 /-- Finite product and direct sum coincide, yielding the actual direct sum of packets. -/
85 noncomputable def directSumEquiv : V ≃ₗ[R] ⨁ i, packet (V := V) (e i) := by
86   classical
87   exact (productEquiv e he).trans (DirectSum.linearEquivFunOnFintype R I _).symm
88 
89 theorem directSumEquiv_apply (v : V) (i : I) :
90     ((directSumEquiv e he v) i : V) = e i • v := by
91   classical
92   rfl
93 
94 theorem directSumEquiv_symm_apply (v : ⨁ i, packet (V := V) (e i)) :
95     (directSumEquiv e he).symm v = ∑ i, (v i : V) := by
96   classical
97   rfl
98 
99 /-- Every denominator has an inverse on the corresponding idempotent summand. -/
100 theorem denominator_inverse (D : ArtinData.Decomposition R) (m : MaximalSpectrum R)
101     (s : m.asIdeal.primeCompl) :
102     ∃ t : R, (s : R) * t * ArtinData.idempotent D m = ArtinData.idempotent D m := by
103   classical
104   obtain ⟨u, hu⟩ := (IsLocalization.map_units (Localization.AtPrime m.asIdeal) s).exists_right_inv
105   let t : R := D.symm (Pi.single m u)
106   refine ⟨t, ?_⟩
107   apply D.injective
108   ext n
109   simp only [map_mul, Pi.mul_apply, ArtinData.map_idempotent]
110   by_cases hn : n = m
111   · subst n
112     simp only [t, AlgEquiv.apply_symm_apply, Pi.single_eq_same, mul_one]
113     rw [ArtinData.coordinate]
114     exact hu
115   · simp [Pi.single_eq_of_ne hn]
116 
117 /-- Multiplication by every denominator is invertible on the actual packet. -/
118 theorem denominator_unit (D : ArtinData.Decomposition R) (m : MaximalSpectrum R)
119     (s : m.asIdeal.primeCompl) :
120     IsUnit (algebraMap R (Module.End R (packet (V := V) (ArtinData.idempotent D m))) s) := by
121   obtain ⟨t, ht⟩ := denominator_inverse D m s
122   let P := packet (V := V) (ArtinData.idempotent D m)
123   refine ⟨⟨algebraMap R (Module.End R P) s, algebraMap R (Module.End R P) t, ?_, ?_⟩, rfl⟩
124   · ext v
125     change (s : R) • (t • (v : V)) = (v : V)
126     calc
127       _ = ((s : R) * t) • (ArtinData.idempotent D m • (v : V)) := by
128         rw [v.property, mul_smul]
129       _ = v := by rw [← mul_smul, ht, v.property]
130   · ext v
131     change t • ((s : R) • (v : V)) = (v : V)
132     rw [smul_comm t (s : R)]
133     calc
134       _ = ((s : R) * t) • (ArtinData.idempotent D m • (v : V)) := by
135         rw [v.property, mul_smul]
136       _ = v := by rw [← mul_smul, ht, v.property]
137 
138 /-- The projection to the packet satisfies the complete localization specification. -/
139 theorem projection_isLocalizedModule (D : ArtinData.Decomposition R) (m : MaximalSpectrum R) :
140     IsLocalizedModule m.asIdeal.primeCompl
141       (projection (V := V) (ArtinData.idempotent D m) (ArtinData.idem D m)) where
142   map_units := denominator_unit D m
143   surj v := ⟨((v : V), 1), by simpa using (projection_packet _ (ArtinData.idem D m) v).symm⟩
144   exists_of_eq h := ⟨⟨ArtinData.idempotent D m, ArtinData.idempotent_not_mem D m⟩,
145     congrArg Subtype.val h⟩
146 
147 /-- The canonical localization equivalence, derived from the ring decomposition. -/
148 noncomputable def localizationEquiv (D : ArtinData.Decomposition R) (m : MaximalSpectrum R) :
149     packet (V := V) (ArtinData.idempotent D m) ≃ₗ[R]
150       LocalizedModule m.asIdeal.primeCompl V := by
151   letI := projection_isLocalizedModule (V := V) D m
152   exact IsLocalizedModule.linearEquiv m.asIdeal.primeCompl
153     (projection (ArtinData.idempotent D m) (ArtinData.idem D m))
154     (LocalizedModule.mkLinearMap m.asIdeal.primeCompl V)
155 
156 /-- This is the original localization map restricted to the packet. -/
157 theorem localizationEquiv_apply (D : ArtinData.Decomposition R) (m : MaximalSpectrum R)
158     (v : packet (V := V) (ArtinData.idempotent D m)) :
159     localizationEquiv D m v = LocalizedModule.mk (v : V) 1 := by
160   let := projection_isLocalizedModule (V := V) D m
161   have h := IsLocalizedModule.linearEquiv_apply m.asIdeal.primeCompl
162     (projection (ArtinData.idempotent D m) (ArtinData.idem D m))
163     (LocalizedModule.mkLinearMap m.asIdeal.primeCompl V) (v : V)
164   simpa [localizationEquiv, projection_packet] using h
165 
166 /-- Occupancy agrees exactly with the ordinary module support. -/
167 theorem occupied_iff_support (D : ArtinData.Decomposition R) (m : MaximalSpectrum R) :
168     packet (V := V) (ArtinData.idempotent D m) ≠ ⊥ ↔
169       m.toPrimeSpectrum ∈ Module.support R V := by
170   rw [← Submodule.nontrivial_iff_ne_bot, Module.mem_support_iff]
171   exact (localizationEquiv (V := V) D m).toEquiv.nontrivial_congr
172 
173 /-- Paper XII 8.2: the actual canonical direct sum over maximal ideals. -/
174 noncomputable def canonicalDirectSumEquiv [Fintype (MaximalSpectrum R)]
175     (D : ArtinData.Decomposition R) :
176     V ≃ₗ[R] ⨁ m, packet (V := V) (ArtinData.idempotent D m) :=
177   directSumEquiv (ArtinData.idempotent D) (ArtinData.complete D)
178 
179 /-- The R-module packet has exactly the field-linear image used in Corollary 8.4. -/
180 theorem packet_restrictScalars {E : Type*} [Field E] [Algebra E R]
181     [Module E V] [IsScalarTower E R V] {a : R} (ha : IsIdempotentElem a) :
182     (packet (V := V) a).restrictScalars E = PacketTrace.packet (E := E) (V := V) a := by
183   ext v
184   exact (mem_packet_iff_image ha v).trans (PacketTrace.mem_packet_iff a v).symm
185 
186 /-- The source-level Theorem 8.2, with finiteness of the maximal spectrum derived
187 from finite dimension. The only supplied algebraic decomposition is external
188 Fact 8.1; all module maps and support conclusions are constructed here. -/
189 theorem canonical_hecke_packet_decomposition {E : Type*} [Field E] [Algebra E R]
190     [FiniteDimensional E R] [Module.Finite R V] (D : ArtinData.Decomposition R) :
191     ∃ F : V ≃ₗ[R] ⨁ m, packet (V := V) (ArtinData.idempotent D m),
192       (∀ (v : V) (m : MaximalSpectrum R), ((F v) m : V) = ArtinData.idempotent D m • v) ∧
193       (∀ m : MaximalSpectrum R,
194         ∃ L : packet (V := V) (ArtinData.idempotent D m) ≃ₗ[R]
195           LocalizedModule m.asIdeal.primeCompl V,
196           (∀ v, L v = LocalizedModule.mk (v : V) 1) ∧
197           (packet (V := V) (ArtinData.idempotent D m) ≠ ⊥ ↔
198             m.toPrimeSpectrum ∈ Module.support R V)) := by
199   let : IsArtinianRing R := IsArtinianRing.of_finite E R
200   let : Fintype (MaximalSpectrum R) := Fintype.ofFinite _
201   refine ⟨canonicalDirectSumEquiv D, ?_, ?_⟩
202   · exact directSumEquiv_apply (ArtinData.idempotent D) (ArtinData.complete D)
203   · intro m
204     exact ⟨localizationEquiv D m, localizationEquiv_apply D m, occupied_iff_support D m⟩
205 
206 end PaperXII.ArtinModules

Back to source controls