OrthogonalLifting.lean

1 import PaperX.CornerProjectors
2 import PaperX.OrthogonalPartial
3 import PaperX.PrecisionAveraging
4 
5 /-! Simultaneous lifting of complete labeled orthogonal projector families.
6 All averaging takes place before correction. The retained depth therefore does
7 not depend on the number of labels. -/
8 set_option autoImplicit false
9 namespace PaperX.OrthogonalLifting
10 open PaperX.RepresentationLimits PaperX.MatrixProjector
11 open PaperX.OrthogonalProjectors PaperX.OrthogonalPartial
12 open PaperX.CornerProjectors
13 open scoped BigOperators
14 
15 variable {R Γ ι J : Type*} [CommRing R] [Group Γ]
16   [Fintype ι] [DecidableEq ι] [Fintype J]
17 
18 /-- Lift an arbitrary finite subset of a supplied orthogonal family, keeping
19 all selected components mutually orthogonal in the integral carrier. -/
20 theorem exists_partial (I : Ideal R) [IsAdicComplete I R]
21     (k : ℕ) (hk : 0 < k) (ρ : MatrixRep R Γ ι)
22     (Q : Family (reduce I ρ k) J) (A : J → Matrix ι ι R)
23     (hA : ∀ i, (A i).map (Ideal.Quotient.mk (I^k)) = (Q.projector i).matrix)
24     (hcomm : ∀ i g, ρ g * A i = A i * ρ g) (s : Finset J) :
25     ∃ P : J → Projector ρ,
26       (∀ i ∈ s, (P i).matrix.map (Ideal.Quotient.mk (I^k)) = (Q.projector i).matrix) ∧
27       ∀ i ∈ s, ∀ j ∈ s, i ≠ j → (P i).matrix * (P j).matrix = 0 := by
28   classical
29   induction s using Finset.induction_on with
30   | empty =>
31     exact ⟨fun _ => ⟨0, by simp, fun _ => by simp⟩, by simp, by simp⟩
32   | @insert a s ha ih =>
33     obtain ⟨P, hred, horth⟩ := ih
34     let f := Ideal.Quotient.mk (I^k)
35     let C := complement P s horth
36     have hCred : C.matrix.map f = 1 - ∑ j ∈ s, (Q.projector j).matrix := by
37       change f.mapMatrix (1 - ∑ j ∈ s, (P j).matrix) = _
38       rw [map_sub, map_one, map_sum]
39       congr 1
40       exact Finset.sum_congr rfl fun j hj => hred j hj
41     have hleft : C.matrix.map f * (A a).map f = (A a).map f := by
42       rw [hCred, hA, sub_mul, one_mul, Finset.sum_mul]
43       have hz : ∑ j ∈ s, (Q.projector j).matrix * (Q.projector a).matrix = 0 := by
44         apply Finset.sum_eq_zero
45         intro j hj
46         exact Q.orthogonal j a (by intro h; subst j; exact ha hj)
47       rw [hz, sub_zero]
48     have hright : (A a).map f * C.matrix.map f = (A a).map f := by
49       rw [hCred, hA, mul_sub, mul_one, Finset.mul_sum]
50       have hz : ∑ j ∈ s, (Q.projector a).matrix * (Q.projector j).matrix = 0 := by
51         apply Finset.sum_eq_zero
52         intro j hj
53         exact Q.orthogonal a j (by intro h; subst j; exact ha hj)
54       rw [hz, sub_zero]
55     obtain ⟨E, hEred, hCE, hEC⟩ := exists_in_corner I k hk ρ C (A a) (hcomm a)
56       (by rw [hA]; simpa only [pow_two] using (Q.projector a).idempotent)
57       hleft hright
58     refine ⟨Function.update P a E, ?_, ?_⟩
59     · intro i hi
60       rcases Finset.mem_insert.mp hi with h | h
61       · subst i
62         simpa only [Function.update_self] using hEred.trans (hA a)
63       · have hia : i ≠ a := by intro hi; subst i; exact ha h
64         simpa only [Function.update_of_ne hia] using hred i h
65     · intro i hi j hj hij
66       by_cases hia : i = a
67       · subst i
68         have hja : j ≠ a := Ne.symm hij
69         have hjs : j ∈ s := (Finset.mem_insert.mp hj).resolve_left hja
70         simp only [Function.update_self, Function.update_of_ne hja]
71         calc
72           E.matrix * (P j).matrix = (E.matrix * C.matrix) * (P j).matrix := by rw [hEC]
73           _ = E.matrix * (C.matrix * (P j).matrix) := by rw [mul_assoc]
74           _ = 0 := by rw [complement_mul_projector P s horth j hjs, mul_zero]
75       · by_cases hja : j = a
76         · subst j
77           have his : i ∈ s := (Finset.mem_insert.mp hi).resolve_left hia
78           simp only [Function.update_self, Function.update_of_ne hia]
79           calc
80             (P i).matrix * E.matrix = (P i).matrix * (C.matrix * E.matrix) := by rw [hCE]
81             _ = ((P i).matrix * C.matrix) * E.matrix := by rw [mul_assoc]
82             _ = 0 := by rw [projector_mul_complement P s horth i his, zero_mul]
83         · simp only [Function.update_of_ne hia, Function.update_of_ne hja]
84           exact horth i ((Finset.mem_insert.mp hi).resolve_left hia)
85             j ((Finset.mem_insert.mp hj).resolve_left hja) hij
86 
87 /-- Completeness recovers the sum-to-one equation, including the empty label
88 case, after all individual orthogonal projectors have been lifted. -/
89 theorem exists_family_of_equivariant_lifts (I : Ideal R) [IsAdicComplete I R]
90     (k : ℕ) (hk : 0 < k) (ρ : MatrixRep R Γ ι)
91     (Q : Family (reduce I ρ k) J) (A : J → Matrix ι ι R)
92     (hA : ∀ i, (A i).map (Ideal.Quotient.mk (I^k)) = (Q.projector i).matrix)
93     (hcomm : ∀ i g, ρ g * A i = A i * ρ g) :
94     ∃ E : Family ρ J,
95       ∀ i, (E.projector i).matrix.map (Ideal.Quotient.mk (I^k)) = (Q.projector i).matrix := by
96   classical
97   obtain ⟨P, hred, horth⟩ := exists_partial I k hk ρ Q A hA hcomm Finset.univ
98   let C := complement P Finset.univ horth
99   have hCzero : C.matrix.map (Ideal.Quotient.mk (I^k)) = 0 := by
100     change (Ideal.Quotient.mk (I^k)).mapMatrix (1 - ∑ i, (P i).matrix) = 0
101     rw [map_sub, map_one, map_sum]
102     have hsum : ∑ i, (P i).matrix.map (Ideal.Quotient.mk (I^k)) = 1 := by
103       calc
104         _ = ∑ i, (Q.projector i).matrix := Finset.sum_congr rfl fun i _ => hred i (Finset.mem_univ i)
105         _ = 1 := Q.total
106     change 1 - (∑ i, (P i).matrix.map (Ideal.Quotient.mk (I^k))) = 0
107     rw [hsum, sub_self]
108   have hC := eq_zero_of_idempotent_reduces_zero I k hk C.matrix C.idempotent hCzero
109   have htotal : ∑ i, (P i).matrix = 1 := (sub_eq_zero.mp hC).symm
110   exact ⟨⟨P, fun i j hij => horth i (Finset.mem_univ i) j (Finset.mem_univ j) hij,
111     htotal⟩, fun i => hred i (Finset.mem_univ i)⟩
112 
113  /-- Simultaneous lifting loses at most the one averaging cost `e`, independent
114 of the number of labels. The integral carrier is supplied; the projectors and
115 their complete orthogonal decomposition are constructed. -/
116 theorem exists_family_lift [IsDomain R] [Fintype Γ]
117     (π : R) [IsAdicComplete (Ideal.span {π}) R]
118     (e k : ℕ) (hk : 0 < k) (ρ : MatrixRep R Γ ι)
119     (hΓ : (Fintype.card Γ : R) ≠ 0)
120     (hdiv : (Fintype.card Γ : R) ∣ π^e)
121     (Q : Family (reduce (Ideal.span {π}) ρ (e+k)) J) :
122     ∃ E : Family ρ J,
123       ∀ i, (E.projector i).matrix.map (Ideal.Quotient.mk ((Ideal.span {π})^k)) =
124         (Q.projector i).matrix.map
125           (Ideal.Quotient.factorPow (Ideal.span {π}) (Nat.le_add_left k e)) := by
126   choose A hA hcomm using fun i =>
127     PaperX.PrecisionAveraging.exists_intertwiner_lift π e k ρ ρ hΓ hdiv
128       (Q.projector i).matrix (Q.projector i).commutes
129   exact exists_family_of_equivariant_lifts (Ideal.span {π}) k hk ρ
130     (reduceFamily (Ideal.span {π}) ρ (Nat.le_add_left k e) Q) A hA hcomm
131 
132 end PaperX.OrthogonalLifting

Back to source controls