AlgebraDiagonal.lean

1 import PaperIRelease.AlgebraSupport
2 
3 set_option autoImplicit false
4 set_option maxHeartbeats 2000000
5 
6 namespace Komorebi.PaperIRelease
7 open Komorebi.Foundation
8 
9 universe u v w
10 variable {K : Type u} [Field K]
11 variable {X : Type v} [AddCommGroup X] [Module K X]
12 variable {I : Type w} [Fintype I]
13 
14 /-- The literal diagonal-block projection on the ambient endomorphism space. -/
15 def diagonalProjection (P : LinearProjectorFamily K X I) :
16     Module.End K (Module.End K X) where
17   toFun T := ∑ i, transferBlock P P T i i
18   map_add' S T := by
19     ext x
20     simp [transferBlock, Finset.sum_add_distrib]
21   map_smul' c T := by
22     ext x
23     simp [transferBlock, Finset.smul_sum]
24 
25 @[simp] theorem diagonalProjection_apply (P : LinearProjectorFamily K X I)
26     (T : Module.End K X) (x : X) :
27     diagonalProjection P T x = ∑ i, P.proj i (T (P.proj i x)) := by
28   simp [diagonalProjection, transferBlock]
29 
30 theorem proj_diagonalProjection (P : LinearProjectorFamily K X I)
31     (T : Module.End K X) (i : I) (x : X) :
32     P.proj i (diagonalProjection P T x) = P.proj i (T (P.proj i x)) := by
33   classical
34   rw [diagonalProjection_apply]
35   rw [map_sum, Finset.sum_eq_single i]
36   · exact P.idempotent i _
37   · intro j _ hji
38     exact P.orthogonal hji.symm _
39   · simp
40 
41 theorem diagonalProjection_proj (P : LinearProjectorFamily K X I)
42     (T : Module.End K X) (i : I) (x : X) :
43     diagonalProjection P T (P.proj i x) = P.proj i (T (P.proj i x)) := by
44   classical
45   rw [diagonalProjection_apply]
46   rw [Finset.sum_eq_single i]
47   · rw [P.idempotent]
48   · intro j _ hji
49     rw [P.orthogonal hji, map_zero, map_zero]
50   · simp
51 
52 theorem diagonalProjection_commutes (P : LinearProjectorFamily K X I)
53     (T : Module.End K X) (i : I) :
54     (diagonalProjection P T).comp (P.proj i) = (P.proj i).comp (diagonalProjection P T) := by
55   ext x
56   exact (diagonalProjection_proj P T i x).trans (proj_diagonalProjection P T i x).symm
57 
58 theorem diagonalProjection_of_commutes (P : LinearProjectorFamily K X I)
59     (T : Module.End K X)
60     (h : ∀ i, T.comp (P.proj i) = (P.proj i).comp T) :
61     diagonalProjection P T = T := by
62   ext x
63   rw [diagonalProjection_apply]
64   calc
65     (∑ i, P.proj i (T (P.proj i x))) = ∑ i, T (P.proj i x) := by
66       apply Finset.sum_congr rfl
67       intro i _
68       have hh := LinearMap.congr_fun (h i) (P.proj i x)
69       simpa only [LinearMap.comp_apply, P.idempotent] using hh.symm
70     _ = T x := by rw [← map_sum, P.complete]
71 
72 theorem commutes_iff_diagonalProjection (P : LinearProjectorFamily K X I)
73     (T : Module.End K X) :
74     (∀ i, T.comp (P.proj i) = (P.proj i).comp T) ↔ diagonalProjection P T = T := by
75   constructor
76   · exact diagonalProjection_of_commutes P T
77   · intro h i
78     rw [← h]
79     exact diagonalProjection_commutes P T i
80 
81 theorem diagonalProjection_idempotent (P : LinearProjectorFamily K X I)
82     (T : Module.End K X) :
83     diagonalProjection P (diagonalProjection P T) = diagonalProjection P T :=
84   diagonalProjection_of_commutes P _ (diagonalProjection_commutes P T)
85 
86 theorem offdiagonal_zero_of_commutes (P : LinearProjectorFamily K X I)
87     (T : Module.End K X)
88     (h : ∀ i, T.comp (P.proj i) = (P.proj i).comp T)
89     {b a : I} (hba : b ≠ a) : transferBlock P P T b a = 0 := by
90   ext x
91   change P.proj b (T (P.proj a x)) = 0
92   have hh := LinearMap.congr_fun (h a) x
93   change T (P.proj a x) = P.proj a (T x) at hh
94   rw [hh, P.orthogonal hba]
95 
96 theorem diagonalProjection_of_offdiagonal_zero (P : LinearProjectorFamily K X I)
97     (T : Module.End K X)
98     (h : ∀ b a, b ≠ a → transferBlock P P T b a = 0) :
99     diagonalProjection P T = T := by
100   classical
101   ext x
102   calc
103     diagonalProjection P T x = ∑ b, ∑ a, P.proj b (T (P.proj a x)) := by
104       rw [diagonalProjection_apply]
105       apply Finset.sum_congr rfl
106       intro b _
107       symm
108       rw [Finset.sum_eq_single b]
109       · intro a _ hab
110         exact LinearMap.congr_fun (h b a hab.symm) x
111       · simp
112     _ = T x := transferBlock_reconstruction P P T x
113 
114 /-- The three commutant criteria are equivalent for actual ambient operators. -/
115 theorem commutes_iff_offdiagonal_zero (P : LinearProjectorFamily K X I)
116     (T : Module.End K X) :
117     (∀ i, T.comp (P.proj i) = (P.proj i).comp T) ↔
118     (∀ b a, b ≠ a → transferBlock P P T b a = 0) := by
119   constructor
120   · intro h b a hba
121     exact offdiagonal_zero_of_commutes P T h hba
122   · intro h
123     exact (commutes_iff_diagonalProjection P T).mpr
124       (diagonalProjection_of_offdiagonal_zero P T h)
125 
126 variable [DecidableEq I]
127 
128 def blockDiagonalSubalgebra (P : LinearProjectorFamily K X I) :
129     Subalgebra K (Module.End K X) :=
130   supportSubalgebra P Eq (fun _ => rfl) (fun _ _ _ hab hbc => hab.trans hbc)
131 
132 /-- The range of the linear idempotent is precisely the block-diagonal subalgebra. -/
133 theorem diagonalProjection_range (P : LinearProjectorFamily K X I) :
134     LinearMap.range (diagonalProjection P) = (blockDiagonalSubalgebra P).toSubmodule := by
135   ext T
136   constructor
137   · rintro ⟨S, rfl⟩
138     apply (operatorSupported_iff_ambient P Eq _).mpr
139     intro b a hab
140     exact offdiagonal_zero_of_commutes P _ (diagonalProjection_commutes P S) (Ne.symm hab)
141   · intro h
142     have hh := (operatorSupported_iff_ambient P Eq T).mp h
143     exact ⟨T, diagonalProjection_of_offdiagonal_zero P T (fun b a hba => hh b a hba.symm)⟩
144 
145 end Komorebi.PaperIRelease

Back to source controls