PacketPureRank.lean

1 import PaperIRelease.PacketCorners
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 
11 universe u
12 variable {𝕜 X I : Type u} [Field 𝕜] [AddCommGroup X] [Module 𝕜 X] [Fintype I]
13 
14 /-- Pure generation uses the actual ambient algebra action. -/
15 def PureGenerates (A : Subalgebra 𝕜 (Module.End 𝕜 X))
16     (P : LinearProjectorFamily 𝕜 X I) (S : Set X) : Prop :=
17   Generates A X S ∧ ∀ x ∈ S, PacketPure P x
18 
19 /-- The minimum cardinality of an actual packet-pure generating set. -/
20 def packetPureSeedRank (A : Subalgebra 𝕜 (Module.End 𝕜 X))
21     (P : LinearProjectorFamily 𝕜 X I) : Cardinal.{u} :=
22   ⨅ (S : {S : Set X // PureGenerates A P S}), #S.1
23 
24 theorem all_pure_generates (A : Subalgebra 𝕜 (Module.End 𝕜 X))
25     (P : LinearProjectorFamily 𝕜 X I) : PureGenerates A P {x | PacketPure P x} := by
26   refine ⟨?_, fun _ hx ↦ hx⟩
27   apply top_unique
28   intro x _
29   rw [← P.complete x]
30   apply Submodule.sum_mem
31   intro i _
32   exact Submodule.subset_span (packetPure_of_mem_range P ⟨x, rfl⟩)
33 
34 theorem packetPureSeedRank_le_card {A : Subalgebra 𝕜 (Module.End 𝕜 X)}
35     {P : LinearProjectorFamily 𝕜 X I} {S : Set X} (hS : PureGenerates A P S) :
36     packetPureSeedRank A P ≤ #S :=
37   ciInf_le' (fun T : {T : Set X // PureGenerates A P T} ↦ #T.1) ⟨S, hS⟩
38 
39 theorem exists_pure_generating_set_card_eq
40     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (P : LinearProjectorFamily 𝕜 X I) :
41     ∃ S : Set X, PureGenerates A P S ∧ #S = packetPureSeedRank A P := by
42   have hmem : packetPureSeedRank A P ∈
43       Set.range (fun S : {S : Set X // PureGenerates A P S} ↦ #S.1) :=
44     csInf_mem ⟨#({x | PacketPure P x} : Set X),
45       ⟨⟨{x | PacketPure P x}, all_pure_generates A P⟩, rfl⟩⟩
46   obtain ⟨S, hS⟩ := hmem
47   exact ⟨S.1, S.2, hS⟩
48 
49 theorem seedRank_le_packetPureSeedRank
50     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (P : LinearProjectorFamily 𝕜 X I) :
51     seedRank A X ≤ packetPureSeedRank A P := by
52   obtain ⟨S, hS, hcard⟩ := exists_pure_generating_set_card_eq A P
53   rw [← hcard]
54   exact seedRank_le_mk_of_generates A X hS.1
55 
56 /-- Union of genuinely minimal corner generating sets proves the cardinal
57 upper bound, with no finite-dimensional assumption on the packet spaces. -/
58 theorem packetPureSeedRank_le_sum_corner
59     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (P : LinearProjectorFamily 𝕜 X I)
60     (hPA : ∀ i, P.proj i ∈ A) :
61     packetPureSeedRank A P ≤ Cardinal.sum (fun i ↦
62       seedRank (packetCornerAlgebra A (P.proj i) (hPA i) (P.idempotent i))
63         (LinearMap.range (P.proj i))) := by
64   classical
65   let C (i : I) := packetCornerAlgebra A (P.proj i) (hPA i) (P.idempotent i)
66   choose S hS hcard using fun i ↦
67     exists_generating_set_card_eq_seedRank (C i) (LinearMap.range (P.proj i))
68   let seeds : Set X := ⋃ i, Subtype.val '' S i
69   let H : Submodule A X := Submodule.span A seeds
70   have hpacket (i : I) (x : LinearMap.range (P.proj i)) : (x : X) ∈ H := by
71     have hx : x ∈ Submodule.span (C i) (S i) := by rw [hS i]; trivial
72     refine Submodule.span_induction
73       (p := fun (x : LinearMap.range (P.proj i)) _ ↦ (x : X) ∈ H) ?_ ?_ ?_ ?_ hx
74     · intro y hy
75       exact Submodule.subset_span (Set.mem_iUnion.mpr ⟨i, ⟨y, hy, rfl⟩⟩)
76     · exact H.zero_mem
77     · intro x y _ _ hx hy
78       exact H.add_mem hx hy
79     · intro a y _ hy
80       obtain ⟨b, hb⟩ := corner_action_ambient A (P.proj i) (hPA i) (P.idempotent i) a
81       rw [hb y]
82       exact H.smul_mem b hy
83   have hgen : PureGenerates A P seeds := by
84     constructor
85     · change H = ⊤
86       apply top_unique
87       intro x _
88       rw [← P.complete x]
89       apply H.sum_mem
90       intro i _
91       exact hpacket i ⟨P.proj i x, ⟨x, rfl⟩⟩
92     · intro x hx
93       obtain ⟨i, y, hy, rfl⟩ := Set.mem_iUnion.mp hx
94       exact packetPure_of_mem_range P y.property
95   calc
96     packetPureSeedRank A P ≤ #seeds := packetPureSeedRank_le_card hgen
97     _ ≤ Cardinal.sum (fun i ↦ #(Subtype.val '' S i : Set X)) := Cardinal.mk_iUnion_le_sum_mk
98     _ ≤ Cardinal.sum (fun i ↦ #(S i)) :=
99       Cardinal.sum_le_sum _ _ (fun _ ↦ Cardinal.mk_image_le)
100     _ = _ := by simp only [hcard, C]
101 
102 theorem packetPureSeedRank_bounds
103     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (P : LinearProjectorFamily 𝕜 X I)
104     (hPA : ∀ i, P.proj i ∈ A) :
105     seedRank A X ≤ packetPureSeedRank A P ∧
106       packetPureSeedRank A P ≤ Cardinal.sum (fun i ↦
107         seedRank (packetCornerAlgebra A (P.proj i) (hPA i) (P.idempotent i))
108           (LinearMap.range (P.proj i))) :=
109   ⟨seedRank_le_packetPureSeedRank A P, packetPureSeedRank_le_sum_corner A P hPA⟩
110 
111 end Komorebi.PaperIRelease
112 
113 #print axioms Komorebi.PaperIRelease.packetPureSeedRank_bounds

Back to source controls