CornerProjectors.lean

1 import PaperX.AdicIdempotent
2 import PaperX.MatrixProjector
3 
4 /-! Polynomial correction inside a supplied equivariant corner, and detection
5 of a zero idempotent in an adically separated matrix algebra. -/
6 set_option autoImplicit false
7 namespace PaperX.CornerProjectors
8 open PaperX.RepresentationLimits PaperX.MatrixProjector PaperX.AdicIdempotent
9 
10 variable {R Γ ι : Type*} [CommRing R] [Group Γ]
11   [Fintype ι] [DecidableEq ι]
12 
13 /-- Correct an approximate idempotent while retaining both support equations
14 in an exact equivariant corner. -/
15 theorem exists_in_corner (I : Ideal R) [IsAdicComplete I R]
16     (k : ℕ) (hk : 0 < k) (ρ : MatrixRep R Γ ι)
17     (C : Projector ρ) (A : Matrix ι ι R)
18     (hcomm : ∀ g, ρ g * A = A * ρ g)
19     (hid : (A.map (Ideal.Quotient.mk (I^k)))^2 =
20       A.map (Ideal.Quotient.mk (I^k)))
21     (hleft : C.matrix.map (Ideal.Quotient.mk (I^k)) *
22         A.map (Ideal.Quotient.mk (I^k)) = A.map (Ideal.Quotient.mk (I^k)))
23     (hright : A.map (Ideal.Quotient.mk (I^k)) *
24         C.matrix.map (Ideal.Quotient.mk (I^k)) = A.map (Ideal.Quotient.mk (I^k))) :
25     ∃ P : Projector ρ,
26       P.matrix.map (Ideal.Quotient.mk (I^k)) = A.map (Ideal.Quotient.mk (I^k)) ∧
27       C.matrix * P.matrix = P.matrix ∧ P.matrix * C.matrix = P.matrix := by
28   let f := Ideal.Quotient.mk (I^k)
29   let B := C.matrix * A * C.matrix
30   have hB : B.map f = A.map f := by
31     dsimp [B]
32     rw [Matrix.map_mul, Matrix.map_mul, hleft, hright]
33   have hBC : C.matrix * B = B * C.matrix := by
34     dsimp [B]
35     simp only [← mul_assoc, C.idempotent]
36     rw [mul_assoc (C.matrix * A), C.idempotent]
37   have hBρ (g : Γ) : ρ g * B = B * ρ g := by
38     dsimp [B]
39     calc
40       ρ g * (C.matrix * A * C.matrix) =
41           (ρ g * C.matrix) * A * C.matrix := by simp only [mul_assoc]
42       _ = (C.matrix * ρ g) * A * C.matrix := by rw [C.commutes]
43       _ = C.matrix * (ρ g * A) * C.matrix := by simp only [mul_assoc]
44       _ = C.matrix * (A * ρ g) * C.matrix := by rw [hcomm]
45       _ = C.matrix * A * (ρ g * C.matrix) := by simp only [mul_assoc]
46       _ = C.matrix * A * (C.matrix * ρ g) := by rw [C.commutes]
47       _ = (C.matrix * A * C.matrix) * ρ g := by simp only [mul_assoc]
48   obtain ⟨Q, hQ, hred, hQcomm⟩ := correct_commuting I k hk B (by rw [hB]; exact hid)
49   have hCQ := hQcomm C.matrix hBC
50   have hQρ (g : Γ) := hQcomm (ρ g) (hBρ g)
51   have hQQ : Q * Q = Q := by simpa only [pow_two] using hQ
52   let P : Projector ρ := {
53     matrix := C.matrix * Q
54     idempotent := by
55       calc
56         C.matrix * Q * (C.matrix * Q) = C.matrix * (Q * C.matrix) * Q := by
57           simp only [mul_assoc]
58         _ = C.matrix * (C.matrix * Q) * Q := by rw [← hCQ]
59         _ = (C.matrix * C.matrix) * (Q * Q) := by simp only [mul_assoc]
60         _ = C.matrix * Q := by rw [C.idempotent, hQQ]
61     commutes := fun g => by
62       calc
63         ρ g * (C.matrix * Q) = (ρ g * C.matrix) * Q := by rw [mul_assoc]
64         _ = (C.matrix * ρ g) * Q := by rw [C.commutes]
65         _ = C.matrix * (ρ g * Q) := by rw [mul_assoc]
66         _ = C.matrix * (Q * ρ g) := by rw [hQρ]
67         _ = (C.matrix * Q) * ρ g := by rw [mul_assoc] }
68   refine ⟨P, ?_, ?_, ?_⟩
69   · change (C.matrix * Q).map f = A.map f
70     rw [Matrix.map_mul, hred, hB, hleft]
71   · change C.matrix * (C.matrix * Q) = C.matrix * Q
72     rw [← mul_assoc, C.idempotent]
73   · change (C.matrix * Q) * C.matrix = C.matrix * Q
74     rw [mul_assoc, ← hCQ, ← mul_assoc, C.idempotent]
75 
76 /-- An idempotent reducing to zero at any positive depth is zero.
77 Only adic separatedness, provided here by completeness, is used. -/
78 theorem eq_zero_of_idempotent_reduces_zero (I : Ideal R) [IsAdicComplete I R]
79     (k : ℕ) (hk : 0 < k) (E : Matrix ι ι R) (hid : E * E = E)
80     (hzero : E.map (Ideal.Quotient.mk (I^k)) = 0) : E = 0 := by
81   have hmem : E ∈ I.matrix ι :=
82     Ideal.matrix_monotone ι (Ideal.pow_le_self (by omega : k ≠ 0))
83       ((map_eq_zero_iff (I^k) E).mp hzero)
84   have hall (n : ℕ) : E ∈ (I^n).matrix ι := by
85     induction n with
86     | zero => simp
87     | succ n ih =>
88       rw [← hid, pow_succ]
89       exact matrix_mul_mem _ _ ih hmem
90   apply matrix_ext I
91   intro n
92   simp only [Matrix.map_zero, map_zero]
93   exact (map_eq_zero_iff (I^n) E).mpr (hall n)
94 
95 end PaperX.CornerProjectors

Back to source controls