PolynomialWeightedInverse.lean

1 module
2 public import Mathlib.NumberTheory.Padics.PadicIntegers
3 public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
4 public import Mathlib.Algebra.MvPolynomial.PDeriv
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 
10 namespace Komorebi.PolynomialWeightedInverse
11 open Matrix
12 variable {d e : ℕ}
13 
14 /-- The actual Jacobian of a polynomial system at the specified base point. -/
15 def jacobian {R : Type*} [CommRing R]
16     (F : Fin e → MvPolynomial (Fin d) R) (a : Fin d → R) : Matrix (Fin e) (Fin d) R :=
17   fun i j => MvPolynomial.eval a (MvPolynomial.pderiv j (F i))
18 
19 /-- Multiplication of a polynomial system by a constant coefficient matrix. -/
20 def precondition {R : Type*} [CommRing R] (A : Matrix (Fin e) (Fin e) R)
21     (F : Fin e → MvPolynomial (Fin d) R) : Fin e → MvPolynomial (Fin d) R :=
22   fun i => ∑ j, MvPolynomial.C (A i j) * F j
23 
24 /-- Constant matrix multiplication commutes with actual polynomial evaluation. -/
25 theorem eval_precondition {R : Type*} [CommRing R] (A : Matrix (Fin e) (Fin e) R)
26     (F : Fin e → MvPolynomial (Fin d) R) (a : Fin d → R) :
27     (fun i => MvPolynomial.eval a (precondition A F i)) =
28       A.mulVec (fun i => MvPolynomial.eval a (F i)) := by
29   ext i
30   simp [precondition, Matrix.mulVec, dotProduct]
31 
32 /-- The Jacobian of the preconditioned system is the actual matrix product. -/
33 theorem jacobian_precondition {R : Type*} [CommRing R]
34     (A : Matrix (Fin e) (Fin e) R) (F : Fin e → MvPolynomial (Fin d) R)
35     (a : Fin d → R) : jacobian (precondition A F) a = A * jacobian F a := by
36   ext i k
37   simp [jacobian, precondition, Matrix.mul_apply]
38 
39 /-- An integral matrix preserves every coordinatewise divisibility condition. -/
40 theorem mulVec_preserves_dvd {R : Type*} [CommRing R]
41     (A : Matrix (Fin e) (Fin d) R) (c : R) (v : Fin d → R)
42     (hv : ∀ j, c ∣ v j) : ∀ i, c ∣ A.mulVec v i := by
43   intro i
44   change c ∣ ∑ j, A i j * v j
45   apply Finset.dvd_sum
46   intro j _
47   exact dvd_mul_of_dvd_right (hv j) (A i j)
48 
49 /-- A nonzero scalar right inverse certificate makes the matrix action injective. -/
50 theorem mulVec_injective_of_scalar_certificate {R : Type*} [CommRing R]
51     [IsDomain R] (A J : Matrix (Fin d) (Fin d) R) (c : R) (hc : c ≠ 0)
52     (hJA : J * A = c • (1 : Matrix (Fin d) (Fin d) R)) :
53     Function.Injective A.mulVec := by
54   intro u v huv
55   have h := congrArg J.mulVec huv
56   simp only [Matrix.mulVec_mulVec, hJA, Matrix.smul_mulVec, Matrix.one_mulVec] at h
57   funext i
58   exact mul_left_cancel₀ hc (congrFun h i)
59 
60 /-- The coefficient inclusion into the fraction field, applied entrywise. -/
61 def rationalMatrix (p : ℕ) [Fact (Nat.Prime p)]
62     (A : Matrix (Fin d) (Fin d) ℤ_[p]) : Matrix (Fin d) (Fin d) ℚ_[p] :=
63   (algebraMap ℤ_[p] ℚ_[p]).mapMatrix A
64 
65 /-- Entrywise inclusion into the fraction field loses no matrix information. -/
66 theorem rationalMatrix_injective (p : ℕ) [Fact (Nat.Prime p)] :
67     Function.Injective (rationalMatrix p (d := d)) := by
68   intro A B h
69   ext i j
70   exact Subtype.coe_injective (congrFun (congrFun h i) j)
71 
72 @[simp] theorem rationalMatrix_mul (p : ℕ) [Fact (Nat.Prime p)]
73     (A J : Matrix (Fin d) (Fin d) ℤ_[p]) :
74     rationalMatrix p (A * J) = rationalMatrix p A * rationalMatrix p J :=
75   map_mul _ A J
76 
77 @[simp] theorem rationalMatrix_scalar (p s : ℕ) [Fact (Nat.Prime p)] :
78     rationalMatrix p ((p : ℤ_[p])^s • (1 : Matrix (Fin d) (Fin d) ℤ_[p])) =
79       (p : ℚ_[p])^s • (1 : Matrix (Fin d) (Fin d) ℚ_[p]) := by
80   ext i j
81   by_cases h : i = j <;> simp [rationalMatrix, h]
82 
83 /-- The written denominator bound on the inverse gives both integral matrix identities. -/
84 theorem certificate_of_integral_inverse (p s : ℕ) [Fact (Nat.Prime p)]
85     (J A : Matrix (Fin d) (Fin d) ℤ_[p]) (hJ : IsUnit (rationalMatrix p J))
86     (hA : rationalMatrix p A = (p : ℚ_[p])^s • (rationalMatrix p J)⁻¹) :
87     A * J = (p : ℤ_[p])^s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]) ∧
88     J * A = (p : ℤ_[p])^s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]) := by
89   have hdet := (Matrix.isUnit_iff_isUnit_det _).mp hJ
90   constructor
91   · apply rationalMatrix_injective p
92     rw [rationalMatrix_mul, rationalMatrix_scalar, hA, Matrix.smul_mul,
93       Matrix.nonsing_inv_mul _ hdet]
94   · apply rationalMatrix_injective p
95     rw [rationalMatrix_mul, rationalMatrix_scalar, hA, Matrix.mul_smul,
96       Matrix.mul_nonsing_inv _ hdet]
97 
98 /-- Conversely, under nonsingularity a scalar left inverse certificate is exactly the
99 integral representative of the bounded rational inverse. -/
100 theorem integral_inverse_of_certificate (p s : ℕ) [Fact (Nat.Prime p)]
101     (J A : Matrix (Fin d) (Fin d) ℤ_[p]) (hJ : IsUnit (rationalMatrix p J))
102     (hAJ : A * J = (p : ℤ_[p])^s • (1 : Matrix (Fin d) (Fin d) ℤ_[p])) :
103     rationalMatrix p A = (p : ℚ_[p])^s • (rationalMatrix p J)⁻¹ := by
104   have hdet := (Matrix.isUnit_iff_isUnit_det _).mp hJ
105   have h := congrArg (rationalMatrix p) hAJ
106   rw [rationalMatrix_mul, rationalMatrix_scalar] at h
107   calc
108     rationalMatrix p A = (rationalMatrix p A * rationalMatrix p J) *
109         (rationalMatrix p J)⁻¹ := by
110       rw [Matrix.mul_assoc, Matrix.mul_nonsing_inv _ hdet, Matrix.mul_one]
111     _ = (p : ℚ_[p])^s • (rationalMatrix p J)⁻¹ := by
112       rw [h, Matrix.smul_mul, Matrix.one_mul]
113 
114 /-- At every exponent the inverse-denominator condition is equivalent to an integral certificate. -/
115 theorem integral_inverse_iff_certificate (p s : ℕ) [Fact (Nat.Prime p)]
116     (J : Matrix (Fin d) (Fin d) ℤ_[p]) (hJ : IsUnit (rationalMatrix p J)) :
117     (∃ A : Matrix (Fin d) (Fin d) ℤ_[p],
118       rationalMatrix p A = (p : ℚ_[p])^s • (rationalMatrix p J)⁻¹) ↔
119     (∃ A : Matrix (Fin d) (Fin d) ℤ_[p],
120       A * J = (p : ℤ_[p])^s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]) ∧
121       J * A = (p : ℤ_[p])^s • (1 : Matrix (Fin d) (Fin d) ℤ_[p])) := by
122   constructor
123   · rintro ⟨A, hA⟩
124     exact ⟨A, certificate_of_integral_inverse p s J A hJ hA⟩
125   · rintro ⟨A, hAJ, _⟩
126     exact ⟨A, integral_inverse_of_certificate p s J A hJ hAJ⟩
127 
128 /-- An integral scalar left inverse certificate itself proves nonsingularity over the fraction field. -/
129 theorem rationalMatrix_isUnit_of_certificate (p s : ℕ) [Fact (Nat.Prime p)]
130     (J A : Matrix (Fin d) (Fin d) ℤ_[p])
131     (hAJ : A * J = (p : ℤ_[p])^s • (1 : Matrix (Fin d) (Fin d) ℤ_[p])) :
132     IsUnit (rationalMatrix p J) := by
133   have h := congrArg (rationalMatrix p) hAJ
134   rw [rationalMatrix_mul, rationalMatrix_scalar] at h
135   apply Matrix.mulVec_injective_iff_isUnit.mp
136   apply mulVec_injective_of_scalar_certificate (rationalMatrix p J)
137     (rationalMatrix p A) ((p : ℚ_[p])^s) _ h
138   exact pow_ne_zero s (Nat.cast_ne_zero.mpr (Fact.out : Nat.Prime p).ne_zero)
139 
140 /-- The effective integral certificate is equivalent to precisely the written rational inverse
141 hypothesis, including nonsingularity and with the same denominator exponent. -/
142 theorem bounded_inverse_iff_certificate (p s : ℕ) [Fact (Nat.Prime p)]
143     (J : Matrix (Fin d) (Fin d) ℤ_[p]) :
144     (IsUnit (rationalMatrix p J) ∧
145       ∃ A : Matrix (Fin d) (Fin d) ℤ_[p],
146         rationalMatrix p A = (p : ℚ_[p])^s • (rationalMatrix p J)⁻¹) ↔
147     (∃ A : Matrix (Fin d) (Fin d) ℤ_[p],
148       A * J = (p : ℤ_[p])^s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]) ∧
149       J * A = (p : ℤ_[p])^s • (1 : Matrix (Fin d) (Fin d) ℤ_[p])) := by
150   constructor
151   · rintro ⟨hJ, hA⟩
152     exact (integral_inverse_iff_certificate p s J hJ).mp hA
153   · rintro ⟨A, hAJ, hJA⟩
154     have hJ := rationalMatrix_isUnit_of_certificate p s J A hAJ
155     exact ⟨hJ, (integral_inverse_iff_certificate p s J hJ).mpr ⟨A, hAJ, hJA⟩⟩
156 
157 /-- The integral inverse certificate yields injectivity even when the Jacobian is singular modulo p. -/
158 theorem padic_mulVec_injective (p s : ℕ) [Fact (Nat.Prime p)]
159     (A J : Matrix (Fin d) (Fin d) ℤ_[p])
160     (hJA : J * A = (p : ℤ_[p])^s • (1 : Matrix (Fin d) (Fin d) ℤ_[p])) :
161     Function.Injective A.mulVec := by
162   apply mulVec_injective_of_scalar_certificate A J ((p : ℤ_[p])^s) _ hJA
163   exact pow_ne_zero s (Nat.cast_ne_zero.mpr (Fact.out : Nat.Prime p).ne_zero)
164 
165 /-- Preconditioning by the bounded inverse certificate preserves exactly the original roots. -/
166 theorem precondition_root_iff (p s : ℕ) [Fact (Nat.Prime p)]
167     (A J : Matrix (Fin d) (Fin d) ℤ_[p])
168     (hJA : J * A = (p : ℤ_[p])^s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
169     (F : Fin d → MvPolynomial (Fin d) ℤ_[p]) (a : Fin d → ℤ_[p]) :
170     (fun i => MvPolynomial.eval a (precondition A F i)) = 0 ↔
171       (fun i => MvPolynomial.eval a (F i)) = 0 := by
172   rw [eval_precondition]
173   constructor
174   · intro h
175     apply padic_mulVec_injective p s A J hJA
176     simpa only [Matrix.mulVec_zero] using h
177   · intro h
178     rw [h, Matrix.mulVec_zero]
179 
180 end Komorebi.PolynomialWeightedInverse

Back to source controls