ReleaseResultantPolynomial.lean

1 import KomorebiVerification.PaperII.ResultantSeparation
2 import Mathlib.LinearAlgebra.Charpoly.Basic
3 import Mathlib.LinearAlgebra.Charpoly.BaseChange
4 import Mathlib.LinearAlgebra.Projection
5 import Mathlib.RingTheory.Localization.FractionRing
6 
7 /-! Polynomial-to-operator bridges for the Paper II release. -/
8 
9 set_option autoImplicit false
10 
11 noncomputable section
12 
13 namespace Komorebi.PaperII.ReleaseResultantPolynomial
14 
15 open Polynomial ResultantSeparation
16 
17 universe u v w
18 
19 variable {K : Type u} {M : Type v}
20 variable [Field K] [AddCommGroup M] [Module K M]
21 
22 theorem evaluated_polynomials_commute (A : Module.End K M) (p q : K[X]) :
23     Commute (aeval A p) (aeval A q) := by
24   change aeval A p * aeval A q = aeval A q * aeval A p
25   rw [← map_mul, ← map_mul, mul_comm p q]
26 
27 /-- Evaluation derives every certificate field from the polynomial identity and
28 the characteristic factorization; annihilation is Cayley--Hamilton. -/
29 theorem certificate_of_charpoly [Module.Free K M] [Module.Finite K M]
30     (A : Module.End K M) (f g u v : K[X]) (r : K)
31     (hr : r ≠ 0) (hchar : A.charpoly = f * g)
32     (hbez : u * f + v * g = C r) :
33     EvaluatedBezoutCertificate (aeval A f) (aeval A g)
34       (aeval A u) (aeval A v) r where
35   r_ne_zero := hr
36   commute_FG := evaluated_polynomials_commute A f g
37   commute_FU := evaluated_polynomials_commute A f u
38   commute_FV := evaluated_polynomials_commute A f v
39   commute_GU := evaluated_polynomials_commute A g u
40   commute_GV := evaluated_polynomials_commute A g v
41   commute_UV := evaluated_polynomials_commute A u v
42   bezout := by
43     have h := congrArg (aeval A) hbez
44     simpa only [map_add, map_mul, aeval_C, Algebra.algebraMap_eq_smul_one] using h
45   annihilate := by
46     rw [← map_mul, ← hchar]
47     exact A.aeval_self_charpoly
48 
49 /-- A monic factor of degree zero is one, so the all-constant boundary case
50 also admits the actual Sylvester resultant as a clearing scalar. -/
51 theorem exists_resultant_bezout {R : Type w} [CommRing R]
52     (f g : R[X]) (hf : f.Monic) :
53     ∃ u v : R[X], u * f + v * g = C (f.resultant g) := by
54   by_cases hf0 : f.natDegree = 0
55   · have hf1 : f = 1 := eq_one_of_monic_natDegree_zero hf hf0
56     subst f
57     exact ⟨C ((1 : R[X]).resultant g), 0, by simp⟩
58   · obtain ⟨u, v, _, _, h⟩ := exists_mul_add_mul_eq_C_resultant f g le_rfl le_rfl
59       (Or.inl hf0)
60     exact ⟨u, v, by simpa only [mul_comm u f, mul_comm v g] using h⟩
61 
62 theorem resultant_nonzero_of_coprime (f g : K[X]) (h : IsCoprime f g) :
63     f.resultant g ≠ 0 := by
64   intro hz
65   exact (Polynomial.resultant_eq_zero_iff.mp hz).2 h
66 
67 /-- The polynomial/resultant endpoint constructs the evaluated certificate,
68 rather than assuming its commutations or its annihilation equation. -/
69 theorem resultant_projector_exists [Module.Free K M] [Module.Finite K M]
70     (A : Module.End K M) (f g : K[X]) (hf : f.Monic)
71     (hc : IsCoprime f g) (hchar : A.charpoly = f * g) :
72     ∃ u v : K[X],
73       u * f + v * g = C (f.resultant g) ∧
74       EvaluatedBezoutCertificate (aeval A f) (aeval A g)
75         (aeval A u) (aeval A v) (f.resultant g) ∧
76       separator (f.resultant g) (aeval A v) (aeval A g) *
77         separator (f.resultant g) (aeval A v) (aeval A g) =
78         separator (f.resultant g) (aeval A v) (aeval A g) := by
79   obtain ⟨u, v, hbez⟩ := exists_resultant_bezout f g hf
80   have cert := certificate_of_charpoly A f g u v (f.resultant g)
81     (resultant_nonzero_of_coprime f g hc) hchar hbez
82   exact ⟨u, v, hbez, cert, separator_idempotent cert⟩
83 
84 section ExactKernels
85 
86 variable {F G U V : Module.End K M} {r : K}
87 
88 theorem first_mul_separator_eq_zero
89     (cert : EvaluatedBezoutCertificate F G U V r) :
90     F * separator r V G = 0 := by
91   rw [separator, mul_smul_comm, separatorNumerator, ← mul_assoc,
92     cert.commute_FV.eq, mul_assoc, cert.annihilate, mul_zero, smul_zero]
93 
94 theorem second_mul_separator_eq_self
95     (cert : EvaluatedBezoutCertificate F G U V r) :
96     G * separator r V G = G := by
97   have hz : G * (U * F) = 0 := by
98     rw [← mul_assoc, cert.commute_GU.eq, mul_assoc, ← cert.commute_FG.eq,
99       cert.annihilate, mul_zero]
100   have hb := congrArg (G * ·) cert.bezout
101   have hvg : G * (V * G) = r • G := by
102     simpa only [mul_add, hz, zero_add, mul_smul_comm, mul_one] using hb
103   rw [separator, mul_smul_comm, separatorNumerator, hvg, smul_smul]
104   simp [cert.r_ne_zero]
105 
106 theorem separator_range_eq_first_kernel
107     (cert : EvaluatedBezoutCertificate F G U V r) :
108     LinearMap.range (separator r V G) = LinearMap.ker F := by
109   ext x
110   constructor
111   · rintro ⟨y, rfl⟩
112     exact LinearMap.congr_fun (first_mul_separator_eq_zero cert) y
113   · intro hx
114     exact ⟨x, separator_apply_of_mem_ker_F cert hx⟩
115 
116 theorem separator_kernel_eq_second_kernel
117     (cert : EvaluatedBezoutCertificate F G U V r) :
118     LinearMap.ker (separator r V G) = LinearMap.ker G := by
119   ext x
120   constructor
121   · intro hx
122     change G x = 0
123     have h := LinearMap.congr_fun (second_mul_separator_eq_self cert) x
124     change separator r V G x = 0 at hx
125     change G (separator r V G x) = G x at h
126     simpa only [hx, map_zero] using h.symm
127   · intro hx
128     exact separator_apply_of_mem_ker_G hx
129 
130 theorem complementary_kernels
131     (cert : EvaluatedBezoutCertificate F G U V r) :
132     IsCompl (LinearMap.ker F) (LinearMap.ker G) := by
133   have hi : IsIdempotentElem (separator r V G) := separator_idempotent cert
134   simpa only [separator_range_eq_first_kernel cert,
135     separator_kernel_eq_second_kernel cert] using LinearMap.IsIdempotentElem.isCompl hi
136 
137 end ExactKernels
138 
139 section IntegralBaseChange
140 
141 open scoped TensorProduct
142 
143 variable {R : Type w} {L : Type v} [CommRing R] [AddCommGroup L]
144 variable [Module R L] [Algebra R K]
145 
146 /-- The image of the actual integral module in its scalar extension. -/
147 def tensorLattice : Submodule R (K ⊗[R] L) :=
148   LinearMap.range (TensorProduct.mk R K L 1)
149 
150 theorem aeval_baseChange (A : Module.End R L) (p : R[X]) :
151     (aeval A p).baseChange K =
152       aeval (A.baseChange K) (p.map (algebraMap R K)) := by
153   apply Polynomial.map_aeval_eq_aeval_map
154     (ψ := (Module.End.baseChangeHom R K L).toRingHom)
155   ext r
156   simp [Algebra.algebraMap_eq_smul_one]
157 
158 theorem integral_evaluation_preserves_tensorLattice (A : Module.End R L) (p : R[X])
159     (x : K ⊗[R] L) (hx : x ∈ tensorLattice (K := K) (R := R) (L := L)) :
160     aeval (A.baseChange K) (p.map (algebraMap R K)) x ∈
161       tensorLattice (K := K) (R := R) (L := L) := by
162   obtain ⟨y, rfl⟩ := hx
163   rw [← aeval_baseChange]
164   exact ⟨aeval A p y, rfl⟩
165 
166 theorem certificate_of_integral_charpoly [Module.Free R L] [Module.Finite R L]
167     (A : Module.End R L) (f g u v : R[X]) (r : R)
168     (hr : algebraMap R K r ≠ 0) (hchar : A.charpoly = f * g)
169     (hbez : u * f + v * g = C r) :
170     EvaluatedBezoutCertificate
171       (aeval (A.baseChange K) (f.map (algebraMap R K)))
172       (aeval (A.baseChange K) (g.map (algebraMap R K)))
173       (aeval (A.baseChange K) (u.map (algebraMap R K)))
174       (aeval (A.baseChange K) (v.map (algebraMap R K))) (algebraMap R K r) := by
175   apply certificate_of_charpoly _ _ _ _ _ _ hr
176   · simp only [LinearMap.charpoly_baseChange, hchar, Polynomial.map_mul]
177   · have h := congrArg (Polynomial.map (algebraMap R K)) hbez
178     simpa only [Polynomial.map_add, Polynomial.map_mul, Polynomial.map_C] using h
179 
180 theorem mapped_resultant_nonzero (f g : R[X]) (hf : f.Monic) (hg : g.Monic)
181     (hc : IsCoprime (f.map (algebraMap R K)) (g.map (algebraMap R K))) :
182     algebraMap R K (f.resultant g) ≠ 0 := by
183   have h := resultant_nonzero_of_coprime _ _ hc
184   simpa only [hf.natDegree_map, hg.natDegree_map,
185     Polynomial.resultant_map_map] using h
186 
187 /-- The arbitrary chosen integral Bezout identity, with the integral
188 endomorphism constructed before extending scalars. -/
189 theorem integral_bezout_projector [IsDomain R] [IsFractionRing R K]
190     [Module.Free R L] [Module.Finite R L]
191     (A : Module.End R L) (f g u v : R[X]) (r : R) (hr : r ≠ 0)
192     (hchar : A.charpoly = f * g) (hbez : u * f + v * g = C r) :
193     let F := aeval (A.baseChange K) (f.map (algebraMap R K))
194     let G := aeval (A.baseChange K) (g.map (algebraMap R K))
195     let V := aeval (A.baseChange K) (v.map (algebraMap R K))
196     let E := separator (algebraMap R K r) V G
197     E * E = E ∧ LinearMap.range E = LinearMap.ker F ∧
198       LinearMap.ker E = LinearMap.ker G ∧
199       IsCompl (LinearMap.ker F) (LinearMap.ker G) ∧
200       (algebraMap R K r) • E = (aeval A (v * g)).baseChange K ∧
201       ∀ x ∈ tensorLattice (K := K) (R := R) (L := L),
202         ((algebraMap R K r) • E) x ∈ tensorLattice (K := K) (R := R) (L := L) := by
203   have hrK : algebraMap R K r ≠ 0 := by
204     intro h
205     apply hr
206     apply IsFractionRing.injective R K
207     simpa only [map_zero] using h
208   have cert := certificate_of_integral_charpoly A f g u v r hrK hchar hbez
209   refine ⟨separator_idempotent cert, separator_range_eq_first_kernel cert,
210     separator_kernel_eq_second_kernel cert, complementary_kernels cert, ?_, ?_⟩
211   · rw [scalar_mul_separator cert, separatorNumerator, aeval_baseChange,
212       Polynomial.map_mul, map_mul]
213   · intro x hx
214     rw [scalar_mul_separator cert]
215     exact integral_evaluation_preserves_tensorLattice A v _
216       (integral_evaluation_preserves_tensorLattice A g x hx)
217 
218 /-- Integral coefficients give actual lattice preservation after clearing the
219 resultant, on the natural tensor image of the original finite free module. -/
220 theorem integral_resultant_projector [Module.Free R L] [Module.Finite R L]
221     (A : Module.End R L) (f g : R[X]) (hf : f.Monic) (hg : g.Monic)
222     (hc : IsCoprime (f.map (algebraMap R K)) (g.map (algebraMap R K)))
223     (hchar : A.charpoly = f * g) :
224     ∃ u v : R[X], u * f + v * g = C (f.resultant g) ∧
225       let F := aeval (A.baseChange K) (f.map (algebraMap R K))
226       let G := aeval (A.baseChange K) (g.map (algebraMap R K))
227       let U := aeval (A.baseChange K) (u.map (algebraMap R K))
228       let V := aeval (A.baseChange K) (v.map (algebraMap R K))
229       let r := algebraMap R K (f.resultant g)
230       let E := separator r V G
231       EvaluatedBezoutCertificate F G U V r ∧
232       E * E = E ∧ LinearMap.range E = LinearMap.ker F ∧
233       LinearMap.ker E = LinearMap.ker G ∧
234       IsCompl (LinearMap.ker F) (LinearMap.ker G) ∧
235       ∀ x ∈ tensorLattice (K := K) (R := R) (L := L),
236         (r • E) x ∈ tensorLattice (K := K) (R := R) (L := L) := by
237   obtain ⟨u, v, hbez⟩ := exists_resultant_bezout f g hf
238   have cert := certificate_of_integral_charpoly A f g u v (f.resultant g)
239     (mapped_resultant_nonzero f g hf hg hc) hchar hbez
240   refine ⟨u, v, hbez, cert, separator_idempotent cert,
241     separator_range_eq_first_kernel cert, separator_kernel_eq_second_kernel cert,
242     complementary_kernels cert, ?_⟩
243   intro x hx
244   rw [scalar_mul_separator cert]
245   exact integral_evaluation_preserves_tensorLattice A v _
246     (integral_evaluation_preserves_tensorLattice A g x hx)
247 
248 end IntegralBaseChange
249 
250 end Komorebi.PaperII.ReleaseResultantPolynomial

Back to source controls