CommonRefinement.lean

1 import KomorebiVerification.PaperII.NestedRefinement
2 
3 /-!
4 # Supported common refinements
5 
6 Explicit constructions for the expanded Paper II common-refinement theorem.
7 The inherited `LinearProjectorFamily` permits zero members. Nonzero hypotheses
8 are therefore stated, and zero products are removed by an actual subtype.
9 No arithmetic, spectral, analytic or executable-algorithm conclusion is claimed.
10 -/
11 
12 set_option autoImplicit false
13 
14 noncomputable section
15 
16 namespace Komorebi.PaperII.CommonRefinement
17 
18 open Komorebi.Foundation Komorebi.PaperII.NestedRefinement
19 
20 universe u v w x y
21 variable {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M]
22 variable {ι : Type w} {κ : Type x} {τ : Type y}
23 variable [Fintype ι] [Fintype κ] [Fintype τ]
24 
25 /-- Nonzero members, not a nonzero ambient-module assumption. -/
26 def Nonzero (P : LinearProjectorFamily R M ι) : Prop := ∀ i, P.proj i ≠ 0
27 
28 /-- All cross pairs commute, stated pointwise on the original module. -/
29 def CrossCommutes (P : LinearProjectorFamily R M ι)
30     (Q : LinearProjectorFamily R M κ) : Prop :=
31   ∀ i j z, P.proj i (Q.proj j z) = Q.proj j (P.proj i z)
32 
33 /-- The actual support of a finite projector family. -/
34 abbrev Support (P : LinearProjectorFamily R M ι) := {i : ι // P.proj i ≠ 0}
35 
36 instance supportFintype (P : LinearProjectorFamily R M ι) : Fintype (Support P) := by
37   classical
38   unfold Support
39   infer_instance
40 
41 /-- Removing zero projectors preserves the identity decomposition. -/
42 theorem support_complete (P : LinearProjectorFamily R M ι) (z : M) :
43     (∑ i : Support P, P.proj i.val z) = z := by
44   classical
45   change (∑ i : {i : ι // P.proj i ≠ 0}, P.proj i.val z) = z
46   rw [← Finset.sum_subtype (Finset.univ.filter (fun i => P.proj i ≠ 0))
47     (by intro i; simp) (fun i => P.proj i z), Finset.sum_filter]
48   calc
49     (∑ i, if P.proj i ≠ 0 then P.proj i z else 0) = ∑ i, P.proj i z := by
50       apply Finset.sum_congr rfl
51       intro i _
52       by_cases h : P.proj i = 0 <;> simp [h]
53     _ = z := P.complete z
54 
55 /-- A zero-free family on its supported index subtype. -/
56 def supported (P : LinearProjectorFamily R M ι) :
57     LinearProjectorFamily R M (Support P) where
58   proj i := P.proj i.val
59   idempotent i := P.idempotent i.val
60   orthogonal := by
61     intro i j h z
62     exact P.orthogonal (fun hij => h (Subtype.ext hij)) z
63   complete := support_complete P
64 
65 theorem supported_nonzero (P : LinearProjectorFamily R M ι) : Nonzero (supported P) :=
66   fun i => i.property
67 
68 /-- The full binary product family, before removing zero members. -/
69 def product (P : LinearProjectorFamily R M ι) (Q : LinearProjectorFamily R M κ)
70     (h : CrossCommutes P Q) : LinearProjectorFamily R M (ι × κ) where
71   proj k := (P.proj k.1).comp (Q.proj k.2)
72   idempotent := by
73     intro k z
74     change P.proj k.1 (Q.proj k.2 (P.proj k.1 (Q.proj k.2 z))) = _
75     rw [← h k.1 k.2 (Q.proj k.2 z), P.idempotent, Q.idempotent]
76     rfl
77   orthogonal := by
78     intro k l hkl z
79     change P.proj k.1 (Q.proj k.2 (P.proj l.1 (Q.proj l.2 z))) = 0
80     rw [← h l.1 k.2 (Q.proj l.2 z)]
81     by_cases hi : k.1 = l.1
82     · have hj : k.2 ≠ l.2 := fun hj => hkl (Prod.ext hi hj)
83       rw [hi, P.idempotent, Q.orthogonal hj, map_zero]
84     · exact P.orthogonal hi _
85   complete := by
86     intro z
87     simp only [Fintype.sum_prod_type, LinearMap.comp_apply]
88     simp_rw [← map_sum, Q.complete]
89     exact P.complete z
90 
91 /-- The nonzero product family that appears in the manuscript. -/
92 def common (P : LinearProjectorFamily R M ι) (Q : LinearProjectorFamily R M κ)
93     (h : CrossCommutes P Q) := supported (product P Q h)
94 
95 /-- Construct a refinement from absorption; nonzero coarse members force surjectivity. -/
96 theorem refines_of_absorption [DecidableEq ι]
97     (P : LinearProjectorFamily R M ι) (S : LinearProjectorFamily R M κ)
98     (hn : Nonzero P) (parent : κ → ι)
99     (ha : ∀ i a z, P.proj i (S.proj a z) = if parent a = i then S.proj a z else 0) :
100     Refines P S parent := by
101   classical
102   have hf : ∀ i, P.proj i = ∑ a ∈ children parent i, S.proj a := by
103     intro i
104     ext z
105     simp only [LinearMap.sum_apply]
106     calc
107       P.proj i z = P.proj i (∑ a, S.proj a z) := by rw [S.complete]
108       _ = ∑ a, P.proj i (S.proj a z) := by rw [map_sum]
109       _ = ∑ a, if parent a = i then S.proj a z else 0 := by
110         apply Finset.sum_congr rfl
111         intro a _
112         exact ha i a z
113       _ = ∑ a ∈ children parent i, S.proj a z := by
114         simp only [children, Finset.sum_filter]
115         apply Finset.sum_congr rfl
116         intro a _
117         split_ifs <;> rfl
118   refine ⟨?_, hf⟩
119   intro i
120   by_contra he
121   have he' : ∀ a, parent a ≠ i := by simpa only [not_exists] using he
122   have hc : children parent i = ∅ := by
123     apply Finset.eq_empty_iff_forall_notMem.mpr
124     intro a ha'
125     exact he' a ((mem_children parent i a).mp ha')
126   exact hn i (by rw [hf i, hc, Finset.sum_empty])
127 
128 /-- The first coordinate is an onto parent map, including support pruning. -/
129 theorem common_refines_left
130     (P : LinearProjectorFamily R M ι) (Q : LinearProjectorFamily R M κ)
131     (h : CrossCommutes P Q) (hn : Nonzero P) :
132     Refines P (common P Q h) (fun k => k.val.1) := by
133   classical
134   apply refines_of_absorption P (common P Q h) hn
135   intro i k z
136   change P.proj i (P.proj k.val.1 (Q.proj k.val.2 z)) =
137     if k.val.1 = i then P.proj k.val.1 (Q.proj k.val.2 z) else 0
138   by_cases hk : k.val.1 = i
139   · simp only [hk, ↓reduceIte]
140     exact P.idempotent i _
141   · simp only [hk, ↓reduceIte]
142     exact P.orthogonal (Ne.symm hk) _
143 
144 /-- The second coordinate is an onto parent map, including support pruning. -/
145 theorem common_refines_right
146     (P : LinearProjectorFamily R M ι) (Q : LinearProjectorFamily R M κ)
147     (h : CrossCommutes P Q) (hn : Nonzero Q) :
148     Refines Q (common P Q h) (fun k => k.val.2) := by
149   classical
150   apply refines_of_absorption Q (common P Q h) hn
151   intro j k z
152   change Q.proj j (P.proj k.val.1 (Q.proj k.val.2 z)) =
153     if k.val.2 = j then P.proj k.val.1 (Q.proj k.val.2 z) else 0
154   rw [← h k.val.1 j (Q.proj k.val.2 z)]
155   by_cases hk : k.val.2 = j
156   · simp only [hk, ↓reduceIte, Q.idempotent]
157   · simp only [hk, ↓reduceIte]
158     rw [Q.orthogonal (Ne.symm hk), map_zero]
159 
160 /-- The joint parent has nonzero product because it absorbs the nonzero child. -/
161 theorem joint_product_nonzero
162     (P : LinearProjectorFamily R M ι) (Q : LinearProjectorFamily R M κ)
163     (S : LinearProjectorFamily R M τ) (hn : Nonzero S)
164     (p : τ → ι) (q : τ → κ) (hp : Refines P S p) (hq : Refines Q S q) (a : τ) :
165     (P.proj (p a)).comp (Q.proj (q a)) ≠ 0 := by
166   intro hz
167   have hab : ((P.proj (p a)).comp (Q.proj (q a))).comp (S.proj a) = S.proj a := by
168     ext z
169     simp only [LinearMap.comp_apply]
170     rw [hq.coarse_fine_apply_eq_self, hp.coarse_fine_apply_eq_self]
171   rw [hz, LinearMap.zero_comp] at hab
172   exact hn a hab.symm
173 
174 /-- Construct the unique joint parent as an element of the supported product subtype. -/
175 def jointParent
176     (P : LinearProjectorFamily R M ι) (Q : LinearProjectorFamily R M κ)
177     (h : CrossCommutes P Q) (S : LinearProjectorFamily R M τ) (hn : Nonzero S)
178     (p : τ → ι) (q : τ → κ) (hp : Refines P S p) (hq : Refines Q S q) :
179     τ → Support (product P Q h) :=
180   fun a => ⟨(p a, q a), joint_product_nonzero P Q S hn p q hp hq a⟩
181 
182 /-- Every nonzero common refinement refines the explicit supported product family. -/
183 theorem common_coarsest
184     (P : LinearProjectorFamily R M ι) (Q : LinearProjectorFamily R M κ)
185     (h : CrossCommutes P Q) (S : LinearProjectorFamily R M τ) (hn : Nonzero S)
186     (p : τ → ι) (q : τ → κ) (hp : Refines P S p) (hq : Refines Q S q) :
187     Refines (common P Q h) S (jointParent P Q h S hn p q hp hq) := by
188   classical
189   apply refines_of_absorption _ S (supported_nonzero _) _
190   intro k a z
191   change P.proj k.val.1 (Q.proj k.val.2 (S.proj a z)) = _
192   by_cases hk : jointParent P Q h S hn p q hp hq a = k
193   · simp only [hk, ↓reduceIte]
194     rw [← hk]
195     change P.proj (p a) (Q.proj (q a) (S.proj a z)) = _
196     rw [hq.coarse_fine_apply_eq_self, hp.coarse_fine_apply_eq_self]
197   · simp only [hk, ↓reduceIte]
198     by_cases hqk : q a = k.val.2
199     · have hqa : Q.proj k.val.2 (S.proj a z) = S.proj a z := by
200         simpa only [LinearMap.comp_apply] using
201           LinearMap.congr_fun (hq.coarse_comp_fine_eq_self hqk) z
202       rw [hqa]
203       have hpk : p a ≠ k.val.1 := by
204         intro hpk
205         exact hk (Subtype.ext (Prod.ext hpk hqk))
206       simpa only [LinearMap.comp_apply, LinearMap.zero_apply] using
207         LinearMap.congr_fun (hp.coarse_comp_fine_eq_zero hpk) z
208     · have hqa : Q.proj k.val.2 (S.proj a z) = 0 := by
209         simpa only [LinearMap.comp_apply, LinearMap.zero_apply] using
210           LinearMap.congr_fun (hq.coarse_comp_fine_eq_zero hqk) z
211       rw [hqa, map_zero]
212 
213 /-- Nonzero children cannot have two different parents in one packet system. -/
214 theorem parent_unique
215     (P : LinearProjectorFamily R M ι) (S : LinearProjectorFamily R M κ)
216     (hn : Nonzero S) (p q : κ → ι) (hp : Refines P S p) (hq : Refines P S q) : p = q := by
217   funext a
218   by_contra h
219   have hself := hp.coarse_comp_fine_eq_self (a := p a) (b := a) rfl
220   have hzero := hq.coarse_comp_fine_eq_zero (a := p a) (b := a) (Ne.symm h)
221   exact hn a (hself.symm.trans hzero)
222 
223 /-- A supplied common refinement forces all original cross pairs to commute. -/
224 theorem commutes_of_common_refinement
225     (P : LinearProjectorFamily R M ι) (Q : LinearProjectorFamily R M κ)
226     (S : LinearProjectorFamily R M τ) (p : τ → ι) (q : τ → κ)
227     (hp : Refines P S p) (hq : Refines Q S q) : CrossCommutes P Q := by
228   classical
229   intro i j z
230   conv_lhs => rw [← S.complete z]
231   conv_rhs => rw [← S.complete z]
232   simp only [map_sum]
233   apply Finset.sum_congr rfl
234   intro a _
235   have hP : P.proj i (S.proj a z) = if p a = i then S.proj a z else 0 := by
236     by_cases hpi : p a = i
237     · simpa only [LinearMap.comp_apply, hpi, ↓reduceIte] using
238         LinearMap.congr_fun (hp.coarse_comp_fine_eq_self hpi) z
239     · simpa only [LinearMap.comp_apply, hpi, ↓reduceIte, LinearMap.zero_apply] using
240         LinearMap.congr_fun (hp.coarse_comp_fine_eq_zero hpi) z
241   have hQ : Q.proj j (S.proj a z) = if q a = j then S.proj a z else 0 := by
242     by_cases hqj : q a = j
243     · simpa only [LinearMap.comp_apply, hqj, ↓reduceIte] using
244         LinearMap.congr_fun (hq.coarse_comp_fine_eq_self hqj) z
245     · simpa only [LinearMap.comp_apply, hqj, ↓reduceIte, LinearMap.zero_apply] using
246         LinearMap.congr_fun (hq.coarse_comp_fine_eq_zero hqj) z
247   by_cases hpi : p a = i <;> by_cases hqj : q a = j <;>
248     simp only [hpi, hqj, ↓reduceIte] at hP hQ <;>
249     simp only [hP, hQ, map_zero]
250 
251 end Komorebi.PaperII.CommonRefinement

Back to source controls