# Library mathcomp.field.separable

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B.                                  *)

From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import choice fintype tuple finfun bigop finset prime.
From mathcomp Require Import binomial ssralg poly polydiv fingroup perm.
From mathcomp Require Import morphism quotient gproduct finalg zmodp cyclic.
From mathcomp Require Import matrix mxalgebra mxpoly polyXY vector falgebra.
From mathcomp Require Import 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.

Local Open 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^().

Lemma separable_poly_neq0 p : separable p p != 0.

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

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

Lemma separable_coprime p u v : separable p u × v %| p coprimep u v.

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

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

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

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

Lemma eqp_separable p q : p %= q separable 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.

Arguments separable_polyP {R p}.

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

Section InfinitePrimitiveElementTheorem.

Variables (F L : fieldType) (iota : {rmorphism F L}).
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) y separable_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.