Library mathcomp.field.fieldext

(* (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 ssrfun ssrbool eqtype ssrnat seq div.
From mathcomp Require Import choice fintype tuple finfun bigop ssralg countalg.
From mathcomp Require Import finalg zmodp matrix vector falgebra poly polydiv.
From mathcomp Require Import mxpoly generic_quotient.

Finite dimensional field extentions

fieldExtType F == the interface type for finite field extensions of F it simply combines the fieldType and FalgType F interfaces. [fieldExtType F of L] == a fieldExt F structure for a type L that has both FalgType F and fieldType canonical instances. The field class instance must be manifest with explicit comRing, idomain, and field mixins. If L has an abstract field class should use the 'for' variant. [fieldExtType F of L for K] == a fieldExtType F structure for a type L that has an FalgType F canonical structure, given a K : fieldType whose unitRingType projection coincides with the canonical unitRingType for F. {subfield L} == the type of subfields of L that are also extensions of F; since we are in a finite dimensional setting these are exactly the F-subalgebras of L, and indeed {subfield L} is just display notation for {aspace L} when L is an extFieldType. > All aspace operations apply to {subfield L}, but there are several additional lemmas and canonical instances specific to {subfield L} spaces, e.g., subvs_of E is an extFieldType F when E : {subfield L}. > Also note that not all constructive subfields have type {subfield E} in the same way that not all constructive subspaces have type {vspace E}. These types only include the so called "detachable" subspaces (and subalgebras).
(E :&: F)%AS, (E * F)%AS == the intersection and product (meet and join) of E and F as subfields. subFExtend iota z p == Given a field morphism iota : F -> L, this is a type for the field F^iota(z) obtained by adjoining z to the image of F in L under iota. The construction requires a non-zero polynomial p in F such that z is a root of p^iota; it returns the field F^iota if this is not so. However, p need not be irredicible. subfx_inj x == The injection of F^iota(z) into L. inj_subfx iota z p x == The injection of F into F^iota(z). subfx_eval iota z p q == Given q : {poly F} returns q. [z] as a value of type F^iota(z). subfx_root iota z p == The generator of F^iota(z) over F. SubFieldExtType pz0 irr_p == A fieldExtType F structure for F^iota(z) (more precisely, subFExtend iota z p), given proofs pz0: root (map_poly iota p) z and irr_p : irreducible_poly p. The corresponding vectType substructure (SubfxVectType pz0 irr_p) has dimension (size p).-1 over F. minPoly K x == the monic minimal polynomial of x over the subfield K. adjoin_degree K x == the degree of the minimial polynomial or the dimension of K(x)/K. Fadjoin_poly K x y == a polynomial p over K such that y = p. [x].
fieldOver F == L, but with an extFieldType (subvs_of F) structure, for F : {subfield L} vspaceOver F V == the smallest subspace of fieldOver F containing V; this coincides with V if V is an F-module. baseFieldType L == L, but with an extFieldType F0 structure, when L has a canonical extFieldType F structure and F in turn has an extFieldType F0 structure. baseVspace V == the subspace of baseFieldType L that coincides with V : {vspace L}. > Some caution must be exercised when using fieldOver and baseFieldType, because these are convertible to L while carrying different Lmodule structures. This means that the safeguards engineered in the ssralg library that normally curb the Coq kernel's inclination to diverge are no longer effectcive, so additional precautions should be taken when matching or rewriting terms of the form a *: u, because Coq may take forever to realize it's dealing with a *: in the wrong structure. The baseField_scaleE and fieldOver_scaleE lemmas should be used to expand or fold such "trans-structure" operations explicitly beforehand.

Set Implicit Arguments.

Local Open Scope ring_scope.
Import GRing.Theory.

#[infer(R), short(type="fieldExtType")]
HB.structure Definition FieldExt (R : ringType) := {T of Falgebra R T &
  GRing.Ring_hasCommutativeMul T & GRing.Field T}.

Module FieldExtExports.
Bind Scope ring_scope with FieldExt.sort.
Notation "[ 'fieldExtType' F 'of' L ]" := (FieldExt.clone F L%type _)
  (at level 0, format "[ 'fieldExtType' F 'of' L ]") : form_scope.
Notation "[ 'fieldExtType' F 'of' L 'for' K ]" := (FieldExt.clone F L%type K)
  (at level 0, format "[ 'fieldExtType' F 'of' L 'for' K ]") : form_scope.
Notation "{ 'subfield' L }" := (@aspace_of _ _ (Phant L))
  (* NB: was (@aspace_of _ (FalgType _) (Phant L)) *)
  (at level 0, format "{ 'subfield' L }") : type_scope.
End FieldExtExports.

FIXME: strange way to build a FieldExt

Section FieldExtTheory.

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

Lemma dim_cosetv U x : x != 0 → \dim (U × <[x]>) = \dim U.

Lemma prodvC : commutative (@prodv F0 L).

Lemma prodvCA : left_commutative (@prodv F0 L).

Lemma prodvAC : right_commutative (@prodv F0 L).

Lemma algid1 K : algid K = 1.

Lemma mem1v K : 1 \in K.
Lemma sub1v K : (1 ≤ K)%VS.

Lemma subfield_closed K : agenv K = K.

Lemma AHom_lker0 (rT : FalgType F0) (f : 'AHom(L, rT)) : lker f == 0%VS.

Lemma AEnd_lker0 (f : 'AEnd(L)) : lker f == 0%VS.

Fact aimg_is_aspace (rT : FalgType F0) (f : 'AHom(L, rT)) (E : {subfield L}) :
  is_aspace (f @: E).
Canonical aimg_aspace rT f E := ASpace (@aimg_is_aspace rT f E).

Lemma Fadjoin_idP {K x} : reflect (<<K; x>>%VS = K) (x \in K).

Lemma Fadjoin0 K : <<K; 0>>%VS = K.

Lemma Fadjoin_nil K : <<K & [::]>>%VS = K.

Lemma FadjoinP {K x E} :
  reflect (K ≤ E ∧ x \in E)%VS (<<K; x>>%AS ≤ E)%VS.

Lemma Fadjoin_seqP {K} {rs : seq L} {E} :
  reflect (K ≤ E ∧ {subset rs ≤ E})%VS (<<K & rs>> ≤ E)%VS.

Lemma alg_polyOver E p : map_poly (in_alg L) p \is a polyOver E.

Lemma sub_adjoin1v x E : (<<1; x>> ≤ E)%VS = (x \in E)%VS.

Fact vsval_multiplicative K : multiplicative (vsval : subvs_of K → L).

Lemma vsval_invf K (w : subvs_of K) : val w^-1 = (vsval w)^-1.

Fact aspace_divr_closed K : divr_closed K.

Note that the ringType structure was built in the SubFalgType section of falgebra.v but the SubRing structure did not stand there, it is thus built only here


Lemma subvs_fieldMixin K : GRing.field_axiom [the idomainType of subvs_of K].

Lemma polyOver_subvs {K} {p : {poly L}} :
  reflect (∃ q : {poly subvs_of K}, p = map_poly vsval q)
          (p \is a polyOver K).

Lemma divp_polyOver K : {in polyOver K &, ∀ p q, p %/ q \is a polyOver K}.

Lemma modp_polyOver K : {in polyOver K &, ∀ p q, p %% q \is a polyOver K}.

Lemma gcdp_polyOver K :
  {in polyOver K &, ∀ p q, gcdp p q \is a polyOver K}.

Fact prodv_is_aspace E F : is_aspace (E × F).
Canonical prodv_aspace E F : {subfield L} := ASpace (prodv_is_aspace E F).

Fact field_mem_algid E F : algid E \in F.
Canonical capv_aspace E F : {subfield L} := aspace_cap (field_mem_algid E F).

Lemma polyOverSv U V : (U ≤ V)%VS → {subset polyOver U ≤ polyOver V}.

Lemma field_subvMl F U : (U ≤ F × U)%VS.

Lemma field_subvMr U F : (U ≤ U × F)%VS.

Lemma field_module_eq F M : (F × M ≤ M)%VS → (F × M)%VS = M.

Lemma sup_field_module F E : (F × E ≤ E)%VS = (F ≤ E)%VS.

Lemma field_module_dimS F M : (F × M ≤ M)%VS → (\dim F %| \dim M)%N.

Lemma field_dimS F E : (F ≤ E)%VS → (\dim F %| \dim E)%N.

Lemma dim_field_module F M : (F × M ≤ M)%VS → \dim M = (\dim_F M × \dim F)%N.

Lemma dim_sup_field F E : (F ≤ E)%VS → \dim E = (\dim_F E × \dim F)%N.

Lemma field_module_semisimple F M (m := \dim_F M) :
    (F × M ≤ M)%VS →
  {X : m.-tuple L | {subset X ≤ M} ∧ 0 \notin X
     & let FX := (\sum_(i < m) F × <[X`_i]>)%VS in FX = M ∧ directv FX}.

Section FadjoinPolyDefinitions.

Variables (U : {vspace L}) (x : L).

Definition adjoin_degree := (\dim_U <<U; x>>).-1.+1.

Definition Fadjoin_sum := (\sum_(i < n) U × <[x ^+ i]>)%VS.

Definition Fadjoin_poly v : {poly L} :=
  \poly_(i < n) (sumv_pi Fadjoin_sum (inord i) v / x ^+ i).

Definition minPoly : {poly L} := 'X^n - Fadjoin_poly (x ^+ n).

Lemma size_Fadjoin_poly v : size (Fadjoin_poly v) ≤ n.

Lemma Fadjoin_polyOver v : Fadjoin_poly v \is a polyOver U.

Fact Fadjoin_poly_is_linear : linear_for (in_alg L \; *:%R) Fadjoin_poly.

Lemma size_minPoly : size minPoly = n.+1.

Lemma monic_minPoly : minPoly \is monic.

End FadjoinPolyDefinitions.

Section FadjoinPoly.

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

Lemma adjoin_degreeE : n = \dim_K <<K; x>>.

Lemma dim_Fadjoin : \dim <<K; x>> = (n × \dim K)%N.

Lemma adjoin0_deg : adjoin_degree K 0 = 1%N.

Lemma adjoin_deg_eq1 : (n == 1%N) = (x \in K).

Lemma Fadjoin_sum_direct : directv sumKx.

Let nz_x_i (i : 'I_n) : x ^+ i != 0.

Lemma Fadjoin_eq_sum : <<K; x>>%VS = sumKx.

Lemma Fadjoin_poly_eq v : v \in <<K; x>>%VS → (Fadjoin_poly K x v).[x] = v.

Lemma mempx_Fadjoin p : p \is a polyOver K → p.[x] \in <<K; x>>%VS.

Lemma Fadjoin_polyP {v} :
  reflect (exists2 p, p \in polyOver K & v = p.[x]) (v \in <<K; x>>%VS).

Lemma Fadjoin_poly_unique p v :
  p \is a polyOver K → size p ≤ n → p.[x] = v → Fadjoin_poly K x v = p.

Lemma Fadjoin_polyC v : v \in K → Fadjoin_poly K x v = v%:P.

Lemma Fadjoin_polyX : x \notin K → Fadjoin_poly K x x = 'X.

Lemma minPolyOver : minPoly K x \is a polyOver K.

Lemma minPolyxx : (minPoly K x).[x] = 0.

Lemma root_minPoly : root (minPoly K x) x.

Lemma Fadjoin_poly_mod p :
  p \is a polyOver K → Fadjoin_poly K x p.[x] = p %% minPoly K x.

Lemma minPoly_XsubC : reflect (minPoly K x = 'X - x%:P) (x \in K).

Lemma root_small_adjoin_poly p :
  p \is a polyOver K → size p ≤ n → root p x = (p == 0).

Lemma minPoly_irr p :
  p \is a polyOver K → p %| minPoly K x → (p %= minPoly K x) || (p %= 1).

Lemma minPoly_dvdp p : p \is a polyOver K → root p x → (minPoly K x) %| p.

End FadjoinPoly.

Lemma minPolyS K E a : (K ≤ E)%VS → minPoly E a %| minPoly K a.

Arguments Fadjoin_polyP {K x v}.
Lemma Fadjoin1_polyP x v :
  reflect (∃ p, v = (map_poly (in_alg L) p).[x]) (v \in <<1; x>>%VS).

Section Horner.

Variables z : L.

Definition fieldExt_horner := horner_morph (fun x ⇒ mulrC z (in_alg L x)).
Lemma fieldExt_hornerC b : fieldExt_horner b%:P = b%:A.
Lemma fieldExt_hornerX : fieldExt_horner 'X = z.
Fact fieldExt_hornerZ : scalable fieldExt_horner.

End Horner.

End FieldExtTheory.

Notation "E :&: F" := (capv_aspace E F) : aspace_scope.
Notation "'C_ E [ x ]" := (capv_aspace E 'C[x]) : aspace_scope.
Notation "'C_ ( E ) [ x ]" := (capv_aspace E 'C[x])
  (only parsing) : aspace_scope.
Notation "'C_ E ( V )" := (capv_aspace E 'C(V)) : aspace_scope.
Notation "'C_ ( E ) ( V )" := (capv_aspace E 'C(V))
  (only parsing) : aspace_scope.
Notation "E * F" := (prodv_aspace E F) : aspace_scope.
Notation "f @: E" := (aimg_aspace f E) : aspace_scope.

Arguments Fadjoin_idP {F0 L K x}.
Arguments FadjoinP {F0 L K x E}.
Arguments Fadjoin_seqP {F0 L K rs E}.
Arguments polyOver_subvs {F0 L K p}.
Arguments Fadjoin_polyP {F0 L K x v}.
Arguments Fadjoin1_polyP {F0 L x v}.
Arguments minPoly_XsubC {F0 L K x}.

Section MapMinPoly.

Variables (F0 : fieldType) (L rL : fieldExtType F0) (f : 'AHom(L, rL)).
Variables (K : {subfield L}) (x : L).

Lemma adjoin_degree_aimg : adjoin_degree (f @: K) (f x) = adjoin_degree K x.

Lemma map_minPoly : map_poly f (minPoly K x) = minPoly (f @: K) (f x).

End MapMinPoly.

Changing up the reference field of a fieldExtType.
Section FieldOver.

Variables (F0 : fieldType) (L : fieldExtType F0) (F : {subfield L}).

Definition fieldOver of {vspace L} : Type := L.


Definition fieldOver_scale (a : K_F) (u : L_F) : L_F := vsval a × u.

Fact fieldOver_scaleA a b u : a ×F: (b ×F: u) = (a × b) ×F: u.

Fact fieldOver_scale1 u : 1 ×F: u = u.

Fact fieldOver_scaleDr a u v : a ×F: (u + v) = a ×F: u + a ×F: v.

Fact fieldOver_scaleDl v a b : (a + b) ×F: v = a ×F: v + b ×F: v.


Lemma fieldOver_scaleE a (u : L) : a *: (u : L_F) = vsval a × u.

Fact fieldOver_scaleAl a u v : a ×F: (u × v) = (a ×F: u) × v.


Fact fieldOver_scaleAr a u v : a ×F: (u × v) = u × (a ×F: v).


Fact fieldOver_vectMixin : Lmodule_hasFinDim [the ringType of K_F] L_F.


Implicit Types (V : {vspace L}) (E : {subfield L}).

Lemma trivial_fieldOver : (1%VS : {vspace L_F}) =i F.

Definition vspaceOver V := <<vbasis V : seq L_F>>%VS.

Lemma mem_vspaceOver V : vspaceOver V =i (F × V)%VS.

Lemma mem_aspaceOver E : (F ≤ E)%VS → vspaceOver E =i E.

Fact aspaceOver_suproof E : is_aspace (vspaceOver E).
Canonical aspaceOver E := ASpace (aspaceOver_suproof E).

Lemma dim_vspaceOver M : (F × M ≤ M)%VS → \dim (vspaceOver M) = \dim_F M.

Lemma dim_aspaceOver E : (F ≤ E)%VS → \dim (vspaceOver E) = \dim_F E.

Lemma vspaceOverP V_F :
  {V | [/\ V_F = vspaceOver V, (F × V ≤ V)%VS & V_F =i V]}.

Lemma aspaceOverP (E_F : {subfield L_F}) :
  {E | [/\ E_F = aspaceOver E, (F ≤ E)%VS & E_F =i E]}.

End FieldOver.

Changing the reference field to a smaller field.
Section BaseField.

Variables (F0 : fieldType) (F : fieldExtType F0) (L : fieldExtType F).

Definition baseField_type of phant L : Type := L.
Notation L0 := (baseField_type (Phant (FieldExt.sort L))).


Definition baseField_scale (a : F0) (u : L0) : L0 := in_alg F a *: u.

Fact baseField_scaleA a b u : a ×F0: (b ×F0: u) = (a × b) ×F0: u.

Fact baseField_scale1 u : 1 ×F0: u = u.

Fact baseField_scaleDr a u v : a ×F0: (u + v) = a ×F0: u + a ×F0: v.

Fact baseField_scaleDl v a b : (a + b) ×F0: v = a ×F0: v + b ×F0: v.


Lemma baseField_scaleE a (u : L) : a *: (u : L0) = a%:A *: u.

Fact baseField_scaleAl a (u v : L0) : a ×F0: (u × v) = (a ×F0: u) × v.


Fact baseField_scaleAr a u v : a ×F0: (u × v) = u × (a ×F0: v).


Let n := \dim {:F}.
Let bF : n.-tuple F := vbasis {:F}.
Let coordF (x : F) := (coord_vbasis (memvf x)).

Fact baseField_vectMixin : Lmodule_hasFinDim [the fieldType of F0] L0.


Let F0ZEZ a x v : a *: ((x *: v : L) : L0) = (a *: x) *: v.

Let baseVspace_basis V : seq L0 :=
  [seq tnth bF ij.2 *: tnth (vbasis V) ij.1 | ij : 'I_(\dim V) × 'I_n].
Definition baseVspace V := <<baseVspace_basis V>>%VS.

Lemma mem_baseVspace V : baseVspace V =i V.

Lemma dim_baseVspace V : \dim (baseVspace V) = (\dim V × n)%N.

Fact baseAspace_suproof (E : {subfield L}) : is_aspace (baseVspace E).
Canonical baseAspace E := ASpace (baseAspace_suproof E).

End BaseField.

Notation baseFieldType L := (baseField_type (Phant L)).

Canonical refBaseField_unlockable := Unlockable refBaseField.unlock.

Section RefBaseField.

Variables (F0 : fieldType) (F : fieldExtType F0) (L : fieldExtType F).

Notation F1 := (refBaseField L).
Notation F1unlock := refBaseField.unlock.
Notation L0 := (baseFieldType L).

Let n := \dim {:F}.
Let bF : n.-tuple F := vbasis {:F}.
Let coordF (x : F) := (coord_vbasis (memvf x)).

Lemma dim_refBaseField : \dim F1 = n.

Lemma baseVspace_module V (V0 := baseVspace V) : (F1 × V0 ≤ V0)%VS.

Lemma sub_baseField (E : {subfield L}) : (F1 ≤ baseVspace E)%VS.

Lemma vspaceOver_refBase V : vspaceOver F1 (baseVspace V) =i V.

Lemma module_baseVspace M0 :
  (F1 × M0 ≤ M0)%VS → {V | M0 = baseVspace V & M0 =i V}.

Lemma module_baseAspace (E0 : {subfield L0}) :
  (F1 ≤ E0)%VS → {E | E0 = baseAspace E & E0 =i E}.

End RefBaseField.

Base of fieldOver, finally.
Section MoreFieldOver.

Variables (F0 : fieldType) (L : fieldExtType F0) (F : {subfield L}).

Lemma base_vspaceOver V : baseVspace (vspaceOver F V) =i (F × V)%VS.

Lemma base_moduleOver V : (F × V ≤ V)%VS → baseVspace (vspaceOver F V) =i V.

Lemma base_aspaceOver (E : {subfield L}) :
  (F ≤ E)%VS → baseVspace (vspaceOver F E) =i E.

End MoreFieldOver.

Section SubFieldExtension.

Local Open Scope quotient_scope.

Variables (F L : fieldType) (iota : {rmorphism F → L}).
Variables (z : L) (p : {poly F}).


Let wf_p := (p != 0) && root p^iota z.
Let p0 : {poly F} := if wf_p then (lead_coef p)^-1 *: p else 'X.
Let z0 := if wf_p then z else 0.
Let n := (size p0).-1.

Let p0_mon : p0 \is monic.

Let nz_p0 : p0 != 0.

Let p0z0 : root p0^iota z0.

Let n_gt0: 0 < n.

Let z0Ciota : commr_rmorph iota z0.
Let iotaFz (x : 'rV[F]_n) := iotaPz (rVpoly x).

Definition equiv_subfext x y := (iotaFz x == iotaFz y).

Fact equiv_subfext_is_equiv : equiv_class_of equiv_subfext.

Canonical equiv_subfext_equiv := EquivRelPack equiv_subfext_is_equiv.
Canonical equiv_subfext_encModRel := defaultEncModRel equiv_subfext.

Definition subFExtend := {eq_quot equiv_subfext}.


Definition subfx_inj := lift_fun1 subFExtend iotaFz.

Fact pi_subfx_inj : {mono \pi : x / iotaFz x >-> subfx_inj x}.
Canonical pi_subfx_inj_morph := PiMono1 pi_subfx_inj.

Let iotaPz_repr x : iotaPz (rVpoly (repr (\pi_(subFExtend) x))) = iotaFz x.

Definition subfext0 := lift_cst subFExtend 0.
Canonical subfext0_morph := PiConst subfext0.

Definition subfext_add := lift_op2 subFExtend +%R.
Fact pi_subfext_add : {morph \pi : x y / x + y >-> subfext_add x y}.
Canonical pi_subfx_add_morph := PiMorph2 pi_subfext_add.

Definition subfext_opp := lift_op1 subFExtend -%R.
Fact pi_subfext_opp : {morph \pi : x / - x >-> subfext_opp x}.
Canonical pi_subfext_opp_morph := PiMorph1 pi_subfext_opp.

Fact addfxA : associative subfext_add.

Fact addfxC : commutative subfext_add.

Fact add0fx : left_id subfext0 subfext_add.

Fact addfxN : left_inverse subfext0 subfext_opp subfext_add.


Let poly_rV_modp_K q : rVpoly (poly_rV (q %% p0) : 'rV[F]_n) = q %% p0.

Let iotaPz_modp q : iotaPz (q %% p0) = iotaPz q.

Definition subfx_mul_rep (x y : 'rV[F]_n) : 'rV[F]_n :=
  poly_rV ((rVpoly x) × (rVpoly y) %% p0).

Definition subfext_mul := lift_op2 subFExtend subfx_mul_rep.
Fact pi_subfext_mul :
  {morph \pi : x y / subfx_mul_rep x y >-> subfext_mul x y}.
Canonical pi_subfext_mul_morph := PiMorph2 pi_subfext_mul.

Definition subfext1 := lift_cst subFExtend (poly_rV 1).
Canonical subfext1_morph := PiConst subfext1.

Fact mulfxA : associative (subfext_mul).

Fact mulfxC : commutative subfext_mul.

Fact mul1fx : left_id subfext1 subfext_mul.

Fact mulfx_addl : left_distributive subfext_mul subfext_add.

Fact nonzero1fx : subfext1 != subfext0.


Definition subfx_poly_inv (q : {poly F}) : {poly F} :=
  if iotaPz q == 0 then 0 else
  let r := gdcop q p0 in let: (u, v) := egcdp q r in
  ((u × q + v × r)`_0)^-1 *: u.

Let subfx_poly_invE q : iotaPz (subfx_poly_inv q) = (iotaPz q)^-1.

Definition subfx_inv_rep (x : 'rV[F]_n) : 'rV[F]_n :=
  poly_rV (subfx_poly_inv (rVpoly x) %% p0).

Definition subfext_inv := lift_op1 subFExtend subfx_inv_rep.
Fact pi_subfext_inv : {morph \pi : x / subfx_inv_rep x >-> subfext_inv x}.
Canonical pi_subfext_inv_morph := PiMorph1 pi_subfext_inv.

Fact subfx_fieldAxiom : ∀ x, x != 0 → subfext_inv x × x = 1.

Fact subfx_inv0 : subfext_inv (0 : subFExtend) = (0 : subFExtend).


Fact subfx_inj_is_additive : additive subfx_inj.

Fact subfx_inj_is_multiplicative : multiplicative subfx_inj.


Definition subfx_eval := lift_embed subFExtend (fun q ⇒ poly_rV (q %% p0)).
Canonical subfx_eval_morph := PiEmbed subfx_eval.

Definition subfx_root := subfx_eval 'X.

Lemma subfx_eval_is_additive : additive subfx_eval.

Lemma subfx_eval_is_multiplicative : multiplicative subfx_eval.


Definition inj_subfx := (subfx_eval \o polyC).

Lemma subfxE x: ∃ p, x = subfx_eval p.

Definition subfx_scale a x := inj_subfx a × x.
Fact subfx_scalerA a b x :
  subfx_scale a (subfx_scale b x) = subfx_scale (a × b) x.
Fact subfx_scaler1r : left_id 1 subfx_scale.
Fact subfx_scalerDr : right_distributive subfx_scale +%R.
Fact subfx_scalerDl x : {morph subfx_scale^~ x : a b / a + b}.


Fact subfx_scaleAl a u v : subfx_scale a (u × v) = (subfx_scale a u) × v.

Fact subfx_scaleAr a u v : subfx_scale a (u × v) = u × (subfx_scale a v).

Fact subfx_evalZ : scalable subfx_eval.

Hypothesis (pz0 : root p^iota z).

Section NonZero.

Hypothesis nz_p : p != 0.

Lemma subfx_inj_eval q : subfx_inj (subfx_eval q) = q^iota.[z].

Lemma subfx_inj_root : subfx_inj subfx_root = z.

Lemma subfx_injZ b x : subfx_inj (b *: x) = iota b × subfx_inj x.

Lemma subfx_inj_base b : subfx_inj b%:A = iota b.

Lemma subfxEroot x : {q | x = (map_poly (in_alg subFExtend) q).[subfx_root]}.

Lemma subfx_irreducibleP :
 (∀ q, root q^iota z → q != 0 → size p ≤ size q) ↔ irreducible_poly p.

End NonZero.

Section Irreducible.

Hypothesis irr_p : irreducible_poly p.
Let nz_p : p != 0.

The Vector axiom requires irreducibility.
Lemma min_subfx_vect : vector_axiom_def (size p).-1 (Phant subFExtend).

Definition SubfxVect := Lmodule_hasFinDim.Build _ subFExtend min_subfx_vect.
Definition SubFieldExtType : fieldExtType F := HB.pack subFExtend SubfxVect.

End Irreducible.

End SubFieldExtension.


Lemma irredp_FAdjoin (F : fieldType) (p : {poly F}) :
    irreducible_poly p →
  {L : fieldExtType F & \dim {:L} = (size p).-1 &
    {z | root (map_poly (in_alg L) p) z & <<1; z>>%VS = fullv}}.

Coq 8.3 processes this shorter proof correctly, but then crashes on Qed. In Coq 8.4 Qed takes about 18s. In Coq 8.7, everything seems to be all right Lemma Xirredp_FAdjoin' (F : fieldType) (p : {poly F}) : irreducible_poly p -> {L : fieldExtType F & \dim {: L} = (size p).-1 & {z | root (map_poly (in_alg L) p) z & 1; z%VS = fullv}}. Proof. case=> p_gt1 irr_p; set n := (size p).-1; pose vL := [vectType F of 'rV_n]. have Dn: n.+1 = size p := ltn_predK p_gt1. have nz_p: p != 0 by rewrite -size_poly_eq0 -Dn. pose toL q : vL := poly_rV (q %% p). have toL_K q : rVpoly (toL q) = q %% p. by rewrite poly_rV_K // -ltnS Dn ?ltn_modp -?Dn. pose mul (x y : vL) : vL := toL (rVpoly x * rVpoly y). pose L1 : vL := poly_rV 1. have L1K: rVpoly L1 = 1 by rewrite poly_rV_K // size_poly1 -ltnS Dn. have mulC: commutative mul by rewrite /mul => x y; rewrite mulrC. have mulA: associative mul. by move=> x y z; rewrite -!(mulC z) /mul !toL_K /toL !modp_mul mulrCA. have mul1: left_id L1 mul. move=> x; rewrite /mul L1K mul1r /toL modp_small ?rVpolyK // -Dn ltnS. by rewrite size_poly. have mulD: left_distributive mul +%R. move=> x y z; apply: canLR rVpolyK _. by rewrite !raddfD mulrDl /= !toL_K /toL modpD. have nzL1: L1 != 0 by rewrite -(can_eq rVpolyK) L1K raddf0 oner_eq0. pose mulM := GRing.Zmodule_isComRing.Build vL mulA mulC mul1 mulD nzL1. pose rL := ComRingType vL mulM. have mulZlM : GRing.Lmodule_isLalgebra F rL. constructor => a x y; apply: canRL rVpolyK _. by rewrite !linearZ /= toL_K -scalerAl modpZl. pose laL := LalgType F rL mulZlM. have mulZrM : GRing.Lalgebra_isAlgebra F laL. by constructor => a x y; rewrite !(mulrC x) scalerAl. pose aL := AlgType F laL mulZrM. pose uLM := Algebra_isFalgebra.Build F aL. pose cuL := ComUnitRingType uLM _. have unitM : GRing.ComUnitRing_isField cuL. constructor => x nz_x; apply/unitrP; set q := rVpoly x. have nz_q: q != 0 by rewrite -(can_eq rVpolyK) raddf0 in nz_x. have /Bezout_eq1_coprimepP[u upq1]: coprimep p q. have /contraR := irr_p _ (dvdp_gcdl p q); apply. have: size (gcdp p q) <= size q by apply: leq_gcdpr. rewrite leqNgt; apply: contra; move/eqp_size ->. by rewrite (polySpred nz_p) ltnS size_poly. suffices: x * toL u.2 = 1 by exists (toL u.2); rewrite mulrC. congr (poly_rV _); rewrite toL_K modp_mul mulrC (canRL (addKr _) upq1). by rewrite -mulNr modp_addl_mul_small ?size_poly1. pose feL := FieldExtType _ unitM _. exists feL; first by rewrite dimvf; apply: mul1n. pose z : vL := toL 'X; set iota := in_alg _. have q_z q: rVpoly (map_poly iota q). [z] = q %% p. elim/poly_ind: q => [|a q IHq]. by rewrite map_poly0 horner0 linear0 mod0p. rewrite rmorphD rmorphM /= map_polyX map_polyC hornerMXaddC linearD /=. rewrite linearZ /= L1K alg_polyC modpD; congr (_ + _); last first. by rewrite modp_small // size_polyC; case: (~~ _) => //; apply: ltnW. by rewrite !toL_K IHq mulrC modp_mul mulrC modp_mul. exists z; first by rewrite /root -(can_eq rVpolyK) q_z modpp linear0. apply/vspaceP=> x; rewrite memvf; apply/Fadjoin_polyP. exists (map_poly iota (rVpoly x)). by apply/polyOverP=> i; rewrite coef_map memvZ ?mem1v. by apply/(can_inj rVpolyK); rewrite q_z modp_small // -Dn ltnS size_poly. Qed.