Library mathcomp.field.galois
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
From HB Require Import structures.
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 HB Require Import structures.
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.
Basic Galois field theory
This file defines:
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
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
The HB class is called SplittingField.
splitting_field_axiom F L == the axiom stating that L is a splitting field
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 (multiplicative f) (kHom 1 {:L} f).
Lemma kHom_lrmorphism (f : 'End(L)) : reflect (lrmorphism f) (kHom 1 {:L} f).
Proof. by rewrite k1HomE; apply: ahomP. Qed.
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.
Section kHomMorphism.
Variables (K E : {subfield L}) (f : 'End(L)).
Let kHomf : subvs_of E → L := f \o vsval.
Lemma kHom_is_additive : kHom K E f → additive kHomf.
Lemma kHom_is_multiplicative : kHom K E f → multiplicative kHomf.
Variable (homKEf : kHom K E f).
Definition kHom_rmorphism := Eval hnf in (kHomf : {rmorphism _ → _}).
End kHomMorphism.
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).
Let kHomf z := (map_poly f (Fadjoin_poly E x z)).[y].
Fact kHomExtend_additive_subproof : additive kHomf.
Fact kHomExtend_scalable_subproof : scalable kHomf.
Let kHomExtendLinear := Eval hnf in (kHomf : {linear _ → _}).
Definition kHomExtend := linfun kHomExtendLinear.
Lemma kHomExtendE z : kHomExtend z = (map_poly f (Fadjoin_poly E x z)).[y].
Hypotheses (sKE : (K ≤ E)%VS) (homKf : kHom K E f).
Local Notation Px := (minPoly E x).
Hypothesis fPx_y_0 : root (map_poly f Px) y.
Lemma kHomExtend_id z : z \in 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.
Arguments kHomP {F L K V f}.
Arguments kAHomP {F L U V f}.
Arguments kHom_lrmorphism {F L f}.
Definition splitting_field_axiom (F : fieldType) (L : fieldExtType F) :=
exists2 p : {poly L}, p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}.
#[mathcomp(axiom="splitting_field_axiom"), short(type="splittingFieldType")]
HB.structure Definition SplittingField F :=
{ T of FieldExt_isSplittingField F T & FieldExt F T }.
Module SplittingFieldExports.
Bind Scope ring_scope with SplittingField.sort.
End SplittingFieldExports.
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 : fieldType) : SplittingField.axiom F^o.
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 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.
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.
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 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 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_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.
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_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.
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>>.
Local Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope.
Canonical galoisG_group E U := Eval hnf in [group of (galoisG E U)].
Local Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope.
Section Automorphism.
Lemma gal_cap U V : 'Gal(V / U) = 'Gal(V / U :&: V).
Lemma gal_kAut K E x : (K ≤ E)%VS → (x \in 'Gal(E / K)) = kAut K E x.
Lemma gal_kHom K E x : (K ≤ E)%VS → (x \in 'Gal(E / K)) = kHom K E x.
Lemma kAut_to_gal K E f :
kAut K E f → {x : gal_of E | x \in 'Gal(E / K) & {in E, f =1 x}}.
Lemma fixed_gal K E x a :
(K ≤ E)%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).
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 [in 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.
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.
Arguments gal_repr_inj {F L V} [x1 x2].
Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope.
Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope.
Arguments fixedFieldP {F L E A a}.
Arguments normalFieldP {F L K E}.
Arguments splitting_galoisField {F L K E}.
Arguments galois_fixedField {F L K E}.
Local Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope.
Canonical galoisG_group E U := Eval hnf in [group of (galoisG E U)].
Local Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope.
Section Automorphism.
Lemma gal_cap U V : 'Gal(V / U) = 'Gal(V / U :&: V).
Lemma gal_kAut K E x : (K ≤ E)%VS → (x \in 'Gal(E / K)) = kAut K E x.
Lemma gal_kHom K E x : (K ≤ E)%VS → (x \in 'Gal(E / K)) = kHom K E x.
Lemma kAut_to_gal K E f :
kAut K E f → {x : gal_of E | x \in 'Gal(E / K) & {in E, f =1 x}}.
Lemma fixed_gal K E x a :
(K ≤ E)%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).
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 [in 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.
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.
Arguments gal_repr_inj {F L V} [x1 x2].
Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope.
Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope.
Arguments fixedFieldP {F L E A a}.
Arguments normalFieldP {F L K E}.
Arguments splitting_galoisField {F L K E}.
Arguments galois_fixedField {F L K E}.