GraphPropagation.lean

1 import PaperIRelease.GraphSources
2 
3 /-! Surjective transfer blocks propagate entire actual packet ranges.
4 The graph is the declared generator TransferEdge graph, and the available
5 blocks are operators in its actual generated algebra. -/
6 
7 noncomputable section
8 set_option autoImplicit false
9 set_option maxHeartbeats 2000000
10 
11 namespace Komorebi.PaperIRelease
12 open Komorebi.Foundation
13 open Komorebi.PacketNaturalityCompletion.Reachability
14 open Komorebi.PacketNaturalityCompletion.FullBlocks
15 open Komorebi.PacketNaturalityCompletion.StrictNaturality
16 open FiniteDigraph
17 
18 universe u v w
19 variable {K : Type u} [Field K]
20 variable {X : Type v} [AddCommGroup X] [Module K X]
21 variable {I : Type w} [Fintype I]
22 
23 /-- Literal edge-surjectivity: for every actual generator edge, some operator
24 in the generated algebra has a surjective source-to-target restricted block. -/
25 def EdgeSurjective (P : LinearProjectorFamily K X I)
26     (ops : Set (Module.End K X)) : Prop :=
27   ∀ ⦃a b : I⦄, TransferEdge P ops a b →
28     ∃ T : packetGeneratedAlgebra P ops, Function.Surjective (restrictBlocks P T.val b a)
29 
30 def AlgebraInvariant (A : Subalgebra K (Module.End K X)) (H : Submodule K X) : Prop :=
31   ∀ T ∈ A, ∀ x ∈ H, T x ∈ H
32 
33 theorem projector_mem_generatedAlgebra (P : LinearProjectorFamily K X I)
34     (ops : Set (Module.End K X)) (a : I) : P.proj a ∈ packetGeneratedAlgebra P ops :=
35   Algebra.subset_adjoin (Or.inl ⟨a, rfl⟩)
36 
37 theorem algebraGeneratedHull_invariant (A : Subalgebra K (Module.End K X))
38     (S : Set X) : AlgebraInvariant A (AlgebraGeneratedHull A S) := by
39   intro T hT x hx
40   induction hx using Submodule.span_induction with
41   | mem x hx =>
42     obtain ⟨U, s, hs, rfl⟩ := hx
43     exact Submodule.subset_span ⟨⟨T * U.val, A.mul_mem hT U.property⟩, s, hs, rfl⟩
44   | zero => simpa only [map_zero] using (AlgebraGeneratedHull A S).zero_mem
45   | add x y hx hy ihx ihy =>
46     simpa only [map_add] using (AlgebraGeneratedHull A S).add_mem ihx ihy
47   | smul c x hx ih =>
48     simpa only [map_smul] using (AlgebraGeneratedHull A S).smul_mem c ih
49 
50 theorem transferBlock_preserves_invariant (P : LinearProjectorFamily K X I)
51     (ops : Set (Module.End K X)) (H : Submodule K X)
52     (hH : AlgebraInvariant (packetGeneratedAlgebra P ops) H)
53     {T : Module.End K X} (hT : T ∈ packetGeneratedAlgebra P ops) (b a : I)
54     {x : X} (hx : x ∈ H) : transferBlock P P T b a x ∈ H := by
55   exact hH _ (projector_mem_generatedAlgebra P ops b) _
56     (hH T hT _ (hH _ (projector_mem_generatedAlgebra P ops a) x hx))
57 
58 /-- Surjectivity of the literal restricted block transfers range containment. -/
59 theorem range_le_of_surjective_block (P : LinearProjectorFamily K X I)
60     (H : Submodule K X) (T : Module.End K X) (a b : I)
61     (hsurj : Function.Surjective (restrictBlocks P T b a))
62     (hstable : ∀ x ∈ H, transferBlock P P T b a x ∈ H)
63     (ha : LinearMap.range (P.proj a) ≤ H) : LinearMap.range (P.proj b) ≤ H := by
64   intro y hy
65   obtain ⟨x, hx⟩ := hsurj ⟨y, hy⟩
66   have hxself : P.proj a (x : X) = x := by
67     obtain ⟨z, hz⟩ := x.property
68     rw [← hz]
69     exact P.idempotent a z
70   have heq : transferBlock P P T b a (x : X) = y := by
71     have heq := congrArg Subtype.val hx
72     change P.proj b (T (x : X)) = y at heq
73     simpa only [transferBlock, LinearMap.comp_apply, hxself] using heq
74   rw [← heq]
75   exact hstable x (ha x.property)
76 
77 theorem edge_range_le (P : LinearProjectorFamily K X I)
78     (ops : Set (Module.End K X)) (hedges : EdgeSurjective P ops)
79     (H : Submodule K X) (hH : AlgebraInvariant (packetGeneratedAlgebra P ops) H)
80     {a b : I} (hab : TransferEdge P ops a b)
81     (ha : LinearMap.range (P.proj a) ≤ H) : LinearMap.range (P.proj b) ≤ H := by
82   obtain ⟨T, hT⟩ := hedges hab
83   exact range_le_of_surjective_block P H T.val a b hT
84     (fun _ hx => transferBlock_preserves_invariant P ops H hH T.property b a hx) ha
85 
86 /-- Surjective edges propagate a full packet along every finite directed path. -/
87 theorem reachable_range_le (P : LinearProjectorFamily K X I)
88     (ops : Set (Module.End K X)) (hedges : EdgeSurjective P ops)
89     (H : Submodule K X) (hH : AlgebraInvariant (packetGeneratedAlgebra P ops) H)
90     {a b : I} (hab : Reach (TransferEdge P ops) a b)
91     (ha : LinearMap.range (P.proj a) ≤ H) : LinearMap.range (P.proj b) ≤ H := by
92   induction hab with
93   | refl => exact ha
94   | tail hab hbc ih => exact edge_range_le P ops hedges H hH hbc ih
95 
96 /-- A variant for a subspace invariant only under blocks internal to one SCC.
97 This is the propagation needed for local corner-algebra cyclicity. -/
98 theorem reachable_range_le_in_component (P : LinearProjectorFamily K X I)
99     (ops : Set (Module.End K X)) (hedges : EdgeSurjective P ops)
100     (C : SCC (TransferEdge P ops)) (H : Submodule K X)
101     (hH : ∀ a b, component (TransferEdge P ops) a = C →
102       component (TransferEdge P ops) b = C → ∀ T ∈ packetGeneratedAlgebra P ops,
103       ∀ x ∈ H, transferBlock P P T b a x ∈ H)
104     {a b : I} (hab : Reach (TransferEdge P ops) a b) :
105     component (TransferEdge P ops) a = C → component (TransferEdge P ops) b = C →
106       LinearMap.range (P.proj a) ≤ H → LinearMap.range (P.proj b) ≤ H := by
107   induction hab using Relation.ReflTransGen.head_induction_on with
108   | refl => intro _ _ ha; exact ha
109   | @head a c hac hcb ih =>
110     intro ha hb hrange
111     have hc : component (TransferEdge P ops) c = C := by
112       exact (intermediate_same_component (TransferEdge P ops) (ha.trans hb.symm)
113         (.single hac) hcb).trans ha
114     apply ih hc hb
115     obtain ⟨T, hT⟩ := hedges hac
116     exact range_le_of_surjective_block P H T.val a c hT (hH a c ha hc T.val T.property) hrange
117 
118 /-- Whole source components generate the ambient space: finite source existence
119 and graph reachability are conclusions of the previous graph theorem. -/
120 theorem submodule_eq_top_of_sources (P : LinearProjectorFamily K X I)
121     (ops : Set (Module.End K X)) (hedges : EdgeSurjective P ops)
122     (H : Submodule K X) (hH : AlgebraInvariant (packetGeneratedAlgebra P ops) H)
123     (hsources : ∀ C : Sources (TransferEdge P ops), ∀ a,
124       component (TransferEdge P ops) a = C.val → LinearMap.range (P.proj a) ≤ H) :
125     H = ⊤ := by
126   apply top_unique
127   intro x _
128   rw [← P.complete x]
129   apply H.sum_mem
130   intro b _
131   obtain ⟨C, a, ha, hab⟩ := exists_source_reaching (TransferEdge P ops) b
132   exact reachable_range_le P ops hedges H hH hab (hsources C a ha) ⟨x, rfl⟩
133 
134 variable [DecidableEq I]
135 
136 /-- The generated algebra has zero blocks from outside into a source SCC. -/
137 theorem source_block_zero (P : LinearProjectorFamily K X I)
138     (ops : Set (Module.End K X)) (C : Sources (TransferEdge P ops))
139     {a b : I} (ha : component (TransferEdge P ops) a ≠ C.val)
140     (hb : component (TransferEdge P ops) b = C.val)
141     {T : Module.End K X} (hT : T ∈ packetGeneratedAlgebra P ops) :
142     transferBlock P P T b a = 0 := by
143   apply generatedAlgebra_block_zero P ops hT
144   intro hab
145   exact ha (no_reach_into_source (TransferEdge P ops) C hb hab)
146 
147 end Komorebi.PaperIRelease

Back to source controls