AdicIdempotent.lean

1 import PaperX.IdempotentNewton
2 import PaperX.MatrixWitnessLimits
3 import Mathlib.LinearAlgebra.Matrix.Ideal
4 
5 /-! Idempotents in a complete matrix algebra lift by polynomial correction.
6 The construction preserves every matrix commuting with the original approximation.
7 No exact idempotent or compatible family is supplied as a premise. -/
8 set_option autoImplicit false
9 
10 namespace PaperX.AdicIdempotent
11 open PaperX.RepresentationLimits PaperX.MatrixWitnessLimits
12 open PaperX.IdempotentNewton
13 
14 variable {R : Type*} [CommRing R]
15 variable {ι : Type*} [Fintype ι] [DecidableEq ι]
16 
17 theorem matrix_map_pow {S : Type*} [CommRing S] (f : R →+* S)
18     (A : Matrix ι ι R) (n : ℕ) : (A^n).map f = (A.map f)^n :=
19   map_pow f.mapMatrix A n
20 
21 theorem matrix_map_sub {S : Type*} [CommRing S] (f : R →+* S)
22     (A B : Matrix ι ι R) : (A-B).map f = A.map f - B.map f :=
23   map_sub f.mapMatrix A B
24 
25 /-- Entrywise reduction detects membership in the matrix ideal. -/
26 theorem map_eq_zero_iff (I : Ideal R) (A : Matrix ι ι R) :
27     A.map (Ideal.Quotient.mk I) = 0 ↔ A ∈ I.matrix ι := by
28   constructor
29   · intro h i j
30     apply Ideal.Quotient.eq_zero_iff_mem.mp
31     exact congrArg (fun M => M i j) h
32   · intro h
33     ext i j
34     exact Ideal.Quotient.eq_zero_iff_mem.mpr (h i j)
35 
36 /-- Entrywise ideal products contain matrix products. -/
37 theorem matrix_mul_mem (I J : Ideal R) {A B : Matrix ι ι R}
38     (hA : A ∈ I.matrix ι) (hB : B ∈ J.matrix ι) :
39     A * B ∈ (I * J).matrix ι := by
40   intro i j
41   rw [Matrix.mul_apply]
42   exact Ideal.sum_mem _ fun l _ => Ideal.mul_mem_mul (hA i l) (hB l j)
43 
44 /-- Multiplication on either side preserves entrywise ideal membership. -/
45 theorem matrix_mul_right_mem (I : Ideal R) {A : Matrix ι ι R}
46     (hA : A ∈ I.matrix ι) (B : Matrix ι ι R) : A * B ∈ I.matrix ι := by
47   intro i j
48   rw [Matrix.mul_apply]
49   exact Ideal.sum_mem _ fun l _ => I.mul_mem_right _ (hA i l)
50 
51 /-- The polynomial iteration, started at an approximate idempotent. -/
52 def iterate (A : Matrix ι ι R) : ℕ → Matrix ι ι R
53   | 0 => A
54   | n+1 => correct (iterate A n)
55 
56 @[simp] theorem iterate_zero (A : Matrix ι ι R) : iterate A 0 = A := rfl
57 @[simp] theorem iterate_succ (A : Matrix ι ι R) (n : ℕ) :
58     iterate A (n+1) = correct (iterate A n) := rfl
59 
60 /-- One correction at least adds one ideal digit when the starting depth is positive. -/
61 theorem iterate_error_mem (I : Ideal R) (k : ℕ) (hk : 0 < k)
62     (A : Matrix ι ι R) (hA : A^2 - A ∈ (I^k).matrix ι) (n : ℕ) :
63     (iterate A n)^2 - iterate A n ∈ (I^(n+k)).matrix ι := by
64   induction n with
65   | zero => simpa using hA
66   | succ n ih =>
67     rw [iterate_succ, correct_error]
68     have hsq : ((iterate A n)^2 - iterate A n)^2 ∈
69         (I^((n+k)+(n+k))).matrix ι := by
70       rw [pow_two, pow_add]
71       exact matrix_mul_mem _ _ ih ih
72     exact Ideal.matrix_monotone ι
73       (Ideal.pow_le_pow_right (by omega : n+1+k ≤ (n+k)+(n+k)))
74       (matrix_mul_right_mem _ hsq _)
75 
76 /-- Each correction has the same precision as the preceding defect. -/
77 theorem iterate_step_mem (I : Ideal R) (k : ℕ) (hk : 0 < k)
78     (A : Matrix ι ι R) (hA : A^2 - A ∈ (I^k).matrix ι) (n : ℕ) :
79     iterate A (n+1) - iterate A n ∈ (I^(n+k)).matrix ι := by
80   rw [iterate_succ, correct_sub]
81   exact (I^(n+k)).matrix ι |>.mul_mem_left _ (iterate_error_mem I k hk A hA n)
82 
83 /-- Every iterate retains the initial prescribed reduction. -/
84 theorem iterate_reduces (I : Ideal R) (k : ℕ) (hk : 0 < k)
85     (A : Matrix ι ι R) (hA : A^2 - A ∈ (I^k).matrix ι) (n : ℕ) :
86     (iterate A n).map (Ideal.Quotient.mk (I^k)) = A.map (Ideal.Quotient.mk (I^k)) := by
87   induction n with
88   | zero => rfl
89   | succ n ih =>
90     have hmem := Ideal.matrix_monotone ι
91       (Ideal.pow_le_pow_right (Nat.le_add_left k n)) (iterate_step_mem I k hk A hA n)
92     have H := (map_eq_zero_iff (I^k) _).mpr hmem
93     rw [matrix_map_sub] at H
94     exact (sub_eq_zero.mp H).trans ih
95 
96 /-- Polynomial iterates commute with any matrix commuting with the input. -/
97 theorem iterate_commutes (A C : Matrix ι ι R) (h : C*A=A*C) (n : ℕ) :
98     C * iterate A n = iterate A n * C := by
99   induction n with
100   | zero => exact h
101   | succ n ih => exact (correct_intertwines (iterate A n) (iterate A n) C ih.symm).symm
102 
103 /-- The corrected finite matrices form a coherent family without supplied choices. -/
104 def family (I : Ideal R) (k : ℕ) (hk : 0 < k)
105     (A : Matrix ι ι R) (hA : A^2 - A ∈ (I^k).matrix ι) : MatrixFamily R I ι :=
106   matrix_family_of_succ I (fun n => (iterate A n).map (Ideal.Quotient.mk (I^n))) (by
107     intro n
108     have hmem := Ideal.matrix_monotone ι
109       (Ideal.pow_le_pow_right (Nat.le_add_right n k)) (iterate_step_mem I k hk A hA n)
110     have H := (map_eq_zero_iff (I^n) _).mpr hmem
111     rw [matrix_map_sub] at H
112     have heq := sub_eq_zero.mp H
113     ext i j
114     simpa using congrArg (fun M => M i j) heq)
115 
116 /-- Actual idempotent correction in the complete matrix algebra, retaining any
117 positive starting precision and every existing commutation relation. -/
118 theorem correct_commuting (I : Ideal R) [IsAdicComplete I R]
119     (k : ℕ) (hk : 0 < k) (A : Matrix ι ι R)
120     (hA : (A.map (Ideal.Quotient.mk (I^k)))^2 = A.map (Ideal.Quotient.mk (I^k))) :
121     ∃ E : Matrix ι ι R, E^2 = E ∧
122       E.map (Ideal.Quotient.mk (I^k)) = A.map (Ideal.Quotient.mk (I^k)) ∧
123       ∀ C : Matrix ι ι R, C*A=A*C → C*E=E*C := by
124   have hmem : A^2 - A ∈ (I^k).matrix ι := by
125     apply (map_eq_zero_iff (I^k) _).mp
126     simp only [matrix_map_sub, matrix_map_pow, hA, sub_self]
127   let F := family I k hk A hmem
128   let E := reconstructMatrix I F
129   have hE (n : ℕ) : E.map (Ideal.Quotient.mk (I^n)) =
130       (iterate A n).map (Ideal.Quotient.mk (I^n)) := reconstructMatrix_reduces I F n
131   refine ⟨E, ?_, ?_, ?_⟩
132   · apply matrix_ext I
133     intro n
134     have hd := Ideal.matrix_monotone ι
135       (Ideal.pow_le_pow_right (Nat.le_add_right n k)) (iterate_error_mem I k hk A hmem n)
136     have H := (map_eq_zero_iff (I^n) _).mpr hd
137     rw [matrix_map_sub] at H
138     have hpow : (E^2).map (Ideal.Quotient.mk (I^n)) =
139         (E.map (Ideal.Quotient.mk (I^n)))^2 := by
140       exact map_pow (Ideal.Quotient.mk (I^n)).mapMatrix E 2
141     rw [hpow, hE]
142     simpa only [matrix_map_pow] using sub_eq_zero.mp H
143   · exact (hE k).trans (iterate_reduces I k hk A hmem k)
144   · intro C hC
145     apply matrix_ext I
146     intro n
147     simp only [Matrix.map_mul, hE]
148     simpa only [Matrix.map_mul] using congrArg (fun M => M.map (Ideal.Quotient.mk (I^n)))
149       (iterate_commutes A C hC n)
150 
151 end PaperX.AdicIdempotent

Back to source controls