Library mathcomp.field.separable
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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 satisfies 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.
Canonical separable_poly_unlockable := Unlockable separable_poly.unlock.
Section SeparablePoly.
Variable R : idomainType.
Implicit Types p q d u v : {poly R}.
Local Notation separable := (@separable_poly R).
Local Notation lcn_neq0 := (Pdiv.Idomain.lc_expn_scalp_neq0 _).
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 → ~~ (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 → (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.
Local Notation "p ^ f" := (map_poly f p) : ring_scope.
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 satisfy 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 : bool :=
all2rel (fun u v ⇒ D (u × v) == D u × v + u × D v) (vbasis K).
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)%VS → Derivation E D → Derivation 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%VS → D x = 0.
Lemma Derivation_exp x m : x \in E → D (x ^+ m) = x ^+ m.-1 *+ m × D x.
Lemma Derivation_horner p x :
p \is a polyOver E → x \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 K → separable_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>> D → separable_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_additive_subproof E (adjEx := Fadjoin_poly E x) :
let body y (p := adjEx y) := (map_poly D p).[x] + p^`().[x] × Dx E in
additive body.
Fact extendDerivation_scalable_subproof E (adjEx := Fadjoin_poly E x) :
let body y (p := adjEx y) := (map_poly D p).[x] + p^`().[x] × Dx E in
scalable body.
Section DerivationLinear.
Variable (E : {subfield L}).
Let body (y : L) (p := Fadjoin_poly E x y) : L :=
(map_poly D p).[x] + p^`().[x] × Dx E.
Let extendDerivationLinear := Eval hnf in (body : {linear _ → _}).
Definition extendDerivation : 'End(L) := linfun extendDerivationLinear.
End DerivationLinear.
Hypothesis derD : Derivation K D.
Lemma extendDerivation_id y : y \in K → extendDerivation K y = D y.
Lemma extendDerivation_horner p :
p \is a polyOver K → separable_element K x →
extendDerivation K p.[x] = (map_poly D p).[x] + p^`().[x] × Dx K.
Lemma extendDerivationP :
separable_element K x → Derivation <<K; x>> (extendDerivation K).
End ExtendDerivation.
all2rel (fun u v ⇒ D (u × v) == D u × v + u × D v) (vbasis K).
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)%VS → Derivation E D → Derivation 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%VS → D x = 0.
Lemma Derivation_exp x m : x \in E → D (x ^+ m) = x ^+ m.-1 *+ m × D x.
Lemma Derivation_horner p x :
p \is a polyOver E → x \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 K → separable_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>> D → separable_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_additive_subproof E (adjEx := Fadjoin_poly E x) :
let body y (p := adjEx y) := (map_poly D p).[x] + p^`().[x] × Dx E in
additive body.
Fact extendDerivation_scalable_subproof E (adjEx := Fadjoin_poly E x) :
let body y (p := adjEx y) := (map_poly D p).[x] + p^`().[x] × Dx E in
scalable body.
Section DerivationLinear.
Variable (E : {subfield L}).
Let body (y : L) (p := Fadjoin_poly E x y) : L :=
(map_poly D p).[x] + p^`().[x] × Dx E.
Let extendDerivationLinear := Eval hnf in (body : {linear _ → _}).
Definition extendDerivation : 'End(L) := linfun extendDerivationLinear.
End DerivationLinear.
Hypothesis derD : Derivation K D.
Lemma extendDerivation_id y : y \in K → extendDerivation K y = D y.
Lemma extendDerivation_horner p :
p \is a polyOver K → separable_element K x →
extendDerivation K p.[x] = (map_poly D p).[x] + p^`().[x] × Dx K.
Lemma extendDerivationP :
separable_element K x → Derivation <<K; x>> (extendDerivation K).
End ExtendDerivation.
Reference:
http://www.math.uconn.edu/~kconrad/blurbs/galoistheory/separable2.pdf
Lemma Derivation_separableP :
reflect
(∀ D, Derivation <<K; x>> D → K ≤ lker D → <<K; x>> ≤ lker D)%VS
(separable_element K x).
End SeparableElement.
Arguments separable_elementP {K x}.
Lemma separable_elementS K E x :
(K ≤ E)%VS → separable_element K x → separable_element E x.
Lemma adjoin_separableP {K x} :
reflect (∀ y, y \in <<K; x>>%VS → separable_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 < n → separable_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 K → purely_inseparable_element K x.
Lemma sub_inseparable K E x :
(K ≤ E)%VS → purely_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>> x → separable_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 x → separable_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 x → separable_element K y → separable_element K (x + y).
Lemma separable_sum I r (P : pred I) (v_ : I → L) K :
(∀ i, P i → separable_element K (v_ i)) →
separable_element K (\sum_(i <- r | P i) v_ i).
Lemma inseparable_add K x y :
purely_inseparable_element K x → purely_inseparable_element K y →
purely_inseparable_element K (x + y).
Lemma inseparable_sum I r (P : pred I) (v_ : I → L) K :
(∀ i, P i → purely_inseparable_element K (v_ i)) →
purely_inseparable_element K (\sum_(i <- r | P i) v_ i).
Lemma separableP {K E} :
reflect (∀ y, y \in E → separable_element K y) (separable K E).
Lemma purely_inseparableP {K E} :
reflect (∀ y, y \in E → purely_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 M → separable M E → separable K E.
Lemma separableS K1 K2 E2 E1 :
(K1 ≤ K2)%VS → (E2 ≤ E1)%VS → separable K1 E1 → separable K2 E2.
Lemma separableSl K M E : (K ≤ M)%VS → separable K E → separable M E.
Lemma separableSr K M E : (M ≤ E)%VS → separable K E → separable K M.
Lemma separable_Fadjoin_seq K rs :
all (separable_element K) rs → separable K <<K & rs>>.
Lemma purely_inseparable_refl K : purely_inseparable K K.
Lemma purely_inseparable_trans M K E :
purely_inseparable K M → purely_inseparable M E → purely_inseparable K E.
End Separable.
Arguments separable_elementP {F L K x}.
Arguments separablePn {F L K x}.
Arguments Derivation_separableP {F L K x}.
Arguments adjoin_separableP {F L K x}.
Arguments purely_inseparable_elementP {F L K x}.
Arguments separableP {F L K E}.
Arguments purely_inseparableP {F L K E}.
reflect
(∀ D, Derivation <<K; x>> D → K ≤ lker D → <<K; x>> ≤ lker D)%VS
(separable_element K x).
End SeparableElement.
Arguments separable_elementP {K x}.
Lemma separable_elementS K E x :
(K ≤ E)%VS → separable_element K x → separable_element E x.
Lemma adjoin_separableP {K x} :
reflect (∀ y, y \in <<K; x>>%VS → separable_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 < n → separable_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 K → purely_inseparable_element K x.
Lemma sub_inseparable K E x :
(K ≤ E)%VS → purely_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>> x → separable_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 x → separable_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 x → separable_element K y → separable_element K (x + y).
Lemma separable_sum I r (P : pred I) (v_ : I → L) K :
(∀ i, P i → separable_element K (v_ i)) →
separable_element K (\sum_(i <- r | P i) v_ i).
Lemma inseparable_add K x y :
purely_inseparable_element K x → purely_inseparable_element K y →
purely_inseparable_element K (x + y).
Lemma inseparable_sum I r (P : pred I) (v_ : I → L) K :
(∀ i, P i → purely_inseparable_element K (v_ i)) →
purely_inseparable_element K (\sum_(i <- r | P i) v_ i).
Lemma separableP {K E} :
reflect (∀ y, y \in E → separable_element K y) (separable K E).
Lemma purely_inseparableP {K E} :
reflect (∀ y, y \in E → purely_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 M → separable M E → separable K E.
Lemma separableS K1 K2 E2 E1 :
(K1 ≤ K2)%VS → (E2 ≤ E1)%VS → separable K1 E1 → separable K2 E2.
Lemma separableSl K M E : (K ≤ M)%VS → separable K E → separable M E.
Lemma separableSr K M E : (M ≤ E)%VS → separable K E → separable K M.
Lemma separable_Fadjoin_seq K rs :
all (separable_element K) rs → separable K <<K & rs>>.
Lemma purely_inseparable_refl K : purely_inseparable K K.
Lemma purely_inseparable_trans M K E :
purely_inseparable K M → purely_inseparable M E → purely_inseparable K E.
End Separable.
Arguments separable_elementP {F L K x}.
Arguments separablePn {F L K x}.
Arguments Derivation_separableP {F L K x}.
Arguments adjoin_separableP {F L K x}.
Arguments purely_inseparable_elementP {F L K x}.
Arguments separableP {F L K E}.
Arguments purely_inseparableP {F L K E}.