(Joint Center)Library MathComp.galois

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import tuple finfun bigop ssralg poly polydiv.
Require Import finset fingroup morphism quotient perm action zmodp cyclic.
Require Import matrix mxalgebra vector falgebra fieldext separable.

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 EsplittingFieldFor 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 fp \is a polyOver Kmap_poly f p = p.

Lemma kHomSl U1 U2 V f : (U1 U2)%VSkHom U2 V fkHom U1 V f.

Lemma kHomSr K V1 V2 f : (V1 V2)%VSkHom K V2 fkHom K V1 f.

Lemma kHomS K1 K2 V1 V2 f :
  (K1 K2)%VS → (V1 V2)%VSkHom K2 V2 fkHom 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 frmorphism (f \o vsval : subvs_of EL).
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 fp \is a polyOver Ex \in Ef p.[x] = (map_poly f p).[f x].

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

Lemma kHom_root_id K E f p x :
   (K E)%VSkHom K E fp \is a polyOver Kx \in Eroot 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).
Local Notation Px := (minPoly E x).
Hypothesis fPx_y_0 : root (map_poly f Px) y.

Lemma kHomExtend_id z : z \in EkHomExtend z = f z.

Lemma kHomExtend_val : kHomExtend x = y.

Lemma kHomExtend_poly p :
  p \in polyOver EkHomExtend 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)%VSkAut U2 V fkAut U1 V f.

Lemma kHom_kAut_sub K E f : kAut K E fkHom 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} flker f == 0%VS.

Lemma inv_kHomf K f : kHom K {:L} fkHom 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) fkHom K E gkHom K E (f \o g).

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

Lemma kHom_extends K E f p U :
    (K E)%VSkHom K E f
     p \is a polyOver KsplittingFieldFor 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)}.
Local Coercion base : class_of >-> FieldExt.class_of.

Structure type (phF : phant F) := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
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.

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 gg \in coset (kAEndf E) g.

Lemma aut_mem_eqP E (x y : coset_of (kAEndf E)) f g :
  f \in xg \in yreflect {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 Ex 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>>.
Local Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope.
Canonical galoisG_group E U := Eval hnf in [group of (galoisG E U)].
Local Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope.

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)%VSx \in 'Gal(E / K)a \in Kx a = a.

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

Lemma root_minPoly_gal K E x a :
  (K E)%VSx \in 'Gal(E / K)a \in Eroot (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 Ereflect ( x, x \in Ax a = a) (a \in fixedField A).

Lemma mem_fixedFieldP E (A : {set gal_of E}) a :
  a \in fixedField Aa \in E ( x, x \in Ax 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 : IL) :
  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 EgalTrace K E a \in fixedField 'Gal(E / K).

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

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

Lemma galNorm_gal a x :
  a \in Ex \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)%VSnormalField K MkAut K E fkAut 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)%VSnormalField K EnormalField 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)%VSnormalField K EkHom K M f
  {x | x \in 'Gal(E / K) & {in M, f =1 x}}.

Lemma normalField_root_minPoly K E a b :
    (K E)%VSnormalField K Ea \in Eroot (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)%VSgalois K Egalois 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 Ea \in EgalTrace K E a \in K.

Lemma mem_galNorm K E a : galois K Ea \in EgalNorm K E a \in K.

Lemma gal_independent_contra E (P : pred (gal_of E)) (c_ : gal_of EL) x :
    P xc_ 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 EL) :
    ( a, a \in E\sum_(x | P x) c_ x × x a = 0) →
  ( x, P xc_ x = 0).

Lemma Hilbert's_theorem_90 K E x a :
   generator 'Gal(E / K) xa \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 EG \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].