GraphSourceCount.lean

1 import PaperIRelease.PacketLocalRank
2 import PaperIRelease.GraphSourceProjection
3 
4 set_option autoImplicit false
5 set_option linter.unnecessarySimpa false
6 set_option maxHeartbeats 3000000
7 noncomputable section
8 
9 namespace Komorebi.PaperIRelease
10 open Cardinal Set Komorebi.Foundation Komorebi.SeedRankBasics
11 open Komorebi.PacketNaturalityCompletion.Reachability
12 open FiniteDigraph PacketAggregation
13 
14 universe u
15 variable {K X I : Type u} [Field K] [AddCommGroup X] [Module K X] [Fintype I]
16 
17 /-- Cyclicity is under the actual diagonal corner of the generated operator algebra. -/
18 def PacketCornerCyclic (P : LinearProjectorFamily K X I)
19     (ops : Set (Module.End K X)) : Prop :=
20   ∀ i, Cyclic (packetCornerAlgebra (packetGeneratedAlgebra P ops) (P.proj i)
21     (projector_mem_generatedAlgebra P ops i) (P.idempotent i)) (LinearMap.range (P.proj i))
22 
23 /-- Literal packet propagation combines actual edge surjections and actual corner cyclicity. -/
24 def PacketPropagating (P : LinearProjectorFamily K X I)
25     (ops : Set (Module.End K X)) : Prop := EdgeSurjective P ops ∧ PacketCornerCyclic P ops
26 
27 /-- One cyclic seed at one vertex per source component supplies the global upper bound. -/
28 theorem packetPureSeedRank_le_source_count (P : LinearProjectorFamily K X I)
29     (ops : Set (Module.End K X)) (hedges : EdgeSurjective P ops)
30     (hcyclic : PacketCornerCyclic P ops) :
31     packetPureSeedRank (packetGeneratedAlgebra P ops) P ≤ #(Sources (TransferEdge P ops)) := by
32   classical
33   let A := packetGeneratedAlgebra P ops
34   let edge := TransferEdge P ops
35   choose s hs using hcyclic
36   choose vertex hv using (fun C : Sources edge => component_surjective edge C.val)
37   let seed : Sources edge → X := fun C => (s (vertex C) : X)
38   let H : Submodule A X := Submodule.span A (Set.range seed)
39   have hpacket (C : Sources edge) : LinearMap.range (P.proj (vertex C)) ≤ H.restrictScalars K := by
40     intro x hx
41     have hgen := hs (vertex C)
42     have hxs : (⟨x,hx⟩ : LinearMap.range (P.proj (vertex C))) ∈
43         Submodule.span (packetCornerAlgebra A (P.proj (vertex C))
44           (projector_mem_generatedAlgebra P ops (vertex C)) (P.idempotent (vertex C)))
45             {s (vertex C)} := by
46       rw [hgen]
47       trivial
48     refine Submodule.span_induction
49       (p := fun (y : LinearMap.range (P.proj (vertex C))) _ => (y : X) ∈ H) ?_ ?_ ?_ ?_ hxs
50     · intro y hy
51       have hy' : y = s (vertex C) := Set.mem_singleton_iff.mp hy
52       subst y
53       exact Submodule.subset_span ⟨C, rfl⟩
54     · exact H.zero_mem
55     · intro y z _ _ hy hz
56       exact H.add_mem hy hz
57     · intro a y _ hy
58       obtain ⟨b,hb⟩ := corner_action_ambient A (P.proj (vertex C))
59         (projector_mem_generatedAlgebra P ops (vertex C)) (P.idempotent (vertex C)) a
60       rw [hb y]
61       exact H.smul_mem b hy
62   have hinvariant : AlgebraInvariant A (H.restrictScalars K) := by
63     intro T hT x hx
64     exact H.smul_mem (⟨T,hT⟩ : A) hx
65   have htop : H.restrictScalars K = ⊤ := by
66     apply submodule_eq_top_of_sources P ops hedges _ hinvariant
67     intro C a ha
68     have hreach : Reach edge (vertex C) a :=
69       ((component_eq_iff edge (vertex C) a).mp ((hv C).trans ha.symm)).1
70     exact reachable_range_le P ops hedges _ hinvariant hreach (hpacket C)
71   have hgen : PureGenerates A P (Set.range seed) := by
72     constructor
73     · apply top_unique
74       intro x _
75       have hx : x ∈ H.restrictScalars K := by rw [htop]; trivial
76       exact hx
77     · rintro x ⟨C,rfl⟩
78       exact packetPure_of_mem_range P (s (vertex C)).property
79   exact (packetPureSeedRank_le_card hgen).trans Cardinal.mk_range_le
80 
81 /-- Every source class contains an original packet, so nonzero packets give a nonzero local rank. -/
82 theorem one_le_source_localPureSeedRank (P : LinearProjectorFamily K X I)
83     (ops : Set (Module.End K X)) [∀ i, Nontrivial (LinearMap.range (P.proj i))]
84     (C : Sources (TransferEdge P ops)) :
85     1 ≤ localPureSeedRank (packetGeneratedAlgebra P ops) P
86       (projector_mem_generatedAlgebra P ops) (component (TransferEdge P ops)) C.val := by
87   classical
88   let A := packetGeneratedAlgebra P ops
89   let σ := component (TransferEdge P ops)
90   let V := LinearMap.range ((groupedFamily P σ).proj C.val)
91   obtain ⟨i, hi⟩ := component_surjective (TransferEdge P ops) C.val
92   obtain ⟨x,hx⟩ := exists_ne (0 : LinearMap.range (P.proj i))
93   have hmem : (x : X) ∈ V := by
94     have h := original_mem_grouped P σ i x
95     simpa only [σ, V, hi] using h
96   have hnonzero : (⟨x,hmem⟩ : V) ≠ 0 := by
97     intro h
98     apply hx
99     exact Subtype.ext (congrArg (fun y : V => (y : X)) h)
100   apply Cardinal.one_le_iff_ne_zero.mpr
101   intro hzero
102   have hle := seedRank_le_packetPureSeedRank
103     (localCornerAlgebra A P (projector_mem_generatedAlgebra P ops) σ C.val)
104     (localPacketFamily P σ C.val)
105   have hs : seedRank (localCornerAlgebra A P (projector_mem_generatedAlgebra P ops) σ C.val) V = 0 :=
106     le_antisymm (hzero ▸ hle) bot_le
107   have hsub := (seedRank_eq_zero_iff _ V).mp hs
108   exact hnonzero (@Subsingleton.elim V hsub _ _)
109 
110 /-- Every generating set must meet each nonzero source component. -/
111 theorem generating_set_meets_source (P : LinearProjectorFamily K X I)
112     (ops : Set (Module.End K X)) [∀ i, Nontrivial (LinearMap.range (P.proj i))]
113     (S : Set X) (hS : Generates (packetGeneratedAlgebra P ops) X S)
114     (C : Sources (TransferEdge P ops)) :
115     ∃ x ∈ S, componentProjection P ops C.val x ≠ 0 := by
116   classical
117   by_contra h
118   have hseed : ∀ x ∈ S, componentProjection P ops C.val x = 0 := by
119     intro x hx
120     by_contra hne
121     exact h ⟨x,hx,hne⟩
122   have hspan : ∀ x ∈ Submodule.span (packetGeneratedAlgebra P ops) S,
123       componentProjection P ops C.val x = 0 := by
124     intro x hx
125     induction hx using Submodule.span_induction with
126     | mem x hx => exact hseed x hx
127     | zero => exact map_zero _
128     | add x y _ _ hx hy => rw [map_add, hx, hy, add_zero]
129     | smul T x _ hx =>
130       change componentProjection P ops C.val (T.val x) = 0
131       rw [sourceProjection_compression P ops C T.property x, hx, map_zero, map_zero]
132   obtain ⟨i,hi⟩ := component_surjective (TransferEdge P ops) C.val
133   obtain ⟨x,hx⟩ := exists_ne (0 : LinearMap.range (P.proj i))
134   have hxs : (x : X) ∈ Submodule.span (packetGeneratedAlgebra P ops) S := by rw [hS]; trivial
135   have hz := hspan x hxs
136   rw [componentProjection_packet P ops C.val hi x.property] at hz
137   exact hx (Subtype.ext hz)
138 
139 /-- Different source components require different pure seeds, even without edge surjectivity. -/
140 theorem source_count_le_packetPureSeedRank (P : LinearProjectorFamily K X I)
141     (ops : Set (Module.End K X)) [∀ i, Nontrivial (LinearMap.range (P.proj i))] :
142     #(Sources (TransferEdge P ops)) ≤ packetPureSeedRank (packetGeneratedAlgebra P ops) P := by
143   classical
144   obtain ⟨S,hS,hcard⟩ := exists_pure_generating_set_card_eq (packetGeneratedAlgebra P ops) P
145   rw [← hcard]
146   choose x hx hnonzero using (fun C : Sources (TransferEdge P ops) =>
147     generating_set_meets_source P ops S hS.1 C)
148   let f : Sources (TransferEdge P ops) → S := fun C => ⟨x C, hx C⟩
149   apply Cardinal.mk_le_of_injective (f := f)
150   intro C D hCD
151   by_contra hne
152   have hval : x C = x D := congrArg Subtype.val hCD
153   let σ := component (TransferEdge P ops)
154   let Q := groupedFamily P σ
155   have hC : Q.proj C.val (x C) = x C :=
156     (pure_grouped_fixed_or_zero P σ C.val (hS.2 (x C) (hx C))).resolve_right (hnonzero C)
157   have hD : Q.proj D.val (x C) = x C := by
158     rw [hval]
159     exact (pure_grouped_fixed_or_zero P σ D.val (hS.2 (x D) (hx D))).resolve_right (hnonzero D)
160   have hindex : C.val ≠ D.val := fun h => hne (Subtype.ext h)
161   have hzero := Q.orthogonal hindex (x C)
162   rw [hD, hC] at hzero
163   exact hnonzero C (hC.trans hzero)
164 
165 /-- Unweighted source-component count for a packet-propagating system. -/
166 theorem packetPureSeedRank_eq_source_count (P : LinearProjectorFamily K X I)
167     (ops : Set (Module.End K X)) [∀ i, Nontrivial (LinearMap.range (P.proj i))]
168     (hpropagating : PacketPropagating P ops) :
169     packetPureSeedRank (packetGeneratedAlgebra P ops) P =
170       #(Sources (TransferEdge P ops)) :=
171   le_antisymm (packetPureSeedRank_le_source_count P ops hpropagating.1 hpropagating.2)
172     (source_count_le_packetPureSeedRank P ops)
173 
174 /-- Natural-number cardinality form of the finite source count. -/
175 theorem packetPureSeedRank_eq_source_card (P : LinearProjectorFamily K X I)
176     (ops : Set (Module.End K X)) [∀ i, Nontrivial (LinearMap.range (P.proj i))]
177     (hpropagating : PacketPropagating P ops) :
178     packetPureSeedRank (packetGeneratedAlgebra P ops) P =
179       (Fintype.card (Sources (TransferEdge P ops)) : Cardinal) := by
180   simpa only [Cardinal.mk_fintype] using packetPureSeedRank_eq_source_count P ops hpropagating
181 
182 end Komorebi.PaperIRelease

Back to source controls