PacketSourceUpper.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 /-- Corner generators in a family of grouped packets generate globally if
17 those whole packets propagate through every invariant submodule. The graph
18 theorem supplies this propagation condition for the actual source SCCs. -/
19 theorem packetPureSeedRank_le_sum_local_of_generation
20     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (P : LinearProjectorFamily 𝕜 X I)
21     (hPA : ∀ i, P.proj i ∈ A) (σ : I → J) (D : Set J)
22     (hwhole : ∀ H : Submodule A X,
23       (∀ C ∈ D, LinearMap.range ((groupedFamily P σ).proj C) ≤ H.restrictScalars 𝕜) → H = ⊤) :
24     packetPureSeedRank A P ≤
25       Cardinal.sum (fun C : D ↦ localPureSeedRank A P hPA σ C.val) := by
26   classical
27   let B (C : D) := localCornerAlgebra A P hPA σ C.val
28   let V (C : D) := LinearMap.range ((groupedFamily P σ).proj C.val)
29   choose S hS hcard using fun C : D ↦
30     exists_pure_generating_set_card_eq (B C) (localPacketFamily P σ C.val)
31   let seeds : Set X := ⋃ C : D, Subtype.val '' S C
32   let H : Submodule A X := Submodule.span A seeds
33   have hgroup (C : D) (x : V C) : (x : X) ∈ H := by
34     have hx : x ∈ Submodule.span (B C) (S C) := by rw [(hS C).1]; trivial
35     refine Submodule.span_induction
36       (p := fun (x : V C) _ ↦ (x : X) ∈ H) ?_ ?_ ?_ ?_ hx
37     · intro y hy
38       exact Submodule.subset_span (Set.mem_iUnion.mpr ⟨C, ⟨y, hy, rfl⟩⟩)
39     · exact H.zero_mem
40     · intro x y _ _ hx hy
41       exact H.add_mem hx hy
42     · intro a y _ hy
43       obtain ⟨b, hb⟩ := corner_action_ambient A ((groupedFamily P σ).proj C.val)
44         (groupedProjection_mem_algebra A P hPA σ C.val)
45         ((groupedFamily P σ).idempotent C.val) a
46       rw [hb y]
47       exact H.smul_mem b hy
48   have hgen : PureGenerates A P seeds := by
49     constructor
50     · apply hwhole H
51       intro C hC x hx
52       exact hgroup ⟨C, hC⟩ ⟨x, hx⟩
53     · intro x hx
54       obtain ⟨C, y, hy, rfl⟩ := Set.mem_iUnion.mp hx
55       exact (local_packetPure_iff P σ C.val y).mp ((hS C).2 y hy)
56   calc
57     packetPureSeedRank A P ≤ #seeds := packetPureSeedRank_le_card hgen
58     _ ≤ Cardinal.sum (fun C : D ↦ #(Subtype.val '' S C : Set X)) :=
59       Cardinal.mk_iUnion_le_sum_mk
60     _ ≤ Cardinal.sum (fun C : D ↦ #(S C)) :=
61       Cardinal.sum_le_sum _ _ (fun _ ↦ Cardinal.mk_image_le)
62     _ = _ := by simp only [hcard, B, localPureSeedRank]
63 
64 end Komorebi.PaperIRelease

Back to source controls