PacketSourceLower.lean

1 import PaperIRelease.PacketLocalRank
2 
3 set_option autoImplicit false
4 set_option linter.unnecessarySimpa false
5 noncomputable section
6 
7 namespace Komorebi.PaperIRelease
8 
9 open Cardinal Set Komorebi.Foundation Komorebi.SeedRankBasics
10 open PacketAggregation
11 
12 universe u
13 variable {𝕜 X I J : Type u} [Field 𝕜] [AddCommGroup X] [Module 𝕜 X]
14 variable [Fintype I] [Fintype J] [DecidableEq J]
15 
16 /-- Nonzero original seeds which actually lie in one grouped range.
17 Removing zero ensures that these sets are disjoint across different groups. -/
18 def localNonzeroSeeds (P : LinearProjectorFamily 𝕜 X I) (σ : I → J)
19     (C : J) (S : Set X) : Set (LinearMap.range ((groupedFamily P σ).proj C)) :=
20   {x | (x : X) ∈ S ∧ (x : X) ≠ 0}
21 
22 /-- At a component with no incoming action, the original pure seeds inside
23 that component generate its genuine corner module. The hypothesis is the
24 literal no-incoming compression identity, later derived for source SCCs. -/
25 theorem localNonzeroSeeds_generate_of_compression
26     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (P : LinearProjectorFamily 𝕜 X I)
27     (hPA : ∀ i, P.proj i ∈ A) (σ : I → J) (C : J)
28     (hcomp : ∀ a ∈ A, ∀ x, (groupedFamily P σ).proj C (a x) =
29       (groupedFamily P σ).proj C (a ((groupedFamily P σ).proj C x)))
30     {S : Set X} (hS : PureGenerates A P S) :
31     PureGenerates (localCornerAlgebra A P hPA σ C) (localPacketFamily P σ C)
32       (localNonzeroSeeds P σ C S) := by
33   let Q := (groupedFamily P σ).proj C
34   let π : X →ₗ[𝕜] LinearMap.range Q := Q.rangeRestrict
35   let B := localCornerAlgebra A P hPA σ C
36   let H : Submodule B (LinearMap.range Q) :=
37     Submodule.span B (localNonzeroSeeds P σ C S)
38   have hproj (x : X) : π x ∈ H := by
39     have hx : x ∈ Submodule.span A S := by rw [hS.1]; trivial
40     refine Submodule.span_induction (p := fun x _ ↦ π x ∈ H) ?_ ?_ ?_ ?_ hx
41     · intro y hy
42       rcases pure_grouped_fixed_or_zero P σ C (hS.2 y hy) with hfixed | hzero
43       · by_cases hy0 : y = 0
44         · simpa [hy0] using H.zero_mem
45         · apply Submodule.subset_span
46           change (groupedFamily P σ).proj C y ∈ S ∧ (groupedFamily P σ).proj C y ≠ 0
47           rw [hfixed]
48           exact ⟨hy, hy0⟩
49       · have hz : π y = 0 := Subtype.ext hzero
50         rw [hz]
51         exact H.zero_mem
52     · simpa using H.zero_mem
53     · intro x y _ _ hx hy
54       simpa using H.add_mem hx hy
55     · intro a x _ hx
56       let c : B := ⟨cornerCompression Q a.val, ⟨a.val, a.property, rfl⟩⟩
57       have heq : π (a • x) = c • π x := by
58         apply Subtype.ext
59         exact hcomp a.val a.property x
60       rw [heq]
61       exact H.smul_mem c hx
62   refine ⟨?_, ?_⟩
63   · change H = ⊤
64     apply top_unique
65     intro x _
66     have hx := hproj (x : X)
67     have heq : π (x : X) = x :=
68       Subtype.ext ((groupedFamily P σ).proj_eq_self_of_mem_range C x.property)
69     rwa [heq] at hx
70   · intro x hx
71     exact (local_packetPure_iff P σ C x).mpr (hS.2 x hx.1)
72 
73 /-- The nonzero seed subsets in distinct grouped packet ranges are disjoint,
74 expressed as an injection from their dependent sum into the original set. -/
75 def localNonzeroSeedsEmbedding (P : LinearProjectorFamily 𝕜 X I)
76     (σ : I → J) (D : Set J) (S : Set X) :
77     (Σ C : D, localNonzeroSeeds P σ C.val S) ↪ S where
78   toFun z := ⟨(z.2.val : X), z.2.property.1⟩
79   inj' := by
80     rintro ⟨C, x⟩ ⟨E, y⟩ h
81     have hxy : (x.val : X) = (y.val : X) := congrArg Subtype.val h
82     have hCE : C = E := by
83       apply Subtype.ext
84       by_contra hne
85       have hz : (groupedFamily P σ).proj C.val (x.val : X) = 0 := by
86         rw [hxy]
87         obtain ⟨z, hz⟩ := y.val.property
88         rw [← hz]
89         exact (groupedFamily P σ).orthogonal hne z
90       rw [(groupedFamily P σ).proj_eq_self_of_mem_range C.val x.val.property] at hz
91       exact x.property.2 hz
92     subst E
93     have hxy' : x = y := Subtype.ext (Subtype.ext hxy)
94     subst y
95     rfl
96 
97 theorem sum_localNonzeroSeeds_card_le (P : LinearProjectorFamily 𝕜 X I)
98     (σ : I → J) (D : Set J) (S : Set X) :
99     Cardinal.sum (fun C : D ↦ #(localNonzeroSeeds P σ C.val S)) ≤ #S := by
100   rw [← Cardinal.mk_sigma]
101   exact Cardinal.mk_le_of_injective (localNonzeroSeedsEmbedding P σ D S).injective
102 
103 /-- Cardinal lower bound from an actual family of source-compression
104 identities. Source SCCs provide these identities from graph reachability. -/
105 theorem sum_localPureSeedRank_le_of_compression
106     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (P : LinearProjectorFamily 𝕜 X I)
107     (hPA : ∀ i, P.proj i ∈ A) (σ : I → J) (D : Set J)
108     (hcomp : ∀ C ∈ D, ∀ a ∈ A, ∀ x, (groupedFamily P σ).proj C (a x) =
109       (groupedFamily P σ).proj C (a ((groupedFamily P σ).proj C x))) :
110     Cardinal.sum (fun C : D ↦ localPureSeedRank A P hPA σ C.val) ≤
111       packetPureSeedRank A P := by
112   obtain ⟨S, hS, hcard⟩ := exists_pure_generating_set_card_eq A P
113   rw [← hcard]
114   calc
115     _ ≤ Cardinal.sum (fun C : D ↦ #(localNonzeroSeeds P σ C.val S)) :=
116       Cardinal.sum_le_sum _ _ (fun C ↦ packetPureSeedRank_le_card
117         (localNonzeroSeeds_generate_of_compression A P hPA σ C.val (hcomp C.val C.property) hS))
118     _ ≤ #S := sum_localNonzeroSeeds_card_le P σ D S
119 
120 end Komorebi.PaperIRelease

Back to source controls