Library mathcomp.algebra.polyXY

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssrnat seq.
From mathcomp Require Import fintype tuple finfun bigop fingroup perm div.
From mathcomp Require Import ssralg zmodp matrix mxalgebra.
From mathcomp 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 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 }).

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 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.