ReleaseCoordinatesAlgebra.lean

1 import KomorebiVerification.PaperII.NestedRefinement
2 
3 /-! Exact manuscript endpoints for block support and coordinate conjugacy. -/
4 set_option autoImplicit false
5 namespace Komorebi.PaperII.NestedRefinement
6 open Komorebi.Foundation Komorebi.Foundation.LinearProjectorFamily
7 universe u v w x y z
8 variable {R : Type u} [Semiring R]
9 variable {M : Type v} {N : Type w}
10 variable [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N]
11 variable {ι : Type x} {κ : Type y} {ι' : Type z} {κ' : Type*}
12 variable [Fintype ι] [Fintype κ] [Fintype ι'] [Fintype κ']
13 
14 /-- Fine blocks are obtained by projecting the corresponding coarse block on both sides. -/
15 theorem transferBlock_descendant
16     {P : LinearProjectorFamily R M ι} {Q : LinearProjectorFamily R M κ}
17     {S : LinearProjectorFamily R N ι'} {V : LinearProjectorFamily R N κ'}
18     {p : κ → ι} {q : κ' → ι'} (hp : Refines P Q p) (hq : Refines S V q)
19     (T : M →ₗ[R] N) (β : κ') (α : κ) :
20     (V.proj β).comp ((transferBlock P S T (q β) (p α)).comp (Q.proj α)) =
21       transferBlock Q V T β α := by
22   ext x
23   simp only [transferBlock, LinearMap.comp_apply]
24   rw [hp.coarse_fine_apply_eq_self, hq.fine_coarse_apply_eq_self]
25 
26 /-- A coarse block vanishes exactly when every descendant fine block vanishes. -/
27 theorem transferBlock_eq_zero_iff_descendants
28     {P : LinearProjectorFamily R M ι} {Q : LinearProjectorFamily R M κ}
29     {S : LinearProjectorFamily R N ι'} {V : LinearProjectorFamily R N κ'}
30     {p : κ → ι} {q : κ' → ι'} (hp : Refines P Q p) (hq : Refines S V q)
31     (T : M →ₗ[R] N) (b : ι') (a : ι) :
32     transferBlock P S T b a = 0 ↔
33       ∀ β ∈ children q b, ∀ α ∈ children p a, transferBlock Q V T β α = 0 := by
34   classical
35   constructor
36   · intro hz β hβ α hα
37     have hb := (mem_children q b β).mp hβ
38     have ha := (mem_children p a α).mp hα
39     have h := transferBlock_descendant hp hq T β α
40     rw [hb, ha, hz, LinearMap.zero_comp, LinearMap.comp_zero] at h
41     exact h.symm
42   · intro h
43     rw [transferBlock_refinement_between hp hq]
44     apply Finset.sum_eq_zero
45     intro β hβ
46     apply Finset.sum_eq_zero
47     intro α hα
48     exact h β hβ α hα
49 
50 /-- Exact operator coordinates transform by synthesis/analysis conjugacy. -/
51 theorem coordinateOperator_conjugation
52     (P : LinearProjectorFamily R M ι) (Q : LinearProjectorFamily R M κ)
53     (S : LinearProjectorFamily R N ι') (V : LinearProjectorFamily R N κ')
54     (T : M →ₗ[R] N) :
55     (coarsenCoordinates S V).comp
56         ((coordinateOperator Q V T).comp (refineCoordinates P Q)) =
57       coordinateOperator P S T := by
58   ext packets
59   simp [coordinateOperator, coarsenCoordinates, refineCoordinates]
60 
61 end Komorebi.PaperII.NestedRefinement
62 
63 #print axioms Komorebi.PaperII.NestedRefinement.transferBlock_eq_zero_iff_descendants
64 #print axioms Komorebi.PaperII.NestedRefinement.coordinateOperator_conjugation

Back to source controls