Library mathcomp.field.fieldext
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
+
+ (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.
+
+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.
+ +
+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.
+ +
+ +
+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.
+ +
+
+
++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.
+ +
+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.
+ +
+ +
+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.
+ 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 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.
+
+
+
+
+