NestedRefinement.lean

1 import KomorebiVerification.ExactCoordinates
2 
3 /-!
4 # Nested refinement of exact projector coordinates
5 
6 Author: Komorebi P.
7 
8 This module formalizes the algebraic nested-refinement results of Paper II.
9 A refinement consists of a surjective parent map together with exact recovery
10 of every coarse projector as the finite sum of its fine children.  The file
11 proves the two absorption orders, canonical reconstruction and uniqueness,
12 transitivity, exact cross-level range coordinates, and refinement of transfer
13 blocks.
14 -/
15 
16 set_option autoImplicit false
17 
18 namespace Komorebi.PaperII.NestedRefinement
19 
20 open Komorebi.Foundation
21 open Komorebi.Foundation.LinearProjectorFamily
22 
23 universe u v w x y z
24 
25 variable {R : Type u} {M : Type v}
26 variable {ι : Type w} {κ : Type x} {τ : Type y}
27 variable [Semiring R] [AddCommMonoid M] [Module R M]
28 variable [Fintype ι] [Fintype κ] [Fintype τ]
29 
30 /-! ## Refinement data -/
31 
32 /-- The finite set of fine indices having the specified coarse parent. -/
33 noncomputable def children (parent : κ → ι) (a : ι) : Finset κ := by
34   classical
35   exact Finset.univ.filter (fun b => parent b = a)
36 
37 omit [Fintype ι] in
38 @[simp] theorem mem_children (parent : κ → ι) (a : ι) (b : κ) :
39     b ∈ children parent a ↔ parent b = a := by
40   classical
41   simp [children]
42 
43 /--
44 `fine` refines `coarse` along `parent` when `parent` is surjective and every
45 coarse projector is exactly the sum of the fine projectors over its fibre.
46 -/
47 structure Refines
48     (coarse : LinearProjectorFamily R M ι)
49     (fine : LinearProjectorFamily R M κ)
50     (parent : κ → ι) : Prop where
51   surjective : Function.Surjective parent
52   coarse_eq_sum_children :
53     ∀ a, coarse.proj a = ∑ b ∈ children parent a, fine.proj b
54 
55 /-! ## Generic finite-packet uniqueness -/
56 
57 /--
58 For any finite collection of mutually orthogonal projector ranges, applying the
59 corresponding projector recovers its summand.  No parent map, surjectivity, or
60 coarse-projector reconstruction is needed.
61 -/
62 theorem finitePacket_decomposition_unique
63     (P : LinearProjectorFamily R M κ) (s : Finset κ) (x : M)
64     (packets : κ → M)
65     (hrange : ∀ b ∈ s, packets b ∈ LinearMap.range (P.proj b))
66     (hsum : ∑ b ∈ s, packets b = x) :
67     ∀ b ∈ s, packets b = P.proj b x := by
68   classical
69   intro b hb
70   have hself : P.proj b (packets b) = packets b := by
71     rcases hrange b hb with ⟨y, hy⟩
72     rw [← hy]
73     exact P.idempotent b y
74   have hproject : P.proj b (∑ j ∈ s, packets j) = packets b := by
75     rw [map_sum]
76     calc
77       (∑ j ∈ s, P.proj b (packets j)) = P.proj b (packets b) := by
78         apply Finset.sum_eq_single_of_mem b hb
79         intro j hj hjb
80         rcases hrange j hj with ⟨y, hy⟩
81         rw [← hy]
82         exact P.orthogonal hjb.symm y
83       _ = packets b := hself
84   calc
85     packets b = P.proj b (∑ j ∈ s, packets j) := hproject.symm
86     _ = P.proj b x := congrArg (P.proj b) hsum
87 
88 /-- Two finite decompositions into the same orthogonal packet ranges agree. -/
89 theorem finitePacket_decomposition_ext
90     (P : LinearProjectorFamily R M κ) (s : Finset κ)
91     (packets packets' : κ → M)
92     (hrange : ∀ b ∈ s, packets b ∈ LinearMap.range (P.proj b))
93     (hrange' : ∀ b ∈ s, packets' b ∈ LinearMap.range (P.proj b))
94     (hsum : ∑ b ∈ s, packets b = ∑ b ∈ s, packets' b) :
95     ∀ b ∈ s, packets b = packets' b := by
96   intro b hb
97   calc
98     packets b = P.proj b (∑ j ∈ s, packets j) :=
99       finitePacket_decomposition_unique P s _ packets hrange rfl b hb
100     _ = P.proj b (∑ j ∈ s, packets' j) := congrArg (P.proj b) hsum
101     _ = packets' b :=
102       (finitePacket_decomposition_unique P s _ packets' hrange' rfl b hb).symm
103 
104 namespace Refines
105 
106 variable {coarse : LinearProjectorFamily R M ι}
107 variable {fine : LinearProjectorFamily R M κ}
108 variable {parent : κ → ι}
109 
110 /-- Pointwise form of the defining coarse-projector reconstruction. -/
111 theorem coarse_proj_apply_eq_sum_children
112     (h : Refines coarse fine parent) (a : ι) (x : M) :
113     coarse.proj a x = ∑ b ∈ children parent a, fine.proj b x := by
114   rw [h.coarse_eq_sum_children a]
115   simp only [LinearMap.sum_apply]
116 
117 /-! ## Absorption in both orders -/
118 
119 /-- A coarse projector absorbs a fine child on the left. -/
120 theorem coarse_comp_fine_eq_self
121     (h : Refines coarse fine parent) {a : ι} {b : κ}
122     (hb : parent b = a) :
123     (coarse.proj a).comp (fine.proj b) = fine.proj b := by
124   classical
125   ext x
126   simp only [LinearMap.comp_apply]
127   rw [h.coarse_proj_apply_eq_sum_children]
128   have hbmem : b ∈ children parent a := (mem_children parent a b).2 hb
129   calc
130     (∑ j ∈ children parent a, fine.proj j (fine.proj b x)) =
131         fine.proj b (fine.proj b x) := by
132           apply Finset.sum_eq_single_of_mem b hbmem
133           intro j _ hjb
134           exact fine.orthogonal hjb x
135     _ = fine.proj b x := fine.idempotent b x
136 
137 /-- A non-parent coarse projector annihilates a fine packet on the left. -/
138 theorem coarse_comp_fine_eq_zero
139     (h : Refines coarse fine parent) {a : ι} {b : κ}
140     (hb : parent b ≠ a) :
141     (coarse.proj a).comp (fine.proj b) = 0 := by
142   classical
143   ext x
144   simp only [LinearMap.comp_apply, LinearMap.zero_apply]
145   rw [h.coarse_proj_apply_eq_sum_children]
146   apply Finset.sum_eq_zero
147   intro j hj
148   have hjparent : parent j = a := (mem_children parent a j).1 hj
149   have hjb : j ≠ b := by
150     intro hjb
151     subst j
152     exact hb hjparent
153   exact fine.orthogonal hjb x
154 
155 /-- A fine child absorbs its coarse parent on the right. -/
156 theorem fine_comp_coarse_eq_self
157     (h : Refines coarse fine parent) {a : ι} {b : κ}
158     (hb : parent b = a) :
159     (fine.proj b).comp (coarse.proj a) = fine.proj b := by
160   classical
161   ext x
162   simp only [LinearMap.comp_apply]
163   rw [h.coarse_proj_apply_eq_sum_children, map_sum]
164   have hbmem : b ∈ children parent a := (mem_children parent a b).2 hb
165   calc
166     (∑ j ∈ children parent a, fine.proj b (fine.proj j x)) =
167         fine.proj b (fine.proj b x) := by
168           apply Finset.sum_eq_single_of_mem b hbmem
169           intro j _ hjb
170           exact fine.orthogonal hjb.symm x
171     _ = fine.proj b x := fine.idempotent b x
172 
173 /-- A fine projector annihilates a non-parent coarse packet on the right. -/
174 theorem fine_comp_coarse_eq_zero
175     (h : Refines coarse fine parent) {a : ι} {b : κ}
176     (hb : parent b ≠ a) :
177     (fine.proj b).comp (coarse.proj a) = 0 := by
178   classical
179   ext x
180   simp only [LinearMap.comp_apply, LinearMap.zero_apply]
181   rw [h.coarse_proj_apply_eq_sum_children, map_sum]
182   apply Finset.sum_eq_zero
183   intro j hj
184   have hjparent : parent j = a := (mem_children parent a j).1 hj
185   have hbj : b ≠ j := by
186     intro hbj
187     subst j
188     exact hb hjparent
189   exact fine.orthogonal hbj x
190 
191 /-- Pointwise left absorption by the parent. -/
192 theorem coarse_fine_apply_eq_self
193     (h : Refines coarse fine parent) (b : κ) (x : M) :
194     coarse.proj (parent b) (fine.proj b x) = fine.proj b x := by
195   exact LinearMap.congr_fun (h.coarse_comp_fine_eq_self rfl) x
196 
197 /-- Pointwise right absorption by the parent. -/
198 theorem fine_coarse_apply_eq_self
199     (h : Refines coarse fine parent) (b : κ) (x : M) :
200     fine.proj b (coarse.proj (parent b) x) = fine.proj b x := by
201   exact LinearMap.congr_fun (h.fine_comp_coarse_eq_self rfl) x
202 
203 /-! ## Reconstruction and uniqueness -/
204 
205 /-- Every vector in a coarse projector range is the sum of its fine children. -/
206 theorem coarse_packet_reconstruction
207     (h : Refines coarse fine parent) (a : ι)
208     (x : LinearMap.range (coarse.proj a)) :
209     (x : M) = ∑ b ∈ children parent a, fine.proj b (x : M) := by
210   have hx : coarse.proj a (x : M) = (x : M) := by
211     rcases x.property with ⟨y, hy⟩
212     rw [← hy]
213     exact coarse.idempotent a y
214   exact hx.symm.trans (h.coarse_proj_apply_eq_sum_children a (x : M))
215 
216 /--
217 A sum of vectors belonging to distinct fine-child ranges has uniquely
218 determined components: the `b`-component is obtained by applying `fine.proj b`.
219 -/
220 theorem child_decomposition_unique
221     (_h : Refines coarse fine parent) (a : ι) (x : M)
222     (packets : κ → M)
223     (hrange : ∀ b ∈ children parent a,
224       packets b ∈ LinearMap.range (fine.proj b))
225     (hsum : ∑ b ∈ children parent a, packets b = x) :
226     ∀ b ∈ children parent a, packets b = fine.proj b x := by
227   exact finitePacket_decomposition_unique
228     fine (children parent a) x packets hrange hsum
229 
230 /-- Two decompositions into the same fine-child ranges with the same sum agree. -/
231 theorem child_decomposition_ext
232     (_h : Refines coarse fine parent) (a : ι)
233     (packets packets' : κ → M)
234     (hrange : ∀ b ∈ children parent a,
235       packets b ∈ LinearMap.range (fine.proj b))
236     (hrange' : ∀ b ∈ children parent a,
237       packets' b ∈ LinearMap.range (fine.proj b))
238     (hsum : ∑ b ∈ children parent a, packets b =
239       ∑ b ∈ children parent a, packets' b) :
240     ∀ b ∈ children parent a, packets b = packets' b := by
241   exact finitePacket_decomposition_ext
242     fine (children parent a) packets packets' hrange hrange' hsum
243 
244 /-! ## Transitivity -/
245 
246 variable {middle : LinearProjectorFamily R M κ}
247 variable {finest : LinearProjectorFamily R M τ}
248 variable {parent₁ : κ → ι} {parent₂ : τ → κ}
249 
250 /-- Refinement is transitive, with the composite parent map. -/
251 theorem trans
252     (h₁ : Refines coarse middle parent₁)
253     (h₂ : Refines middle finest parent₂) :
254     Refines coarse finest (parent₁ ∘ parent₂) := by
255   classical
256   refine ⟨?_, ?_⟩
257   · intro a
258     rcases h₁.surjective a with ⟨b, rfl⟩
259     rcases h₂.surjective b with ⟨c, rfl⟩
260     exact ⟨c, rfl⟩
261   · intro a
262     ext x
263     simp only [LinearMap.sum_apply]
264     calc
265       coarse.proj a x = coarse.proj a (∑ c, finest.proj c x) := by
266         rw [finest.complete x]
267       _ = ∑ c, coarse.proj a (finest.proj c x) := by
268         rw [map_sum]
269       _ = ∑ c, if parent₁ (parent₂ c) = a then finest.proj c x else 0 := by
270         apply Finset.sum_congr rfl
271         intro c _
272         by_cases hc : parent₁ (parent₂ c) = a
273         · simp only [hc, ↓reduceIte]
274           rw [← h₂.coarse_fine_apply_eq_self c x]
275           exact LinearMap.congr_fun (h₁.coarse_comp_fine_eq_self hc) _
276         · simp only [hc, ↓reduceIte]
277           rw [← h₂.coarse_fine_apply_eq_self c x]
278           exact LinearMap.congr_fun (h₁.coarse_comp_fine_eq_zero hc) _
279       _ = ∑ c ∈ children (parent₁ ∘ parent₂) a, finest.proj c x := by
280         rw [children, Finset.sum_filter]
281         simp only [Function.comp_apply]
282 
283 end Refines
284 
285 /-! ## Exact range-coordinate transport -/
286 
287 section Coordinates
288 
289 variable (coarse : LinearProjectorFamily R M ι)
290 variable (fine : LinearProjectorFamily R M κ)
291 
292 /-- Resolve coarse range coordinates by synthesis followed by fine analysis. -/
293 def refineCoordinates : PacketSpace coarse →ₗ[R] PacketSpace fine :=
294   fine.rangeAnalysis.comp coarse.rangeSynthesis
295 
296 /-- Regroup fine range coordinates by synthesis followed by coarse analysis. -/
297 def coarsenCoordinates : PacketSpace fine →ₗ[R] PacketSpace coarse :=
298   coarse.rangeAnalysis.comp fine.rangeSynthesis
299 
300 @[simp] theorem refineCoordinates_apply (packets : PacketSpace coarse) :
301     refineCoordinates coarse fine packets =
302       fine.rangeAnalysis (coarse.rangeSynthesis packets) := rfl
303 
304 @[simp] theorem coarsenCoordinates_apply (packets : PacketSpace fine) :
305     coarsenCoordinates coarse fine packets =
306       coarse.rangeAnalysis (fine.rangeSynthesis packets) := rfl
307 
308 /-- Refinement carries the coarse analysis of a vector to its fine analysis. -/
309 @[simp] theorem refineCoordinates_rangeAnalysis (x : M) :
310     refineCoordinates coarse fine (coarse.rangeAnalysis x) =
311       fine.rangeAnalysis x := by
312   simp [refineCoordinates]
313 
314 /-- Fine synthesis after refinement is the original coarse synthesis. -/
315 @[simp] theorem rangeSynthesis_refineCoordinates
316     (packets : PacketSpace coarse) :
317     fine.rangeSynthesis (refineCoordinates coarse fine packets) =
318       coarse.rangeSynthesis packets := by
319   simp [refineCoordinates]
320 
321 /-- Coarsening carries the fine analysis of a vector to its coarse analysis. -/
322 @[simp] theorem coarsenCoordinates_rangeAnalysis (x : M) :
323     coarsenCoordinates coarse fine (fine.rangeAnalysis x) =
324       coarse.rangeAnalysis x := by
325   simp [coarsenCoordinates]
326 
327 /-- Coarse synthesis after coarsening is the original fine synthesis. -/
328 @[simp] theorem rangeSynthesis_coarsenCoordinates
329     (packets : PacketSpace fine) :
330     coarse.rangeSynthesis (coarsenCoordinates coarse fine packets) =
331       fine.rangeSynthesis packets := by
332   simp [coarsenCoordinates]
333 
334 /-- Coarsening after refinement is the identity on coarse range coordinates. -/
335 @[simp] theorem coarsenCoordinates_refineCoordinates
336     (packets : PacketSpace coarse) :
337     coarsenCoordinates coarse fine (refineCoordinates coarse fine packets) =
338       packets := by
339   simp [coarsenCoordinates, refineCoordinates]
340 
341 /-- Refinement after coarsening is the identity on fine range coordinates. -/
342 @[simp] theorem refineCoordinates_coarsenCoordinates
343     (packets : PacketSpace fine) :
344     refineCoordinates coarse fine (coarsenCoordinates coarse fine packets) =
345       packets := by
346   simp [coarsenCoordinates, refineCoordinates]
347 
348 /-- The exact linear equivalence between the two independent range products. -/
349 def coordinateRefinementEquiv : PacketSpace coarse ≃ₗ[R] PacketSpace fine where
350   toFun := refineCoordinates coarse fine
351   invFun := coarsenCoordinates coarse fine
352   left_inv := coarsenCoordinates_refineCoordinates coarse fine
353   right_inv := refineCoordinates_coarsenCoordinates coarse fine
354   map_add' := (refineCoordinates coarse fine).map_add
355   map_smul' := (refineCoordinates coarse fine).map_smul
356 
357 @[simp] theorem coordinateRefinementEquiv_apply (packets : PacketSpace coarse) :
358     coordinateRefinementEquiv coarse fine packets =
359       refineCoordinates coarse fine packets := rfl
360 
361 @[simp] theorem coordinateRefinementEquiv_symm_apply (packets : PacketSpace fine) :
362     (coordinateRefinementEquiv coarse fine).symm packets =
363       coarsenCoordinates coarse fine packets := rfl
364 
365 /-! ## Identity and cocycle laws -/
366 
367 /-- Refining a coordinate system to itself is pointwise the identity. -/
368 @[simp] theorem refineCoordinates_self (packets : PacketSpace coarse) :
369     refineCoordinates coarse coarse packets = packets := by
370   simp [refineCoordinates]
371 
372 /-- Coarsening a coordinate system to itself is pointwise the identity. -/
373 @[simp] theorem coarsenCoordinates_self (packets : PacketSpace coarse) :
374     coarsenCoordinates coarse coarse packets = packets := by
375   simp [coarsenCoordinates]
376 
377 /-- Coarsening is definitionally refinement in the reverse direction. -/
378 theorem coarsenCoordinates_eq_refineCoordinates_reverse :
379     coarsenCoordinates coarse fine = refineCoordinates fine coarse := rfl
380 
381 variable (middle : LinearProjectorFamily R M τ)
382 
383 /-- Exact coordinate refinement obeys the pointwise cocycle law. -/
384 @[simp] theorem refineCoordinates_cocycle (packets : PacketSpace coarse) :
385     refineCoordinates middle fine (refineCoordinates coarse middle packets) =
386       refineCoordinates coarse fine packets := by
387   simp [refineCoordinates]
388 
389 /-- The cocycle law as an equality of linear coordinate-change maps. -/
390 theorem refineCoordinates_comp :
391     (refineCoordinates middle fine).comp (refineCoordinates coarse middle) =
392       refineCoordinates coarse fine := by
393   apply LinearMap.ext
394   intro packets
395   exact refineCoordinates_cocycle coarse fine middle packets
396 
397 /-- Reverse coordinate transport obeys the corresponding cocycle law. -/
398 @[simp] theorem coarsenCoordinates_cocycle (packets : PacketSpace fine) :
399     coarsenCoordinates coarse middle (coarsenCoordinates middle fine packets) =
400       coarsenCoordinates coarse fine packets := by
401   simp [coarsenCoordinates]
402 
403 /-- The exact coordinate equivalence at one level is the identity equivalence. -/
404 @[simp] theorem coordinateRefinementEquiv_self :
405     coordinateRefinementEquiv coarse coarse = LinearEquiv.refl R (PacketSpace coarse) := by
406   apply LinearEquiv.ext
407   intro packets
408   simp
409 
410 /-- Reversing the coordinate equivalence swaps its endpoint families. -/
411 theorem coordinateRefinementEquiv_symm :
412     (coordinateRefinementEquiv coarse fine).symm =
413       coordinateRefinementEquiv fine coarse := by
414   apply LinearEquiv.ext
415   intro packets
416   rfl
417 
418 /-- Exact coordinate equivalences compose coherently through an intermediate level. -/
419 theorem coordinateRefinementEquiv_trans :
420     (coordinateRefinementEquiv coarse middle).trans
421         (coordinateRefinementEquiv middle fine) =
422       coordinateRefinementEquiv coarse fine := by
423   apply LinearEquiv.ext
424   intro packets
425   exact refineCoordinates_cocycle coarse fine middle packets
426 
427 end Coordinates
428 
429 /-! ## Typed operator coordinates and naturality -/
430 
431 section CoordinateNaturality
432 
433 variable {N : Type z} {L : Type*}
434 variable [AddCommMonoid N] [Module R N]
435 variable [AddCommMonoid L] [Module R L]
436 variable {ι' : Type*} {κ' : Type*} {τ' : Type*}
437 variable [Fintype ι'] [Fintype κ'] [Fintype τ']
438 
439 /--
440 The typed coordinate representation of a linear map between two independently
441 chosen exact packet systems.
442 -/
443 def coordinateOperator
444     (source : LinearProjectorFamily R M ι)
445     (target : LinearProjectorFamily R N κ')
446     (T : M →ₗ[R] N) : PacketSpace source →ₗ[R] PacketSpace target :=
447   target.rangeAnalysis.comp (T.comp source.rangeSynthesis)
448 
449 @[simp] theorem coordinateOperator_apply
450     (source : LinearProjectorFamily R M ι)
451     (target : LinearProjectorFamily R N κ')
452     (T : M →ₗ[R] N) (packets : PacketSpace source) :
453     coordinateOperator source target T packets =
454       target.rangeAnalysis (T (source.rangeSynthesis packets)) := rfl
455 
456 /-- Analysis intertwines a linear map with its exact coordinate representation. -/
457 @[simp] theorem coordinateOperator_rangeAnalysis
458     (source : LinearProjectorFamily R M ι)
459     (target : LinearProjectorFamily R N κ')
460     (T : M →ₗ[R] N) (x : M) :
461     coordinateOperator source target T (source.rangeAnalysis x) =
462       target.rangeAnalysis (T x) := by
463   simp [coordinateOperator]
464 
465 /-- Synthesis intertwines an exact coordinate representation with its linear map. -/
466 @[simp] theorem rangeSynthesis_coordinateOperator
467     (source : LinearProjectorFamily R M ι)
468     (target : LinearProjectorFamily R N κ')
469     (T : M →ₗ[R] N) (packets : PacketSpace source) :
470     target.rangeSynthesis (coordinateOperator source target T packets) =
471       T (source.rangeSynthesis packets) := by
472   simp [coordinateOperator]
473 
474 /-- Representing the identity between two packet systems is coordinate refinement. -/
475 theorem coordinateOperator_id_eq_refineCoordinates
476     (source : LinearProjectorFamily R M ι)
477     (target : LinearProjectorFamily R M κ) :
478     coordinateOperator source target LinearMap.id =
479       refineCoordinates source target := by
480   apply LinearMap.ext
481   intro packets
482   rfl
483 
484 /-- In one fixed packet system, the represented identity is the identity map. -/
485 @[simp] theorem coordinateOperator_id
486     (source : LinearProjectorFamily R M ι) :
487     coordinateOperator source source LinearMap.id = LinearMap.id := by
488   rw [coordinateOperator_id_eq_refineCoordinates]
489   apply LinearMap.ext
490   intro packets
491   simp
492 
493 /-- Coordinate representation preserves typed composition. -/
494 theorem coordinateOperator_comp
495     (source : LinearProjectorFamily R M ι)
496     (middle : LinearProjectorFamily R N κ')
497     (target : LinearProjectorFamily R L τ')
498     (T : M →ₗ[R] N) (U : N →ₗ[R] L) :
499     (coordinateOperator middle target U).comp
500         (coordinateOperator source middle T) =
501       coordinateOperator source target (U.comp T) := by
502   ext packets
503   simp [coordinateOperator]
504 
505 /--
506 Changing exact coordinates on both source and target commutes with the typed
507 coordinate representation of every linear map.
508 -/
509 theorem coordinateOperator_naturality
510     (sourceCoarse : LinearProjectorFamily R M ι)
511     (sourceFine : LinearProjectorFamily R M κ)
512     (targetCoarse : LinearProjectorFamily R N ι')
513     (targetFine : LinearProjectorFamily R N κ')
514     (T : M →ₗ[R] N) :
515     (refineCoordinates targetCoarse targetFine).comp
516         (coordinateOperator sourceCoarse targetCoarse T) =
517       (coordinateOperator sourceFine targetFine T).comp
518         (refineCoordinates sourceCoarse sourceFine) := by
519   ext packets
520   simp [coordinateOperator, refineCoordinates]
521 
522 /-- The pointwise commuting-square form of coordinate-operator naturality. -/
523 theorem coordinateOperator_naturality_apply
524     (sourceCoarse : LinearProjectorFamily R M ι)
525     (sourceFine : LinearProjectorFamily R M κ)
526     (targetCoarse : LinearProjectorFamily R N ι')
527     (targetFine : LinearProjectorFamily R N κ')
528     (T : M →ₗ[R] N) (packets : PacketSpace sourceCoarse) :
529     refineCoordinates targetCoarse targetFine
530         (coordinateOperator sourceCoarse targetCoarse T packets) =
531       coordinateOperator sourceFine targetFine T
532         (refineCoordinates sourceCoarse sourceFine packets) := by
533   exact LinearMap.congr_fun
534     (coordinateOperator_naturality
535       sourceCoarse sourceFine targetCoarse targetFine T) packets
536 
537 end CoordinateNaturality
538 
539 /-! ## Parent/child formulas for exact coordinates -/
540 
541 namespace Refines
542 
543 variable {coarse : LinearProjectorFamily R M ι}
544 variable {fine : LinearProjectorFamily R M κ}
545 variable {parent : κ → ι}
546 
547 /-- A refined coordinate only sees the coarse coordinate of its parent. -/
548 theorem refineCoordinates_component
549     (h : Refines coarse fine parent) (packets : PacketSpace coarse) (b : κ) :
550     ((refineCoordinates coarse fine packets b :
551       LinearMap.range (fine.proj b)) : M) =
552       fine.proj b (packets (parent b) : M) := by
553   classical
554   change fine.proj b (∑ a, (packets a : M)) = _
555   rw [map_sum]
556   apply Finset.sum_eq_single_of_mem (parent b) (Finset.mem_univ _)
557   intro a _ hab
558   rcases (packets a).property with ⟨x, hx⟩
559   rw [← hx]
560   exact LinearMap.congr_fun
561     (h.fine_comp_coarse_eq_zero (Ne.symm hab)) x
562 
563 /-- A coarsened coordinate is the sum of the fine coordinates over its fibre. -/
564 theorem coarsenCoordinates_component
565     (h : Refines coarse fine parent) (packets : PacketSpace fine) (a : ι) :
566     ((coarsenCoordinates coarse fine packets a :
567       LinearMap.range (coarse.proj a)) : M) =
568       ∑ b ∈ children parent a, (packets b : M) := by
569   classical
570   change coarse.proj a (∑ b, (packets b : M)) = _
571   rw [map_sum]
572   calc
573     (∑ b, coarse.proj a (packets b : M)) =
574         ∑ b, if parent b = a then (packets b : M) else 0 := by
575           apply Finset.sum_congr rfl
576           intro b _
577           rcases (packets b).property with ⟨x, hx⟩
578           rw [← hx]
579           by_cases hb : parent b = a
580           · simp only [hb, ↓reduceIte]
581             exact LinearMap.congr_fun (h.coarse_comp_fine_eq_self hb) x
582           · simp only [hb, ↓reduceIte]
583             exact LinearMap.congr_fun (h.coarse_comp_fine_eq_zero hb) x
584     _ = ∑ b ∈ children parent a, (packets b : M) := by
585       rw [children, Finset.sum_filter]
586 
587 end Refines
588 
589 /-! ## Transfer-block refinement -/
590 
591 section TransferBlocks
592 
593 variable {N : Type z} {ι' : Type*} {κ' : Type*}
594 variable [AddCommMonoid N] [Module R N]
595 variable [Fintype ι'] [Fintype κ']
596 
597 variable {sourceCoarse : LinearProjectorFamily R M ι}
598 variable {sourceFine : LinearProjectorFamily R M κ}
599 variable {targetCoarse : LinearProjectorFamily R N ι'}
600 variable {targetFine : LinearProjectorFamily R N κ'}
601 variable {sourceParent : κ → ι} {targetParent : κ' → ι'}
602 
603 /--
604 Both sides of a linear transfer block refine independently into their fine
605 descendants.  This is the two-module strengthening of the Paper II formula.
606 -/
607 theorem transferBlock_refinement_between
608     (hsource : Refines sourceCoarse sourceFine sourceParent)
609     (htarget : Refines targetCoarse targetFine targetParent)
610     (T : M →ₗ[R] N) (b : ι') (a : ι) :
611     transferBlock sourceCoarse targetCoarse T b a =
612       ∑ β ∈ children targetParent b,
613         ∑ α ∈ children sourceParent a,
614           transferBlock sourceFine targetFine T β α := by
615   classical
616   ext x
617   simp only [transferBlock, LinearMap.comp_apply, LinearMap.sum_apply]
618   rw [hsource.coarse_proj_apply_eq_sum_children, map_sum]
619   calc
620     targetCoarse.proj b
621         (∑ α ∈ children sourceParent a, T (sourceFine.proj α x)) =
622       ∑ α ∈ children sourceParent a,
623         targetCoarse.proj b (T (sourceFine.proj α x)) := by
624           rw [map_sum]
625     _ = ∑ α ∈ children sourceParent a,
626         ∑ β ∈ children targetParent b,
627           targetFine.proj β (T (sourceFine.proj α x)) := by
628           apply Finset.sum_congr rfl
629           intro α _
630           exact htarget.coarse_proj_apply_eq_sum_children b _
631     _ = ∑ β ∈ children targetParent b,
632         ∑ α ∈ children sourceParent a,
633           targetFine.proj β (T (sourceFine.proj α x)) := by
634           exact Finset.sum_comm
635 
636 variable {coarse : LinearProjectorFamily R M ι}
637 variable {fine : LinearProjectorFamily R M κ}
638 variable {parent : κ → ι}
639 
640 /-- Every endomorphism block is the sum of all fine descendant blocks. -/
641 theorem transferBlock_refinement
642     (h : Refines coarse fine parent) (T : Module.End R M) (b a : ι) :
643     transferBlock coarse coarse T b a =
644       ∑ β ∈ children parent b,
645         ∑ α ∈ children parent a,
646           transferBlock fine fine T β α :=
647   transferBlock_refinement_between h h T b a
648 
649 /--
650 Direct traceability wrapper for the complete transfer-block statement in the
651 Paper II manuscript.  It records the refined block identity together with
652 reconstruction of the same linear map from all coarse and all fine blocks.
653 -/
654 theorem transferBlock_refinement_and_reconstruction
655     (hsource : Refines sourceCoarse sourceFine sourceParent)
656     (htarget : Refines targetCoarse targetFine targetParent)
657     (T : M →ₗ[R] N) (b : ι') (a : ι) :
658     transferBlock sourceCoarse targetCoarse T b a =
659         ∑ β ∈ children targetParent b,
660           ∑ α ∈ children sourceParent a,
661             transferBlock sourceFine targetFine T β α ∧
662       (∀ x : M,
663         (∑ β, ∑ α,
664           targetCoarse.proj β (T (sourceCoarse.proj α x))) = T x) ∧
665       (∀ x : M,
666         (∑ β, ∑ α,
667           targetFine.proj β (T (sourceFine.proj α x))) = T x) := by
668   exact ⟨transferBlock_refinement_between hsource htarget T b a,
669     transferBlock_reconstruction sourceCoarse targetCoarse T,
670     transferBlock_reconstruction sourceFine targetFine T⟩
671 
672 end TransferBlocks
673 
674 end Komorebi.PaperII.NestedRefinement
675 
676 #print axioms Komorebi.PaperII.NestedRefinement.Refines.trans
677 #print axioms Komorebi.PaperII.NestedRefinement.coordinateRefinementEquiv
678 #print axioms Komorebi.PaperII.NestedRefinement.finitePacket_decomposition_unique
679 #print axioms Komorebi.PaperII.NestedRefinement.refineCoordinates_comp
680 #print axioms Komorebi.PaperII.NestedRefinement.coordinateRefinementEquiv_trans
681 #print axioms Komorebi.PaperII.NestedRefinement.coordinateOperator_naturality
682 #print axioms Komorebi.PaperII.NestedRefinement.transferBlock_refinement

Back to source controls