Library mathcomp.field.separable
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ 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.
+ +
+ +
+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)).
+ +
+
+
++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.
+ +
+ +
+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.
+
+
+Definition Derivation (s := vbasis K) : bool :=
+ all (fun u ⇒ all (fun v ⇒ D (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)%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_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 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.
+ +
+
+
++ all (fun u ⇒ all (fun v ⇒ D (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)%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_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 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.
+ +
+ +
+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.
+ +
+
++ reflect
+ (∀ D, Derivation <<K; x>> D → K ≤ lker D → <<K; x>> ≤ lker D)%VS
+ (separable_element K x).
+ +
+End SeparableElement.
+ +
+ +
+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.
+ +
+