Library mathcomp.field.galois
(* (c) Copyright 2006-2015 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.
Implicit Arguments kHomP [F L K V f].
Implicit Arguments kAHomP [F L U V f].
Implicit Arguments kHom_lrmorphism [F L f].
Module SplittingField.
Import GRing.
Section ClassDef.
Variable F : fieldType.
Definition axiom (L : fieldExtType F) :=
exists2 p : {poly L}, p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}.
Record class_of (L : Type) : Type :=
Class {base : FieldExt.class_of F L; _ : axiom (FieldExt.Pack _ base L)}.
Structure type (phF : phant F) := Pack {sort; _ : class_of sort; _ : Type}.
Variable (phF : phant F) (T : Type) (cT : type phF).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).
Definition clone c of phant_id class c := @Pack phF T c T.
Definition pack b0 (ax0 : axiom (@FieldExt.Pack F (Phant F) T b0 T)) :=
fun bT b & phant_id (@FieldExt.class F phF bT) b ⇒
fun ax & phant_id ax0 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.
Implicit Arguments normalFieldP [K E].
Lemma normalField_factors K E :
(K ≤ E)%VS →
reflect {in E, ∀ a, exists2 r : seq (gal_of E),
r \subset 'Gal(E / K)
& minPoly K a = \prod_(x <- r) ('X - (x a)%:P)}
(normalField K E).
Definition galois U V := [&& (U ≤ V)%VS, separable U V & normalField U V].
Lemma galoisS K M E : (K ≤ M ≤ E)%VS → galois K E → galois M E.
Lemma galois_dim K E : galois K E → \dim_K E = #|'Gal(E / K)|.
Lemma galois_factors K E :
(K ≤ E)%VS →
reflect {in E, ∀ a, ∃ r, let r_a := [seq x a | x : gal_of E <- r] in
[/\ r \subset 'Gal(E / K), uniq r_a
& minPoly K a = \prod_(b <- r_a) ('X - b%:P)]}
(galois K E).
Lemma splitting_galoisField K E :
reflect (∃ p, [/\ p \is a polyOver K, separable_poly p
& splittingFieldFor K p E])
(galois K E).
Lemma galois_fixedField K E :
reflect (fixedField 'Gal(E / K) = K) (galois K E).
Lemma mem_galTrace K E a : galois K E → a \in E → galTrace K E a \in K.
Lemma mem_galNorm K E a : galois K E → a \in E → galNorm K E a \in K.
Lemma gal_independent_contra E (P : pred (gal_of E)) (c_ : gal_of E → L) x :
P x → c_ x != 0 →
exists2 a, a \in E & \sum_(y | P y) c_ y × y a != 0.
Lemma gal_independent E (P : pred (gal_of E)) (c_ : gal_of E → L) :
(∀ a, a \in E → \sum_(x | P x) c_ x × x a = 0) →
(∀ x, P x → c_ x = 0).
Lemma Hilbert's_theorem_90 K E x a :
generator 'Gal(E / K) x → a \in E →
reflect (exists2 b, b \in E ∧ b != 0 & a = b / x b) (galNorm K E a == 1).
Section Matrix.
Variable (E : {subfield L}) (A : {set gal_of E}).
Let K := fixedField A.
Lemma gal_matrix :
{w : #|A|.-tuple L | {subset w ≤ E} ∧ 0 \notin w &
[/\ \matrix_(i, j < #|A|) enum_val i (tnth w j) \in unitmx,
directv (\sum_i K × <[tnth w i]>) &
group_set A → (\sum_i K × <[tnth w i]>)%VS = E] }.
End Matrix.
Lemma dim_fixedField E (G : {group gal_of E}) : #|G| = \dim_(fixedField G) E.
Lemma dim_fixed_galois K E (G : {group gal_of E}) :
galois K E → G \subset 'Gal(E / K) →
\dim_K (fixedField G) = #|'Gal(E / K) : G|.
Lemma gal_fixedField E (G : {group gal_of E}): 'Gal(E / fixedField G) = G.
Lemma gal_generated E (A : {set gal_of E}) : 'Gal(E / fixedField A) = <<A>>.
Lemma fixedField_galois E (A : {set gal_of E}): galois (fixedField A) E.
Section FundamentalTheoremOfGaloisTheory.
Variables E K : {subfield L}.
Hypothesis galKE : galois K E.
Section IntermediateField.
Variable M : {subfield L}.
Hypothesis (sKME : (K ≤ M ≤ E)%VS) (nKM : normalField K M).
Lemma normalField_galois : galois K M.
Definition normalField_cast (x : gal_of E) : gal_of M := gal M x.
Lemma normalField_cast_eq x :
x \in 'Gal(E / K) → {in M, normalField_cast x =1 x}.
Lemma normalField_castM :
{in 'Gal(E / K) &, {morph normalField_cast : x y / (x × y)%g}}.
Canonical normalField_cast_morphism := Morphism normalField_castM.
Lemma normalField_ker : 'ker normalField_cast = 'Gal(E / M).
Lemma normalField_normal : 'Gal(E / M) <| 'Gal(E / K).
Lemma normalField_img : normalField_cast @* 'Gal(E / K) = 'Gal(M / K).
Lemma normalField_isom :
{f : {morphism ('Gal(E / K) / 'Gal(E / M)) >-> gal_of M} |
isom ('Gal(E / K) / 'Gal (E / M)) 'Gal(M / K) f
& (∀ A, f @* (A / 'Gal(E / M)) = normalField_cast @* A)
∧ {in 'Gal(E / K) & M, ∀ x, f (coset 'Gal (E / M) x) =1 x} }%g.
Lemma normalField_isog : 'Gal(E / K) / 'Gal(E / M) \isog 'Gal(M / K).
End IntermediateField.
Section IntermediateGroup.
Variable G : {group gal_of E}.
Hypothesis nsGgalE : G <| 'Gal(E / K).
Lemma normal_fixedField_galois : galois K (fixedField G).
End IntermediateGroup.
End FundamentalTheoremOfGaloisTheory.
End GaloisTheory.
Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope.
Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope.
Implicit Arguments fixedFieldP [F L E A a].
Implicit Arguments normalFieldP [F L K E].
Implicit Arguments splitting_galoisField [F L K E].
Implicit Arguments galois_fixedField [F L K E].
Canonical galoisG_group E U := Eval hnf in [group of (galoisG E U)].
Section Automorphism.
Lemma gal_cap U V : 'Gal(V / U) = 'Gal(V / U :&: V).
Lemma gal_kAut K E x : (K ≤ E)%VS → (x \in 'Gal(E / K)) = kAut K E x.
Lemma gal_kHom K E x : (K ≤ E)%VS → (x \in 'Gal(E / K)) = kHom K E x.
Lemma kAut_to_gal K E f :
kAut K E f → {x : gal_of E | x \in 'Gal(E / K) & {in E, f =1 x}}.
Lemma fixed_gal K E x a :
(K ≤ E)%VS → x \in 'Gal(E / K) → a \in K → x a = a.
Lemma fixedPoly_gal K E x p :
(K ≤ E)%VS → x \in 'Gal(E / K) → p \is a polyOver K → map_poly x p = p.
Lemma root_minPoly_gal K E x a :
(K ≤ E)%VS → x \in 'Gal(E / K) → a \in E → root (minPoly K a) (x a).
End Automorphism.
Lemma gal_adjoin_eq K a x y :
x \in 'Gal(<<K; a>> / K) → y \in 'Gal(<<K; a>> / K) →
(x == y) = (x a == y a).
Lemma galS K M E : (K ≤ M)%VS → 'Gal(E / M) \subset 'Gal(E / K).
Lemma gal_conjg K E x : 'Gal(E / K) :^ x = 'Gal(E / x @: K).
Definition fixedField V (A : {set gal_of V}) :=
(V :&: \bigcap_(x in A) fixedSpace x)%VS.
Lemma fixedFieldP E {A : {set gal_of E}} a :
a \in E → reflect (∀ x, x \in A → x a = a) (a \in fixedField A).
Lemma mem_fixedFieldP E (A : {set gal_of E}) a :
a \in fixedField A → a \in E ∧ (∀ x, x \in A → x a = a).
Fact fixedField_is_aspace E (A : {set gal_of E}) : is_aspace (fixedField A).
Canonical fixedField_aspace E A : {subfield L} :=
ASpace (@fixedField_is_aspace E A).
Lemma fixedField_bound E (A : {set gal_of E}) : (fixedField A ≤ E)%VS.
Lemma fixedFieldS E (A B : {set gal_of E}) :
A \subset B → (fixedField B ≤ fixedField A)%VS.
Lemma galois_connection_subv K E :
(K ≤ E)%VS → (K ≤ fixedField ('Gal(E / K)))%VS.
Lemma galois_connection_subset E (A : {set gal_of E}):
A \subset 'Gal(E / fixedField A).
Lemma galois_connection K E (A : {set gal_of E}):
(K ≤ E)%VS → (A \subset 'Gal(E / K)) = (K ≤ fixedField A)%VS.
Definition galTrace U V a := \sum_(x in 'Gal(V / U)) (x a).
Definition galNorm U V a := \prod_(x in 'Gal(V / U)) (x a).
Section TraceAndNormMorphism.
Variables U V : {vspace L}.
Fact galTrace_is_additive : additive (galTrace U V).
Canonical galTrace_additive := Additive galTrace_is_additive.
Lemma galNorm1 : galNorm U V 1 = 1.
Lemma galNormM : {morph galNorm U V : a b / a × b}.
Lemma galNormV : {morph galNorm U V : a / a^-1}.
Lemma galNormX n : {morph galNorm U V : a / a ^+ n}.
Lemma galNorm_prod (I : Type) (r : seq I) (P : pred I) (B : I → L) :
galNorm U V (\prod_(i <- r | P i) B i)
= \prod_(i <- r | P i) galNorm U V (B i).
Lemma galNorm0 : galNorm U V 0 = 0.
Lemma galNorm_eq0 a : (galNorm U V a == 0) = (a == 0).
End TraceAndNormMorphism.
Section TraceAndNormField.
Variables K E : {subfield L}.
Lemma galTrace_fixedField a :
a \in E → galTrace K E a \in fixedField 'Gal(E / K).
Lemma galTrace_gal a x :
a \in E → x \in 'Gal(E / K) → galTrace K E (x a) = galTrace K E a.
Lemma galNorm_fixedField a :
a \in E → galNorm K E a \in fixedField 'Gal(E / K).
Lemma galNorm_gal a x :
a \in E → x \in 'Gal(E / K) → galNorm K E (x a) = galNorm K E a.
End TraceAndNormField.
Definition normalField U V := [∀ x in kAEndf U, x @: V == V]%VS.
Lemma normalField_kAut K M E f :
(K ≤ M ≤ E)%VS → normalField K M → kAut K E f → kAut K M f.
Lemma normalFieldP K E :
reflect {in E, ∀ a, exists2 r,
all (mem E) r & minPoly K a = \prod_(b <- r) ('X - b%:P)}
(normalField K E).
Lemma normalFieldf K : normalField K {:L}.
Lemma normalFieldS K M E : (K ≤ M)%VS → normalField K E → normalField M E.
Lemma splitting_normalField E K :
(K ≤ E)%VS →
reflect (exists2 p, p \is a polyOver K & splittingFieldFor K p E)
(normalField K E).
Lemma kHom_to_gal K M E f :
(K ≤ M ≤ E)%VS → normalField K E → kHom K M f →
{x | x \in 'Gal(E / K) & {in M, f =1 x}}.
Lemma normalField_root_minPoly K E a b :
(K ≤ E)%VS → normalField K E → a \in E → root (minPoly K a) b →
exists2 x, x \in 'Gal(E / K) & x a = b.
Implicit Arguments normalFieldP [K E].
Lemma normalField_factors K E :
(K ≤ E)%VS →
reflect {in E, ∀ a, exists2 r : seq (gal_of E),
r \subset 'Gal(E / K)
& minPoly K a = \prod_(x <- r) ('X - (x a)%:P)}
(normalField K E).
Definition galois U V := [&& (U ≤ V)%VS, separable U V & normalField U V].
Lemma galoisS K M E : (K ≤ M ≤ E)%VS → galois K E → galois M E.
Lemma galois_dim K E : galois K E → \dim_K E = #|'Gal(E / K)|.
Lemma galois_factors K E :
(K ≤ E)%VS →
reflect {in E, ∀ a, ∃ r, let r_a := [seq x a | x : gal_of E <- r] in
[/\ r \subset 'Gal(E / K), uniq r_a
& minPoly K a = \prod_(b <- r_a) ('X - b%:P)]}
(galois K E).
Lemma splitting_galoisField K E :
reflect (∃ p, [/\ p \is a polyOver K, separable_poly p
& splittingFieldFor K p E])
(galois K E).
Lemma galois_fixedField K E :
reflect (fixedField 'Gal(E / K) = K) (galois K E).
Lemma mem_galTrace K E a : galois K E → a \in E → galTrace K E a \in K.
Lemma mem_galNorm K E a : galois K E → a \in E → galNorm K E a \in K.
Lemma gal_independent_contra E (P : pred (gal_of E)) (c_ : gal_of E → L) x :
P x → c_ x != 0 →
exists2 a, a \in E & \sum_(y | P y) c_ y × y a != 0.
Lemma gal_independent E (P : pred (gal_of E)) (c_ : gal_of E → L) :
(∀ a, a \in E → \sum_(x | P x) c_ x × x a = 0) →
(∀ x, P x → c_ x = 0).
Lemma Hilbert's_theorem_90 K E x a :
generator 'Gal(E / K) x → a \in E →
reflect (exists2 b, b \in E ∧ b != 0 & a = b / x b) (galNorm K E a == 1).
Section Matrix.
Variable (E : {subfield L}) (A : {set gal_of E}).
Let K := fixedField A.
Lemma gal_matrix :
{w : #|A|.-tuple L | {subset w ≤ E} ∧ 0 \notin w &
[/\ \matrix_(i, j < #|A|) enum_val i (tnth w j) \in unitmx,
directv (\sum_i K × <[tnth w i]>) &
group_set A → (\sum_i K × <[tnth w i]>)%VS = E] }.
End Matrix.
Lemma dim_fixedField E (G : {group gal_of E}) : #|G| = \dim_(fixedField G) E.
Lemma dim_fixed_galois K E (G : {group gal_of E}) :
galois K E → G \subset 'Gal(E / K) →
\dim_K (fixedField G) = #|'Gal(E / K) : G|.
Lemma gal_fixedField E (G : {group gal_of E}): 'Gal(E / fixedField G) = G.
Lemma gal_generated E (A : {set gal_of E}) : 'Gal(E / fixedField A) = <<A>>.
Lemma fixedField_galois E (A : {set gal_of E}): galois (fixedField A) E.
Section FundamentalTheoremOfGaloisTheory.
Variables E K : {subfield L}.
Hypothesis galKE : galois K E.
Section IntermediateField.
Variable M : {subfield L}.
Hypothesis (sKME : (K ≤ M ≤ E)%VS) (nKM : normalField K M).
Lemma normalField_galois : galois K M.
Definition normalField_cast (x : gal_of E) : gal_of M := gal M x.
Lemma normalField_cast_eq x :
x \in 'Gal(E / K) → {in M, normalField_cast x =1 x}.
Lemma normalField_castM :
{in 'Gal(E / K) &, {morph normalField_cast : x y / (x × y)%g}}.
Canonical normalField_cast_morphism := Morphism normalField_castM.
Lemma normalField_ker : 'ker normalField_cast = 'Gal(E / M).
Lemma normalField_normal : 'Gal(E / M) <| 'Gal(E / K).
Lemma normalField_img : normalField_cast @* 'Gal(E / K) = 'Gal(M / K).
Lemma normalField_isom :
{f : {morphism ('Gal(E / K) / 'Gal(E / M)) >-> gal_of M} |
isom ('Gal(E / K) / 'Gal (E / M)) 'Gal(M / K) f
& (∀ A, f @* (A / 'Gal(E / M)) = normalField_cast @* A)
∧ {in 'Gal(E / K) & M, ∀ x, f (coset 'Gal (E / M) x) =1 x} }%g.
Lemma normalField_isog : 'Gal(E / K) / 'Gal(E / M) \isog 'Gal(M / K).
End IntermediateField.
Section IntermediateGroup.
Variable G : {group gal_of E}.
Hypothesis nsGgalE : G <| 'Gal(E / K).
Lemma normal_fixedField_galois : galois K (fixedField G).
End IntermediateGroup.
End FundamentalTheoremOfGaloisTheory.
End GaloisTheory.
Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope.
Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope.
Implicit Arguments fixedFieldP [F L E A a].
Implicit Arguments normalFieldP [F L K E].
Implicit Arguments splitting_galoisField [F L K E].
Implicit Arguments galois_fixedField [F L K E].