Library mathcomp.algebra.polyXY
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ This file provides additional primitives and theory for bivariate
+ polynomials (polynomials of two variables), represented as polynomials
+ with (univariate) polynomial coefficients :
+ 'Y == the (generic) second variable (:= 'X%:P).
+ p^:P == the bivariate polynomial p['X], for p univariate.
+ := map_poly polyC p (this notation is defined in poly.v).
+ u. [x, y] == the bivariate polynomial u evaluated at 'X = x, 'Y = y.
+ := u. [x%:P]. [y].
+ sizeY u == the size of u in 'Y (1 + the 'Y-degree of u, if u != 0).
+ := \max(i < size u) size u`i.
+ swapXY u == the bivariate polynomial u['Y, 'X], for u bivariate.
+ poly_XaY p == the bivariate polynomial p['X + 'Y], for p univariate.
+ := p^:P \Po ('X + 'Y).
+ poly_XmY p == the bivariate polynomial p['X * 'Y], for p univariate.
+ := P^:P \Po ('X * 'Y).
+ sub_annihilant p q == for univariate p, q != 0, a nonzero polynomial whose
+ roots include all the differences of roots of p and q, in
+ all field extensions (:= resultant (poly_XaY p) q^:P).
+ div_annihilant p q == for polynomials p != 0, q with q. [0] != 0, a nonzero
+ polynomial whose roots include all the quotients of roots
+ of p by roots of q, in all field extensions
+ (:= resultant (poly_XmY p) q^:P).
+ The latter two "annhilants" provide uniform witnesses for an alternative
+ proof of the closure of the algebraicOver predicate (see mxpoly.v). The
+ fact that the annhilant does not depend on the particular choice of roots
+ of p and q is crucial for the proof of the Primitive Element Theorem (file
+ separable.v).
+
+
+
+
+Set Implicit Arguments.
+ +
+Local Open Scope ring_scope.
+Import GRing.Theory.
+ +
+ +
+Notation "'Y" := 'X%:P : ring_scope.
+Notation "p ^:P" := (p ^ polyC) (at level 2, format "p ^:P") : ring_scope.
+Notation "p .[ x , y ]" := (p.[x%:P].[y])
+ (at level 2, left associativity, format "p .[ x , y ]") : ring_scope.
+ +
+Section PolyXY_Ring.
+ +
+Variable R : ringType.
+Implicit Types (u : {poly {poly R}}) (p q : {poly R}) (x : R).
+ +
+Fact swapXY_key : unit.
+Definition swapXY_def u : {poly {poly R}} := (u ^ map_poly polyC).['Y].
+Definition swapXY := locked_with swapXY_key swapXY_def.
+Canonical swapXY_unlockable := [unlockable fun swapXY].
+ +
+Definition sizeY u : nat := \max_(i < size u) (size u`_i).
+Definition poly_XaY p : {poly {poly R}} := p^:P \Po ('X + 'Y).
+Definition poly_XmY p : {poly {poly R}} := p^:P \Po ('X × 'Y).
+Definition sub_annihilant p q := resultant (poly_XaY p) q^:P.
+Definition div_annihilant p q := resultant (poly_XmY p) q^:P.
+ +
+Lemma swapXY_polyC p : swapXY p%:P = p^:P.
+ +
+Lemma swapXY_X : swapXY 'X = 'Y.
+ +
+Lemma swapXY_Y : swapXY 'Y = 'X.
+ +
+Lemma swapXY_is_additive : additive swapXY.
+ Canonical swapXY_addf := Additive swapXY_is_additive.
+ +
+Lemma coef_swapXY u i j : (swapXY u)`_i`_j = u`_j`_i.
+ +
+Lemma swapXYK : involutive swapXY.
+ +
+Lemma swapXY_map_polyC p : swapXY p^:P = p%:P.
+ +
+Lemma swapXY_eq0 u : (swapXY u == 0) = (u == 0).
+ +
+Lemma swapXY_is_multiplicative : multiplicative swapXY.
+Canonical swapXY_rmorphism := AddRMorphism swapXY_is_multiplicative.
+ +
+Lemma swapXY_is_scalable : scalable_for (map_poly polyC \; *%R) swapXY.
+ Canonical swapXY_linear := AddLinear swapXY_is_scalable.
+Canonical swapXY_lrmorphism := [lrmorphism of swapXY].
+ +
+Lemma swapXY_comp_poly p u : swapXY (p^:P \Po u) = p^:P \Po swapXY u.
+ +
+Lemma max_size_coefXY u i : size u`_i ≤ sizeY u.
+ +
+Lemma max_size_lead_coefXY u : size (lead_coef u) ≤ sizeY u.
+ +
+Lemma max_size_evalX u : size u.['X] ≤ sizeY u + (size u).-1.
+ +
+Lemma max_size_evalC u x : size u.[x%:P] ≤ sizeY u.
+ +
+Lemma sizeYE u : sizeY u = size (swapXY u).
+ +
+Lemma sizeY_eq0 u : (sizeY u == 0%N) = (u == 0).
+ +
+Lemma sizeY_mulX u : sizeY (u × 'X) = sizeY u.
+ +
+Lemma swapXY_poly_XaY p : swapXY (poly_XaY p) = poly_XaY p.
+ +
+Lemma swapXY_poly_XmY p : swapXY (poly_XmY p) = poly_XmY p.
+ +
+Lemma poly_XaY0 : poly_XaY 0 = 0.
+ +
+Lemma poly_XmY0 : poly_XmY 0 = 0.
+ +
+End PolyXY_Ring.
+ +
+ +
+Lemma swapXY_map (R S : ringType) (f : {additive R → S}) u :
+ swapXY (u ^ map_poly f) = swapXY u ^ map_poly f.
+ +
+Section PolyXY_ComRing.
+ +
+Variable R : comRingType.
+Implicit Types (u : {poly {poly R}}) (p : {poly R}) (x y : R).
+ +
+Lemma horner_swapXY u x : (swapXY u).[x%:P] = u ^ eval x.
+ +
+Lemma horner_polyC u x : u.[x%:P] = swapXY u ^ eval x.
+ +
+Lemma horner2_swapXY u x y : (swapXY u).[x, y] = u.[y, x].
+ +
+Lemma horner_poly_XaY p v : (poly_XaY p).[v] = p \Po (v + 'X).
+ +
+Lemma horner_poly_XmY p v : (poly_XmY p).[v] = p \Po (v × 'X).
+ +
+End PolyXY_ComRing.
+ +
+Section PolyXY_Idomain.
+ +
+Variable R : idomainType.
+Implicit Types (p q : {poly R}) (x y : R).
+ +
+Lemma size_poly_XaY p : size (poly_XaY p) = size p.
+ +
+Lemma poly_XaY_eq0 p : (poly_XaY p == 0) = (p == 0).
+ +
+Lemma size_poly_XmY p : size (poly_XmY p) = size p.
+ +
+Lemma poly_XmY_eq0 p : (poly_XmY p == 0) = (p == 0).
+ +
+Lemma lead_coef_poly_XaY p : lead_coef (poly_XaY p) = (lead_coef p)%:P.
+ +
+Lemma sub_annihilant_in_ideal p q :
+ 1 < size p → 1 < size q →
+ {uv : {poly {poly R}} × {poly {poly R}}
+ | size uv.1 < size q ∧ size uv.2 < size p
+ & ∀ x y,
+ (sub_annihilant p q).[y] = uv.1.[x, y] × p.[x + y] + uv.2.[x, y] × q.[x]}.
+ +
+Lemma sub_annihilantP p q x y :
+ p != 0 → q != 0 → p.[x] = 0 → q.[y] = 0 →
+ (sub_annihilant p q).[x - y] = 0.
+ +
+Lemma sub_annihilant_neq0 p q : p != 0 → q != 0 → sub_annihilant p q != 0.
+ +
+Lemma div_annihilant_in_ideal p q :
+ 1 < size p → 1 < size q →
+ {uv : {poly {poly R}} × {poly {poly R}}
+ | size uv.1 < size q ∧ size uv.2 < size p
+ & ∀ x y,
+ (div_annihilant p q).[y] = uv.1.[x, y] × p.[x × y] + uv.2.[x, y] × q.[x]}.
+ +
+Lemma div_annihilant_neq0 p q : p != 0 → q.[0] != 0 → div_annihilant p q != 0.
+ +
+End PolyXY_Idomain.
+ +
+Section PolyXY_Field.
+ +
+Variables (F E : fieldType) (FtoE : {rmorphism F → E}).
+ +
+ +
+Lemma div_annihilantP (p q : {poly E}) (x y : E) :
+ p != 0 → q != 0 → y != 0 → p.[x] = 0 → q.[y] = 0 →
+ (div_annihilant p q).[x / y] = 0.
+ +
+Lemma map_sub_annihilantP (p q : {poly F}) (x y : E) :
+ p != 0 → q != 0 →(p ^ FtoE).[x] = 0 → (q ^ FtoE).[y] = 0 →
+ (sub_annihilant p q ^ FtoE).[x - y] = 0.
+ +
+Lemma map_div_annihilantP (p q : {poly F}) (x y : E) :
+ p != 0 → q != 0 → y != 0 → (p ^ FtoE).[x] = 0 → (q ^ FtoE).[y] = 0 →
+ (div_annihilant p q ^ FtoE).[x / y] = 0.
+ +
+Lemma root_annihilant x p (pEx := (p ^ pFtoE).[x%:P]) :
+ pEx != 0 → algebraicOver FtoE x →
+ exists2 r : {poly F}, r != 0 & ∀ y, root pEx y → root (r ^ FtoE) y.
+ +
+Lemma algebraic_root_polyXY x y :
+ (let pEx p := (p ^ map_poly FtoE).[x%:P] in
+ exists2 p, pEx p != 0 & root (pEx p) y) →
+ algebraicOver FtoE x → algebraicOver FtoE y.
+ +
+End PolyXY_Field.
+
++Set Implicit Arguments.
+ +
+Local Open Scope ring_scope.
+Import GRing.Theory.
+ +
+ +
+Notation "'Y" := 'X%:P : ring_scope.
+Notation "p ^:P" := (p ^ polyC) (at level 2, format "p ^:P") : ring_scope.
+Notation "p .[ x , y ]" := (p.[x%:P].[y])
+ (at level 2, left associativity, format "p .[ x , y ]") : ring_scope.
+ +
+Section PolyXY_Ring.
+ +
+Variable R : ringType.
+Implicit Types (u : {poly {poly R}}) (p q : {poly R}) (x : R).
+ +
+Fact swapXY_key : unit.
+Definition swapXY_def u : {poly {poly R}} := (u ^ map_poly polyC).['Y].
+Definition swapXY := locked_with swapXY_key swapXY_def.
+Canonical swapXY_unlockable := [unlockable fun swapXY].
+ +
+Definition sizeY u : nat := \max_(i < size u) (size u`_i).
+Definition poly_XaY p : {poly {poly R}} := p^:P \Po ('X + 'Y).
+Definition poly_XmY p : {poly {poly R}} := p^:P \Po ('X × 'Y).
+Definition sub_annihilant p q := resultant (poly_XaY p) q^:P.
+Definition div_annihilant p q := resultant (poly_XmY p) q^:P.
+ +
+Lemma swapXY_polyC p : swapXY p%:P = p^:P.
+ +
+Lemma swapXY_X : swapXY 'X = 'Y.
+ +
+Lemma swapXY_Y : swapXY 'Y = 'X.
+ +
+Lemma swapXY_is_additive : additive swapXY.
+ Canonical swapXY_addf := Additive swapXY_is_additive.
+ +
+Lemma coef_swapXY u i j : (swapXY u)`_i`_j = u`_j`_i.
+ +
+Lemma swapXYK : involutive swapXY.
+ +
+Lemma swapXY_map_polyC p : swapXY p^:P = p%:P.
+ +
+Lemma swapXY_eq0 u : (swapXY u == 0) = (u == 0).
+ +
+Lemma swapXY_is_multiplicative : multiplicative swapXY.
+Canonical swapXY_rmorphism := AddRMorphism swapXY_is_multiplicative.
+ +
+Lemma swapXY_is_scalable : scalable_for (map_poly polyC \; *%R) swapXY.
+ Canonical swapXY_linear := AddLinear swapXY_is_scalable.
+Canonical swapXY_lrmorphism := [lrmorphism of swapXY].
+ +
+Lemma swapXY_comp_poly p u : swapXY (p^:P \Po u) = p^:P \Po swapXY u.
+ +
+Lemma max_size_coefXY u i : size u`_i ≤ sizeY u.
+ +
+Lemma max_size_lead_coefXY u : size (lead_coef u) ≤ sizeY u.
+ +
+Lemma max_size_evalX u : size u.['X] ≤ sizeY u + (size u).-1.
+ +
+Lemma max_size_evalC u x : size u.[x%:P] ≤ sizeY u.
+ +
+Lemma sizeYE u : sizeY u = size (swapXY u).
+ +
+Lemma sizeY_eq0 u : (sizeY u == 0%N) = (u == 0).
+ +
+Lemma sizeY_mulX u : sizeY (u × 'X) = sizeY u.
+ +
+Lemma swapXY_poly_XaY p : swapXY (poly_XaY p) = poly_XaY p.
+ +
+Lemma swapXY_poly_XmY p : swapXY (poly_XmY p) = poly_XmY p.
+ +
+Lemma poly_XaY0 : poly_XaY 0 = 0.
+ +
+Lemma poly_XmY0 : poly_XmY 0 = 0.
+ +
+End PolyXY_Ring.
+ +
+ +
+Lemma swapXY_map (R S : ringType) (f : {additive R → S}) u :
+ swapXY (u ^ map_poly f) = swapXY u ^ map_poly f.
+ +
+Section PolyXY_ComRing.
+ +
+Variable R : comRingType.
+Implicit Types (u : {poly {poly R}}) (p : {poly R}) (x y : R).
+ +
+Lemma horner_swapXY u x : (swapXY u).[x%:P] = u ^ eval x.
+ +
+Lemma horner_polyC u x : u.[x%:P] = swapXY u ^ eval x.
+ +
+Lemma horner2_swapXY u x y : (swapXY u).[x, y] = u.[y, x].
+ +
+Lemma horner_poly_XaY p v : (poly_XaY p).[v] = p \Po (v + 'X).
+ +
+Lemma horner_poly_XmY p v : (poly_XmY p).[v] = p \Po (v × 'X).
+ +
+End PolyXY_ComRing.
+ +
+Section PolyXY_Idomain.
+ +
+Variable R : idomainType.
+Implicit Types (p q : {poly R}) (x y : R).
+ +
+Lemma size_poly_XaY p : size (poly_XaY p) = size p.
+ +
+Lemma poly_XaY_eq0 p : (poly_XaY p == 0) = (p == 0).
+ +
+Lemma size_poly_XmY p : size (poly_XmY p) = size p.
+ +
+Lemma poly_XmY_eq0 p : (poly_XmY p == 0) = (p == 0).
+ +
+Lemma lead_coef_poly_XaY p : lead_coef (poly_XaY p) = (lead_coef p)%:P.
+ +
+Lemma sub_annihilant_in_ideal p q :
+ 1 < size p → 1 < size q →
+ {uv : {poly {poly R}} × {poly {poly R}}
+ | size uv.1 < size q ∧ size uv.2 < size p
+ & ∀ x y,
+ (sub_annihilant p q).[y] = uv.1.[x, y] × p.[x + y] + uv.2.[x, y] × q.[x]}.
+ +
+Lemma sub_annihilantP p q x y :
+ p != 0 → q != 0 → p.[x] = 0 → q.[y] = 0 →
+ (sub_annihilant p q).[x - y] = 0.
+ +
+Lemma sub_annihilant_neq0 p q : p != 0 → q != 0 → sub_annihilant p q != 0.
+ +
+Lemma div_annihilant_in_ideal p q :
+ 1 < size p → 1 < size q →
+ {uv : {poly {poly R}} × {poly {poly R}}
+ | size uv.1 < size q ∧ size uv.2 < size p
+ & ∀ x y,
+ (div_annihilant p q).[y] = uv.1.[x, y] × p.[x × y] + uv.2.[x, y] × q.[x]}.
+ +
+Lemma div_annihilant_neq0 p q : p != 0 → q.[0] != 0 → div_annihilant p q != 0.
+ +
+End PolyXY_Idomain.
+ +
+Section PolyXY_Field.
+ +
+Variables (F E : fieldType) (FtoE : {rmorphism F → E}).
+ +
+ +
+Lemma div_annihilantP (p q : {poly E}) (x y : E) :
+ p != 0 → q != 0 → y != 0 → p.[x] = 0 → q.[y] = 0 →
+ (div_annihilant p q).[x / y] = 0.
+ +
+Lemma map_sub_annihilantP (p q : {poly F}) (x y : E) :
+ p != 0 → q != 0 →(p ^ FtoE).[x] = 0 → (q ^ FtoE).[y] = 0 →
+ (sub_annihilant p q ^ FtoE).[x - y] = 0.
+ +
+Lemma map_div_annihilantP (p q : {poly F}) (x y : E) :
+ p != 0 → q != 0 → y != 0 → (p ^ FtoE).[x] = 0 → (q ^ FtoE).[y] = 0 →
+ (div_annihilant p q ^ FtoE).[x / y] = 0.
+ +
+Lemma root_annihilant x p (pEx := (p ^ pFtoE).[x%:P]) :
+ pEx != 0 → algebraicOver FtoE x →
+ exists2 r : {poly F}, r != 0 & ∀ y, root pEx y → root (r ^ FtoE) y.
+ +
+Lemma algebraic_root_polyXY x y :
+ (let pEx p := (p ^ map_poly FtoE).[x%:P] in
+ exists2 p, pEx p != 0 & root (pEx p) y) →
+ algebraicOver FtoE x → algebraicOver FtoE y.
+ +
+End PolyXY_Field.
+