(Joint Center)Library MathComp.polyXY

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool choice eqtype ssrnat seq div fintype.
Require Import tuple finfun bigop fingroup perm ssralg zmodp matrix mxalgebra.
Require Import poly polydiv mxpoly binomial.

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.

Local Notation "p ^ f" := (map_poly f p) : ring_scope.
Local Notation eval := horner_eval.

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 RS}) 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 FE}).

Local Notation pFtoE := (map_poly (GRing.RMorphism.apply FtoE)).

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 yroot (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 xalgebraicOver FtoE y.

End PolyXY_Field.