PacketLocalRank.lean

1 import PaperIRelease.PacketPureRank
2 import PaperIRelease.PacketAggregation
3 
4 set_option autoImplicit false
5 set_option linter.unnecessarySimpa false
6 noncomputable section
7 
8 namespace Komorebi.PaperIRelease
9 
10 open Cardinal Set Komorebi.Foundation Komorebi.SeedRankBasics
11 open PacketAggregation
12 
13 universe u
14 variable {𝕜 X I J : Type u} [Field 𝕜] [AddCommGroup X] [Module 𝕜 X]
15 variable [Fintype I] [Fintype J] [DecidableEq J]
16 
17 theorem groupedRange_preserved (P : LinearProjectorFamily 𝕜 X I)
18     (σ : I → J) (C : J) :
19     P.Preserves (LinearMap.range ((groupedFamily P σ).proj C)) := by
20   intro i x hx
21   obtain ⟨y, rfl⟩ := hx
22   change P.proj i (groupedProjection P σ C y) ∈ _
23   rw [proj_groupedProjection]
24   by_cases hi : σ i = C
25   · rw [ite_eq_left hi]
26     simpa only [hi] using original_mem_grouped P σ i ⟨P.proj i y, ⟨y, rfl⟩⟩
27   · rw [ite_eq_right hi]
28     exact Submodule.zero_mem _
29 
30 /-- The original packets restricted to the grouped range. Indices outside
31 the group give zero maps; deleting those zero maps preserves the pure rank. -/
32 def localPacketFamily (P : LinearProjectorFamily 𝕜 X I) (σ : I → J) (C : J) :
33     LinearProjectorFamily 𝕜 (LinearMap.range ((groupedFamily P σ).proj C)) I :=
34   P.restrictTo _ (groupedRange_preserved P σ C)
35 
36 theorem local_packetPure_iff (P : LinearProjectorFamily 𝕜 X I)
37     (σ : I → J) (C : J) (x : LinearMap.range ((groupedFamily P σ).proj C)) :
38     PacketPure (localPacketFamily P σ C) x ↔ PacketPure P (x : X) := by
39   constructor
40   · intro hx a ha b hb
41     apply hx
42     · intro h
43       exact ha (congrArg Subtype.val h)
44     · intro h
45       exact hb (congrArg Subtype.val h)
46   · intro hx a ha b hb
47     apply hx
48     · intro h
49       exact ha (Subtype.ext h)
50     · intro h
51       exact hb (Subtype.ext h)
52 
53 /-- With nonzero original packets, the only zero local projectors are the
54 indices outside the group. Thus zero removal gives exactly `P|_C`. -/
55 theorem local_proj_zero_iff (P : LinearProjectorFamily 𝕜 X I)
56     (hP : ∀ i, P.proj i ≠ 0) (σ : I → J) (C : J) (i : I) :
57     (localPacketFamily P σ C).proj i = 0 ↔ σ i ≠ C := by
58   constructor
59   · intro hzero hi
60     apply hP i
61     ext x
62     have hx : P.proj i x ∈ LinearMap.range ((groupedFamily P σ).proj C) := by
63       simpa only [hi] using original_mem_grouped P σ i ⟨P.proj i x, ⟨x, rfl⟩⟩
64     have hh := congrArg (fun f ↦ f ⟨P.proj i x, hx⟩) hzero
65     have hval := congrArg Subtype.val hh
66     change P.proj i (P.proj i x) = 0 at hval
67     rwa [P.idempotent] at hval
68   · intro hi
69     apply LinearMap.ext
70     intro x
71     apply Subtype.ext
72     obtain ⟨y, hy⟩ := x.property
73     change P.proj i (x : X) = 0
74     rw [← hy]
75     change P.proj i (groupedProjection P σ C y) = 0
76     simpa only [ite_eq_right hi] using proj_groupedProjection P σ i C y
77 
78 theorem groupedProjection_mem_algebra
79     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (P : LinearProjectorFamily 𝕜 X I)
80     (hPA : ∀ i, P.proj i ∈ A) (σ : I → J) (C : J) :
81     (groupedFamily P σ).proj C ∈ A := by
82   classical
83   change (∑ i with σ i = C, P.proj i) ∈ A
84   exact A.sum_mem (fun i _ ↦ hPA i)
85 
86 abbrev localCornerAlgebra (A : Subalgebra 𝕜 (Module.End 𝕜 X))
87     (P : LinearProjectorFamily 𝕜 X I) (hPA : ∀ i, P.proj i ∈ A)
88     (σ : I → J) (C : J) :=
89   packetCornerAlgebra A ((groupedFamily P σ).proj C)
90     (groupedProjection_mem_algebra A P hPA σ C) ((groupedFamily P σ).idempotent C)
91 
92 /-- Local cardinal minimum under the genuine grouped corner action. -/
93 def localPureSeedRank (A : Subalgebra 𝕜 (Module.End 𝕜 X))
94     (P : LinearProjectorFamily 𝕜 X I) (hPA : ∀ i, P.proj i ∈ A)
95     (σ : I → J) (C : J) : Cardinal.{u} :=
96   packetPureSeedRank (localCornerAlgebra A P hPA σ C) (localPacketFamily P σ C)
97 
98 /-- A pure vector has either its whole value or zero in a grouped packet. -/
99 theorem pure_grouped_fixed_or_zero (P : LinearProjectorFamily 𝕜 X I)
100     (σ : I → J) (C : J) {x : X} (hx : PacketPure P x) :
101     (groupedFamily P σ).proj C x = x ∨ (groupedFamily P σ).proj C x = 0 := by
102   classical
103   by_cases hx0 : x = 0
104   · simp [hx0]
105   have hsome : ∃ i, P.proj i x ≠ 0 := by
106     by_contra hn
107     apply hx0
108     rw [← P.complete x]
109     apply Finset.sum_eq_zero
110     intro i _
111     by_contra hi
112     exact hn ⟨i, hi⟩
113   obtain ⟨i, hi⟩ := hsome
114   have hxi := packetPure_mem_range P hx hi
115   have hxgroup : x ∈ LinearMap.range ((groupedFamily P σ).proj (σ i)) :=
116     original_mem_grouped P σ i ⟨x, hxi⟩
117   by_cases hC : C = σ i
118   · left
119     rw [hC]
120     exact (groupedFamily P σ).proj_eq_self_of_mem_range _ hxgroup
121   · right
122     obtain ⟨y, rfl⟩ := hxgroup
123     exact (groupedFamily P σ).orthogonal hC y
124 
125 /-- Removing zero projectors has no effect on which vectors are packet pure. -/
126 theorem packetPure_discardZeros_iff (P : LinearProjectorFamily 𝕜 X I) (x : X) :
127     PacketPure P.discardZeros x ↔ PacketPure P x := by
128   constructor
129   · intro hx i hi j hj
130     have hi0 : P.proj i ≠ 0 := by intro h; exact hi (by rw [h]; rfl)
131     have hj0 : P.proj j ≠ 0 := by intro h; exact hj (by rw [h]; rfl)
132     exact congrArg Subtype.val (hx (x := ⟨i, hi0⟩) (y := ⟨j, hj0⟩) hi hj)
133   · intro hx i hi j hj
134     exact Subtype.ext (hx hi hj)
135 
136 theorem packetPureSeedRank_discardZeros
137     (A : Subalgebra 𝕜 (Module.End 𝕜 X)) (P : LinearProjectorFamily 𝕜 X I) :
138     packetPureSeedRank A P.discardZeros = packetPureSeedRank A P := by
139   apply le_antisymm
140   · obtain ⟨S, hS, hc⟩ := exists_pure_generating_set_card_eq A P
141     rw [← hc]
142     exact packetPureSeedRank_le_card ⟨hS.1, fun x hx ↦
143       (packetPure_discardZeros_iff P x).mpr (hS.2 x hx)⟩
144   · obtain ⟨S, hS, hc⟩ := exists_pure_generating_set_card_eq A P.discardZeros
145     rw [← hc]
146     exact packetPureSeedRank_le_card ⟨hS.1, fun x hx ↦
147       (packetPure_discardZeros_iff P x).mp (hS.2 x hx)⟩
148 
149 end Komorebi.PaperIRelease

Back to source controls