Library mathcomp.field.fieldext

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
From mathcomp Require Import choice fintype tuple finfun bigop ssralg finalg.
From mathcomp Require Import zmodp matrix vector falgebra poly polydiv mxpoly.
From mathcomp Require Import 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.

Module FieldExt.

Import GRing.

Section FieldExt.

Variable R : ringType.

Record class_of T := Class {
  base : Falgebra.class_of R T;
  comm_ext : commutative (Ring.mul base);
  idomain_ext : IntegralDomain.axiom (Ring.Pack base);
  field_ext : Field.mixin_of (UnitRing.Pack base)
}.


Section Bases.
Variables (T : Type) (c : class_of T).
Definition base1 := ComRing.Class (@comm_ext T c).
Definition base2 := @ComUnitRing.Class T base1 c.
Definition base3 := @IntegralDomain.Class T base2 (@idomain_ext T c).
Definition base4 := @Field.Class T base3 (@field_ext T c).
Definition base5 := @ComAlgebra.Class R T (@base T c) (@comm_ext T c).
Definition base6 := @ComUnitAlgebra.Class R T base5 c.
End Bases.

Structure type (phR : phant R) := Pack {sort; _ : class_of sort}.

Variables (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c := cT return class_of cT in c.

Definition pack :=
  fun (bT : Falgebra.type phR) b
    & phant_id (Falgebra.class bT : Falgebra.class_of R bT)
               (b : Falgebra.class_of R T) ⇒
  fun mT Cm IDm Fm
    & phant_id (GRing.ComRing.mixin (Field.class mT)) Cm
    & phant_id (GRing.IntegralDomain.mixin (Field.class mT)) IDm
    & phant_id (GRing.Field.mixin (Field.class mT)) Fm ⇒
    Pack phR (@Class T b Cm IDm Fm).

Definition pack_eta K :=
  let cK := Field.class K in let Cm := ComRing.mixin cK in
  let IDm := IntegralDomain.mixin cK in let Fm := Field.mixin cK in
  fun (bT : Falgebra.type phR) b & phant_id (Falgebra.class bT) b ⇒
  fun cT_ & phant_id (@Class T b) cT_ ⇒ @Pack phR T (cT_ Cm IDm Fm).

Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.
Definition unitRingType := @UnitRing.Pack cT class.
Definition comRingType := @ComRing.Pack cT class.
Definition comUnitRingType := @ComUnitRing.Pack cT class.
Definition idomainType := @IntegralDomain.Pack cT class.
Definition fieldType := @Field.Pack cT class.
Definition lmodType := @Lmodule.Pack R phR cT class.
Definition lalgType := @Lalgebra.Pack R phR cT class.
Definition algType := @Algebra.Pack R phR cT class.
Definition unitAlgType := @UnitAlgebra.Pack R phR cT class.
Definition comAlgType := @ComAlgebra.Pack R phR cT class.
Definition comUnitAlgType := @ComUnitAlgebra.Pack R phR cT class.
Definition vectType := @Vector.Pack R phR cT class.
Definition FalgType := @Falgebra.Pack R phR cT class.

Definition Falg_comRingType := @ComRing.Pack FalgType class.
Definition Falg_comUnitRingType := @ComUnitRing.Pack FalgType class.
Definition Falg_comAlgType := @ComAlgebra.Pack R phR FalgType class.
Definition Falg_comUnitAlgType := @ComUnitAlgebra.Pack R phR FalgType class.
Definition Falg_idomainType := @IntegralDomain.Pack FalgType class.
Definition Falg_fieldType := @Field.Pack FalgType class.

Definition vect_comRingType := @ComRing.Pack vectType class.
Definition vect_comUnitRingType := @ComUnitRing.Pack vectType class.
Definition vect_comAlgType := @ComAlgebra.Pack R phR vectType class.
Definition vect_comUnitAlgType := @ComUnitAlgebra.Pack R phR vectType class.
Definition vect_idomainType := @IntegralDomain.Pack vectType class.
Definition vect_fieldType := @Field.Pack vectType class.

Definition comUnitAlg_idomainType := @IntegralDomain.Pack comUnitAlgType class.
Definition comUnitAlg_fieldType := @Field.Pack comUnitAlgType class.

Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType class.
Definition unitAlg_fieldType := @Field.Pack unitAlgType class.

Definition comAlg_idomainType := @IntegralDomain.Pack comAlgType class.
Definition comAlg_fieldType := @Field.Pack comAlgType class.

Definition alg_idomainType := @IntegralDomain.Pack algType class.
Definition alg_fieldType := @Field.Pack algType class.

Definition lalg_idomainType := @IntegralDomain.Pack lalgType class.
Definition lalg_fieldType := @Field.Pack lalgType class.

Definition lmod_idomainType := @IntegralDomain.Pack lmodType class.
Definition lmod_fieldType := @Field.Pack lmodType class.

End FieldExt.

Module Exports.

Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion base : class_of >-> Falgebra.class_of.
Coercion base4 : class_of >-> Field.class_of.
Coercion base6 : class_of >-> ComUnitAlgebra.class_of.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion zmodType : type >-> Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> Ring.type.
Canonical ringType.
Coercion unitRingType : type >-> UnitRing.type.
Canonical unitRingType.
Coercion comRingType : type >-> ComRing.type.
Canonical comRingType.
Coercion comUnitRingType : type >-> ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> IntegralDomain.type.
Canonical idomainType.
Coercion fieldType : type >-> Field.type.
Canonical fieldType.
Coercion lmodType : type >-> Lmodule.type.
Canonical lmodType.
Coercion lalgType : type >-> Lalgebra.type.
Canonical lalgType.
Coercion algType : type >-> Algebra.type.
Canonical algType.
Coercion unitAlgType : type >-> UnitAlgebra.type.
Canonical unitAlgType.
Coercion comAlgType : type >-> ComAlgebra.type.
Canonical comAlgType.
Coercion comUnitAlgType : type >-> ComUnitAlgebra.type.
Canonical comUnitAlgType.
Coercion vectType : type >-> Vector.type.
Canonical vectType.
Coercion FalgType : type >-> Falgebra.type.
Canonical FalgType.

Canonical Falg_comRingType.
Canonical Falg_comUnitRingType.
Canonical Falg_comAlgType.
Canonical Falg_comUnitAlgType.
Canonical Falg_idomainType.
Canonical Falg_fieldType.
Canonical vect_comRingType.
Canonical vect_comUnitRingType.
Canonical vect_comAlgType.
Canonical vect_comUnitAlgType.
Canonical vect_idomainType.
Canonical vect_fieldType.
Canonical comUnitAlg_idomainType.
Canonical comUnitAlg_fieldType.
Canonical unitAlg_idomainType.
Canonical unitAlg_fieldType.
Canonical comAlg_idomainType.
Canonical comAlg_fieldType.
Canonical alg_idomainType.
Canonical alg_fieldType.
Canonical lalg_idomainType.
Canonical lalg_fieldType.
Canonical lmod_idomainType.
Canonical lmod_fieldType.
Notation fieldExtType R := (type (Phant R)).

Notation "[ 'fieldExtType' F 'of' L ]" :=
  (@pack _ (Phant F) L _ _ id _ _ _ _ id id id)
  (at level 0, format "[ 'fieldExtType' F 'of' L ]") : form_scope.

Notation "[ 'fieldExtType' F 'of' L 'for' K ]" :=
  (@pack_eta _ (Phant F) L K _ _ id _ id)
  (at level 0, format "[ 'fieldExtType' F 'of' L 'for' K ]") : form_scope.

Notation "{ 'subfield' L }" := (@aspace_of _ (FalgType _) (Phant L))
  (at level 0, format "{ 'subfield' L }") : type_scope.

End Exports.
End FieldExt.
Export FieldExt.Exports.

Canonical regular_fieldExtType (F : fieldType) := [fieldExtType F of F^o for F].

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).
Canonical prodv_comoid := Monoid.ComLaw prodvC.

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).
Canonical vsval_rmorphism K := AddRMorphism (vsval_multiplicative K).
Canonical vsval_lrmorphism K : {lrmorphism subvs_of K → L} :=
  [lrmorphism of vsval].

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

Fact aspace_divr_closed K : divr_closed K.
Canonical aspace_mulrPred K := MulrPred (aspace_divr_closed K).
Canonical aspace_divrPred K := DivrPred (aspace_divr_closed K).
Canonical aspace_smulrPred K := SmulrPred (aspace_divr_closed K).
Canonical aspace_sdivrPred K := SdivrPred (aspace_divr_closed K).
Canonical aspace_semiringPred K := SemiringPred (aspace_divr_closed K).
Canonical aspace_subringPred K := SubringPred (aspace_divr_closed K).
Canonical aspace_subalgPred K := SubalgPred (memv_submod_closed K).
Canonical aspace_divringPred K := DivringPred (aspace_divr_closed K).
Canonical aspace_divalgPred K := DivalgPred (memv_submod_closed K).

Definition subvs_mulC K := [comRingMixin of subvs_of K by <:].
Canonical subvs_comRingType K :=
  Eval hnf in ComRingType (subvs_of K) (@subvs_mulC K).
Canonical subvs_comUnitRingType K :=
  Eval hnf in [comUnitRingType of subvs_of K].
Definition subvs_mul_eq0 K := [idomainMixin of subvs_of K by <:].
Canonical subvs_idomainType K :=
  Eval hnf in IdomainType (subvs_of K) (@subvs_mul_eq0 K).
Lemma subvs_fieldMixin K : GRing.Field.mixin_of (@subvs_idomainType K).
Canonical subvs_fieldType K :=
  Eval hnf in FieldType (subvs_of K) (@subvs_fieldMixin K).
Canonical subvs_fieldExtType K := Eval hnf in [fieldExtType F0 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.
Canonical Fadjoin_poly_additive := Additive Fadjoin_poly_is_linear.
Canonical Fadjoin_poly_linear := AddLinear Fadjoin_poly_is_linear.

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)).
Canonical fieldExtHorner_additive := [additive of fieldExt_horner].
Canonical fieldExtHorner_rmorphism := [rmorphism of fieldExt_horner].
Lemma fieldExt_hornerC b : fieldExt_horner b%:P = b%:A.
Lemma fieldExt_hornerX : fieldExt_horner 'X = z.
Fact fieldExt_hornerZ : scalable fieldExt_horner.
Canonical fieldExt_horner_linear := AddLinear fieldExt_hornerZ.
Canonical fieldExt_horner_lrmorhism := [lrmorphism of 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.

Canonical fieldOver_eqType := [eqType of L_F].
Canonical fieldOver_choiceType := [choiceType of L_F].
Canonical fieldOver_zmodType := [zmodType of L_F].
Canonical fieldOver_ringType := [ringType of L_F].
Canonical fieldOver_unitRingType := [unitRingType of L_F].
Canonical fieldOver_comRingType := [comRingType of L_F].
Canonical fieldOver_comUnitRingType := [comUnitRingType of L_F].
Canonical fieldOver_idomainType := [idomainType of L_F].
Canonical fieldOver_fieldType := [fieldType of L_F].

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.

Definition fieldOver_lmodMixin :=
  LmodMixin fieldOver_scaleA fieldOver_scale1
            fieldOver_scaleDr fieldOver_scaleDl.

Canonical fieldOver_lmodType := LmodType K_F L_F fieldOver_lmodMixin.

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.

Canonical fieldOver_lalgType := LalgType K_F L_F fieldOver_scaleAl.

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

Canonical fieldOver_algType := AlgType K_F L_F fieldOver_scaleAr.
Canonical fieldOver_unitAlgType := [unitAlgType K_F of L_F].
Canonical fieldOver_comAlgType := [comAlgType K_F of L_F].
Canonical fieldOver_comUnitAlgType := [comUnitAlgType K_F of L_F].

Fact fieldOver_vectMixin : Vector.mixin_of fieldOver_lmodType.

Canonical fieldOver_vectType := VectType K_F L_F fieldOver_vectMixin.
Canonical fieldOver_FalgType := [FalgType K_F of L_F].
Canonical fieldOver_fieldExtType := [fieldExtType K_F of 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))).

Canonical baseField_eqType := [eqType of L0].
Canonical baseField_choiceType := [choiceType of L0].
Canonical baseField_zmodType := [zmodType of L0].
Canonical baseField_ringType := [ringType of L0].
Canonical baseField_unitRingType := [unitRingType of L0].
Canonical baseField_comRingType := [comRingType of L0].
Canonical baseField_comUnitRingType := [comUnitRingType of L0].
Canonical baseField_idomainType := [idomainType of L0].
Canonical baseField_fieldType := [fieldType of L0].

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.

Definition baseField_lmodMixin :=
  LmodMixin baseField_scaleA baseField_scale1
            baseField_scaleDr baseField_scaleDl.

Canonical baseField_lmodType := LmodType F0 L0 baseField_lmodMixin.

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.

Canonical baseField_lalgType := LalgType F0 L0 baseField_scaleAl.

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

Canonical baseField_algType := AlgType F0 L0 baseField_scaleAr.
Canonical baseField_unitAlgType := [unitAlgType F0 of L0].

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

Fact baseField_vectMixin : Vector.mixin_of baseField_lmodType.

Canonical baseField_vectType := VectType F0 L0 baseField_vectMixin.
Canonical baseField_FalgType := [FalgType F0 of L0].
Canonical baseField_extFieldType := [fieldExtType F0 of 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).

Fact refBaseField_key : unit.
Definition refBaseField := locked_with refBaseField_key (baseAspace 1).
Canonical refBaseField_unlockable := [unlockable of refBaseField].
Notation F1 := refBaseField.

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 BaseField.

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

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}.
Canonical subFExtend_eqType := [eqType of subFExtend].
Canonical subFExtend_choiceType := [choiceType of subFExtend].
Canonical subFExtend_quotType := [quotType of subFExtend].
Canonical subFExtend_eqQuotType := [eqQuotType equiv_subfext of subFExtend].

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.

Definition subfext_zmodMixin := ZmodMixin addfxA addfxC add0fx addfxN.
Canonical subfext_zmodType :=
  Eval hnf in ZmodType subFExtend subfext_zmodMixin.

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 subfext_comRingMixin :=
  ComRingMixin mulfxA mulfxC mul1fx mulfx_addl nonzero1fx.
Canonical subfext_Ring := Eval hnf in RingType subFExtend subfext_comRingMixin.
Canonical subfext_comRing := Eval hnf in ComRingType subFExtend mulfxC.

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 :
  GRing.Field.axiom (subfext_inv : subFExtend → subFExtend).

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

Definition subfext_unitRingMixin := FieldUnitMixin subfx_fieldAxiom subfx_inv0.
Canonical subfext_unitRingType :=
  Eval hnf in UnitRingType subFExtend subfext_unitRingMixin.
Canonical subfext_comUnitRing := Eval hnf in [comUnitRingType of subFExtend].
Definition subfext_fieldMixin := @FieldMixin _ _ subfx_fieldAxiom subfx_inv0.
Definition subfext_idomainMixin := FieldIdomainMixin subfext_fieldMixin.
Canonical subfext_idomainType :=
  Eval hnf in IdomainType subFExtend subfext_idomainMixin.
Canonical subfext_fieldType :=
  Eval hnf in FieldType subFExtend subfext_fieldMixin.

Fact subfx_inj_is_rmorphism : rmorphism subfx_inj.
Canonical subfx_inj_additive := Additive subfx_inj_is_rmorphism.
Canonical subfx_inj_rmorphism := RMorphism subfx_inj_is_rmorphism.

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_rmorphism : rmorphism subfx_eval.
Canonical subfx_eval_additive := Additive subfx_eval_is_rmorphism.
Canonical subfx_eval_rmorphism := AddRMorphism subfx_eval_is_rmorphism.

Definition inj_subfx := (subfx_eval \o polyC).
Canonical inj_subfx_addidive := [additive of inj_subfx].
Canonical inj_subfx_rmorphism := [rmorphism of inj_subfx].

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}.
Definition subfx_lmodMixin :=
  LmodMixin subfx_scalerA subfx_scaler1r subfx_scalerDr subfx_scalerDl.
Canonical subfx_lmodType := LmodType F subFExtend subfx_lmodMixin.

Fact subfx_scaleAl : GRing.Lalgebra.axiom ( *%R : subFExtend → _).
Canonical subfx_lalgType := LalgType F subFExtend subfx_scaleAl.

Fact subfx_scaleAr : GRing.Algebra.axiom subfx_lalgType.
Canonical subfx_algType := AlgType F subFExtend subfx_scaleAr.
Canonical subfext_unitAlgType := [unitAlgType F of subFExtend].

Fact subfx_evalZ : scalable subfx_eval.
Canonical subfx_eval_linear := AddLinear subfx_evalZ.
Canonical subfx_eval_lrmorphism := [lrmorphism of 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_vectAxiom : Vector.axiom (size p).-1 subfx_lmodType.

Definition SubfxVectMixin := VectMixin min_subfx_vectAxiom.
Definition SubfxVectType := VectType F subFExtend SubfxVectMixin.
Definition SubfxFalgType := Eval simpl in [FalgType F of SubfxVectType].
Definition SubFieldExtType := Eval simpl in [fieldExtType F of SubfxFalgType].

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 & Vector.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 := ComRingMixin mulA mulC mul1 mulD nzL1. pose rL := ComRingType (RingType vL mulM) mulC. have mulZl: GRing.Lalgebra.axiom mul. move=> a x y; apply: canRL rVpolyK _. by rewrite !linearZ /= toL_K -scalerAl modpZl. have mulZr: @GRing.Algebra.axiom _ (LalgType F rL mulZl). by move=> a x y; rewrite !(mulrC x) scalerAl. pose aL := AlgType F _ mulZr; pose urL := FalgUnitRingType aL. pose uaL := [unitAlgType F of AlgType F urL mulZr]. pose faL := [FalgType F of uaL]. have unitE: GRing.Field.mixin_of urL. move=> 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 ucrL := [comUnitRingType of ComRingType urL mulC]. pose fL := FieldType (IdomainType ucrL (GRing.Field.IdomainMixin unitE)) unitE. exists [fieldExtType F of faL for fL]; first exact: 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.