JointOccupancy.lean

1 import PaperX.SpectralProjectors
2 
3 /-! Finite products of actual commuting spectral projectors; exact image,
4 idempotence and trace-rank. Empty lists give the identity. Characteristic zero
5 is needed only to recover integer occupancy from the field-valued trace. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.JointOccupancy
9 
10 open scoped BigOperators
11 open LinearMap Module.End PaperX.SpectralProjectors
12 universe u v w
13 variable {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V]
14   [FiniteDimensional K V] {I : Type w}
15 
16 /-- An actual intersection, not a range stipulated to be the desired one. -/
17 def jointSpace (T : I → Module.End K V) (a : I → K) : List I → Submodule K V
18   | [] => ⊤
19   | i :: l => (T i).eigenspace (a i) ⊓ jointSpace T a l
20 
21 omit [FiniteDimensional K V] in
22 theorem mem_jointSpace (T : I → Module.End K V) (a : I → K) (l : List I) (x : V) :
23     x ∈ jointSpace T a l ↔ ∀ i ∈ l, T i x = a i • x := by
24   induction l with
25   | nil => simp [jointSpace]
26   | cons i l ih => simp [jointSpace, ih]
27 
28 /-- Ordered product of polynomially constructed individual projectors. -/
29 def joint (T : I → Module.End K V) (a : I → K) (l : List I) : Module.End K V :=
30   (l.map fun i => spectral (T i) (a i)).prod
31 
32 theorem joint_nil (T : I → Module.End K V) (a : I → K) : joint T a [] = 1 := rfl
33 
34 theorem joint_cons (T : I → Module.End K V) (a : I → K) (i : I) (l : List I) :
35     joint T a (i :: l) = spectral (T i) (a i) * joint T a l := rfl
36 
37 omit [FiniteDimensional K V] in
38 /-- The product projects onto the intersection, provided the projections commute. -/
39 theorem product_isProj {p q : Submodule K V} {P Q : Module.End K V}
40     (hp : IsProj p P) (hq : IsProj q Q) (h : Commute P Q) :
41     IsProj (p ⊓ q) (P * Q) := by
42   constructor
43   · intro x
44     refine ⟨hp.map_mem _, hq.mem_iff_map_id.mpr ?_⟩
45     change Q (P (Q x)) = P (Q x)
46     rw [← Module.End.mul_apply, ← h.eq, Module.End.mul_apply]
47     rw [hq.map_id _ (hq.map_mem x)]
48   · intro x hx
49     change P (Q x) = x
50     rw [hq.map_id x hx.2, hp.map_id x hx.1]
51 
52 theorem spectral_commute_joint (T : I → Module.End K V) (a : I → K)
53     (hc : ∀ i j, Commute (T i) (T j)) (i : I) (l : List I) :
54     Commute (spectral (T i) (a i)) (joint T a l) := by
55   apply Commute.list_prod_right
56   intro P hP
57   obtain ⟨j, _, rfl⟩ := List.mem_map.mp hP
58   exact spectral_commute _ _ (hc i j) _ _
59 
60 /-- The ordered implementation is independent of ordering for commuting inputs. -/
61 theorem joint_perm (T : I → Module.End K V) (a : I → K)
62     (hc : ∀ i j, Commute (T i) (T j)) {l m : List I} (h : l.Perm m) :
63     joint T a l = joint T a m := by
64   induction h with
65   | nil => rfl
66   | cons i _ ih => simp only [joint_cons, ih]
67   | swap i j l =>
68       simp only [joint_cons, ← mul_assoc]
69       rw [(spectral_commute (T j) (T i) (hc j i) (a j) (a i)).eq]
70   | trans _ _ ih1 ih2 => exact ih1.trans ih2
71 
72 theorem joint_isProj (T : I → Module.End K V) (a : I → K)
73     (hs : ∀ i, Split (T i)) (hc : ∀ i j, Commute (T i) (T j)) (l : List I) :
74     IsProj (jointSpace T a l) (joint T a l) := by
75   induction l with
76   | nil => exact ⟨fun _ => Submodule.mem_top, fun _ _ => rfl⟩
77   | cons i l ih =>
78     exact product_isProj (spectral_isProj (T i) (hs i) (a i)) ih
79       (spectral_commute_joint T a hc i l)
80 
81 theorem joint_idempotent (T : I → Module.End K V) (a : I → K)
82     (hs : ∀ i, Split (T i)) (hc : ∀ i j, Commute (T i) (T j)) (l : List I) :
83     IsIdempotentElem (joint T a l) := (joint_isProj T a hs hc l).isIdempotentElem
84 
85 theorem joint_range (T : I → Module.End K V) (a : I → K)
86     (hs : ∀ i, Split (T i)) (hc : ∀ i j, Commute (T i) (T j)) (l : List I) :
87     LinearMap.range (joint T a l) = jointSpace T a l := (joint_isProj T a hs hc l).range
88 
89 theorem joint_fixed_iff (T : I → Module.End K V) (a : I → K)
90     (hs : ∀ i, Split (T i)) (hc : ∀ i j, Commute (T i) (T j)) (l : List I) (x : V) :
91     joint T a l x = x ↔ ∀ i ∈ l, T i x = a i • x := by
92   rw [← (joint_isProj T a hs hc l).mem_iff_map_id, mem_jointSpace]
93 
94 /-- Trace equality is valid in every characteristic as an equality in K. -/
95 theorem trace_eq_dimension (T : I → Module.End K V) (a : I → K)
96     (hs : ∀ i, Split (T i)) (hc : ∀ i j, Commute (T i) (T j)) (l : List I) :
97     LinearMap.trace K V (joint T a l) = (Module.finrank K (jointSpace T a l) : K) :=
98   (joint_isProj T a hs hc l).trace
99 
100 /-- Occupancy means an actual nonzero joint eigenvector. -/
101 def Occupied (T : I → Module.End K V) (a : I → K) (l : List I) : Prop :=
102   ∃ x : V, x ≠ 0 ∧ ∀ i ∈ l, T i x = a i • x
103 
104 theorem occupied_iff_dimension_pos (T : I → Module.End K V) (a : I → K) (l : List I) :
105     Occupied T a l ↔ 0 < Module.finrank K (jointSpace T a l) := by
106   rw [Module.finrank_pos_iff_exists_ne_zero]
107   constructor
108   · rintro ⟨x, hx, h⟩
109     exact ⟨⟨x, (mem_jointSpace T a l x).2 h⟩, fun hz => hx (congrArg Subtype.val hz)⟩
110   · rintro ⟨x, hx⟩
111     exact ⟨x, fun hz => hx (Subtype.ext hz), (mem_jointSpace T a l x).1 x.property⟩
112 
113 theorem occupied_iff_trace_ne_zero [CharZero K] (T : I → Module.End K V) (a : I → K)
114     (hs : ∀ i, Split (T i)) (hc : ∀ i j, Commute (T i) (T j)) (l : List I) :
115     Occupied T a l ↔ LinearMap.trace K V (joint T a l) ≠ 0 := by
116   rw [trace_eq_dimension T a hs hc l, Nat.cast_ne_zero, occupied_iff_dimension_pos]
117   exact Nat.pos_iff_ne_zero
118 
119 /-- The natural integer encoded by trace is unique in characteristic zero. -/
120 theorem trace_integer_unique [CharZero K] (T : I → Module.End K V) (a : I → K)
121     (hs : ∀ i, Split (T i)) (hc : ∀ i j, Commute (T i) (T j)) (l : List I) :
122     ∃! n : ℕ, LinearMap.trace K V (joint T a l) = (n : K) := by
123   refine ⟨Module.finrank K (jointSpace T a l), trace_eq_dimension T a hs hc l, ?_⟩
124   intro n hn
125   exact Nat.cast_injective (hn.symm.trans (trace_eq_dimension T a hs hc l))
126 
127 omit [FiniteDimensional K V] in
128 /-- Adding conditions cannot increase the actual joint eigenspace. -/
129 theorem space_antitone (T : I → Module.End K V) (a : I → K)
130     {l m : List I} (h : ∀ i ∈ l, i ∈ m) : jointSpace T a m ≤ jointSpace T a l := by
131   intro x hx
132   exact (mem_jointSpace T a l x).2 fun i hi => (mem_jointSpace T a m x).1 hx i (h i hi)
133 
134 theorem dimension_antitone (T : I → Module.End K V) (a : I → K)
135     {l m : List I} (h : ∀ i ∈ l, i ∈ m) :
136     Module.finrank K (jointSpace T a m) ≤ Module.finrank K (jointSpace T a l) :=
137   Submodule.finrank_mono (space_antitone T a h)
138 
139 /-- This is the literal finite-index version, with every condition imposed. -/
140 theorem finite_occupancy [Fintype I] [CharZero K] (T : I → Module.End K V) (a : I → K)
141     (hs : ∀ i, Split (T i)) (hc : ∀ i j, Commute (T i) (T j)) :
142     ∃ E : Module.End K V,
143       E = joint T a (Finset.univ.toList) ∧ IsIdempotentElem E ∧
144       (∀ x, x ∈ LinearMap.range E ↔ ∀ i, T i x = a i • x) ∧
145       LinearMap.trace K V E = (Module.finrank K (jointSpace T a Finset.univ.toList) : K) ∧
146       ((∃ x : V, x ≠ 0 ∧ ∀ i, T i x = a i • x) ↔ LinearMap.trace K V E ≠ 0) := by
147   classical
148   refine ⟨joint T a Finset.univ.toList, rfl, joint_idempotent T a hs hc _, ?_,
149     trace_eq_dimension T a hs hc _, ?_⟩
150   · intro x
151     rw [joint_range T a hs hc, mem_jointSpace]
152     simp
153   · simpa [Occupied] using occupied_iff_trace_ne_zero T a hs hc Finset.univ.toList
154 
155 end PaperX.JointOccupancy

Back to source controls