PaperITransport.lean

1 import KomorebiVerification.ProjectorCore
2 
3 /-!
4 # Paper I: coordinate transport and block naturality
5 
6 This module formalizes the algebraic content of Paper I, Section 8.  The
7 target-side operator is supplied explicitly in the naturality theorem, avoiding
8 the manuscript's ill-typed expression `φ(T)` when `T` has not been assumed to
9 belong to the domain of `φ`.
10 -/
11 
12 set_option autoImplicit false
13 
14 namespace Komorebi.Foundation
15 
16 universe u v w x
17 
18 variable {R : Type u} {M : Type v} {N : Type w} {ι : Type x}
19 variable [Semiring R]
20 variable [AddCommMonoid M] [Module R M]
21 variable [AddCommMonoid N] [Module R N]
22 variable [Fintype ι]
23 
24 namespace LinearProjectorFamily
25 
26 /-- Transport a finite projector family through a linear equivalence. -/
27 def conjugate
28     (P : LinearProjectorFamily R M ι) (U : M ≃ₗ[R] N) :
29     LinearProjectorFamily R N ι where
30   proj i := U.toLinearMap.comp ((P.proj i).comp U.symm.toLinearMap)
31   idempotent i y := by
32     change U (P.proj i (U.symm (U (P.proj i (U.symm y))))) =
33       U (P.proj i (U.symm y))
34     rw [U.symm_apply_apply, P.idempotent]
35   orthogonal hij y := by
36     change U (P.proj _ (U.symm (U (P.proj _ (U.symm y))))) = 0
37     rw [U.symm_apply_apply, P.orthogonal hij, map_zero]
38   complete y := by
39     change (∑ i, U (P.proj i (U.symm y))) = y
40     rw [← map_sum, P.complete, U.apply_symm_apply]
41 
42 @[simp] theorem conjugate_proj_apply
43     (P : LinearProjectorFamily R M ι) (U : M ≃ₗ[R] N)
44     (i : ι) (y : N) :
45     (P.conjugate U).proj i y = U (P.proj i (U.symm y)) :=
46   rfl
47 
48 end LinearProjectorFamily
49 
50 /-- Conjugate an endomorphism through a linear equivalence. -/
51 def conjugateEnd (U : M ≃ₗ[R] N) (T : Module.End R M) : Module.End R N :=
52   U.toLinearMap.comp (T.comp U.symm.toLinearMap)
53 
54 @[simp] theorem conjugateEnd_apply
55     (U : M ≃ₗ[R] N) (T : Module.End R M) (y : N) :
56     conjugateEnd U T y = U (T (U.symm y)) :=
57   rfl
58 
59 /-- Transfer blocks commute exactly with coordinate conjugation. -/
60 theorem conjugate_transferBlock
61     (P : LinearProjectorFamily R M ι) (U : M ≃ₗ[R] N)
62     (T : Module.End R M) (j i : ι) :
63     transferBlock (P.conjugate U) (P.conjugate U)
64         (conjugateEnd U T) j i =
65       conjugateEnd U (transferBlock P P T j i) := by
66   apply LinearMap.ext
67   intro y
68   simp [transferBlock, conjugateEnd]
69 
70 /--
71 Packet blocks commute with an intertwiner when both the operator and every
72 projector intertwine.  This is the type-correct algebraic naturality statement.
73 -/
74 theorem transferBlock_natural
75     (P : LinearProjectorFamily R M ι)
76     (Q : LinearProjectorFamily R N ι)
77     (Φ : M →ₗ[R] N) (T : Module.End R M) (T' : Module.End R N)
78     (hT : Φ.comp T = T'.comp Φ)
79     (hproj : ∀ i, Φ.comp (P.proj i) = (Q.proj i).comp Φ)
80     (j i : ι) :
81     Φ.comp (transferBlock P P T j i) =
82       (transferBlock Q Q T' j i).comp Φ := by
83   apply LinearMap.ext
84   intro x
85   have hpj (z : M) : Φ (P.proj j z) = Q.proj j (Φ z) := by
86     simpa only [LinearMap.comp_apply] using
87       congrArg (fun f : M →ₗ[R] N => f z) (hproj j)
88   have hTi (z : M) : Φ (T z) = T' (Φ z) := by
89     simpa only [LinearMap.comp_apply] using
90       congrArg (fun f : M →ₗ[R] N => f z) hT
91   have hpi : Φ (P.proj i x) = Q.proj i (Φ x) := by
92     simpa only [LinearMap.comp_apply] using
93       congrArg (fun f : M →ₗ[R] N => f x) (hproj i)
94   change Φ (P.proj j (T (P.proj i x))) =
95     Q.proj j (T' (Q.proj i (Φ x)))
96   rw [hpj, hTi, hpi]
97 
98 end Komorebi.Foundation
99 

Back to source controls