Library mathcomp.field.fieldext
(* (c) Copyright 2006-2015 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.
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).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 T);
field_ext : Field.mixin_of (UnitRing.Pack base T)
}.
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).
End Bases.
Structure type (phR : phant R) := Pack {sort; _ : class_of sort; _ : Type}.
Variables (phR : phant R) (T : Type) (cT : type phR).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
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 (Field.class mT) (@Field.Class T
(@IntegralDomain.Class T (@ComUnitRing.Class T (@ComRing.Class T b
Cm) b) IDm) Fm) ⇒ Pack phR (@Class T b Cm IDm Fm) T.
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) T.
Definition eqType := @Equality.Pack cT xclass xT.
Definition choiceType := @Choice.Pack cT xclass xT.
Definition zmodType := @Zmodule.Pack cT xclass xT.
Definition ringType := @Ring.Pack cT xclass xT.
Definition unitRingType := @UnitRing.Pack cT xclass xT.
Definition comRingType := @ComRing.Pack cT xclass xT.
Definition comUnitRingType := @ComUnitRing.Pack cT xclass xT.
Definition idomainType := @IntegralDomain.Pack cT xclass xT.
Definition fieldType := @Field.Pack cT xclass xT.
Definition lmodType := @Lmodule.Pack R phR cT xclass xT.
Definition lalgType := @Lalgebra.Pack R phR cT xclass xT.
Definition algType := @Algebra.Pack R phR cT xclass xT.
Definition unitAlgType := @UnitAlgebra.Pack R phR cT xclass xT.
Definition vectType := @Vector.Pack R phR cT xclass xT.
Definition FalgType := @Falgebra.Pack R phR cT xclass xT.
Definition Falg_comRingType := @ComRing.Pack FalgType xclass xT.
Definition Falg_comUnitRingType := @ComUnitRing.Pack FalgType xclass xT.
Definition Falg_idomainType := @IntegralDomain.Pack FalgType xclass xT.
Definition Falg_fieldType := @Field.Pack FalgType xclass xT.
Definition vect_comRingType := @ComRing.Pack vectType xclass xT.
Definition vect_comUnitRingType := @ComUnitRing.Pack vectType xclass xT.
Definition vect_idomainType := @IntegralDomain.Pack vectType xclass xT.
Definition vect_fieldType := @Field.Pack vectType xclass xT.
Definition unitAlg_comRingType := @ComRing.Pack unitAlgType xclass xT.
Definition unitAlg_comUnitRingType := @ComUnitRing.Pack unitAlgType xclass xT.
Definition unitAlg_idomainType := @IntegralDomain.Pack unitAlgType xclass xT.
Definition unitAlg_fieldType := @Field.Pack unitAlgType xclass xT.
Definition alg_comRingType := @ComRing.Pack algType xclass xT.
Definition alg_comUnitRingType := @ComUnitRing.Pack algType xclass xT.
Definition alg_idomainType := @IntegralDomain.Pack algType xclass xT.
Definition alg_fieldType := @Field.Pack algType xclass xT.
Definition lalg_comRingType := @ComRing.Pack lalgType xclass xT.
Definition lalg_comUnitRingType := @ComUnitRing.Pack lalgType xclass xT.
Definition lalg_idomainType := @IntegralDomain.Pack lalgType xclass xT.
Definition lalg_fieldType := @Field.Pack lalgType xclass xT.
Definition lmod_comRingType := @ComRing.Pack lmodType xclass xT.
Definition lmod_comUnitRingType := @ComUnitRing.Pack lmodType xclass xT.
Definition lmod_idomainType := @IntegralDomain.Pack lmodType xclass xT.
Definition lmod_fieldType := @Field.Pack lmodType xclass xT.
End FieldExt.
Module Exports.
Coercion sort : type >-> Sortclass.
Coercion base : class_of >-> Falgebra.class_of.
Coercion base4 : class_of >-> Field.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 vectType : type >-> Vector.type.
Canonical vectType.
Coercion FalgType : type >-> Falgebra.type.
Canonical FalgType.
Canonical Falg_comRingType.
Canonical Falg_comUnitRingType.
Canonical Falg_idomainType.
Canonical Falg_fieldType.
Canonical vect_comRingType.
Canonical vect_comUnitRingType.
Canonical vect_idomainType.
Canonical vect_fieldType.
Canonical unitAlg_comRingType.
Canonical unitAlg_comUnitRingType.
Canonical unitAlg_idomainType.
Canonical unitAlg_fieldType.
Canonical alg_comRingType.
Canonical alg_comUnitRingType.
Canonical alg_idomainType.
Canonical alg_fieldType.
Canonical lalg_comRingType.
Canonical lalg_comUnitRingType.
Canonical lalg_idomainType.
Canonical lalg_fieldType.
Canonical lmod_comRingType.
Canonical lmod_comUnitRingType.
Canonical lmod_idomainType.
Canonical lmod_fieldType.
Notation fieldExtType R := (type (Phant R)).
Notation "[ 'fieldExtType' F 'of' L ]" :=
(@pack _ (Phant F) L _ _ 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.
Implicit 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.
Implicit Arguments Fadjoin_idP [F0 L K x].
Implicit Arguments FadjoinP [F0 L K x E].
Implicit Arguments Fadjoin_seqP [F0 L K rs E].
Implicit Arguments polyOver_subvs [F0 L K p].
Implicit Arguments Fadjoin_polyP [F0 L K x v].
Implicit Arguments Fadjoin1_polyP [F0 L x v].
Implicit 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].
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.
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].
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)).
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.
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}}.
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.
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 modp_add.
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 _ ) _; rewrite !linearZ /= toL_K.
by rewrite -scalerAl modp_scalel.
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 modp_add; 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.
apply: (can_inj (@rVpolyK _ )).
by rewrite q_z modp_small // -Dn ltnS size_poly.
Qed.