ReleaseGluing.lean

1 import Mathlib.LinearAlgebra.Quotient.Basic
2 import Mathlib.Algebra.Module.Submodule.Lattice
3 import Mathlib.Data.Fintype.BigOperators
4 
5 /-!
6 # Actual lattice gluing quotients
7 
8 The constructions use O-submodules and their actual quotients.  The algebraic
9 core holds over any commutative ring.  Rational projectors on a K-vector space
10 are used here by restricting scalars along O → K.  No quotient, injectivity,
11 annihilator, or splitting conclusion is supplied as a certificate.
12 -/
13 
14 set_option autoImplicit false
15 open scoped BigOperators
16 
17 namespace Komorebi.PaperII.ReleaseGluing
18 
19 universe u v w
20 variable {O : Type u} {V : Type v} {I : Type w}
21 variable [CommRing O] [AddCommGroup V] [Module O V] [Fintype I]
22 
23 /-- A finite complete orthogonal family; zero packets are harmless to the quotient construction. -/
24 structure Projectors (O : Type u) (V : Type v) (I : Type w)
25     [CommRing O] [AddCommGroup V] [Module O V] [Fintype I] where
26   proj : I → Module.End O V
27   idem : ∀ i, proj i * proj i = proj i
28   orthogonal : ∀ i j, i ≠ j → proj i * proj j = 0
29   complete : ∑ i, proj i = 1
30 
31 variable (P : Projectors O V I) (Λ : Submodule O V)
32 
33 theorem reconstruct (x : V) : ∑ i, P.proj i x = x := by
34   simpa only [LinearMap.sum_apply, Module.End.one_apply] using
35     LinearMap.congr_fun P.complete x
36 
37 theorem proj_idem (i : I) (x : V) : P.proj i (P.proj i x) = P.proj i x :=
38   LinearMap.congr_fun (P.idem i) x
39 
40 theorem proj_other (i j : I) (hij : i ≠ j) (x : V) :
41     P.proj i (P.proj j x) = 0 :=
42   LinearMap.congr_fun (P.orthogonal i j hij) x
43 
44 /-- Λ_i = Λ ∩ im(E_i), as an O-submodule of the ambient space. -/
45 def packetLattice (i : I) : Submodule O V := Λ ⊓ LinearMap.range (P.proj i)
46 
47 /-- The actual split sublattice, the finite sum of packet intersections. -/
48 def splitLattice : Submodule O V := ⨆ i, packetLattice P Λ i
49 
50 theorem splitLattice_le : splitLattice P Λ ≤ Λ :=
51   iSup_le fun _ => inf_le_left
52 
53 theorem proj_mem_of_mem_packetLattice (i j : I) {x : V}
54     (hx : x ∈ packetLattice P Λ j) : P.proj i x ∈ Λ := by
55   classical
56   obtain ⟨hxΛ, y, hy⟩ := hx
57   by_cases hij : i = j
58   · subst j
59     rw [← hy, proj_idem]
60     exact hy ▸ hxΛ
61   · rw [← hy, proj_other P i j hij]
62     exact Λ.zero_mem
63 
64 theorem proj_mem_of_mem_split (i : I) {x : V}
65     (hx : x ∈ splitLattice P Λ) : P.proj i x ∈ Λ := by
66   have hle : splitLattice P Λ ≤ Λ.comap (P.proj i) :=
67     iSup_le fun j => fun y hy => proj_mem_of_mem_packetLattice P Λ i j hy
68   exact hle hx
69 
70 /-- Membership in the split sublattice is exactly integrality of every packet component. -/
71 theorem mem_splitLattice_iff (x : V) :
72     x ∈ splitLattice P Λ ↔ ∀ i, P.proj i x ∈ Λ := by
73   constructor
74   · intro hx i
75     exact proj_mem_of_mem_split P Λ i hx
76   · intro hx
77     rw [← reconstruct P x]
78     exact Submodule.sum_mem_iSup fun i => ⟨hx i, x, rfl⟩
79 
80 /-- Applying a packet projector recovers its summand in a sum of packet intersections. -/
81 theorem project_sum_packet_components (x : I → V)
82     (hx : ∀ i, x i ∈ packetLattice P Λ i) (i : I) :
83     P.proj i (∑ j, x j) = x i := by
84   classical
85   rw [map_sum, Finset.sum_eq_single i]
86   · obtain ⟨_hi, y, hy⟩ := hx i
87     rw [← hy, proj_idem]
88   · intro j _hj hji
89     obtain ⟨_hi, y, hy⟩ := hx j
90     rw [← hy, proj_other P i j hji.symm]
91   · simp
92 
93 /-- The sum defining the split lattice is internal: its packet components are independent. -/
94 theorem sum_packet_components_eq_zero_iff (x : I → V)
95     (hx : ∀ i, x i ∈ packetLattice P Λ i) :
96     (∑ i, x i) = 0 ↔ ∀ i, x i = 0 := by
97   constructor
98   · intro h i
99     have hi := project_sum_packet_components P Λ x hx i
100     rw [h, map_zero] at hi
101     exact hi.symm
102   · intro h
103     simp only [h, Finset.sum_const_zero]
104 
105 /-- The split lattice as a submodule of Λ itself. -/
106 def splitInside : Submodule O Λ := (splitLattice P Λ).comap Λ.subtype
107 
108 /-- The manuscript's gluing module Λ / ⊕_i(Λ ∩ im(E_i)). -/
109 abbrev GluingModule := Λ ⧸ splitInside P Λ
110 
111 /-- The projected lattice E_i Λ. -/
112 def projectedLattice (i : I) : Submodule O V := Λ.map (P.proj i)
113 
114 /-- Its integral part, as a submodule of E_i Λ.  Its ambient image is Λ_i. -/
115 def projectedIntegral (i : I) : Submodule O (projectedLattice P Λ i) :=
116   Λ.comap (projectedLattice P Λ i).subtype
117 
118 theorem projectedIntegral_ambient (i : I) (x : projectedLattice P Λ i) :
119     x ∈ projectedIntegral P Λ i ↔ (x : V) ∈ packetLattice P Λ i := by
120   constructor
121   · intro hx
122     refine ⟨hx, ?_⟩
123     obtain ⟨y, _hy, hyeq⟩ := x.property
124     exact ⟨y, hyeq⟩
125   · exact fun hx => hx.1
126 
127 abbrev CoordinateQuotient (i : I) :=
128   projectedLattice P Λ i ⧸ projectedIntegral P Λ i
129 
130 /-- The genuine projection of an element of Λ into its projected lattice. -/
131 def projectionToLattice (i : I) : Λ →ₗ[O] projectedLattice P Λ i :=
132   ((P.proj i).comp Λ.subtype).codRestrict _ fun x => ⟨x, x.property, rfl⟩
133 
134 theorem projectionToLattice_surjective (i : I) :
135     Function.Surjective (projectionToLattice P Λ i) := by
136   intro y
137   obtain ⟨x, hx, heq⟩ := y.property
138   refine ⟨⟨x, hx⟩, ?_⟩
139   exact Subtype.ext heq
140 
141 def rawCoordinate (i : I) : Λ →ₗ[O] CoordinateQuotient P Λ i :=
142   (projectedIntegral P Λ i).mkQ.comp (projectionToLattice P Λ i)
143 
144 theorem rawCoordinate_eq_zero_iff (i : I) (x : Λ) :
145     rawCoordinate P Λ i x = 0 ↔ P.proj i x ∈ Λ := by
146   change ((projectedIntegral P Λ i).mkQ (projectionToLattice P Λ i x) = 0) ↔ _
147   rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]
148   rfl
149 
150 theorem splitInside_le_ker_rawCoordinate (i : I) :
151     splitInside P Λ ≤ LinearMap.ker (rawCoordinate P Λ i) := by
152   intro x hx
153   exact (rawCoordinate_eq_zero_iff P Λ i x).mpr (proj_mem_of_mem_split P Λ i hx)
154 
155 /-- One coordinate of the actual gluing homomorphism. -/
156 def gluingCoordinate (i : I) : GluingModule P Λ →ₗ[O] CoordinateQuotient P Λ i :=
157   (splitInside P Λ).liftQ (rawCoordinate P Λ i) (splitInside_le_ker_rawCoordinate P Λ i)
158 
159 /-- The canonical map [x] ↦ ([E_i x])_i into the finite product of packet quotients. -/
160 def gluingMap : GluingModule P Λ →ₗ[O] (∀ i, CoordinateQuotient P Λ i) :=
161   LinearMap.pi (gluingCoordinate P Λ)
162 
163 theorem gluingCoordinate_mk (i : I) (x : Λ) :
164     gluingCoordinate P Λ i ((splitInside P Λ).mkQ x) = rawCoordinate P Λ i x := rfl
165 
166 theorem gluingMap_injective : Function.Injective (gluingMap P Λ) := by
167   apply (LinearMap.ker_eq_bot).mp
168   apply le_antisymm
169   · intro z hz
170     obtain ⟨x, rfl⟩ := (splitInside P Λ).mkQ_surjective z
171     have hx : x ∈ splitInside P Λ := by
172       apply (mem_splitLattice_iff P Λ x).mpr
173       intro i
174       apply (rawCoordinate_eq_zero_iff P Λ i x).mp
175       exact congrFun hz i
176     simpa only [Submodule.mem_bot, Submodule.mkQ_apply,
177       Submodule.Quotient.mk_eq_zero] using hx
178   · exact bot_le
179 
180 theorem gluingCoordinate_surjective (i : I) :
181     Function.Surjective (gluingCoordinate P Λ i) := by
182   intro y
183   obtain ⟨v, rfl⟩ := (projectedIntegral P Λ i).mkQ_surjective y
184   obtain ⟨x, rfl⟩ := projectionToLattice_surjective P Λ i v
185   exact ⟨(splitInside P Λ).mkQ x, rfl⟩
186 
187 /-- An actual scalar annihilates the gluing quotient precisely when it sends Λ into the split lattice. -/
188 theorem annihilates_gluing_iff (a : O) :
189     (∀ z : GluingModule P Λ, a • z = 0) ↔
190       ∀ x : V, x ∈ Λ → a • x ∈ splitLattice P Λ := by
191   constructor
192   · intro h x hx
193     have heq := h ((splitInside P Λ).mkQ ⟨x, hx⟩)
194     rw [← map_smul, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero] at heq
195     exact heq
196   · intro h z
197     obtain ⟨x, rfl⟩ := (splitInside P Λ).mkQ_surjective z
198     rw [← map_smul, Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]
199     exact h x x.property
200 
201 /-- The exact exponent-level gluing theorem, before taking least exponents. -/
202 theorem annihilates_gluing_iff_clears (pi : O) (s : ℕ) :
203     (∀ z : GluingModule P Λ, (pi ^ s) • z = 0) ↔
204       ∀ i x, x ∈ Λ → (pi ^ s) • P.proj i x ∈ Λ := by
205   rw [annihilates_gluing_iff]
206   constructor
207   · intro h i x hx
208     simpa only [map_smul] using (mem_splitLattice_iff P Λ _).mp (h x hx) i
209   · intro h x hx
210     apply (mem_splitLattice_iff P Λ _).mpr
211     intro i
212     simpa only [map_smul] using h i x hx
213 
214 /-- Integral splitting is equivalent to integral action of every packet projector. -/
215 theorem splitLattice_eq_iff : splitLattice P Λ = Λ ↔
216     ∀ i x, x ∈ Λ → P.proj i x ∈ Λ := by
217   constructor
218   · intro h i x hx
219     exact proj_mem_of_mem_split P Λ i (h.symm ▸ hx)
220   · intro h
221     apply le_antisymm (splitLattice_le P Λ)
222     intro x hx
223     exact (mem_splitLattice_iff P Λ x).mpr fun i => h i x hx
224 
225 /-- A packet's clearing predicate; this is integrality of the scaled actual operator. -/
226 def ClearsPacket (pi : O) (i : I) (s : ℕ) : Prop :=
227   ∀ x : V, x ∈ Λ → (pi ^ s) • P.proj i x ∈ Λ
228 
229 theorem clearsPacket_mono (pi : O) (i : I) {s t : ℕ}
230     (hs : ClearsPacket P Λ pi i s) (hst : s ≤ t) :
231     ClearsPacket P Λ pi i t := by
232   intro x hx
233   have ht : t = (t - s) + s := (Nat.sub_add_cancel hst).symm
234   rw [ht, pow_add, mul_smul]
235   exact Λ.smul_mem _ (hs x hx)
236 
237 /-- Least packet weight, with the existence proof explicitly attached. -/
238 noncomputable def packetWeight (pi : O) (i : I)
239     (finite : ∃ s, ClearsPacket P Λ pi i s) : ℕ := by
240   classical
241   exact Nat.find finite
242 
243 theorem clearsPacket_iff_weight_le (pi : O) (i : I)
244     (finite : ∃ s, ClearsPacket P Λ pi i s) (s : ℕ) :
245     ClearsPacket P Λ pi i s ↔ packetWeight P Λ pi i finite ≤ s := by
246   classical
247   constructor
248   · exact Nat.find_min' finite
249   · exact clearsPacket_mono P Λ pi i (Nat.find_spec finite)
250 
251 /-- The maximum of the genuine least packet weights; the empty maximum is zero. -/
252 noncomputable def globalWeight (pi : O)
253     (finite : ∀ i, ∃ s, ClearsPacket P Λ pi i s) : ℕ :=
254   Finset.univ.sup fun i => packetWeight P Λ pi i (finite i)
255 
256 theorem gluing_annihilated_iff_globalWeight_le (pi : O)
257     (finite : ∀ i, ∃ s, ClearsPacket P Λ pi i s) (s : ℕ) :
258     (∀ z : GluingModule P Λ, (pi ^ s) • z = 0) ↔ globalWeight P Λ pi finite ≤ s := by
259   rw [annihilates_gluing_iff_clears]
260   change (∀ i, ClearsPacket P Λ pi i s) ↔ _
261   simp only [globalWeight, Finset.sup_le_iff, Finset.mem_univ, true_implies]
262   exact forall_congr' fun i => clearsPacket_iff_weight_le P Λ pi i (finite i) s
263 
264 theorem gluing_finite_exponent (pi : O)
265     (finite : ∀ i, ∃ s, ClearsPacket P Λ pi i s) :
266     ∃ s : ℕ, ∀ z : GluingModule P Λ, (pi ^ s) • z = 0 :=
267   ⟨globalWeight P Λ pi finite,
268     (gluing_annihilated_iff_globalWeight_le P Λ pi finite _).mpr le_rfl⟩
269 
270 /-- Vanishing of the global weight is exactly integral splitting. -/
271 theorem globalWeight_eq_zero_iff_splitLattice_eq (pi : O)
272     (finite : ∀ i, ∃ s, ClearsPacket P Λ pi i s) :
273     globalWeight P Λ pi finite = 0 ↔ splitLattice P Λ = Λ := by
274   rw [← Nat.le_zero, ← gluing_annihilated_iff_globalWeight_le P Λ pi finite 0,
275     annihilates_gluing_iff_clears, splitLattice_eq_iff]
276   simp only [pow_zero, one_smul]
277 
278 /-- The actual gluing quotient vanishes exactly when the global weight is zero. -/
279 theorem globalWeight_eq_zero_iff_subsingleton (pi : O)
280     (finite : ∀ i, ∃ s, ClearsPacket P Λ pi i s) :
281     globalWeight P Λ pi finite = 0 ↔ Subsingleton (GluingModule P Λ) := by
282   rw [← Nat.le_zero, ← gluing_annihilated_iff_globalWeight_le P Λ pi finite 0]
283   simp only [pow_zero, one_smul]
284   constructor
285   · intro h
286     exact ⟨fun x y => (h x).trans (h y).symm⟩
287   · intro h x
288     exact @Subsingleton.elim _ h x 0
289 
290 /-- An individual packet quotient has precisely the packet clearing annihilators. -/
291 theorem annihilates_coordinate_iff_clears (pi : O) (i : I) (s : ℕ) :
292     (∀ z : CoordinateQuotient P Λ i, (pi ^ s) • z = 0) ↔
293       ClearsPacket P Λ pi i s := by
294   constructor
295   · intro h x hx
296     have hz := h (rawCoordinate P Λ i ⟨x, hx⟩)
297     rw [← map_smul] at hz
298     have hm := (rawCoordinate_eq_zero_iff P Λ i ((pi ^ s) • (⟨x, hx⟩ : Λ))).mp hz
299     simpa only [Submodule.coe_smul, map_smul] using hm
300   · intro h z
301     obtain ⟨q, rfl⟩ := gluingCoordinate_surjective P Λ i z
302     obtain ⟨x, rfl⟩ := (splitInside P Λ).mkQ_surjective q
303     rw [gluingCoordinate_mk, ← map_smul]
304     apply (rawCoordinate_eq_zero_iff P Λ i _).mpr
305     simpa only [Submodule.coe_smul, map_smul] using h x x.property
306 
307 noncomputable def gluingExponent (pi : O)
308     (finite : ∀ i, ∃ s, ClearsPacket P Λ pi i s) : ℕ := by
309   classical
310   exact Nat.find (gluing_finite_exponent P Λ pi finite)
311 
312 /-- The exponent of the actual gluing quotient equals the maximum of the least packet weights. -/
313 theorem gluing_exponent_eq_globalWeight (pi : O)
314     (finite : ∀ i, ∃ s, ClearsPacket P Λ pi i s) :
315     gluingExponent P Λ pi finite = globalWeight P Λ pi finite := by
316   classical
317   unfold gluingExponent
318   apply le_antisymm
319   · exact Nat.find_min' _
320       ((gluing_annihilated_iff_globalWeight_le P Λ pi finite _).mpr le_rfl)
321   · exact (gluing_annihilated_iff_globalWeight_le P Λ pi finite _).mp
322       (Nat.find_spec (gluing_finite_exponent P Λ pi finite))
323 
324 section Refinement
325 variable {J : Type*} [Fintype J] (Q : Projectors O V J)
326 
327 /-- Range containment is the exact part of refinement needed by lattice gluing. -/
328 theorem splitLattice_le_of_refines
329     (parent : J → I)
330     (hrange : ∀ j, LinearMap.range (Q.proj j) ≤ LinearMap.range (P.proj (parent j))) :
331     splitLattice Q Λ ≤ splitLattice P Λ := by
332   apply iSup_le
333   intro j
334   exact le_iSup_of_le (parent j) (inf_le_inf_left Λ (hrange j))
335 
336 theorem splitInside_le_of_refines
337     (parent : J → I)
338     (hrange : ∀ j, LinearMap.range (Q.proj j) ≤ LinearMap.range (P.proj (parent j))) :
339     splitInside Q Λ ≤ splitInside P Λ :=
340   Submodule.comap_mono (splitLattice_le_of_refines P Λ Q parent hrange)
341 
342 theorem globalWeight_mono_of_refines (pi : O)
343     (finiteP : ∀ i, ∃ s, ClearsPacket P Λ pi i s)
344     (finiteQ : ∀ j, ∃ s, ClearsPacket Q Λ pi j s)
345     (parent : J → I)
346     (hrange : ∀ j, LinearMap.range (Q.proj j) ≤ LinearMap.range (P.proj (parent j))) :
347     globalWeight P Λ pi finiteP ≤ globalWeight Q Λ pi finiteQ := by
348   apply (gluing_annihilated_iff_globalWeight_le P Λ pi finiteP _).mp
349   apply (annihilates_gluing_iff P Λ _).mpr
350   intro x hx
351   apply splitLattice_le_of_refines P Λ Q parent hrange
352   apply (annihilates_gluing_iff Q Λ _).mp
353     ((gluing_annihilated_iff_globalWeight_le Q Λ pi finiteQ _).mpr le_rfl) x hx
354 
355 end Refinement
356 
357 section NestedQuotients
358 variable {W : Type*} [AddCommGroup W] [Module O W]
359 variable (S T : Submodule O W) (hST : S ≤ T)
360 
361 /-- The inclusion T/S → W/S for genuinely nested submodules. -/
362 def quotientInclusion : (T ⧸ S.comap T.subtype) →ₗ[O] W ⧸ S :=
363   (S.comap T.subtype).mapQ S T.subtype le_rfl
364 
365 theorem quotientInclusion_injective :
366     Function.Injective (quotientInclusion S T) := by
367   apply LinearMap.ker_eq_bot.mp
368   rw [quotientInclusion, Submodule.ker_mapQ]
369   exact Submodule.mkQ_map_self _
370 
371 theorem quotientFactor_surjective : Function.Surjective (Submodule.factor hST) := by
372   intro z
373   obtain ⟨x, rfl⟩ := T.mkQ_surjective z
374   exact ⟨S.mkQ x, rfl⟩
375 
376 theorem quotientInclusion_range_eq_factor_ker :
377     LinearMap.range (quotientInclusion S T) = LinearMap.ker (Submodule.factor hST) := by
378   rw [quotientInclusion, Submodule.range_mapQ, Submodule.range_subtype]
379   rw [Submodule.factor, Submodule.ker_mapQ, Submodule.comap_id]
380 
381 /-- All three exactness obligations of 0 → T/S → W/S → W/T → 0. -/
382 theorem nested_quotient_short_exact :
383     Function.Injective (quotientInclusion S T) ∧
384     LinearMap.range (quotientInclusion S T) = LinearMap.ker (Submodule.factor hST) ∧
385     Function.Surjective (Submodule.factor hST) :=
386   ⟨quotientInclusion_injective S T,
387     quotientInclusion_range_eq_factor_ker S T hST,
388     quotientFactor_surjective S T hST⟩
389 
390 end NestedQuotients
391 
392 /-- The actual gluing short exact sequence for a refinement. -/
393 theorem gluing_refinement_short_exact
394     {J : Type*} [Fintype J] (Q : Projectors O V J) (parent : J → I)
395     (hrange : ∀ j, LinearMap.range (Q.proj j) ≤ LinearMap.range (P.proj (parent j))) :
396     let h := splitInside_le_of_refines P Λ Q parent hrange
397     Function.Injective (quotientInclusion (splitInside Q Λ) (splitInside P Λ)) ∧
398     LinearMap.range (quotientInclusion (splitInside Q Λ) (splitInside P Λ)) =
399       LinearMap.ker (Submodule.factor h) ∧
400     Function.Surjective (Submodule.factor h) := by
401   exact nested_quotient_short_exact _ _ (splitInside_le_of_refines P Λ Q parent hrange)
402 
403 end Komorebi.PaperII.ReleaseGluing

Back to source controls