(Joint Center)Library separable

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import tuple finfun bigop finset prime binomial ssralg poly polydiv.
Require Import fingroup perm morphism quotient gproduct finalg zmodp cyclic.
Require Import matrix mxalgebra mxpoly polyXY vector falgebra fieldext.

This file provides a theory of separable and inseparable field extensions.
separable_poly p <=> p has no multiple roots in any field extension. separable_element K x <=> the minimal polynomial of x over K is separable. separable K E <=> every member of E is separable over K. separable_generator K E == some x \in E that generates the largest subfield K[x] that is separable over K. purely_inseparable_element K x <=> there is a [char L].-nat n such that x ^+ n \in K. purely_inseparable K E <=> every member of E is purely inseparable over K.
Derivations are introduced to prove the adjoin_separableP Lemma: Derivation K D <=> the linear operator D satifies the Leibniz product rule inside K. extendDerivation x D K == given a derivation D on K and a separable element x over K, this function returns the unique extension of D to K(x).

Set Implicit Arguments.

Open Local Scope ring_scope.
Import GRing.Theory.

Section SeparablePoly.

Variable R : idomainType.
Implicit Types p q d u v : {poly R}.

Definition separable_poly p := coprimep p p^`.

Local Notation separable := separable_poly.
Local Notation lcn_neq0 := (Pdiv.Idomain.lc_expn_scalp_neq0 _).

Lemma separable_poly_neq0 p : separable pp != 0.

Lemma poly_square_freeP p :
  ( u v, u × v %| pcoprimep u v)
   ( u, size u != 1%N~~ (u ^+ 2 %| p)).

Lemma separable_polyP {p} :
  reflect [/\ u v, u × v %| pcoprimep u v
            & u, u %| p → 1 < size uu^` != 0]
          (separable p).

Lemma separable_coprime p u v : separable pu × v %| pcoprimep u v.

Lemma separable_nosquare p u k :
  separable p → 1 < ksize u != 1%N(u ^+ k %| p) = false.

Lemma separable_deriv_eq0 p u :
  separable pu %| p → 1 < size u(u^` == 0) = false.

Lemma dvdp_separable p q : q %| pseparable pseparable q.

Lemma separable_mul p q :
  separable (p × q) = [&& separable p, separable q & coprimep p q].

Lemma eqp_separable p q : p %= qseparable p = separable q.

Lemma separable_root p x :
  separable (p × ('X - x%:P)) = separable p && ~~ root p x.

Lemma separable_prod_XsubC (r : seq R) :
  separable (\prod_(x <- r) ('X - x%:P)) = uniq r.

Lemma make_separable p : p != 0 → separable (p %/ gcdp p p^`).

End SeparablePoly.

Implicit Arguments separable_polyP [R p].

Lemma separable_map (F : fieldType) (R : idomainType)
                    (f : {rmorphism FR}) (p : {poly F}) :
  separable_poly (map_poly f p) = separable_poly p.

Section InfinitePrimitiveElementTheorem.

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

Variables (F L : fieldType) (iota : {rmorphism FL}).
Variables (x y : L) (p : {poly F}).
Hypotheses (nz_p : p != 0) (px_0 : root (p ^ iota) x).

Let inFz z w := q, (q ^ iota).[z] = w.

Lemma large_field_PET q :
    root (q ^ iota) yseparable_poly q
  exists2 r, r != 0
  & t (z := iota t × y - x), ~~ root r (iota t) → inFz z x inFz z y.

Lemma char0_PET (q : {poly F}) :
    q != 0 → root (q ^ iota) y[char F] =i pred0
   n, let z := y *+ n - x in inFz z x inFz z y.

End InfinitePrimitiveElementTheorem.

Section Separable.

Variables (F : fieldType) (L : fieldExtType F).
Implicit Types (U V W : {vspace L}) (E K M : {subfield L}) (D : 'End(L)).

Section Derivation.

Variables (K : {vspace L}) (D : 'End(L)).

A deriviation only needs to be additive and satify Lebniz's law, but all the deriviations used here are going to be linear, so we only define the Derivation predicate for linear endomorphisms.
Definition Derivation (s := vbasis K) : bool :=
  all (fun uall (fun vD (u × v) == D u × v + u × D v) s) s.

Hypothesis derD : Derivation.

Lemma Derivation_mul : {in K &, u v, D (u × v) = D u × v + u × D v}.

Lemma Derivation_mul_poly (Dp := map_poly D) :
  {in polyOver K &, p q, Dp (p × q) = Dp p × q + p × Dp q}.

End Derivation.

Lemma DerivationS E K D : (K E)%VSDerivation E DDerivation K D.

Section DerivationAlgebra.

Variables (E : {subfield L}) (D : 'End(L)).
Hypothesis derD : Derivation E D.

Lemma Derivation1 : D 1 = 0.

Lemma Derivation_scalar x : x \in 1%VSD x = 0.

Lemma Derivation_exp x m : x \in ED (x ^+ m) = x ^+ m.-1 *+ m × D x.

Lemma Derivation_horner p x :
    p \is a polyOver Ex \in E
  D p.[x] = (map_poly D p).[x] + p^`.[x] × D x.

End DerivationAlgebra.

Definition separable_element U x := separable_poly (minPoly U x).

Section SeparableElement.

Variables (K : {subfield L}) (x : L).

Lemma separable_elementP :
  reflect ( f, [/\ f \is a polyOver K, root f x & separable_poly f])
          (separable_element K x).

Lemma base_separable : x \in Kseparable_element K x.

Lemma separable_nz_der : separable_element K x = ((minPoly K x)^` != 0).

Lemma separablePn :
  reflect (exists2 p, p \in [char L] &
            exists2 g, g \is a polyOver K & minPoly K x = g \Po 'X^p)
          (~~ separable_element K x).

Lemma separable_root_der : separable_element K x (+) root (minPoly K x)^` x.

Lemma Derivation_separable D :
    Derivation <<K; x>> Dseparable_element K x
  D x = - (map_poly D (minPoly K x)).[x] / (minPoly K x)^`.[x].

Section ExtendDerivation.

Variable D : 'End(L).

Let Dx E := - (map_poly D (minPoly E x)).[x] / ((minPoly E x)^`).[x].

Fact extendDerivation_subproof E (adjEx := Fadjoin_poly E x) :
  let body y (p := adjEx y) := (map_poly D p).[x] + p^`.[x] × Dx E in
  linear body.

Definition extendDerivation E : 'End(L) :=
  linfun (Linear (extendDerivation_subproof E)).

Hypothesis derD : Derivation K D.

Lemma extendDerivation_id y : y \in KextendDerivation K y = D y.

Lemma extendDerivation_horner p :
    p \is a polyOver Kseparable_element K x
  extendDerivation K p.[x] = (map_poly D p).[x] + p^`.[x] × Dx K.

Lemma extendDerivationP :
  separable_element K xDerivation <<K; x>> (extendDerivation K).

End ExtendDerivation.

Reference: http://www.math.uconn.edu/~kconrad/blurbs/galoistheory/separable2.pdf
Lemma Derivation_separableP :
    ( D, Derivation <<K; x>> DK lker D<<K; x>> lker D)%VS
    (separable_element K x).

End SeparableElement.

Implicit Arguments separable_elementP [K x].

Lemma separable_elementS K E x :
  (K E)%VSseparable_element K xseparable_element E x.

Lemma adjoin_separableP {K x} :
  reflect ( y, y \in <<K; x>>%VSseparable_element K y)
          (separable_element K x).

Lemma separable_exponent K x :
   n, [char L].-nat n && separable_element K (x ^+ n).

Lemma charf0_separable K : [char L] =i pred0 x, separable_element K x.

Lemma charf_p_separable K x e p :
  p \in [char L]separable_element K x = (x \in <<K; x ^+ (p ^ e.+1)>>%VS).

Lemma charf_n_separable K x n :
  [char L].-nat n → 1 < nseparable_element K x = (x \in <<K; x ^+ n>>%VS).

Definition purely_inseparable_element U x :=
  x ^+ ex_minn (separable_exponent <<U>> x) \in U.

Lemma purely_inseparable_elementP {K x} :
  reflect (exists2 n, [char L].-nat n & x ^+ n \in K)
          (purely_inseparable_element K x).

Lemma separable_inseparable_element K x :
  separable_element K x && purely_inseparable_element K x = (x \in K).

Lemma base_inseparable K x : x \in Kpurely_inseparable_element K x.

Lemma sub_inseparable K E x :
    (K E)%VSpurely_inseparable_element K x
 purely_inseparable_element E x.

Section PrimitiveElementTheorem.

Variables (K : {subfield L}) (x y : L).

Section FiniteCase.

Variable N : nat.

Let K_is_large := s, [/\ uniq s, {subset s K} & N < size s].

Let cyclic_or_large (z : L) : z != 0 → K_is_large a, z ^+ a.+1 = 1.

Lemma finite_PET : K_is_large z, (<< <<K; y>>; x>> = <<K; z>>)%VS.

End FiniteCase.

Hypothesis sepKy : separable_element K y.

Lemma Primitive_Element_Theorem : z, (<< <<K; y>>; x>> = <<K; z>>)%VS.

Lemma adjoin_separable : separable_element <<K; y>> xseparable_element K x.

End PrimitiveElementTheorem.

Lemma strong_Primitive_Element_Theorem K x y :
    separable_element <<K; x>> y
  exists2 z : L, (<< <<K; y>>; x>> = <<K; z>>)%VS
               & separable_element K xseparable_element K y.

Definition separable U W : bool :=
  all (separable_element U) (vbasis W).

Definition purely_inseparable U W : bool :=
  all (purely_inseparable_element U) (vbasis W).

Lemma separable_add K x y :
  separable_element K xseparable_element K yseparable_element K (x + y).

Lemma separable_sum I r (P : pred I) (v_ : IL) K :
    ( i, P iseparable_element K (v_ i)) →
  separable_element K (\sum_(i <- r | P i) v_ i).

Lemma inseparable_add K x y :
    purely_inseparable_element K xpurely_inseparable_element K y
  purely_inseparable_element K (x + y).

Lemma inseparable_sum I r (P : pred I) (v_ : IL) K :
    ( i, P ipurely_inseparable_element K (v_ i)) →
  purely_inseparable_element K (\sum_(i <- r | P i) v_ i).

Lemma separableP {K E} :
  reflect ( y, y \in Eseparable_element K y) (separable K E).

Lemma purely_inseparableP {K E} :
  reflect ( y, y \in Epurely_inseparable_element K y)
          (purely_inseparable K E).

Lemma adjoin_separable_eq K x : separable_element K x = separable K <<K; x>>%VS.

Lemma separable_inseparable_decomposition E K :
  {x | x \in E separable_element K x & purely_inseparable <<K; x>> E}.

Definition separable_generator K E : L :=
   s2val (locked (separable_inseparable_decomposition E K)).

Lemma separable_generator_mem E K : separable_generator K E \in E.

Lemma separable_generatorP E K : separable_element K (separable_generator K E).

Lemma separable_generator_maximal E K :
  purely_inseparable <<K; separable_generator K E>> E.

Lemma sub_adjoin_separable_generator E K :
  separable K E → (E <<K; separable_generator K E>>)%VS.

Lemma eq_adjoin_separable_generator E K :
    separable K E → (K E)%VS
  E = <<K; separable_generator K E>>%VS :> {vspace _}.

Lemma separable_refl K : separable K K.

Lemma separable_trans M K E : separable K Mseparable M Eseparable K E.

Lemma separableS K1 K2 E2 E1 :
  (K1 K2)%VS → (E2 E1)%VSseparable K1 E1separable K2 E2.

Lemma separableSl K M E : (K M)%VSseparable K Eseparable M E.

Lemma separableSr K M E : (M E)%VSseparable K Eseparable K M.

Lemma separable_Fadjoin_seq K rs :
  all (separable_element K) rsseparable K <<K & rs>>.

Lemma purely_inseparable_refl K : purely_inseparable K K.

Lemma purely_inseparable_trans M K E :
  purely_inseparable K Mpurely_inseparable M Epurely_inseparable K E.

End Separable.

Implicit Arguments separable_elementP [F L K x].
Implicit Arguments separablePn [F L K x].
Implicit Arguments Derivation_separableP [F L K x].
Implicit Arguments adjoin_separableP [F L K x].
Implicit Arguments purely_inseparable_elementP [F L K x].
Implicit Arguments separableP [F L K E].
Implicit Arguments purely_inseparableP [F L K E].