OrthogonalPartial.lean

1 import PaperX.OrthogonalProjectors
2 
3 /-! Sums and complements of finite, not necessarily complete, orthogonal
4 families of actual equivariant projectors. -/
5 set_option autoImplicit false
6 namespace PaperX.OrthogonalPartial
7 open PaperX.RepresentationLimits PaperX.MatrixProjector
8 open scoped BigOperators
9 
10 variable {R Γ ι J : Type*} [CommRing R] [Group Γ]
11   [Fintype ι] [DecidableEq ι]
12   {ρ : MatrixRep R Γ ι}
13 
14 variable (P : J → Projector ρ) (s : Finset J)
15   (horth : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → (P i).matrix * (P j).matrix = 0)
16 
17 include horth in
18 theorem sum_mul_projector (i : J) (hi : i ∈ s) :
19     (∑ j ∈ s, (P j).matrix) * (P i).matrix = (P i).matrix := by
20   rw [Finset.sum_mul]
21   exact Finset.sum_eq_single i
22     (fun j hj hji => horth j hj i hi hji)
23     (fun h => (h hi).elim) |>.trans (P i).idempotent
24 
25 include horth in
26 theorem projector_mul_sum (i : J) (hi : i ∈ s) :
27     (P i).matrix * (∑ j ∈ s, (P j).matrix) = (P i).matrix := by
28   rw [Finset.mul_sum]
29   exact Finset.sum_eq_single i
30     (fun j hj hji => horth i hi j hj (Ne.symm hji))
31     (fun h => (h hi).elim) |>.trans (P i).idempotent
32 
33 include horth in
34 theorem sum_idempotent :
35     (∑ i ∈ s, (P i).matrix) * (∑ i ∈ s, (P i).matrix) =
36       ∑ i ∈ s, (P i).matrix := by
37   rw [Finset.mul_sum]
38   exact Finset.sum_congr rfl (fun i hi => sum_mul_projector P s horth i hi)
39 
40 theorem sum_commutes (g : Γ) :
41     ρ g * (∑ i ∈ s, (P i).matrix) = (∑ i ∈ s, (P i).matrix) * ρ g := by
42   rw [Finset.mul_sum, Finset.sum_mul]
43   exact Finset.sum_congr rfl (fun i _ => (P i).commutes g)
44 
45 def complement : Projector ρ where
46   matrix := 1 - ∑ i ∈ s, (P i).matrix
47   idempotent := by
48     simp only [sub_mul, mul_sub, one_mul, mul_one, sum_idempotent P s horth,
49       sub_self, sub_zero]
50   commutes g := by
51     rw [mul_sub, sub_mul, mul_one, one_mul, sum_commutes P s g]
52 
53 theorem complement_matrix :
54     (complement P s horth).matrix = 1 - ∑ i ∈ s, (P i).matrix := rfl
55 
56 theorem complement_mul_projector (i : J) (hi : i ∈ s) :
57     (complement P s horth).matrix * (P i).matrix = 0 := by
58   rw [complement_matrix, sub_mul, one_mul, sum_mul_projector P s horth i hi,
59     sub_self]
60 
61 theorem projector_mul_complement (i : J) (hi : i ∈ s) :
62     (P i).matrix * (complement P s horth).matrix = 0 := by
63   rw [complement_matrix, mul_sub, mul_one, projector_mul_sum P s horth i hi,
64     sub_self]
65 
66 theorem complement_add_sum :
67     (complement P s horth).matrix + (∑ i ∈ s, (P i).matrix) = 1 := by
68   exact sub_add_cancel _ _
69 
70 /-- A family at one quotient precision, transported to a shallower precision
71 of the same supplied integral carrier. The matrix formula is definitional. -/
72 def reduceFamily [Fintype J] (I : Ideal R) (ρ : MatrixRep R Γ ι)
73     {k m : ℕ} (h : k ≤ m)
74     (Q : OrthogonalProjectors.Family (reduce I ρ m) J) :
75     OrthogonalProjectors.Family (reduce I ρ k) J where
76   projector i := {
77     matrix := (Q.projector i).matrix.map (Ideal.Quotient.factorPow I h)
78     idempotent := by rw [← Matrix.map_mul, (Q.projector i).idempotent]
79     commutes g := by
80       have hc := ((Q.projector i).changeCoefficients
81         (Ideal.Quotient.factorPow I h)).commutes g
82       change transition I h (reduce I ρ m) g *
83         ((Q.projector i).matrix.map (Ideal.Quotient.factorPow I h)) =
84         ((Q.projector i).matrix.map (Ideal.Quotient.factorPow I h)) *
85           transition I h (reduce I ρ m) g at hc
86       simpa only [transition_reduce] using hc }
87   orthogonal i j hij := by
88     change ((Q.projector i).matrix.map (Ideal.Quotient.factorPow I h)) *
89       ((Q.projector j).matrix.map (Ideal.Quotient.factorPow I h)) = 0
90     rw [← Matrix.map_mul, Q.orthogonal i j hij, Matrix.map_zero]
91     exact map_zero _
92   total := by
93     change ∑ i, (Ideal.Quotient.factorPow I h).mapMatrix (Q.projector i).matrix = 1
94     rw [← map_sum, Q.total, map_one]
95 
96 theorem reduceFamily_matrix [Fintype J] (I : Ideal R) (ρ : MatrixRep R Γ ι)
97     {k m : ℕ} (h : k ≤ m)
98     (Q : OrthogonalProjectors.Family (reduce I ρ m) J) (i : J) :
99     ((reduceFamily I ρ h Q).projector i).matrix =
100       (Q.projector i).matrix.map (Ideal.Quotient.factorPow I h) := rfl
101 
102 end PaperX.OrthogonalPartial

Back to source controls