Library mathcomp.field.galois
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import choice fintype tuple finfun bigop ssralg poly.
From mathcomp Require Import polydiv finset fingroup morphism quotient perm.
From mathcomp Require Import action zmodp cyclic matrix mxalgebra vector.
From mathcomp Require Import falgebra fieldext separable.
Distributed under the terms of CeCILL-B. *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
From mathcomp Require Import choice fintype tuple finfun bigop ssralg poly.
From mathcomp Require Import polydiv finset fingroup morphism quotient perm.
From mathcomp Require Import action zmodp cyclic matrix mxalgebra vector.
From mathcomp Require Import 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 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; mixin : axiom (FieldExt.Pack _ base)}.
Structure type (phF : phant F) := Pack {sort; _ : class_of sort}.
Variable (phF : phant F) (T : Type) (cT : type phF).
Definition class := let: Pack _ c as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack phF T c.
Definition pack b0 (ax0 : axiom (@FieldExt.Pack F (Phant F) T b0)) :=
fun bT b & phant_id (@FieldExt.class F phF bT) b ⇒
fun ax & phant_id ax0 ax ⇒ Pack (Phant F) (@Class T b ax).
Definition eqType := @Equality.Pack cT class.
Definition choiceType := @Choice.Pack cT class.
Definition zmodType := @Zmodule.Pack cT class.
Definition ringType := @Ring.Pack cT class.
Definition unitRingType := @UnitRing.Pack cT class.
Definition comRingType := @ComRing.Pack cT class.
Definition comUnitRingType := @ComUnitRing.Pack cT class.
Definition idomainType := @IntegralDomain.Pack cT class.
Definition fieldType := @Field.Pack cT class.
Definition lmodType := @Lmodule.Pack F phF cT class.
Definition lalgType := @Lalgebra.Pack F phF cT class.
Definition algType := @Algebra.Pack F phF cT class.
Definition unitAlgType := @UnitAlgebra.Pack F phF cT class.
Definition comAlgType := @ComAlgebra.Pack F phF cT class.
Definition comUnitAlgType := @ComUnitAlgebra.Pack F phF cT class.
Definition vectType := @Vector.Pack F phF cT class.
Definition FalgType := @Falgebra.Pack F phF cT class.
Definition fieldExtType := @FieldExt.Pack F phF cT class.
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 comAlgType : type >-> ComAlgebra.type.
Canonical comAlgType.
Coercion unitAlgType : type >-> UnitAlgebra.type.
Canonical unitAlgType.
Coercion comUnitAlgType : type >-> ComUnitAlgebra.type.
Canonical comUnitAlgType.
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.