PaperIBlockCompletion.lean

1 import KomorebiVerification.ProjectorCore
2 
3 /-!
4 # Paper I: operator-level block completion
5 
6 This file upgrades the pointwise transfer-block formulas in `ProjectorCore` to
7 equalities of linear maps.  It also records sharp converses for support of the
8 ordinary identity matrix and closure of ordinary supported matrices under
9 multiplication.
10 -/
11 
12 set_option autoImplicit false
13 
14 namespace Komorebi
15 
16 namespace Foundation
17 
18 universe u v w x y z
19 
20 variable {R : Type u} {M : Type v} {N : Type w} {L : Type x}
21 variable {ι : Type y} {κ : Type z} {τ : Type*}
22 variable [Semiring R]
23 variable [AddCommMonoid M] [Module R M]
24 variable [AddCommMonoid N] [Module R N]
25 variable [AddCommMonoid L] [Module R L]
26 variable [Fintype ι] [Fintype κ] [Fintype τ]
27 
28 /-- A linear map is the finite sum of all of its transfer blocks. -/
29 theorem transferBlock_reconstruction_linearMap
30     (P : LinearProjectorFamily R M ι)
31     (Q : LinearProjectorFamily R N κ)
32     (T : M →ₗ[R] N) :
33     (∑ j, ∑ i, transferBlock P Q T j i) = T := by
34   ext x
35   simp only [LinearMap.sum_apply]
36   exact transferBlock_reconstruction P Q T x
37 
38 /-- Endomorphism-specialized operator-level transfer-block reconstruction. -/
39 theorem transferBlock_reconstruction_end
40     (P : LinearProjectorFamily R M ι) (T : Module.End R M) :
41     (∑ j, ∑ i, transferBlock P P T j i) = T :=
42   transferBlock_reconstruction_linearMap P P T
43 
44 /--
45 The `(k,i)` transfer block of a composite is the sum, over the intermediate
46 packet, of the corresponding composites of transfer blocks.
47 -/
48 theorem transferBlock_comp_linearMap
49     (P : LinearProjectorFamily R M ι)
50     (Q : LinearProjectorFamily R N κ)
51     (S : LinearProjectorFamily R L τ)
52     (T : M →ₗ[R] N) (U : N →ₗ[R] L)
53     (k : τ) (i : ι) :
54     transferBlock P S (U.comp T) k i =
55       ∑ j, (transferBlock Q S U k j).comp (transferBlock P Q T j i) := by
56   ext x
57   simp only [LinearMap.sum_apply, transferBlock, LinearMap.comp_apply,
58     Q.idempotent]
59   exact transferBlock_comp P Q S T U k i x
60 
61 /-- Endomorphism-specialized block multiplication formula. -/
62 theorem transferBlock_comp_end
63     (P : LinearProjectorFamily R M ι)
64     (T U : Module.End R M) (k i : ι) :
65     transferBlock P P (U.comp T) k i =
66       ∑ j, (transferBlock P P U k j).comp (transferBlock P P T j i) :=
67   transferBlock_comp_linearMap P P P T U k i
68 
69 /-- Reconstruct a composite endomorphism from its blockwise products. -/
70 theorem end_comp_eq_sum_transferBlock_comps
71     (P : LinearProjectorFamily R M ι) (T U : Module.End R M) :
72     U.comp T =
73       ∑ k, ∑ i, ∑ j,
74         (transferBlock P P U k j).comp (transferBlock P P T j i) := by
75   rw [← transferBlock_reconstruction_end P (U.comp T)]
76   apply Finset.sum_congr rfl
77   intro k hk
78   apply Finset.sum_congr rfl
79   intro i hi
80   exact transferBlock_comp_end P T U k i
81 
82 end Foundation
83 
84 namespace Algebra
85 
86 universe u v
87 
88 /-- Closure of relation-supported ordinary square matrices under multiplication. -/
89 def MatrixSupportMulClosed
90     {ι : Type u} {A : Type v}
91     [Fintype ι] [DecidableEq ι] [Semiring A]
92     (rel : ι → ι → Prop) : Prop :=
93   ∀ M N : Matrix ι ι A,
94     MatrixSupported rel M → MatrixSupported rel N → MatrixSupported rel (M * N)
95 
96 /-- The ordinary identity matrix has support in `rel` exactly when `rel` is reflexive. -/
97 theorem matrixSupported_one_iff_reflexive
98     {ι : Type u} {A : Type v}
99     [DecidableEq ι] [Semiring A] [Nontrivial A]
100     (rel : ι → ι → Prop) :
101     MatrixSupported rel (1 : Matrix ι ι A) ↔ ∀ i, rel i i := by
102   constructor
103   · intro h i
104     by_contra hii
105     have hzero : (1 : Matrix ι ι A) i i = 0 := h i i hii
106     rw [Matrix.one_apply, ite_eq_left rfl] at hzero
107     exact (one_ne_zero : (1 : A) ≠ 0) hzero
108   · intro hrefl i j hij
109     have hne : i ≠ j := by
110       intro h
111       subst j
112       exact hij (hrefl i)
113     simp [hne]
114 
115 /--
116 Supported ordinary matrices are closed under multiplication exactly when the
117 support relation is transitive.  `Nontrivial A` is needed for the converse so
118 that matrix units can detect a missing composite edge.
119 -/
120 theorem matrixSupportMulClosed_iff_transitive
121     {ι : Type u} {A : Type v}
122     [Fintype ι] [DecidableEq ι] [Semiring A] [Nontrivial A]
123     (rel : ι → ι → Prop) :
124     MatrixSupportMulClosed (A := A) rel ↔
125       ∀ i j k, rel i j → rel j k → rel i k := by
126   constructor
127   · intro hclosed i j k hij hjk
128     let Eij : Matrix ι ι A := Matrix.single i j 1
129     let Ejk : Matrix ι ι A := Matrix.single j k 1
130     have hEij : MatrixSupported rel Eij := by
131       intro a b hab
132       change (if i = a ∧ j = b then (1 : A) else 0) = 0
133       split_ifs with h
134       · rcases h with ⟨rfl, rfl⟩
135         exact (hab hij).elim
136       · rfl
137     have hEjk : MatrixSupported rel Ejk := by
138       intro a b hab
139       change (if j = a ∧ k = b then (1 : A) else 0) = 0
140       split_ifs with h
141       · rcases h with ⟨rfl, rfl⟩
142         exact (hab hjk).elim
143       · rfl
144     by_contra hik
145     have hzero : (Eij * Ejk) i k = 0 :=
146       hclosed Eij Ejk hEij hEjk i k hik
147     have hone : (Eij * Ejk) i k = 1 := by
148       simp [Eij, Ejk, Matrix.mul_apply, Matrix.single_apply]
149     exact (one_ne_zero : (1 : A) ≠ 0) (hone.symm.trans hzero)
150   · intro htrans M N hM hN
151     exact MatrixSupported.mul htrans hM hN
152 
153 end Algebra
154 
155 end Komorebi

Back to source controls