Library mathcomp.field.galois
+ +
+(* (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.
+ +
+
+ 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.
+ +
+ +
+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 ax ⇒ Pack (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.
+ +
+
+
++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.
+ +
+ +
+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 ax ⇒ Pack (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)].
+ +
+
+
++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}).
+ +
+
+
++ +
+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.
+
+
+
+
+ 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}.
+ +
+
+
++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.
+ +
+ +
+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.
+ +
+
++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.
+ +
+ +
+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.
+ +
+