PowerSeriesComponent.lean

1 import PaperXII.ModuleSupport
2 import Mathlib.RingTheory.MvPowerSeries.Equiv
3 import Mathlib.RingTheory.PowerSeries.NoZeroDivisors
4 import Mathlib.RingTheory.Ideal.Quotient.Operations
5 import Mathlib.RingTheory.Spectrum.Prime.Topology
6 
7 /-! Paper XII, claim 7.3: the actual formal node k[[x,y]]/(xy).
8 The two variables are indexed by `Option Unit`: none is x and some () is y. -/
9 namespace PaperXII.PowerSeriesComponent
10 
11 noncomputable section
12 variable (k : Type*) [Field k]
13 
14 abbrev Series := MvPowerSeries (Option Unit) k
15 
16 def xSeries : Series k := MvPowerSeries.X none
17 def ySeries : Series k := MvPowerSeries.X (some ())
18 
19 def xExpansion : Series k ≃+* PowerSeries (PowerSeries k) :=
20   (MvPowerSeries.optionEquivLeft Unit k).toRingEquiv
21 
22 def yExpansion : Series k ≃+* PowerSeries (PowerSeries k) :=
23   ((MvPowerSeries.renameEquiv k (Equiv.swap none (some ()))).trans
24     (MvPowerSeries.optionEquivLeft Unit k)).toRingEquiv
25 
26 @[simp] theorem xExpansion_x : xExpansion k (xSeries k) = PowerSeries.X := by
27   simp [xExpansion, xSeries]
28 @[simp] theorem xExpansion_y : xExpansion k (ySeries k) = PowerSeries.C PowerSeries.X := by
29   simp [xExpansion, ySeries, PowerSeries.X]
30 @[simp] theorem yExpansion_x : yExpansion k (xSeries k) = PowerSeries.C PowerSeries.X := by
31   simp [yExpansion, xSeries, MvPowerSeries.renameEquiv, PowerSeries.X]
32 @[simp] theorem yExpansion_y : yExpansion k (ySeries k) = PowerSeries.X := by
33   simp [yExpansion, ySeries, MvPowerSeries.renameEquiv]
34 
35 def evaluateX : Series k →+* PowerSeries k :=
36   PowerSeries.constantCoeff.comp (xExpansion k).toRingHom
37 
38 def evaluateY : Series k →+* PowerSeries k :=
39   PowerSeries.constantCoeff.comp (yExpansion k).toRingHom
40 
41 @[simp] theorem evaluateX_x : evaluateX k (xSeries k) = 0 := by simp [evaluateX]
42 @[simp] theorem evaluateX_y : evaluateX k (ySeries k) = PowerSeries.X := by simp [evaluateX]
43 @[simp] theorem evaluateY_x : evaluateY k (xSeries k) = PowerSeries.X := by simp [evaluateY]
44 @[simp] theorem evaluateY_y : evaluateY k (ySeries k) = 0 := by simp [evaluateY]
45 
46 theorem expansion_kernel {A : Type*} [CommRing A]
47     (e : A ≃+* PowerSeries (PowerSeries k)) (a : A) (ha : e a = PowerSeries.X) :
48     RingHom.ker (PowerSeries.constantCoeff.comp e.toRingHom) = Ideal.span {a} := by
49   ext f
50   simp only [RingHom.mem_ker, RingHom.coe_comp, Function.comp_apply,
51     Ideal.mem_span_singleton]
52   rw [← PowerSeries.X_dvd_iff, ← ha]
53   constructor
54   · rintro ⟨b, hb⟩
55     refine ⟨e.symm b, e.injective ?_⟩
56     simpa using hb
57   · rintro ⟨b, rfl⟩
58     exact ⟨e b, map_mul e a b⟩
59 
60 theorem ker_evaluateX : RingHom.ker (evaluateX k) = Ideal.span {xSeries k} :=
61   expansion_kernel k (xExpansion k) (xSeries k) (xExpansion_x k)
62 theorem ker_evaluateY : RingHom.ker (evaluateY k) = Ideal.span {ySeries k} :=
63   expansion_kernel k (yExpansion k) (ySeries k) (yExpansion_y k)
64 
65 def nodeIdeal : Ideal (Series k) := Ideal.span {xSeries k * ySeries k}
66 abbrev Node := Series k ⧸ nodeIdeal k
67 
68 def x : Node k := Ideal.Quotient.mk (nodeIdeal k) (xSeries k)
69 def y : Node k := Ideal.Quotient.mk (nodeIdeal k) (ySeries k)
70 
71 theorem xy_zero : x k * y k = 0 := by
72   rw [x, y, ← map_mul, Ideal.Quotient.eq_zero_iff_mem]
73   exact Ideal.subset_span (Set.mem_singleton _)
74 
75 def toYAxis : Node k →+* PowerSeries k :=
76   Ideal.Quotient.lift (nodeIdeal k) (evaluateX k) (by
77     change nodeIdeal k ≤ RingHom.ker (evaluateX k)
78     rw [nodeIdeal, Ideal.span_le]
79     rintro a rfl
80     simp) 
81 
82 def toXAxis : Node k →+* PowerSeries k :=
83   Ideal.Quotient.lift (nodeIdeal k) (evaluateY k) (by
84     change nodeIdeal k ≤ RingHom.ker (evaluateY k)
85     rw [nodeIdeal, Ideal.span_le]
86     rintro a rfl
87     simp)
88 
89 @[simp] theorem toYAxis_x : toYAxis k (x k) = 0 := by simp [toYAxis, x]
90 @[simp] theorem toYAxis_y : toYAxis k (y k) = PowerSeries.X := by simp [toYAxis, y]
91 @[simp] theorem toXAxis_x : toXAxis k (x k) = PowerSeries.X := by simp [toXAxis, x]
92 @[simp] theorem toXAxis_y : toXAxis k (y k) = 0 := by simp [toXAxis, y]
93 
94 theorem toYAxis_surjective : Function.Surjective (toYAxis k) := by
95   intro f
96   refine ⟨Ideal.Quotient.mk _ ((xExpansion k).symm (PowerSeries.C f)), ?_⟩
97   simp [toYAxis, evaluateX]
98 
99 theorem toXAxis_surjective : Function.Surjective (toXAxis k) := by
100   intro f
101   refine ⟨Ideal.Quotient.mk _ ((yExpansion k).symm (PowerSeries.C f)), ?_⟩
102   simp [toXAxis, evaluateY]
103 
104 def xIdeal : Ideal (Node k) := Ideal.span {x k}
105 def yIdeal : Ideal (Node k) := Ideal.span {y k}
106 
107 set_option backward.isDefEq.respectTransparency false in
108 theorem ker_toYAxis : RingHom.ker (toYAxis k) = xIdeal k := by
109   rw [toYAxis, Ideal.ker_quotient_lift, ker_evaluateX, Ideal.map_span]
110   simp [xIdeal, x]
111 
112 set_option backward.isDefEq.respectTransparency false in
113 theorem ker_toXAxis : RingHom.ker (toXAxis k) = yIdeal k := by
114   rw [toXAxis, Ideal.ker_quotient_lift, ker_evaluateY, Ideal.map_span]
115   simp [yIdeal, y]
116 
117 abbrev Carrier := Node k ⧸ xIdeal k
118 
119 def carrierEquiv : Carrier k ≃+* PowerSeries k :=
120   (Ideal.quotEquivOfEq (ker_toYAxis k).symm).trans
121     (RingHom.quotientKerEquivOfSurjective (toYAxis_surjective k))
122 
123 
124 /-- The quotient equivalence is the canonical operation of setting x to zero. -/
125 theorem carrierEquiv_mk (f : Series k) :
126     carrierEquiv k (Ideal.Quotient.mk (xIdeal k) (Ideal.Quotient.mk (nodeIdeal k) f)) =
127       evaluateX k f := by
128   rw [carrierEquiv, RingEquiv.trans_apply, Ideal.quotEquivOfEq_mk,
129     RingHom.quotientKerEquivOfSurjective_apply_mk]
130   rfl
131 
132 theorem xIdeal_prime : (xIdeal k).IsPrime := by
133   rw [← ker_toYAxis]
134   exact RingHom.ker_isPrime (toYAxis k)
135 
136 theorem yIdeal_prime : (yIdeal k).IsPrime := by
137   rw [← ker_toXAxis]
138   exact RingHom.ker_isPrime (toXAxis k)
139 
140 theorem x_notMem_yIdeal : x k ∉ yIdeal k := by
141   rw [← ker_toXAxis, RingHom.mem_ker, toXAxis_x]
142   exact PowerSeries.X_ne_zero
143 
144 theorem y_notMem_xIdeal : y k ∉ xIdeal k := by
145   rw [← ker_toYAxis, RingHom.mem_ker, toYAxis_y]
146   exact PowerSeries.X_ne_zero
147 
148 theorem xIdeal_minimalPrime : IsMinimalPrime (xIdeal k) := by
149   rw [IsMinimalPrime.iff_minimal]
150   refine ⟨xIdeal_prime k, ?_⟩
151   intro q hq hqx
152   rw [xIdeal, Ideal.span_singleton_le_iff_mem]
153   have hxy : x k * y k ∈ q := by rw [xy_zero]; exact q.zero_mem
154   exact (hq.mem_or_mem hxy).resolve_right (fun hy ↦ y_notMem_xIdeal k (hqx hy))
155 
156 theorem yIdeal_minimalPrime : IsMinimalPrime (yIdeal k) := by
157   rw [IsMinimalPrime.iff_minimal]
158   refine ⟨yIdeal_prime k, ?_⟩
159   intro q hq hqy
160   rw [yIdeal, Ideal.span_singleton_le_iff_mem]
161   have hxy : x k * y k ∈ q := by rw [xy_zero]; exact q.zero_mem
162   exact (hq.mem_or_mem hxy).resolve_left (fun hx ↦ x_notMem_yIdeal k (hqy hx))
163 
164 theorem minimalPrimes_node : minimalPrimes (Node k) = {xIdeal k, yIdeal k} := by
165   ext q
166   constructor
167   · intro hq
168     have hxy : x k * y k ∈ q := by rw [xy_zero]; exact q.zero_mem
169     rcases hq.isPrime.mem_or_mem hxy with hx | hy
170     · have hle : xIdeal k ≤ q := by rwa [xIdeal, Ideal.span_singleton_le_iff_mem]
171       have heq : q = xIdeal k := le_antisymm
172         (((IsMinimalPrime.iff_minimal q).mp hq).2 (xIdeal_prime k) hle) hle
173       simp [heq]
174     · have hle : yIdeal k ≤ q := by rwa [yIdeal, Ideal.span_singleton_le_iff_mem]
175       have heq : q = yIdeal k := le_antisymm
176         (((IsMinimalPrime.iff_minimal q).mp hq).2 (yIdeal_prime k) hle) hle
177       simp [heq]
178   · intro hq
179     rcases Set.mem_insert_iff.mp hq with rfl | hq
180     · exact xIdeal_minimalPrime k
181     · obtain rfl := Set.mem_singleton_iff.mp hq
182       exact yIdeal_minimalPrime k
183 
184 def missingPoint : PrimeSpectrum (Node k) := ⟨yIdeal k, yIdeal_prime k⟩
185 
186 theorem missingPoint_generic :
187     IsGenericPoint (missingPoint k) (PrimeSpectrum.zeroLocus (yIdeal k)) := by
188   exact PrimeSpectrum.closure_singleton (missingPoint k)
189 
190 theorem y_component : PrimeSpectrum.zeroLocus (yIdeal k) ∈
191     irreducibleComponents (PrimeSpectrum (Node k)) := by
192   apply PrimeSpectrum.zeroLocus_ideal_mem_irreducibleComponents.mpr
193   rw [(yIdeal_prime k).isRadical.radical]
194   exact yIdeal_minimalPrime k
195 
196 theorem x_component : PrimeSpectrum.zeroLocus (xIdeal k) ∈
197     irreducibleComponents (PrimeSpectrum (Node k)) := by
198   apply PrimeSpectrum.zeroLocus_ideal_mem_irreducibleComponents.mpr
199   rw [(xIdeal_prime k).isRadical.radical]
200   exact xIdeal_minimalPrime k
201 
202 theorem annihilator_carrier : Module.annihilator (Node k) (Carrier k) = xIdeal k :=
203   Ideal.annihilator_quotient
204 
205 theorem support_carrier : Module.support (Node k) (Carrier k) =
206     PrimeSpectrum.zeroLocus (xIdeal k) := by
207   rw [Module.support_eq_zeroLocus, annihilator_carrier]
208 
209 theorem missingPoint_not_support : missingPoint k ∉ Module.support (Node k) (Carrier k) := by
210   rw [support_carrier]
211   intro h
212   exact x_notMem_yIdeal k (h (Ideal.mem_span_singleton_self (x k)))
213 
214 theorem carrier_not_full_support :
215     ¬ PaperXII.ModuleSupport.FullSupport (Node k) (Carrier k) := by
216   intro h
217   exact missingPoint_not_support k (by rw [PaperXII.ModuleSupport.FullSupport] at h; simp [h])
218 
219 /-- The node has precisely its two axis components. -/
220 theorem irreducibleComponents_node : irreducibleComponents (PrimeSpectrum (Node k)) =
221     {PrimeSpectrum.zeroLocus (xIdeal k), PrimeSpectrum.zeroLocus (yIdeal k)} := by
222   rw [← PrimeSpectrum.zeroLocus_minimalPrimes, minimalPrimes_node]
223   simp
224 
225 theorem components_distinct : PrimeSpectrum.zeroLocus (xIdeal k : Set (Node k)) ≠
226     PrimeSpectrum.zeroLocus (yIdeal k : Set (Node k)) := by
227   intro h
228   apply missingPoint_not_support k
229   rw [support_carrier, h]
230   exact fun _ ha ↦ ha
231 
232 /-- Manuscript 7.3, for an arbitrary field and the literal formal power-series node. -/
233 theorem node_quotient_misses_component :
234     Function.Surjective (Ideal.Quotient.mk (xIdeal k)) ∧
235     Nonempty (Carrier k ≃+* PowerSeries k) ∧
236     Module.support (Node k) (Carrier k) = PrimeSpectrum.zeroLocus (xIdeal k) ∧
237     IsGenericPoint (missingPoint k) (PrimeSpectrum.zeroLocus (yIdeal k)) ∧
238     PrimeSpectrum.zeroLocus (yIdeal k) ∈ irreducibleComponents (PrimeSpectrum (Node k)) ∧
239     missingPoint k ∉ Module.support (Node k) (Carrier k) ∧
240     ¬ PaperXII.ModuleSupport.FullSupport (Node k) (Carrier k) :=
241   ⟨Ideal.Quotient.mk_surjective, ⟨carrierEquiv k⟩, support_carrier k,
242     missingPoint_generic k, y_component k, missingPoint_not_support k,
243     carrier_not_full_support k⟩
244 
245 end
246 end PaperXII.PowerSeriesComponent

Back to source controls