Library mathcomp.field.galois

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)

Require Import mathcomp.ssreflect.ssreflect.

This file develops some basic Galois field theory, defining: splittingFieldFor K p E <-> E is the smallest field over K that splits p into linear factors. kHom K E f <=> f : 'End(L) is a ring morphism on E and fixes K. kAut K E f <=> f : 'End(L) is a kHom K E and f @: E == E. kHomExtend E f x y == a kHom K E; x that extends f and maps x to y, when f \is a kHom K E and root (minPoly E x) y.
splittingFieldFor K p E <-> E is splitting field for p over K: p splits in E and its roots generate E from K. splittingFieldType F == the interface type of splitting field extensions of F, that is, extensions generated by all the algebraic roots of some polynomial, or, equivalently, normal field extensions of F. SplittingField.axiom F L == the axiom stating that L is a splitting field. SplittingFieldType F L FsplitL == packs a proof FsplitL of the splitting field axiom for L into a splitingFieldType F, provided L has a fieldExtType F structure. [splittingFieldType F of L] == a clone of the canonical splittingFieldType structure for L. [splittingFieldType F of L for M] == an L-clone of the canonical splittingFieldType structure on M.
gal_of E == the group_type of automorphisms of E over the base field F. 'Gal(E / K) == the group of automorphisms of E that fix K. fixedField s == the field fixed by the set of automorphisms s. fixedField set0 = E when set0 : {set: gal_of E} normalField K E <=> E is invariant for every 'Gal(L / K) for every L. galois K E <=> E is a normal and separable field extension of K. galTrace K E a == \sum(f in 'Gal(E / K)) (f a). galNorm K E a == \prod(f in 'Gal(E / K)) (f a).

Set Implicit Arguments.

Reserved Notation "''Gal' ( A / B )"
  (at level 8, A at level 35, format "''Gal' ( A / B )").

Import GroupScope GRing.Theory.
Local Open Scope ring_scope.

Section SplittingFieldFor.

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

Definition splittingFieldFor (U : {vspace L}) (p : {poly L}) (V : {vspace L}) :=
  exists2 rs, p %= \prod_(z <- rs) ('X - z%:P) & <<U & rs>>%VS = V.

Lemma splittingFieldForS (K M E : {subfield L}) p :
    (K M)%VS (M E)%VS
  splittingFieldFor K p E splittingFieldFor M p E.

End SplittingFieldFor.

Section kHom.

Variables (F : fieldType) (L : fieldExtType F).
Implicit Types (U V : {vspace L}) (K E : {subfield L}) (f g : 'End(L)).

Definition kHom U V f := ahom_in V f && (U fixedSpace f)%VS.

Lemma kHomP {K V f} :
  reflect [/\ {in V &, x y, f (x × y) = f x × f y}
            & {in K, x, f x = x}]
          (kHom K V f).

Lemma kAHomP {U V} {f : 'AEnd(L)} :
  reflect {in U, x, f x = x} (kHom U V f).

Lemma kHom1 U V : kHom U V \1.

Lemma k1HomE V f : kHom 1 V f = ahom_in V f.

Lemma kHom_lrmorphism (f : 'End(L)) : reflect (lrmorphism f) (kHom 1 {:L} f).

Lemma k1AHom V (f : 'AEnd(L)) : kHom 1 V f.

Lemma kHom_poly_id K E f p :
  kHom K E f p \is a polyOver K map_poly f p = p.

Lemma kHomSl U1 U2 V f : (U1 U2)%VS kHom U2 V f kHom U1 V f.

Lemma kHomSr K V1 V2 f : (V1 V2)%VS kHom K V2 f kHom K V1 f.

Lemma kHomS K1 K2 V1 V2 f :
  (K1 K2)%VS (V1 V2)%VS kHom K2 V2 f kHom K1 V1 f.

Lemma kHom_eq K E f g :
  (K E)%VS {in E, f =1 g} kHom K E f = kHom K E g.

Lemma kHom_inv K E f : kHom K E f {in E, {morph f : x / x^-1}}.

Lemma kHom_dim K E f : kHom K E f \dim (f @: E) = \dim E.

Lemma kHom_is_rmorphism K E f :
  kHom K E f rmorphism (f \o vsval : subvs_of E L).
Definition kHom_rmorphism K E f homKEf :=
  RMorphism (@kHom_is_rmorphism K E f homKEf).

Lemma kHom_horner K E f p x :
  kHom K E f p \is a polyOver E x \in E f p.[x] = (map_poly f p).[f x].

Lemma kHom_root K E f p x :
    kHom K E f p \is a polyOver E x \in E root p x
  root (map_poly f p) (f x).

Lemma kHom_root_id K E f p x :
   (K E)%VS kHom K E f p \is a polyOver K x \in E root p x
  root p (f x).

Section kHomExtend.

Variables (K E : {subfield L}) (f : 'End(L)) (x y : L).

Fact kHomExtend_subproof :
  linear (fun z(map_poly f (Fadjoin_poly E x z)).[y]).
Definition kHomExtend := linfun (Linear kHomExtend_subproof).

Lemma kHomExtendE z : kHomExtend z = (map_poly f (Fadjoin_poly E x z)).[y].

Hypotheses (sKE : (K E)%VS) (homKf : kHom K E f).
Hypothesis fPx_y_0 : root (map_poly f Px) y.

Lemma kHomExtend_id z : z \in E kHomExtend z = f z.

Lemma kHomExtend_val : kHomExtend x = y.

Lemma kHomExtend_poly p :
  p \in polyOver E kHomExtend p.[x] = (map_poly f p).[y].

Lemma kHomExtendP : kHom K <<E; x>> kHomExtend.

End kHomExtend.

Definition kAut U V f := kHom U V f && (f @: V == V)%VS.

Lemma kAutE K E f : kAut K E f = kHom K E f && (f @: E E)%VS.

Lemma kAutS U1 U2 V f : (U1 U2)%VS kAut U2 V f kAut U1 V f.

Lemma kHom_kAut_sub K E f : kAut K E f kHom K E f.

Lemma kAut_eq K E (f g : 'End(L)) :
  (K E)%VS {in E, f =1 g} kAut K E f = kAut K E g.

Lemma kAutfE K f : kAut K {:L} f = kHom K {:L} f.

Lemma kAut1E E (f : 'AEnd(L)) : kAut 1 E f = (f @: E E)%VS.

Lemma kAutf_lker0 K f : kHom K {:L} f lker f == 0%VS.

Lemma inv_kHomf K f : kHom K {:L} f kHom K {:L} f^-1.

Lemma inv_is_ahom (f : 'AEnd(L)) : ahom_in {:L} f^-1.

Canonical inv_ahom (f : 'AEnd(L)) : 'AEnd(L) := AHom (inv_is_ahom f).
Notation "f ^-1" := (inv_ahom f) : lrfun_scope.

Lemma comp_kHom_img K E f g :
  kHom K (g @: E) f kHom K E g kHom K E (f \o g).

Lemma comp_kHom K E f g : kHom K {:L} f kHom K E g kHom K E (f \o g).

Lemma kHom_extends K E f p U :
    (K E)%VS kHom K E f
     p \is a polyOver K splittingFieldFor E p U
  {g | kHom K U g & {in E, f =1 g}}.

End kHom.

Notation "f ^-1" := (inv_ahom f) : lrfun_scope.

Implicit Arguments kHomP [F L K V f].
Implicit Arguments kAHomP [F L U V f].
Implicit Arguments kHom_lrmorphism [F L f].

Module SplittingField.

Import GRing.

Section ClassDef.

Variable F : fieldType.

Definition axiom (L : fieldExtType F) :=
  exists2 p : {poly L}, p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}.

Record class_of (L : Type) : Type :=
  Class {base : FieldExt.class_of F L; _ : axiom (FieldExt.Pack _ base L)}.

Structure type (phF : phant F) := Pack {sort; _ : class_of sort; _ : Type}.
Variable (phF : phant F) (T : Type) (cT : type phF).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition clone c of phant_id class c := @Pack phF T c T.

Definition pack b0 (ax0 : axiom (@FieldExt.Pack F (Phant F) T b0 T)) :=
 fun bT b & phant_id (@FieldExt.class F phF bT) b
 fun ax & phant_id ax0 axPack (Phant F) (@Class T b ax) 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 F phF cT xclass xT.
Definition lalgType := @Lalgebra.Pack F phF cT xclass xT.
Definition algType := @Algebra.Pack F phF cT xclass xT.
Definition unitAlgType := @UnitAlgebra.Pack F phF cT xclass xT.
Definition vectType := @Vector.Pack F phF cT xclass xT.
Definition FalgType := @Falgebra.Pack F phF cT xclass xT.
Definition fieldExtType := @FieldExt.Pack F phF cT xclass xT.

End ClassDef.

Module Exports.

Coercion sort : type >-> Sortclass.
Coercion base : class_of >-> FieldExt.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.
Coercion fieldExtType : type >-> FieldExt.type.
Canonical fieldExtType.

Notation splittingFieldType F := (type (Phant F)).
Notation SplittingFieldType F L ax := (@pack _ (Phant F) L _ ax _ _ id _ id).
Notation "[ 'splittingFieldType' F 'of' L 'for' K ]" :=
  (@clone _ (Phant F) L K _ idfun)
  (at level 0, format "[ 'splittingFieldType' F 'of' L 'for' K ]")
  : form_scope.
Notation "[ 'splittingFieldType' F 'of' L ]" :=
  (@clone _ (Phant F) L _ _ id)
  (at level 0, format "[ 'splittingFieldType' F 'of' L ]") : form_scope.

End Exports.
End SplittingField.
Export SplittingField.Exports.

Lemma normal_field_splitting (F : fieldType) (L : fieldExtType F) :
  ( (K : {subfield L}) x,
     r, minPoly K x == \prod_(y <- r) ('X - y%:P))
  SplittingField.axiom L.

Fact regular_splittingAxiom F : SplittingField.axiom (regular_fieldExtType F).

Canonical regular_splittingFieldType (F : fieldType) :=
  SplittingFieldType F F^o (regular_splittingAxiom F).

Section SplittingFieldTheory.

Variables (F : fieldType) (L : splittingFieldType F).

Implicit Types (U V W : {vspace L}).
Implicit Types (K M E : {subfield L}).

Lemma splittingFieldP : SplittingField.axiom L.

Lemma splittingPoly :
  {p : {poly L} | p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}}.

Fact fieldOver_splitting E : SplittingField.axiom (fieldOver_fieldExtType E).
Canonical fieldOver_splittingFieldType E :=
  SplittingFieldType (subvs_of E) (fieldOver E) (fieldOver_splitting E).

Lemma enum_AEnd : {kAutL : seq 'AEnd(L) | f, f \in kAutL}.

Lemma splitting_field_normal K x :
   r, minPoly K x == \prod_(y <- r) ('X - y%:P).

Lemma kHom_to_AEnd K E f : kHom K E f {g : 'AEnd(L) | {in E, f =1 val g}}.

End SplittingFieldTheory.

Hide the finGroup structure on 'AEnd(L) in a module so that we can control when it is exported. Most people will want to use the finGroup structure on 'Gal(E / K) and will not need this module.
Module Import AEnd_FinGroup.
Section AEnd_FinGroup.

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

Definition inAEnd f := SeqSub (svalP (enum_AEnd L) f).
Fact inAEndK : cancel inAEnd val.

Definition AEnd_countMixin := Eval hnf in CanCountMixin inAEndK.
Canonical AEnd_countType := Eval hnf in CountType 'AEnd(L) AEnd_countMixin.
Canonical AEnd_subCountType := Eval hnf in [subCountType of 'AEnd(L)].
Definition AEnd_finMixin := Eval hnf in CanFinMixin inAEndK.
Canonical AEnd_finType := Eval hnf in FinType 'AEnd(L) AEnd_finMixin.
Canonical AEnd_subFinType := Eval hnf in [subFinType of 'AEnd(L)].

the group operation is the categorical composition operation
Definition comp_AEnd (f g : 'AEnd(L)) : 'AEnd(L) := (g \o f)%AF.

Fact comp_AEndA : associative comp_AEnd.

Fact comp_AEnd1l : left_id \1%AF comp_AEnd.

Fact comp_AEndK : left_inverse \1%AF (@inv_ahom _ L) comp_AEnd.

Definition AEnd_baseFinGroupMixin :=
  FinGroup.Mixin comp_AEndA comp_AEnd1l comp_AEndK.
Canonical AEnd_baseFinGroupType :=
  BaseFinGroupType 'AEnd(L) AEnd_baseFinGroupMixin.
Canonical AEnd_finGroupType := FinGroupType comp_AEndK.

Definition kAEnd U V := [set f : 'AEnd(L) | kAut U V f].
Definition kAEndf U := kAEnd U {:L}.

Lemma kAEnd_group_set K E : group_set (kAEnd K E).
Canonical kAEnd_group K E := group (kAEnd_group_set K E).
Canonical kAEndf_group K := [group of kAEndf K].

Lemma kAEnd_norm K E : kAEnd K E \subset 'N(kAEndf E)%g.

Lemma mem_kAut_coset K E (g : 'AEnd(L)) :
  kAut K E g g \in coset (kAEndf E) g.

Lemma aut_mem_eqP E (x y : coset_of (kAEndf E)) f g :
  f \in x g \in y reflect {in E, f =1 g} (x == y).

End AEnd_FinGroup.
End AEnd_FinGroup.

Section GaloisTheory.

Variables (F : fieldType) (L : splittingFieldType F).

Implicit Types (U V W : {vspace L}).
Implicit Types (K M E : {subfield L}).

We take Galois automorphisms for a subfield E to be automorphisms of the full field {:L} that operate in E taken modulo those that fix E pointwise. The type of Galois automorphisms of E is then the subtype of elements of the quotient kAEnd 1 E / kAEndf E, which we encapsulate in a specific wrapper to ensure stability of the gal_repr coercion insertion.
Section gal_of_Definition.

Variable V : {vspace L}.

The _, which becomes redundant when V is a {subfield L}, ensures that the argument of [subg _ ] is syntactically a group.
Inductive gal_of := Gal of [subg kAEnd_group 1 <<V>> / kAEndf (agenv V)].
Definition gal (f : 'AEnd(L)) := Gal (subg _ (coset _ f)).
Definition gal_sgval x := let: Gal u := x in u.

Fact gal_sgvalK : cancel gal_sgval Gal.
Let gal_sgval_inj := can_inj gal_sgvalK.

Definition gal_eqMixin := CanEqMixin gal_sgvalK.
Canonical gal_eqType := Eval hnf in EqType gal_of gal_eqMixin.
Definition gal_choiceMixin := CanChoiceMixin gal_sgvalK.
Canonical gal_choiceType := Eval hnf in ChoiceType gal_of gal_choiceMixin.
Definition gal_countMixin := CanCountMixin gal_sgvalK.
Canonical gal_countType := Eval hnf in CountType gal_of gal_countMixin.
Definition gal_finMixin := CanFinMixin gal_sgvalK.
Canonical gal_finType := Eval hnf in FinType gal_of gal_finMixin.

Definition gal_one := Gal 1%g.
Definition gal_inv x := Gal (gal_sgval x)^-1.
Definition gal_mul x y := Gal (gal_sgval x × gal_sgval y).
Fact gal_oneP : left_id gal_one gal_mul.
Fact gal_invP : left_inverse gal_one gal_inv gal_mul.
Fact gal_mulP : associative gal_mul.

Definition gal_finGroupMixin :=
  FinGroup.Mixin gal_mulP gal_oneP gal_invP.
Canonical gal_finBaseGroupType :=
  Eval hnf in BaseFinGroupType gal_of gal_finGroupMixin.
Canonical gal_finGroupType := Eval hnf in FinGroupType gal_invP.

Coercion gal_repr u : 'AEnd(L) := repr (sgval (gal_sgval u)).

Fact gal_is_morphism : {in kAEnd 1 (agenv V) &, {morph gal : x y / x × y}%g}.
Canonical gal_morphism := Morphism gal_is_morphism.

Lemma gal_reprK : cancel gal_repr gal.

Lemma gal_repr_inj : injective gal_repr.

Lemma gal_AEnd x : gal_repr x \in kAEnd 1 (agenv V).

End gal_of_Definition.

Lemma gal_eqP E {x y : gal_of E} : reflect {in E, x =1 y} (x == y).

Lemma galK E (f : 'AEnd(L)) : (f @: E E)%VS {in E, gal E f =1 f}.

Lemma eq_galP E (f g : 'AEnd(L)) :
   (f @: E E)%VS (g @: E E)%VS
  reflect {in E, f =1 g} (gal E f == gal E g).

Lemma limg_gal E (x : gal_of E) : (x @: E)%VS = E.

Lemma memv_gal E (x : gal_of E) a : a \in E x a \in E.

Lemma gal_id E a : (1 : gal_of E)%g a = a.

Lemma galM E (x y : gal_of E) a : a \in E (x × y)%g a = y (x a).

Lemma galV E (x : gal_of E) : {in E, (x^-1)%g =1 x^-1%VF}.

Standard mathematical notation for 'Gal(E / K) puts the larger field first.
Definition galoisG V U := gal V @* <<kAEnd (U :&: V) V>>.
Canonical galoisG_group E U := Eval hnf in [group of (galoisG E U)].

Section Automorphism.

Lemma gal_cap U V : 'Gal(V / U) = 'Gal(V / U :&: V).

Lemma gal_kAut K E x : (K E)%VS (x \in 'Gal(E / K)) = kAut K E x.

Lemma gal_kHom K E x : (K E)%VS (x \in 'Gal(E / K)) = kHom K E x.

Lemma kAut_to_gal K E f :
  kAut K E f {x : gal_of E | x \in 'Gal(E / K) & {in E, f =1 x}}.

Lemma fixed_gal K E x a :
  (K E)%VS x \in 'Gal(E / K) a \in K x a = a.

Lemma fixedPoly_gal K E x p :
  (K E)%VS x \in 'Gal(E / K) p \is a polyOver K map_poly x p = p.

Lemma root_minPoly_gal K E x a :
  (K E)%VS x \in 'Gal(E / K) a \in E root (minPoly K a) (x a).

End Automorphism.

Lemma gal_adjoin_eq K a x y :
    x \in 'Gal(<<K; a>> / K) y \in 'Gal(<<K; a>> / K)
  (x == y) = (x a == y a).

Lemma galS K M E : (K M)%VS 'Gal(E / M) \subset 'Gal(E / K).

Lemma gal_conjg K E x : 'Gal(E / K) :^ x = 'Gal(E / x @: K).

Definition fixedField V (A : {set gal_of V}) :=
  (V :&: \bigcap_(x in A) fixedSpace x)%VS.

Lemma fixedFieldP E {A : {set gal_of E}} a :
  a \in E reflect ( x, x \in A x a = a) (a \in fixedField A).

Lemma mem_fixedFieldP E (A : {set gal_of E}) a :
  a \in fixedField A a \in E ( x, x \in A x a = a).

Fact fixedField_is_aspace E (A : {set gal_of E}) : is_aspace (fixedField A).
Canonical fixedField_aspace E A : {subfield L} :=
  ASpace (@fixedField_is_aspace E A).

Lemma fixedField_bound E (A : {set gal_of E}) : (fixedField A E)%VS.

Lemma fixedFieldS E (A B : {set gal_of E}) :
   A \subset B (fixedField B fixedField A)%VS.

Lemma galois_connection_subv K E :
  (K E)%VS (K fixedField ('Gal(E / K)))%VS.

Lemma galois_connection_subset E (A : {set gal_of E}):
  A \subset 'Gal(E / fixedField A).

Lemma galois_connection K E (A : {set gal_of E}):
  (K E)%VS (A \subset 'Gal(E / K)) = (K fixedField A)%VS.

Definition galTrace U V a := \sum_(x in 'Gal(V / U)) (x a).

Definition galNorm U V a := \prod_(x in 'Gal(V / U)) (x a).

Section TraceAndNormMorphism.

Variables U V : {vspace L}.

Fact galTrace_is_additive : additive (galTrace U V).
Canonical galTrace_additive := Additive galTrace_is_additive.

Lemma galNorm1 : galNorm U V 1 = 1.

Lemma galNormM : {morph galNorm U V : a b / a × b}.

Lemma galNormV : {morph galNorm U V : a / a^-1}.

Lemma galNormX n : {morph galNorm U V : a / a ^+ n}.

Lemma galNorm_prod (I : Type) (r : seq I) (P : pred I) (B : I L) :
  galNorm U V (\prod_(i <- r | P i) B i)
   = \prod_(i <- r | P i) galNorm U V (B i).

Lemma galNorm0 : galNorm U V 0 = 0.

Lemma galNorm_eq0 a : (galNorm U V a == 0) = (a == 0).

End TraceAndNormMorphism.

Section TraceAndNormField.

Variables K E : {subfield L}.

Lemma galTrace_fixedField a :
  a \in E galTrace K E a \in fixedField 'Gal(E / K).

Lemma galTrace_gal a x :
  a \in E x \in 'Gal(E / K) galTrace K E (x a) = galTrace K E a.

Lemma galNorm_fixedField a :
  a \in E galNorm K E a \in fixedField 'Gal(E / K).

Lemma galNorm_gal a x :
  a \in E x \in 'Gal(E / K) galNorm K E (x a) = galNorm K E a.

End TraceAndNormField.

Definition normalField U V := [ x in kAEndf U, x @: V == V]%VS.

Lemma normalField_kAut K M E f :
  (K M E)%VS normalField K M kAut K E f kAut K M f.

Lemma normalFieldP K E :
  reflect {in E, a, exists2 r,
            all (mem E) r & minPoly K a = \prod_(b <- r) ('X - b%:P)}
          (normalField K E).

Lemma normalFieldf K : normalField K {:L}.

Lemma normalFieldS K M E : (K M)%VS normalField K E normalField M E.

Lemma splitting_normalField E K :
   (K E)%VS
  reflect (exists2 p, p \is a polyOver K & splittingFieldFor K p E)
          (normalField K E).

Lemma kHom_to_gal K M E f :
    (K M E)%VS normalField K E kHom K M f
  {x | x \in 'Gal(E / K) & {in M, f =1 x}}.

Lemma normalField_root_minPoly K E a b :
    (K E)%VS normalField K E a \in E root (minPoly K a) b
  exists2 x, x \in 'Gal(E / K) & x a = b.

Implicit Arguments normalFieldP [K E].

Lemma normalField_factors K E :
   (K E)%VS
 reflect {in E, a, exists2 r : seq (gal_of E),
            r \subset 'Gal(E / K)
          & minPoly K a = \prod_(x <- r) ('X - (x a)%:P)}
   (normalField K E).

Definition galois U V := [&& (U V)%VS, separable U V & normalField U V].

Lemma galoisS K M E : (K M E)%VS galois K E galois M E.

Lemma galois_dim K E : galois K E \dim_K E = #|'Gal(E / K)|.

Lemma galois_factors K E :
    (K E)%VS
  reflect {in E, a, r, let r_a := [seq x a | x : gal_of E <- r] in
            [/\ r \subset 'Gal(E / K), uniq r_a
              & minPoly K a = \prod_(b <- r_a) ('X - b%:P)]}
          (galois K E).

Lemma splitting_galoisField K E :
  reflect ( p, [/\ p \is a polyOver K, separable_poly p
                       & splittingFieldFor K p E])
          (galois K E).

Lemma galois_fixedField K E :
  reflect (fixedField 'Gal(E / K) = K) (galois K E).

Lemma mem_galTrace K E a : galois K E a \in E galTrace K E a \in K.

Lemma mem_galNorm K E a : galois K E a \in E galNorm K E a \in K.

Lemma gal_independent_contra E (P : pred (gal_of E)) (c_ : gal_of E L) x :
    P x c_ x != 0
  exists2 a, a \in E & \sum_(y | P y) c_ y × y a != 0.

Lemma gal_independent E (P : pred (gal_of E)) (c_ : gal_of E L) :
    ( a, a \in E \sum_(x | P x) c_ x × x a = 0)
  ( x, P x c_ x = 0).

Lemma Hilbert's_theorem_90 K E x a :
   generator 'Gal(E / K) x a \in E
 reflect (exists2 b, b \in E b != 0 & a = b / x b) (galNorm K E a == 1).

Section Matrix.

Variable (E : {subfield L}) (A : {set gal_of E}).

Let K := fixedField A.

Lemma gal_matrix :
  {w : #|A|.-tuple L | {subset w E} 0 \notin w &
    [/\ \matrix_(i, j < #|A|) enum_val i (tnth w j) \in unitmx,
        directv (\sum_i K × <[tnth w i]>) &
        group_set A (\sum_i K × <[tnth w i]>)%VS = E] }.

End Matrix.

Lemma dim_fixedField E (G : {group gal_of E}) : #|G| = \dim_(fixedField G) E.

Lemma dim_fixed_galois K E (G : {group gal_of E}) :
    galois K E G \subset 'Gal(E / K)
  \dim_K (fixedField G) = #|'Gal(E / K) : G|.

Lemma gal_fixedField E (G : {group gal_of E}): 'Gal(E / fixedField G) = G.

Lemma gal_generated E (A : {set gal_of E}) : 'Gal(E / fixedField A) = <<A>>.

Lemma fixedField_galois E (A : {set gal_of E}): galois (fixedField A) E.

Section FundamentalTheoremOfGaloisTheory.

Variables E K : {subfield L}.
Hypothesis galKE : galois K E.

Section IntermediateField.

Variable M : {subfield L}.
Hypothesis (sKME : (K M E)%VS) (nKM : normalField K M).

Lemma normalField_galois : galois K M.

Definition normalField_cast (x : gal_of E) : gal_of M := gal M x.

Lemma normalField_cast_eq x :
  x \in 'Gal(E / K) {in M, normalField_cast x =1 x}.

Lemma normalField_castM :
  {in 'Gal(E / K) &, {morph normalField_cast : x y / (x × y)%g}}.
Canonical normalField_cast_morphism := Morphism normalField_castM.

Lemma normalField_ker : 'ker normalField_cast = 'Gal(E / M).

Lemma normalField_normal : 'Gal(E / M) <| 'Gal(E / K).

Lemma normalField_img : normalField_cast @* 'Gal(E / K) = 'Gal(M / K).

Lemma normalField_isom :
  {f : {morphism ('Gal(E / K) / 'Gal(E / M)) >-> gal_of M} |
     isom ('Gal(E / K) / 'Gal (E / M)) 'Gal(M / K) f
   & ( A, f @* (A / 'Gal(E / M)) = normalField_cast @* A)
   {in 'Gal(E / K) & M, x, f (coset 'Gal (E / M) x) =1 x} }%g.

Lemma normalField_isog : 'Gal(E / K) / 'Gal(E / M) \isog 'Gal(M / K).

End IntermediateField.

Section IntermediateGroup.

Variable G : {group gal_of E}.
Hypothesis nsGgalE : G <| 'Gal(E / K).

Lemma normal_fixedField_galois : galois K (fixedField G).

End IntermediateGroup.

End FundamentalTheoremOfGaloisTheory.

End GaloisTheory.

Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope.
Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope.

Implicit Arguments fixedFieldP [F L E A a].
Implicit Arguments normalFieldP [F L K E].
Implicit Arguments splitting_galoisField [F L K E].
Implicit Arguments galois_fixedField [F L K E].