IdempotentNewton.lean

1 import Mathlib.Tactic.NoncommRing
2 import Mathlib.Algebra.Ring.Hom.Defs
3 import Mathlib.Algebra.Ring.Nat
4 import Mathlib.Tactic.NormNum
5 
6 /-! Polynomial correction of an approximate idempotent in a possibly
7 noncommutative ring. No inverse of two is needed. -/
8 set_option autoImplicit false
9 
10 namespace PaperX.IdempotentNewton
11 
12 variable {A B : Type*} [Ring A] [Ring B]
13 
14 /-- The universal integral polynomial used to correct an idempotent. -/
15 def correct (a : A) : A := 3 * a ^ 2 - 2 * a ^ 3
16 
17 /-- The correction changes the input by a multiple of its idempotence error. -/
18 theorem correct_sub (a : A) :
19     correct a - a = -(2 * a - 1) * (a ^ 2 - a) := by
20   unfold correct
21   simp only [show (2 : A) = 1 + 1 by norm_num,
22     show (3 : A) = 1 + 1 + 1 by norm_num]
23   noncomm_ring
24 
25 /-- One correction squares the idempotence error. -/
26 theorem correct_error (a : A) :
27     correct a ^ 2 - correct a =
28       (a ^ 2 - a) ^ 2 * (4 * a ^ 2 - 4 * a - 3) := by
29   unfold correct
30   simp only [show (2 : A) = 1 + 1 by norm_num,
31     show (3 : A) = 1 + 1 + 1 by norm_num,
32     show (4 : A) = 1 + 1 + 1 + 1 by norm_num]
33   noncomm_ring
34 
35 /-- Polynomial correction fixes exact idempotents. -/
36 theorem correct_eq_of_idempotent (a : A) (ha : a * a = a) :
37     correct a = a := by
38   have hz : a ^ 2 - a = 0 := by simp [pow_two, ha]
39   have hd := correct_sub a
40   rw [hz, mul_zero, sub_eq_zero] at hd
41   exact hd
42 
43 /-- Correction commutes with every unital ring homomorphism. -/
44 theorem map_correct (f : A →+* B) (a : A) :
45     f (correct a) = correct (f a) := by
46   unfold correct
47   rw [show (2 : A) = 1 + 1 by norm_num,
48     show (3 : A) = 1 + 1 + 1 by norm_num]
49   simp only [map_sub, map_mul, map_pow, map_add, map_one]
50   norm_num
51 
52 /-- If one matrix intertwines two endomorphisms, it intertwines their powers. -/
53 theorem pow_intertwines (a b p : A) (h : a * p = p * b) (n : ℕ) :
54     a ^ n * p = p * b ^ n := by
55   induction n with
56   | zero => simp
57   | succ n hn =>
58       rw [pow_succ', mul_assoc, hn, ← mul_assoc, h, mul_assoc, ← pow_succ']
59 
60 /-- Polynomial correction preserves every supplied intertwiner. -/
61 theorem correct_intertwines (a b p : A) (h : a * p = p * b) :
62     correct a * p = p * correct b := by
63   have h2 := pow_intertwines a b p h 2
64   have h3 := pow_intertwines a b p h 3
65   unfold correct
66   calc
67     (3 * a ^ 2 - 2 * a ^ 3) * p =
68         3 * (a ^ 2 * p) - 2 * (a ^ 3 * p) := by simp only [sub_mul, mul_assoc]
69     _ = 3 * (p * b ^ 2) - 2 * (p * b ^ 3) := by rw [h2, h3]
70     _ = p * (3 * b ^ 2 - 2 * b ^ 3) := by
71       simp only [show (2 : A) = 1 + 1 by norm_num,
72         show (3 : A) = 1 + 1 + 1 by norm_num]
73       noncomm_ring
74 
75 end PaperX.IdempotentNewton

Back to source controls