AlgebraSupport.lean

1 import KomorebiVerification.PacketNaturalityCompletion
2 
3 set_option autoImplicit false
4 set_option maxHeartbeats 2000000
5 
6 namespace Komorebi.PaperIRelease
7 open Komorebi.Foundation
8 open Komorebi.PacketNaturalityCompletion.FullBlocks
9 
10 universe u v w
11 variable {K : Type u} [Field K]
12 variable {X : Type v} [AddCommGroup X] [Module K X]
13 variable {I : Type w} [Fintype I]
14 
15 /-- Relation arguments are source first and target second. -/
16 def OperatorSupported (P : LinearProjectorFamily K X I)
17     (rel : I → I → Prop) (T : Module.End K X) : Prop :=
18   BlocksSupported P rel (restrictBlocks P T)
19 
20 /-- The range-restricted and ambient formulations of zero transfer agree. -/
21 theorem restricted_block_zero_iff
22     (P : LinearProjectorFamily K X I) (T : Module.End K X) (b a : I) :
23     restrictBlocks P T b a = 0 ↔ transferBlock P P T b a = 0 := by
24   constructor
25   · intro h
26     ext x
27     have hh := LinearMap.congr_fun h (packetProjection P a x)
28     exact congrArg Subtype.val hh
29   · intro h
30     ext x
31     have hh := LinearMap.congr_fun h (x : X)
32     change P.proj b (T (x : X)) = 0
33     have hx : P.proj a (x : X) = x := by
34       rcases x.property with ⟨y, hy⟩
35       rw [← hy]
36       exact P.idempotent a y
37     simpa only [transferBlock, LinearMap.comp_apply, LinearMap.zero_apply, hx] using hh
38 
39 /-- Exact correspondence with the support space printed in Paper I. -/
40 theorem operatorSupported_iff_ambient
41     (P : LinearProjectorFamily K X I) (rel : I → I → Prop) (T : Module.End K X) :
42     OperatorSupported P rel T ↔ ∀ b a, ¬ rel a b → transferBlock P P T b a = 0 := by
43   constructor
44   · intro h b a hab
45     exact (restricted_block_zero_iff P T b a).mp (h b a hab)
46   · intro h b a hab
47     exact (restricted_block_zero_iff P T b a).mpr (h b a hab)
48 
49 variable [DecidableEq I]
50 
51 /-- Ambient operators with a prescribed zero pattern form a linear subspace. -/
52 def supportSubmodule (P : LinearProjectorFamily K X I) (rel : I → I → Prop) :
53     Submodule K (Module.End K X) where
54   carrier := {T | OperatorSupported P rel T}
55   zero_mem' := by intro b a hab; ext x; simp [restrictBlocks, packetProjection, packetInclusion]
56   add_mem' := by
57     intro S T hS hT b a hab
58     have h := (restrictBlocksLinear P).map_add S T
59     have hh := congrFun (congrFun h b) a
60     change restrictBlocks P (S + T) b a = restrictBlocks P S b a + restrictBlocks P T b a at hh
61     change restrictBlocks P (S + T) b a = 0
62     rw [hh, hS b a hab, hT b a hab]
63     exact add_zero _
64   smul_mem' := by
65     intro c T hT b a hab
66     have h := (restrictBlocksLinear P).map_smul c T
67     have hh := congrFun (congrFun h b) a
68     change restrictBlocks P (c • T) b a = c • restrictBlocks P T b a at hh
69     change restrictBlocks P (c • T) b a = 0
70     rw [hh, hT b a hab]
71     exact smul_zero _
72 
73 /-- Ambient multiplication closure is exactly block multiplication closure. -/
74 theorem support_mul_closed_iff
75     (P : LinearProjectorFamily K X I) (rel : I → I → Prop) :
76     (∀ S T : Module.End K X, OperatorSupported P rel S → OperatorSupported P rel T →
77       OperatorSupported P rel (S * T)) ↔ BlockMulClosed P rel := by
78   constructor
79   · intro h B C hB hC
80     obtain ⟨S, rfl⟩ := restrictBlocks_surjective P B
81     obtain ⟨T, rfl⟩ := restrictBlocks_surjective P C
82     have hh := h S T hB hC
83     change BlocksSupported P rel (restrictBlocks P (S.comp T)) at hh
84     rw [restrictBlocks_comp] at hh
85     exact hh
86   · intro h S T hS hT
87     change BlocksSupported P rel (restrictBlocks P (S.comp T))
88     rw [restrictBlocks_comp]
89     exact h _ _ hS hT
90 
91 /-- The support space is a unital subalgebra for every reflexive transitive pattern. -/
92 def supportSubalgebra (P : LinearProjectorFamily K X I) (rel : I → I → Prop)
93     (hrefl : ∀ a, rel a a) (htrans : ∀ a c b, rel a c → rel c b → rel a b) :
94     Subalgebra K (Module.End K X) where
95   carrier := {T | OperatorSupported P rel T}
96   zero_mem' := (supportSubmodule P rel).zero_mem
97   add_mem' := fun hS hT => (supportSubmodule P rel).add_mem hS hT
98   mul_mem' := fun hS hT =>
99     (support_mul_closed_iff P rel).mpr (blockMulClosed_of_transitive P rel htrans) _ _ hS hT
100   algebraMap_mem' c := by
101     intro b a hab
102     have hba : b ≠ a := fun h => by subst b; exact hab (hrefl a)
103     ext x
104     change P.proj b (c • (x : X)) = 0
105     rw [map_smul]
106     have hx : P.proj b (x : X) = 0 := by
107       rcases x.property with ⟨y, hy⟩
108       rw [← hy]
109       exact P.orthogonal hba y
110     rw [hx, smul_zero]
111 
112 /-- Both hard converses are transported back to the ambient operator space. -/
113 theorem support_pattern_algebra_criterion
114     (P : LinearProjectorFamily K X I)
115     [∀ i, Nontrivial (LinearMap.range (P.proj i))] (rel : I → I → Prop) :
116     (∃ A : Subalgebra K (Module.End K X),
117       ∀ T, T ∈ A ↔ OperatorSupported P rel T) ↔
118     (∀ a, rel a a) ∧ (∀ a c b, rel a c → rel c b → rel a b) := by
119   constructor
120   · rintro ⟨A, hA⟩
121     refine ⟨(identity_blocks_supported_iff_reflexive P rel).mp ((hA 1).mp A.one_mem), ?_⟩
122     apply (blockMulClosed_iff_transitive P rel).mp
123     apply (support_mul_closed_iff P rel).mp
124     intro S T hS hT
125     exact (hA (S*T)).mp (A.mul_mem ((hA S).mpr hS) ((hA T).mpr hT))
126   · rintro ⟨hrefl, htrans⟩
127     exact ⟨supportSubalgebra P rel hrefl htrans, fun _ => Iff.rfl⟩
128 
129 end Komorebi.PaperIRelease

Back to source controls