GraphReachability.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 open Komorebi.PacketNaturalityCompletion.Reachability
9 open Komorebi.PacketNaturalityCompletion.StrictNaturality
10 
11 universe u v w
12 variable {K : Type u} [Field K]
13 variable {X : Type v} [AddCommGroup X] [Module K X]
14 variable {I : Type w} [Fintype I] [DecidableEq I]
15 
16 def packetGeneratedAlgebra (P : LinearProjectorFamily K X I)
17     (ops : Set (Module.End K X)) : Subalgebra K (Module.End K X) :=
18   Algebra.adjoin K (Set.range P.proj ∪ ops)
19 
20 def packetReachabilityAlgebra (P : LinearProjectorFamily K X I)
21     (ops : Set (Module.End K X)) : Subalgebra K (Module.End K X) :=
22   supportSubalgebra P (Relation.ReflTransGen (TransferEdge P ops))
23     (fun _ => Relation.ReflTransGen.refl) (fun _ _ _ hac hcb => hac.trans hcb)
24 
25 /-- Every element of the algebra generated by the projectors and declared operators
26 has zero blocks outside graph reachability. -/
27 theorem generatedAlgebra_le_reachability (P : LinearProjectorFamily K X I)
28     (ops : Set (Module.End K X)) :
29     packetGeneratedAlgebra P ops ≤ packetReachabilityAlgebra P ops := by
30   apply Algebra.adjoin_le
31   intro T hT
32   apply (operatorSupported_iff_ambient P _ T).mpr
33   intro b a hab
34   rcases hT with ⟨j, rfl⟩ | hT
35   · ext x
36     change P.proj b (P.proj j (P.proj a x)) = 0
37     by_cases hja : j = a
38     · subst j
39       rw [P.idempotent]
40       have hba : b ≠ a := fun h => by subst b; exact hab Relation.ReflTransGen.refl
41       exact P.orthogonal hba x
42     · rw [P.orthogonal hja, map_zero]
43   · by_contra h
44     exact hab (Relation.ReflTransGen.single ⟨T, hT, h⟩)
45 
46 theorem generatedAlgebra_block_zero (P : LinearProjectorFamily K X I)
47     (ops : Set (Module.End K X)) {T : Module.End K X}
48     (hT : T ∈ packetGeneratedAlgebra P ops) {a b : I}
49     (hab : ¬ Relation.ReflTransGen (TransferEdge P ops) a b) :
50     transferBlock P P T b a = 0 :=
51   (operatorSupported_iff_ambient P _ T).mp
52     (generatedAlgebra_le_reachability P ops hT) b a hab
53 
54 /-- The full generated algebra preserves the reachable-support space. -/
55 theorem generatedAlgebra_preserves_reachable (P : LinearProjectorFamily K X I)
56     (ops : Set (Module.End K X)) (S₀ : Set I) {T : Module.End K X}
57     (hT : T ∈ packetGeneratedAlgebra P ops) {x : X}
58     (hx : VectorSupported P (ReachableFrom P ops S₀) x) :
59     VectorSupported P (ReachableFrom P ops S₀) (T x) := by
60   intro b hb
61   calc
62     P.proj b (T x) = ∑ a, P.proj b (T (P.proj a x)) := by
63       rw [← map_sum, ← map_sum, P.complete]
64     _ = 0 := by
65       apply Finset.sum_eq_zero
66       intro a _
67       by_cases ha : ReachableFrom P ops S₀ a
68       · have hab : ¬ Relation.ReflTransGen (TransferEdge P ops) a b := by
69           intro hab
70           rcases ha with ⟨s, hs, hsa⟩
71           exact hb ⟨s, hs, hsa.trans hab⟩
72         exact LinearMap.congr_fun (generatedAlgebra_block_zero P ops hT hab) x
73       · rw [hx a ha, map_zero, map_zero]
74 
75 /-- Printed hull obstruction for the actual algebra adjoined from projectors and generators. -/
76 theorem generatedAlgebra_hull_le_reachable (P : LinearProjectorFamily K X I)
77     (ops : Set (Module.End K X)) (S₀ : Set I) (seeds : Set X)
78     (hseeds : ∀ x ∈ seeds, VectorSupported P S₀ x) :
79     AlgebraGeneratedHull (packetGeneratedAlgebra P ops) seeds ≤
80       supportedSubmodule P (ReachableFrom P ops S₀) := by
81   apply Submodule.span_le.mpr
82   rintro _ ⟨T, s, hs, rfl⟩
83   apply generatedAlgebra_preserves_reachable P ops S₀ T.property
84   intro b hb
85   apply hseeds s hs b
86   intro hb0
87   exact hb (source_reachable P ops S₀ hb0)
88 
89 /-- A nonzero unreachable packet cannot lie in the generated hull. -/
90 theorem generatedAlgebra_unreachable_obstruction (P : LinearProjectorFamily K X I)
91     (ops : Set (Module.End K X)) (S₀ : Set I) (seeds : Set X)
92     (hseeds : ∀ x ∈ seeds, VectorSupported P S₀ x)
93     {b : I} (hb : ¬ ReachableFrom P ops S₀ b) {x : X}
94     (hx : P.proj b x ≠ 0) :
95     x ∉ AlgebraGeneratedHull (packetGeneratedAlgebra P ops) seeds := by
96   intro h
97   exact hx (generatedAlgebra_hull_le_reachable P ops S₀ seeds hseeds h b hb)
98 
99 end Komorebi.PaperIRelease

Back to source controls