AlgebraPreorder.lean

1 import PaperIRelease.AlgebraSupport
2 import PaperIRelease.AlgebraTransfer
3 import PaperIRelease.PacketAggregation
4 import Mathlib.Order.Antisymmetrization
5 import Mathlib.RingTheory.TwoSidedIdeal.Operations
6 import Mathlib.Order.ConditionallyCompleteLattice.Basic
7 import Mathlib.RingTheory.Ideal.Operations
8 
9 set_option autoImplicit false
10 set_option linter.unusedSectionVars false
11 set_option maxHeartbeats 3000000
12 noncomputable section
13 
14 namespace Komorebi.PaperIRelease
15 open Komorebi.Foundation
16 
17 universe u v w
18 variable {K : Type u} [Field K]
19 variable {X : Type v} [AddCommGroup X] [Module K X]
20 variable {I : Type w} [Fintype I] [DecidableEq I] [Preorder I]
21 
22 abbrev preorderSupportAlgebra (P : LinearProjectorFamily K X I) :=
23   supportSubalgebra P (· ≤ ·) (fun _ => le_rfl) (fun _ _ _ => le_trans)
24 
25 theorem strictSupport_mul_left (P : LinearProjectorFamily K X I)
26     {S T : Module.End K X} (hS : OperatorSupported P (· ≤ ·) S)
27     (hT : OperatorSupported P (· < ·) T) :
28     OperatorSupported P (· < ·) (S*T) := by
29   apply (operatorSupported_iff_ambient P _ _).mpr
30   intro b a hab
31   change transferBlock P P (S.comp T) b a = 0
32   rw [transferBlock_comp_end]
33   apply Finset.sum_eq_zero
34   intro c _
35   by_cases hac : a < c
36   · have hcb : ¬ c ≤ b := fun h => hab (lt_of_lt_of_le hac h)
37     rw [(operatorSupported_iff_ambient P _ S).mp hS b c hcb]
38     simp
39   · rw [(operatorSupported_iff_ambient P _ T).mp hT c a hac]
40     simp
41 
42 theorem strictSupport_mul_right (P : LinearProjectorFamily K X I)
43     {S T : Module.End K X} (hS : OperatorSupported P (· < ·) S)
44     (hT : OperatorSupported P (· ≤ ·) T) :
45     OperatorSupported P (· < ·) (S*T) := by
46   apply (operatorSupported_iff_ambient P _ _).mpr
47   intro b a hab
48   change transferBlock P P (S.comp T) b a = 0
49   rw [transferBlock_comp_end]
50   apply Finset.sum_eq_zero
51   intro c _
52   by_cases hac : a ≤ c
53   · have hcb : ¬ c < b := fun h => hab (lt_of_le_of_lt hac h)
54     rw [(operatorSupported_iff_ambient P _ S).mp hS b c hcb]
55     simp
56   · rw [(operatorSupported_iff_ambient P _ T).mp hT c a hac]
57     simp
58 
59 /-- The strict-class blocks form a genuine two-sided ideal of the preorder support algebra. -/
60 def strictSupportIdeal (P : LinearProjectorFamily K X I) :
61     TwoSidedIdeal (preorderSupportAlgebra P) :=
62   TwoSidedIdeal.mk' {T | OperatorSupported P (· < ·) T.1}
63     ((supportSubmodule P (· < ·)).zero_mem)
64     (fun hS hT => (supportSubmodule P (· < ·)).add_mem hS hT)
65     (fun hT => (supportSubmodule P (· < ·)).neg_mem hT)
66     (fun {S _T} hT => strictSupport_mul_left P S.property hT)
67     (fun {_S T} hS => strictSupport_mul_right P hS T.property)
68 
69 @[simp] theorem mem_strictSupportIdeal (P : LinearProjectorFamily K X I)
70     (T : preorderSupportAlgebra P) :
71     T ∈ strictSupportIdeal P ↔ OperatorSupported P (· < ·) T.1 :=
72   TwoSidedIdeal.mem_mk' _ _ _ _ _ _ T
73 
74 /-- Inside the preorder support algebra, strict support means zero on every equivalence class. -/
75 theorem strictSupport_iff_same_class_zero (P : LinearProjectorFamily K X I)
76     (T : preorderSupportAlgebra P) :
77     OperatorSupported P (· < ·) T.1 ↔
78       ∀ a b, AntisymmRel (· ≤ ·) a b → transferBlock P P T.1 b a = 0 := by
79   constructor
80   · intro h a b hab
81     exact (operatorSupported_iff_ambient P _ T.1).mp h b a
82       (fun hlt => (not_le_of_gt hlt) hab.2)
83   · intro h
84     apply (operatorSupported_iff_ambient P _ T.1).mpr
85     intro b a hab
86     by_cases hle : a ≤ b
87     · exact h a b ⟨hle, by by_contra hback; exact hab (lt_of_le_not_ge hle hback)⟩
88     · exact (operatorSupported_iff_ambient P _ T.1).mp T.property b a hle
89 
90 /-- A strict path records its exact number of strict steps. -/
91 def StrictPath : ℕ → I → I → Prop
92   | 0, a, b => a = b
93   | n+1, a, b => ∃ c, StrictPath n a c ∧ c < b
94 
95 private def strictPredecessors (b : I) : Finset I := by
96   classical
97   exact Finset.univ.filter (fun a => a < b)
98 
99 private theorem predecessors_strict_mono {a b : I} (hab : a < b) :
100     (strictPredecessors a).card < (strictPredecessors b).card := by
101   classical
102   apply Finset.card_lt_card
103   apply Finset.ssubset_iff_subset_ne.mpr
104   refine ⟨?_, ?_⟩
105   · intro c hc
106     simp only [strictPredecessors, Finset.mem_filter, Finset.mem_univ, true_and] at hc ⊢
107     exact lt_trans hc hab
108   · intro heq
109     have ha : a ∈ strictPredecessors b := by simp [strictPredecessors, hab]
110     rw [← heq] at ha
111     simp [strictPredecessors] at ha
112 
113 private theorem strictPath_height {n : ℕ} {a b : I} (h : StrictPath n a b) :
114     (strictPredecessors a).card + n ≤ (strictPredecessors b).card := by
115   induction n generalizing b with
116   | zero =>
117     change a = b at h
118     subst b
119     simp
120   | succ n ih =>
121     obtain ⟨c, hac, hcb⟩ := h
122     have hc := ih hac
123     have hb := predecessors_strict_mono hcb
124     omega
125 
126 private theorem strictPath_length_bound {n : ℕ} {a b : I} (h : StrictPath n a b) :
127     n ≤ Fintype.card I := by
128   have hn := strictPath_height h
129   have hb : (strictPredecessors b).card ≤ Fintype.card I := by
130     exact (Finset.card_le_card (Finset.subset_univ _)).trans_eq (Finset.card_univ)
131   omega
132 
133 /-- Maximum number of strict steps, with value zero for the empty preorder. -/
134 def maximalStrictSteps (I : Type w) [Fintype I] [DecidableEq I] [Preorder I] : ℕ :=
135   sSup {n | ∃ a b : I, StrictPath n a b}
136 
137 private theorem strictPath_lengths_bdd :
138     BddAbove {n | ∃ a b : I, StrictPath n a b} := by
139   refine ⟨Fintype.card I, ?_⟩
140   rintro n ⟨a, b, h⟩
141   exact strictPath_length_bound h
142 
143 theorem strictPath_le_maximal {n : ℕ} {a b : I} (h : StrictPath n a b) :
144     n ≤ maximalStrictSteps I :=
145   le_csSup strictPath_lengths_bdd ⟨a,b,h⟩
146 
147 theorem maximalStrictSteps_attained [Nonempty I] :
148     ∃ a b : I, StrictPath (maximalStrictSteps I) a b := by
149   apply Nat.sSup_mem _ strictPath_lengths_bdd
150   obtain ⟨a⟩ := ‹Nonempty I›
151   exact ⟨0, a, a, rfl⟩
152 
153 theorem no_strictPath_after_maximal (a b : I) :
154     ¬ StrictPath (maximalStrictSteps I + 1) a b := by
155   intro h
156   have hh := strictPath_le_maximal h
157   omega
158 
159 /-- A nonzero block of a product of strict operators forces a strict path of the same length. -/
160 theorem nonzero_word_block_strictPath (P : LinearProjectorFamily K X I)
161     (ts : List (Module.End K X))
162     (hstrict : ∀ T ∈ ts, OperatorSupported P (· < ·) T) (b a : I)
163     (hne : transferBlock P P (operatorWord ts) b a ≠ 0) :
164     StrictPath ts.length a b := by
165   induction ts generalizing b a with
166   | nil =>
167     change a = b
168     by_contra hab
169     apply hne
170     ext x
171     exact P.orthogonal (Ne.symm hab) x
172   | cons T ts ih =>
173     have hsum : (∑ c, (transferBlock P P T b c).comp
174         (transferBlock P P (operatorWord ts) c a)) ≠ 0 := by
175       simpa only [operatorWord, transferBlock_comp_end] using hne
176     obtain ⟨c, _, hc⟩ := Finset.exists_ne_zero_of_sum_ne_zero hsum
177     have hTc : transferBlock P P T b c ≠ 0 := by
178       intro h
179       apply hc
180       simp [h]
181     have hts : transferBlock P P (operatorWord ts) c a ≠ 0 := by
182       intro h
183       apply hc
184       simp [h]
185     have hcb : c < b := by
186       by_contra h
187       exact hTc ((operatorSupported_iff_ambient P _ T).mp (hstrict T (by simp)) b c h)
188     exact ⟨c, ih (fun S hS => hstrict S (by simp [hS])) c a hts, hcb⟩
189 
190 /-- Every product of more factors than the maximal strict chain length is zero. -/
191 theorem strict_word_zero (P : LinearProjectorFamily K X I)
192     (ts : List (Module.End K X))
193     (hlen : ts.length = maximalStrictSteps I + 1)
194     (hstrict : ∀ T ∈ ts, OperatorSupported P (· < ·) T) :
195     operatorWord ts = 0 := by
196   have hblocks : ∀ b a, transferBlock P P (operatorWord ts) b a = 0 := by
197     intro b a
198     by_contra h
199     have hp := nonzero_word_block_strictPath P ts hstrict b a h
200     rw [hlen] at hp
201     exact no_strictPath_after_maximal a b hp
202   ext x
203   rw [← transferBlock_reconstruction P P (operatorWord ts) x]
204   change (∑ b, ∑ a, transferBlock P P (operatorWord ts) b a x) = 0
205   simp [hblocks]
206 
207 /-- The ideal power is the span of all products of the declared number of factors. -/
208 def strictSupportPower (P : LinearProjectorFamily K X I) (n : ℕ) :
209     Submodule K (Module.End K X) :=
210   Submodule.span K {T | ∃ ts : List (Module.End K X), ts.length = n ∧
211     (∀ S ∈ ts, OperatorSupported P (· < ·) S) ∧ T = operatorWord ts}
212 
213 /-- Literal ideal-power nilpotence with the maximal-chain exponent. -/
214 theorem strictSupportPower_eq_bot (P : LinearProjectorFamily K X I) :
215     strictSupportPower P (maximalStrictSteps I + 1) = ⊥ := by
216   apply le_antisymm _ bot_le
217   apply Submodule.span_le.mpr
218   rintro T ⟨ts, hlen, hstrict, rfl⟩
219   exact strict_word_zero P ts hlen hstrict
220 
221 private theorem strict_mul_power_mem (P : LinearProjectorFamily K X I)
222     {S T : Module.End K X} {n : ℕ} (hS : OperatorSupported P (· < ·) S)
223     (hT : T ∈ strictSupportPower P n) : S*T ∈ strictSupportPower P (n+1) := by
224   induction hT using Submodule.span_induction with
225   | mem T hT =>
226     obtain ⟨ts, hlen, hstrict, rfl⟩ := hT
227     apply Submodule.subset_span
228     refine ⟨S :: ts, by simp [hlen], ?_, rfl⟩
229     intro U hU
230     rcases List.mem_cons.mp hU with rfl | hU
231     · exact hS
232     · exact hstrict U hU
233   | zero => simp
234   | add T U _ _ hT hU =>
235     rw [mul_add]
236     exact (strictSupportPower P (n+1)).add_mem hT hU
237   | smul c T _ hT =>
238     rw [mul_smul_comm]
239     exact (strictSupportPower P (n+1)).smul_mem c hT
240 
241 /-- Standard ideal powers are controlled by the explicit span-of-products construction. -/
242 theorem strictIdeal_power_mem (P : LinearProjectorFamily K X I) (n : ℕ)
243     {T : preorderSupportAlgebra P}
244     (hT : T ∈ (strictSupportIdeal P).asIdeal ^ (n+1)) :
245     T.1 ∈ strictSupportPower P (n+1) := by
246   induction n generalizing T with
247   | zero =>
248     have hs : OperatorSupported P (· < ·) T.1 := by
249       simpa only [Nat.zero_add, Submodule.pow_one, TwoSidedIdeal.mem_asIdeal,
250         mem_strictSupportIdeal] using hT
251     apply Submodule.subset_span
252     exact ⟨[T.1], rfl, by simpa using hs, by ext x; rfl⟩
253   | succ n ih =>
254     rw [Submodule.pow_succ' _ (by omega)] at hT
255     refine Submodule.smul_induction_on
256       (p := fun V : preorderSupportAlgebra P => V.1 ∈ strictSupportPower P (n+1+1)) hT ?_ ?_
257     · intro S hS U hU
258       have hs : OperatorSupported P (· < ·) S.1 := by
259         simpa only [TwoSidedIdeal.mem_asIdeal, mem_strictSupportIdeal] using hS
260       exact strict_mul_power_mem P hs (ih hU)
261     · intro U V hU hV
262       exact (strictSupportPower P (n+1+1)).add_mem hU hV
263 
264 /-- Nilpotency in Mathlib's ordinary ideal-power operation, with the exact chain-height bound. -/
265 theorem strictSupportIdeal_pow_eq_bot (P : LinearProjectorFamily K X I) :
266     (strictSupportIdeal P).asIdeal ^ (maximalStrictSteps I + 1) = ⊥ := by
267   apply le_antisymm _ bot_le
268   intro T hT
269   have h := strictIdeal_power_mem P (maximalStrictSteps I) hT
270   rw [strictSupportPower_eq_bot] at h
271   change T.1 = 0 at h
272   exact Subtype.ext h
273 
274 end Komorebi.PaperIRelease

Back to source controls