Library mathcomp.field.galois
- -
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-
-
-- Distributed under the terms of CeCILL-B. *)
- -
-
- This file develops some basic Galois field theory, defining:
- splittingFieldFor K p E <-> E is the smallest field over K that splits p
- into linear factors.
- kHom K E f <=> f : 'End(L) is a ring morphism on E and fixes K.
- kAut K E f <=> f : 'End(L) is a kHom K E and f @: E == E.
- kHomExtend E f x y == a kHom K E; x that extends f and maps x to y,
- when f \is a kHom K E and root (minPoly E x) y.
-
-
-
- splittingFieldFor K p E <-> E is splitting field for p over K: p splits in
- E and its roots generate E from K.
- splittingFieldType F == the interface type of splitting field extensions
- of F, that is, extensions generated by all the
- algebraic roots of some polynomial, or,
- equivalently, normal field extensions of F.
- SplittingField.axiom F L == the axiom stating that L is a splitting field.
- SplittingFieldType F L FsplitL == packs a proof FsplitL of the splitting
- field axiom for L into a splitingFieldType F,
- provided L has a fieldExtType F structure.
- [splittingFieldType F of L] == a clone of the canonical splittingFieldType
- structure for L.
-[splittingFieldType F of L for M] == an L-clone of the canonical
- splittingFieldType structure on M.
-
-
-
- gal_of E == the group_type of automorphisms of E over the
- base field F.
- 'Gal(E / K) == the group of automorphisms of E that fix K.
- fixedField s == the field fixed by the set of automorphisms s.
- fixedField set0 = E when set0 : {set: gal_of E}
- normalField K E <=> E is invariant for every 'Gal(L / K) for every L.
- galois K E <=> E is a normal and separable field extension of K.
- galTrace K E a == \sum(f in 'Gal(E / K)) (f a).
- galNorm K E a == \prod(f in 'Gal(E / K)) (f a).
-
-
-
-
-
-Set Implicit Arguments.
- -
-Reserved Notation "''Gal' ( A / B )"
- (at level 8, A at level 35, format "''Gal' ( A / B )").
- -
-Import GroupScope GRing.Theory.
-Local Open Scope ring_scope.
- -
-Section SplittingFieldFor.
- -
-Variables (F : fieldType) (L : fieldExtType F).
- -
-Definition splittingFieldFor (U : {vspace L}) (p : {poly L}) (V : {vspace L}) :=
- exists2 rs, p %= \prod_(z <- rs) ('X - z%:P) & <<U & rs>>%VS = V.
- -
-Lemma splittingFieldForS (K M E : {subfield L}) p :
- (K ≤ M)%VS → (M ≤ E)%VS →
- splittingFieldFor K p E → splittingFieldFor M p E.
- -
-End SplittingFieldFor.
- -
-Section kHom.
- -
-Variables (F : fieldType) (L : fieldExtType F).
-Implicit Types (U V : {vspace L}) (K E : {subfield L}) (f g : 'End(L)).
- -
-Definition kHom U V f := ahom_in V f && (U ≤ fixedSpace f)%VS.
- -
-Lemma kHomP {K V f} :
- reflect [/\ {in V &, ∀ x y, f (x × y) = f x × f y}
- & {in K, ∀ x, f x = x}]
- (kHom K V f).
- -
-Lemma kAHomP {U V} {f : 'AEnd(L)} :
- reflect {in U, ∀ x, f x = x} (kHom U V f).
- -
-Lemma kHom1 U V : kHom U V \1.
- -
-Lemma k1HomE V f : kHom 1 V f = ahom_in V f.
- -
-Lemma kHom_lrmorphism (f : 'End(L)) : reflect (lrmorphism f) (kHom 1 {:L} f).
- -
-Lemma k1AHom V (f : 'AEnd(L)) : kHom 1 V f.
- -
-Lemma kHom_poly_id K E f p :
- kHom K E f → p \is a polyOver K → map_poly f p = p.
- -
-Lemma kHomSl U1 U2 V f : (U1 ≤ U2)%VS → kHom U2 V f → kHom U1 V f.
- -
-Lemma kHomSr K V1 V2 f : (V1 ≤ V2)%VS → kHom K V2 f → kHom K V1 f.
- -
-Lemma kHomS K1 K2 V1 V2 f :
- (K1 ≤ K2)%VS → (V1 ≤ V2)%VS → kHom K2 V2 f → kHom K1 V1 f.
- -
-Lemma kHom_eq K E f g :
- (K ≤ E)%VS → {in E, f =1 g} → kHom K E f = kHom K E g.
- -
-Lemma kHom_inv K E f : kHom K E f → {in E, {morph f : x / x^-1}}.
- -
-Lemma kHom_dim K E f : kHom K E f → \dim (f @: E) = \dim E.
- -
-Lemma kHom_is_rmorphism K E f :
- kHom K E f → rmorphism (f \o vsval : subvs_of E → L).
-Definition kHom_rmorphism K E f homKEf :=
- RMorphism (@kHom_is_rmorphism K E f homKEf).
- -
-Lemma kHom_horner K E f p x :
- kHom K E f → p \is a polyOver E → x \in E → f p.[x] = (map_poly f p).[f x].
- -
-Lemma kHom_root K E f p x :
- kHom K E f → p \is a polyOver E → x \in E → root p x →
- root (map_poly f p) (f x).
- -
-Lemma kHom_root_id K E f p x :
- (K ≤ E)%VS → kHom K E f → p \is a polyOver K → x \in E → root p x →
- root p (f x).
- -
-Section kHomExtend.
- -
-Variables (K E : {subfield L}) (f : 'End(L)) (x y : L).
- -
-Fact kHomExtend_subproof :
- linear (fun z ⇒ (map_poly f (Fadjoin_poly E x z)).[y]).
-Definition kHomExtend := linfun (Linear kHomExtend_subproof).
- -
-Lemma kHomExtendE z : kHomExtend z = (map_poly f (Fadjoin_poly E x z)).[y].
- -
-Hypotheses (sKE : (K ≤ E)%VS) (homKf : kHom K E f).
-Hypothesis fPx_y_0 : root (map_poly f Px) y.
- -
-Lemma kHomExtend_id z : z \in E → kHomExtend z = f z.
- -
-Lemma kHomExtend_val : kHomExtend x = y.
- -
-Lemma kHomExtend_poly p :
- p \in polyOver E → kHomExtend p.[x] = (map_poly f p).[y].
- -
-Lemma kHomExtendP : kHom K <<E; x>> kHomExtend.
- -
-End kHomExtend.
- -
-Definition kAut U V f := kHom U V f && (f @: V == V)%VS.
- -
-Lemma kAutE K E f : kAut K E f = kHom K E f && (f @: E ≤ E)%VS.
- -
-Lemma kAutS U1 U2 V f : (U1 ≤ U2)%VS → kAut U2 V f → kAut U1 V f.
- -
-Lemma kHom_kAut_sub K E f : kAut K E f → kHom K E f.
- -
-Lemma kAut_eq K E (f g : 'End(L)) :
- (K ≤ E)%VS → {in E, f =1 g} → kAut K E f = kAut K E g.
- -
-Lemma kAutfE K f : kAut K {:L} f = kHom K {:L} f.
- -
-Lemma kAut1E E (f : 'AEnd(L)) : kAut 1 E f = (f @: E ≤ E)%VS.
- -
-Lemma kAutf_lker0 K f : kHom K {:L} f → lker f == 0%VS.
- -
-Lemma inv_kHomf K f : kHom K {:L} f → kHom K {:L} f^-1.
- -
-Lemma inv_is_ahom (f : 'AEnd(L)) : ahom_in {:L} f^-1.
- -
-Canonical inv_ahom (f : 'AEnd(L)) : 'AEnd(L) := AHom (inv_is_ahom f).
-Notation "f ^-1" := (inv_ahom f) : lrfun_scope.
- -
-Lemma comp_kHom_img K E f g :
- kHom K (g @: E) f → kHom K E g → kHom K E (f \o g).
- -
-Lemma comp_kHom K E f g : kHom K {:L} f → kHom K E g → kHom K E (f \o g).
- -
-Lemma kHom_extends K E f p U :
- (K ≤ E)%VS → kHom K E f →
- p \is a polyOver K → splittingFieldFor E p U →
- {g | kHom K U g & {in E, f =1 g}}.
- -
-End kHom.
- -
-Notation "f ^-1" := (inv_ahom f) : lrfun_scope.
- -
- -
-Module SplittingField.
- -
-Import GRing.
- -
-Section ClassDef.
- -
-Variable F : fieldType.
- -
-Definition axiom (L : fieldExtType F) :=
- exists2 p : {poly L}, p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}.
- -
-Record class_of (L : Type) : Type :=
- Class {base : FieldExt.class_of F L; _ : axiom (FieldExt.Pack _ base)}.
- -
-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.
-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.
- -
-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 xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
-Definition ringType := @Ring.Pack cT xclass.
-Definition unitRingType := @UnitRing.Pack cT xclass.
-Definition comRingType := @ComRing.Pack cT xclass.
-Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
-Definition idomainType := @IntegralDomain.Pack cT xclass.
-Definition fieldType := @Field.Pack cT xclass.
-Definition lmodType := @Lmodule.Pack F phF cT xclass.
-Definition lalgType := @Lalgebra.Pack F phF cT xclass.
-Definition algType := @Algebra.Pack F phF cT xclass.
-Definition unitAlgType := @UnitAlgebra.Pack F phF cT xclass.
-Definition vectType := @Vector.Pack F phF cT xclass.
-Definition FalgType := @Falgebra.Pack F phF cT xclass.
-Definition fieldExtType := @FieldExt.Pack F phF cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
- -
-Coercion sort : type >-> Sortclass.
-Coercion base : class_of >-> FieldExt.class_of.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> Ring.type.
-Canonical ringType.
-Coercion unitRingType : type >-> UnitRing.type.
-Canonical unitRingType.
-Coercion comRingType : type >-> ComRing.type.
-Canonical comRingType.
-Coercion comUnitRingType : type >-> ComUnitRing.type.
-Canonical comUnitRingType.
-Coercion idomainType : type >-> IntegralDomain.type.
-Canonical idomainType.
-Coercion fieldType : type >-> Field.type.
-Canonical fieldType.
-Coercion lmodType : type >-> Lmodule.type.
-Canonical lmodType.
-Coercion lalgType : type >-> Lalgebra.type.
-Canonical lalgType.
-Coercion algType : type >-> Algebra.type.
-Canonical algType.
-Coercion unitAlgType : type >-> UnitAlgebra.type.
-Canonical unitAlgType.
-Coercion vectType : type >-> Vector.type.
-Canonical vectType.
-Coercion FalgType : type >-> Falgebra.type.
-Canonical FalgType.
-Coercion fieldExtType : type >-> FieldExt.type.
-Canonical fieldExtType.
- -
-Notation splittingFieldType F := (type (Phant F)).
-Notation SplittingFieldType F L ax := (@pack _ (Phant F) L _ ax _ _ id _ id).
-Notation "[ 'splittingFieldType' F 'of' L 'for' K ]" :=
- (@clone _ (Phant F) L K _ idfun)
- (at level 0, format "[ 'splittingFieldType' F 'of' L 'for' K ]")
- : form_scope.
-Notation "[ 'splittingFieldType' F 'of' L ]" :=
- (@clone _ (Phant F) L _ _ id)
- (at level 0, format "[ 'splittingFieldType' F 'of' L ]") : form_scope.
- -
-End Exports.
-End SplittingField.
-Export SplittingField.Exports.
- -
-Lemma normal_field_splitting (F : fieldType) (L : fieldExtType F) :
- (∀ (K : {subfield L}) x,
- ∃ r, minPoly K x == \prod_(y <- r) ('X - y%:P)) →
- SplittingField.axiom L.
- -
-Fact regular_splittingAxiom F : SplittingField.axiom (regular_fieldExtType F).
- -
-Canonical regular_splittingFieldType (F : fieldType) :=
- SplittingFieldType F F^o (regular_splittingAxiom F).
- -
-Section SplittingFieldTheory.
- -
-Variables (F : fieldType) (L : splittingFieldType F).
- -
-Implicit Types (U V W : {vspace L}).
-Implicit Types (K M E : {subfield L}).
- -
-Lemma splittingFieldP : SplittingField.axiom L.
- -
-Lemma splittingPoly :
- {p : {poly L} | p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}}.
- -
-Fact fieldOver_splitting E : SplittingField.axiom (fieldOver_fieldExtType E).
-Canonical fieldOver_splittingFieldType E :=
- SplittingFieldType (subvs_of E) (fieldOver E) (fieldOver_splitting E).
- -
-Lemma enum_AEnd : {kAutL : seq 'AEnd(L) | ∀ f, f \in kAutL}.
- -
-Lemma splitting_field_normal K x :
- ∃ r, minPoly K x == \prod_(y <- r) ('X - y%:P).
- -
-Lemma kHom_to_AEnd K E f : kHom K E f → {g : 'AEnd(L) | {in E, f =1 val g}}.
- -
-End SplittingFieldTheory.
- -
-
-
--Set Implicit Arguments.
- -
-Reserved Notation "''Gal' ( A / B )"
- (at level 8, A at level 35, format "''Gal' ( A / B )").
- -
-Import GroupScope GRing.Theory.
-Local Open Scope ring_scope.
- -
-Section SplittingFieldFor.
- -
-Variables (F : fieldType) (L : fieldExtType F).
- -
-Definition splittingFieldFor (U : {vspace L}) (p : {poly L}) (V : {vspace L}) :=
- exists2 rs, p %= \prod_(z <- rs) ('X - z%:P) & <<U & rs>>%VS = V.
- -
-Lemma splittingFieldForS (K M E : {subfield L}) p :
- (K ≤ M)%VS → (M ≤ E)%VS →
- splittingFieldFor K p E → splittingFieldFor M p E.
- -
-End SplittingFieldFor.
- -
-Section kHom.
- -
-Variables (F : fieldType) (L : fieldExtType F).
-Implicit Types (U V : {vspace L}) (K E : {subfield L}) (f g : 'End(L)).
- -
-Definition kHom U V f := ahom_in V f && (U ≤ fixedSpace f)%VS.
- -
-Lemma kHomP {K V f} :
- reflect [/\ {in V &, ∀ x y, f (x × y) = f x × f y}
- & {in K, ∀ x, f x = x}]
- (kHom K V f).
- -
-Lemma kAHomP {U V} {f : 'AEnd(L)} :
- reflect {in U, ∀ x, f x = x} (kHom U V f).
- -
-Lemma kHom1 U V : kHom U V \1.
- -
-Lemma k1HomE V f : kHom 1 V f = ahom_in V f.
- -
-Lemma kHom_lrmorphism (f : 'End(L)) : reflect (lrmorphism f) (kHom 1 {:L} f).
- -
-Lemma k1AHom V (f : 'AEnd(L)) : kHom 1 V f.
- -
-Lemma kHom_poly_id K E f p :
- kHom K E f → p \is a polyOver K → map_poly f p = p.
- -
-Lemma kHomSl U1 U2 V f : (U1 ≤ U2)%VS → kHom U2 V f → kHom U1 V f.
- -
-Lemma kHomSr K V1 V2 f : (V1 ≤ V2)%VS → kHom K V2 f → kHom K V1 f.
- -
-Lemma kHomS K1 K2 V1 V2 f :
- (K1 ≤ K2)%VS → (V1 ≤ V2)%VS → kHom K2 V2 f → kHom K1 V1 f.
- -
-Lemma kHom_eq K E f g :
- (K ≤ E)%VS → {in E, f =1 g} → kHom K E f = kHom K E g.
- -
-Lemma kHom_inv K E f : kHom K E f → {in E, {morph f : x / x^-1}}.
- -
-Lemma kHom_dim K E f : kHom K E f → \dim (f @: E) = \dim E.
- -
-Lemma kHom_is_rmorphism K E f :
- kHom K E f → rmorphism (f \o vsval : subvs_of E → L).
-Definition kHom_rmorphism K E f homKEf :=
- RMorphism (@kHom_is_rmorphism K E f homKEf).
- -
-Lemma kHom_horner K E f p x :
- kHom K E f → p \is a polyOver E → x \in E → f p.[x] = (map_poly f p).[f x].
- -
-Lemma kHom_root K E f p x :
- kHom K E f → p \is a polyOver E → x \in E → root p x →
- root (map_poly f p) (f x).
- -
-Lemma kHom_root_id K E f p x :
- (K ≤ E)%VS → kHom K E f → p \is a polyOver K → x \in E → root p x →
- root p (f x).
- -
-Section kHomExtend.
- -
-Variables (K E : {subfield L}) (f : 'End(L)) (x y : L).
- -
-Fact kHomExtend_subproof :
- linear (fun z ⇒ (map_poly f (Fadjoin_poly E x z)).[y]).
-Definition kHomExtend := linfun (Linear kHomExtend_subproof).
- -
-Lemma kHomExtendE z : kHomExtend z = (map_poly f (Fadjoin_poly E x z)).[y].
- -
-Hypotheses (sKE : (K ≤ E)%VS) (homKf : kHom K E f).
-Hypothesis fPx_y_0 : root (map_poly f Px) y.
- -
-Lemma kHomExtend_id z : z \in E → kHomExtend z = f z.
- -
-Lemma kHomExtend_val : kHomExtend x = y.
- -
-Lemma kHomExtend_poly p :
- p \in polyOver E → kHomExtend p.[x] = (map_poly f p).[y].
- -
-Lemma kHomExtendP : kHom K <<E; x>> kHomExtend.
- -
-End kHomExtend.
- -
-Definition kAut U V f := kHom U V f && (f @: V == V)%VS.
- -
-Lemma kAutE K E f : kAut K E f = kHom K E f && (f @: E ≤ E)%VS.
- -
-Lemma kAutS U1 U2 V f : (U1 ≤ U2)%VS → kAut U2 V f → kAut U1 V f.
- -
-Lemma kHom_kAut_sub K E f : kAut K E f → kHom K E f.
- -
-Lemma kAut_eq K E (f g : 'End(L)) :
- (K ≤ E)%VS → {in E, f =1 g} → kAut K E f = kAut K E g.
- -
-Lemma kAutfE K f : kAut K {:L} f = kHom K {:L} f.
- -
-Lemma kAut1E E (f : 'AEnd(L)) : kAut 1 E f = (f @: E ≤ E)%VS.
- -
-Lemma kAutf_lker0 K f : kHom K {:L} f → lker f == 0%VS.
- -
-Lemma inv_kHomf K f : kHom K {:L} f → kHom K {:L} f^-1.
- -
-Lemma inv_is_ahom (f : 'AEnd(L)) : ahom_in {:L} f^-1.
- -
-Canonical inv_ahom (f : 'AEnd(L)) : 'AEnd(L) := AHom (inv_is_ahom f).
-Notation "f ^-1" := (inv_ahom f) : lrfun_scope.
- -
-Lemma comp_kHom_img K E f g :
- kHom K (g @: E) f → kHom K E g → kHom K E (f \o g).
- -
-Lemma comp_kHom K E f g : kHom K {:L} f → kHom K E g → kHom K E (f \o g).
- -
-Lemma kHom_extends K E f p U :
- (K ≤ E)%VS → kHom K E f →
- p \is a polyOver K → splittingFieldFor E p U →
- {g | kHom K U g & {in E, f =1 g}}.
- -
-End kHom.
- -
-Notation "f ^-1" := (inv_ahom f) : lrfun_scope.
- -
- -
-Module SplittingField.
- -
-Import GRing.
- -
-Section ClassDef.
- -
-Variable F : fieldType.
- -
-Definition axiom (L : fieldExtType F) :=
- exists2 p : {poly L}, p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}.
- -
-Record class_of (L : Type) : Type :=
- Class {base : FieldExt.class_of F L; _ : axiom (FieldExt.Pack _ base)}.
- -
-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.
-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.
- -
-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 xclass.
-Definition choiceType := @Choice.Pack cT xclass.
-Definition zmodType := @Zmodule.Pack cT xclass.
-Definition ringType := @Ring.Pack cT xclass.
-Definition unitRingType := @UnitRing.Pack cT xclass.
-Definition comRingType := @ComRing.Pack cT xclass.
-Definition comUnitRingType := @ComUnitRing.Pack cT xclass.
-Definition idomainType := @IntegralDomain.Pack cT xclass.
-Definition fieldType := @Field.Pack cT xclass.
-Definition lmodType := @Lmodule.Pack F phF cT xclass.
-Definition lalgType := @Lalgebra.Pack F phF cT xclass.
-Definition algType := @Algebra.Pack F phF cT xclass.
-Definition unitAlgType := @UnitAlgebra.Pack F phF cT xclass.
-Definition vectType := @Vector.Pack F phF cT xclass.
-Definition FalgType := @Falgebra.Pack F phF cT xclass.
-Definition fieldExtType := @FieldExt.Pack F phF cT xclass.
- -
-End ClassDef.
- -
-Module Exports.
- -
-Coercion sort : type >-> Sortclass.
-Coercion base : class_of >-> FieldExt.class_of.
-Coercion eqType : type >-> Equality.type.
-Canonical eqType.
-Coercion choiceType : type >-> Choice.type.
-Canonical choiceType.
-Coercion zmodType : type >-> Zmodule.type.
-Canonical zmodType.
-Coercion ringType : type >-> Ring.type.
-Canonical ringType.
-Coercion unitRingType : type >-> UnitRing.type.
-Canonical unitRingType.
-Coercion comRingType : type >-> ComRing.type.
-Canonical comRingType.
-Coercion comUnitRingType : type >-> ComUnitRing.type.
-Canonical comUnitRingType.
-Coercion idomainType : type >-> IntegralDomain.type.
-Canonical idomainType.
-Coercion fieldType : type >-> Field.type.
-Canonical fieldType.
-Coercion lmodType : type >-> Lmodule.type.
-Canonical lmodType.
-Coercion lalgType : type >-> Lalgebra.type.
-Canonical lalgType.
-Coercion algType : type >-> Algebra.type.
-Canonical algType.
-Coercion unitAlgType : type >-> UnitAlgebra.type.
-Canonical unitAlgType.
-Coercion vectType : type >-> Vector.type.
-Canonical vectType.
-Coercion FalgType : type >-> Falgebra.type.
-Canonical FalgType.
-Coercion fieldExtType : type >-> FieldExt.type.
-Canonical fieldExtType.
- -
-Notation splittingFieldType F := (type (Phant F)).
-Notation SplittingFieldType F L ax := (@pack _ (Phant F) L _ ax _ _ id _ id).
-Notation "[ 'splittingFieldType' F 'of' L 'for' K ]" :=
- (@clone _ (Phant F) L K _ idfun)
- (at level 0, format "[ 'splittingFieldType' F 'of' L 'for' K ]")
- : form_scope.
-Notation "[ 'splittingFieldType' F 'of' L ]" :=
- (@clone _ (Phant F) L _ _ id)
- (at level 0, format "[ 'splittingFieldType' F 'of' L ]") : form_scope.
- -
-End Exports.
-End SplittingField.
-Export SplittingField.Exports.
- -
-Lemma normal_field_splitting (F : fieldType) (L : fieldExtType F) :
- (∀ (K : {subfield L}) x,
- ∃ r, minPoly K x == \prod_(y <- r) ('X - y%:P)) →
- SplittingField.axiom L.
- -
-Fact regular_splittingAxiom F : SplittingField.axiom (regular_fieldExtType F).
- -
-Canonical regular_splittingFieldType (F : fieldType) :=
- SplittingFieldType F F^o (regular_splittingAxiom F).
- -
-Section SplittingFieldTheory.
- -
-Variables (F : fieldType) (L : splittingFieldType F).
- -
-Implicit Types (U V W : {vspace L}).
-Implicit Types (K M E : {subfield L}).
- -
-Lemma splittingFieldP : SplittingField.axiom L.
- -
-Lemma splittingPoly :
- {p : {poly L} | p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}}.
- -
-Fact fieldOver_splitting E : SplittingField.axiom (fieldOver_fieldExtType E).
-Canonical fieldOver_splittingFieldType E :=
- SplittingFieldType (subvs_of E) (fieldOver E) (fieldOver_splitting E).
- -
-Lemma enum_AEnd : {kAutL : seq 'AEnd(L) | ∀ f, f \in kAutL}.
- -
-Lemma splitting_field_normal K x :
- ∃ r, minPoly K x == \prod_(y <- r) ('X - y%:P).
- -
-Lemma kHom_to_AEnd K E f : kHom K E f → {g : 'AEnd(L) | {in E, f =1 val g}}.
- -
-End SplittingFieldTheory.
- -
-
- Hide the finGroup structure on 'AEnd(L) in a module so that we can control
- when it is exported. Most people will want to use the finGroup structure
- on 'Gal(E / K) and will not need this module.
-
-
-Module Import AEnd_FinGroup.
-Section AEnd_FinGroup.
- -
-Variables (F : fieldType) (L : splittingFieldType F).
-Implicit Types (U V W : {vspace L}) (K M E : {subfield L}).
- -
-Definition inAEnd f := SeqSub (svalP (enum_AEnd L) f).
-Fact inAEndK : cancel inAEnd val.
- -
-Definition AEnd_countMixin := Eval hnf in CanCountMixin inAEndK.
-Canonical AEnd_countType := Eval hnf in CountType 'AEnd(L) AEnd_countMixin.
-Canonical AEnd_subCountType := Eval hnf in [subCountType of 'AEnd(L)].
-Definition AEnd_finMixin := Eval hnf in CanFinMixin inAEndK.
-Canonical AEnd_finType := Eval hnf in FinType 'AEnd(L) AEnd_finMixin.
-Canonical AEnd_subFinType := Eval hnf in [subFinType of 'AEnd(L)].
- -
-
-
--Section AEnd_FinGroup.
- -
-Variables (F : fieldType) (L : splittingFieldType F).
-Implicit Types (U V W : {vspace L}) (K M E : {subfield L}).
- -
-Definition inAEnd f := SeqSub (svalP (enum_AEnd L) f).
-Fact inAEndK : cancel inAEnd val.
- -
-Definition AEnd_countMixin := Eval hnf in CanCountMixin inAEndK.
-Canonical AEnd_countType := Eval hnf in CountType 'AEnd(L) AEnd_countMixin.
-Canonical AEnd_subCountType := Eval hnf in [subCountType of 'AEnd(L)].
-Definition AEnd_finMixin := Eval hnf in CanFinMixin inAEndK.
-Canonical AEnd_finType := Eval hnf in FinType 'AEnd(L) AEnd_finMixin.
-Canonical AEnd_subFinType := Eval hnf in [subFinType of 'AEnd(L)].
- -
-
- the group operation is the categorical composition operation
-
-
-Definition comp_AEnd (f g : 'AEnd(L)) : 'AEnd(L) := (g \o f)%AF.
- -
-Fact comp_AEndA : associative comp_AEnd.
- -
-Fact comp_AEnd1l : left_id \1%AF comp_AEnd.
- -
-Fact comp_AEndK : left_inverse \1%AF (@inv_ahom _ L) comp_AEnd.
- -
-Definition AEnd_baseFinGroupMixin :=
- FinGroup.Mixin comp_AEndA comp_AEnd1l comp_AEndK.
-Canonical AEnd_baseFinGroupType :=
- BaseFinGroupType 'AEnd(L) AEnd_baseFinGroupMixin.
-Canonical AEnd_finGroupType := FinGroupType comp_AEndK.
- -
-Definition kAEnd U V := [set f : 'AEnd(L) | kAut U V f].
-Definition kAEndf U := kAEnd U {:L}.
- -
-Lemma kAEnd_group_set K E : group_set (kAEnd K E).
-Canonical kAEnd_group K E := group (kAEnd_group_set K E).
-Canonical kAEndf_group K := [group of kAEndf K].
- -
-Lemma kAEnd_norm K E : kAEnd K E \subset 'N(kAEndf E)%g.
- -
-Lemma mem_kAut_coset K E (g : 'AEnd(L)) :
- kAut K E g → g \in coset (kAEndf E) g.
- -
-Lemma aut_mem_eqP E (x y : coset_of (kAEndf E)) f g :
- f \in x → g \in y → reflect {in E, f =1 g} (x == y).
- -
-End AEnd_FinGroup.
-End AEnd_FinGroup.
- -
-Section GaloisTheory.
- -
-Variables (F : fieldType) (L : splittingFieldType F).
- -
-Implicit Types (U V W : {vspace L}).
-Implicit Types (K M E : {subfield L}).
- -
-
-
-- -
-Fact comp_AEndA : associative comp_AEnd.
- -
-Fact comp_AEnd1l : left_id \1%AF comp_AEnd.
- -
-Fact comp_AEndK : left_inverse \1%AF (@inv_ahom _ L) comp_AEnd.
- -
-Definition AEnd_baseFinGroupMixin :=
- FinGroup.Mixin comp_AEndA comp_AEnd1l comp_AEndK.
-Canonical AEnd_baseFinGroupType :=
- BaseFinGroupType 'AEnd(L) AEnd_baseFinGroupMixin.
-Canonical AEnd_finGroupType := FinGroupType comp_AEndK.
- -
-Definition kAEnd U V := [set f : 'AEnd(L) | kAut U V f].
-Definition kAEndf U := kAEnd U {:L}.
- -
-Lemma kAEnd_group_set K E : group_set (kAEnd K E).
-Canonical kAEnd_group K E := group (kAEnd_group_set K E).
-Canonical kAEndf_group K := [group of kAEndf K].
- -
-Lemma kAEnd_norm K E : kAEnd K E \subset 'N(kAEndf E)%g.
- -
-Lemma mem_kAut_coset K E (g : 'AEnd(L)) :
- kAut K E g → g \in coset (kAEndf E) g.
- -
-Lemma aut_mem_eqP E (x y : coset_of (kAEndf E)) f g :
- f \in x → g \in y → reflect {in E, f =1 g} (x == y).
- -
-End AEnd_FinGroup.
-End AEnd_FinGroup.
- -
-Section GaloisTheory.
- -
-Variables (F : fieldType) (L : splittingFieldType F).
- -
-Implicit Types (U V W : {vspace L}).
-Implicit Types (K M E : {subfield L}).
- -
-
- We take Galois automorphisms for a subfield E to be automorphisms of the
- full field {:L} that operate in E taken modulo those that fix E pointwise.
- The type of Galois automorphisms of E is then the subtype of elements of
- the quotient kAEnd 1 E / kAEndf E, which we encapsulate in a specific
- wrapper to ensure stability of the gal_repr coercion insertion.
-
-
-
-
- The _, which becomes redundant when V is a {subfield L}, ensures that
- the argument of [subg _ ] is syntactically a group.
-
-
-Inductive gal_of := Gal of [subg kAEnd_group 1 <<V>> / kAEndf (agenv V)].
-Definition gal (f : 'AEnd(L)) := Gal (subg _ (coset _ f)).
-Definition gal_sgval x := let: Gal u := x in u.
- -
-Fact gal_sgvalK : cancel gal_sgval Gal.
-Let gal_sgval_inj := can_inj gal_sgvalK.
- -
-Definition gal_eqMixin := CanEqMixin gal_sgvalK.
-Canonical gal_eqType := Eval hnf in EqType gal_of gal_eqMixin.
-Definition gal_choiceMixin := CanChoiceMixin gal_sgvalK.
-Canonical gal_choiceType := Eval hnf in ChoiceType gal_of gal_choiceMixin.
-Definition gal_countMixin := CanCountMixin gal_sgvalK.
-Canonical gal_countType := Eval hnf in CountType gal_of gal_countMixin.
-Definition gal_finMixin := CanFinMixin gal_sgvalK.
-Canonical gal_finType := Eval hnf in FinType gal_of gal_finMixin.
- -
-Definition gal_one := Gal 1%g.
-Definition gal_inv x := Gal (gal_sgval x)^-1.
-Definition gal_mul x y := Gal (gal_sgval x × gal_sgval y).
-Fact gal_oneP : left_id gal_one gal_mul.
- Fact gal_invP : left_inverse gal_one gal_inv gal_mul.
- Fact gal_mulP : associative gal_mul.
- -
-Definition gal_finGroupMixin :=
- FinGroup.Mixin gal_mulP gal_oneP gal_invP.
-Canonical gal_finBaseGroupType :=
- Eval hnf in BaseFinGroupType gal_of gal_finGroupMixin.
-Canonical gal_finGroupType := Eval hnf in FinGroupType gal_invP.
- -
-Coercion gal_repr u : 'AEnd(L) := repr (sgval (gal_sgval u)).
- -
-Fact gal_is_morphism : {in kAEnd 1 (agenv V) &, {morph gal : x y / x × y}%g}.
-Canonical gal_morphism := Morphism gal_is_morphism.
- -
-Lemma gal_reprK : cancel gal_repr gal.
- -
-Lemma gal_repr_inj : injective gal_repr.
- -
-Lemma gal_AEnd x : gal_repr x \in kAEnd 1 (agenv V).
- -
-End gal_of_Definition.
- -
- -
-Lemma gal_eqP E {x y : gal_of E} : reflect {in E, x =1 y} (x == y).
- -
-Lemma galK E (f : 'AEnd(L)) : (f @: E ≤ E)%VS → {in E, gal E f =1 f}.
- -
-Lemma eq_galP E (f g : 'AEnd(L)) :
- (f @: E ≤ E)%VS → (g @: E ≤ E)%VS →
- reflect {in E, f =1 g} (gal E f == gal E g).
- -
-Lemma limg_gal E (x : gal_of E) : (x @: E)%VS = E.
- -
-Lemma memv_gal E (x : gal_of E) a : a \in E → x a \in E.
- -
-Lemma gal_id E a : (1 : gal_of E)%g a = a.
- -
-Lemma galM E (x y : gal_of E) a : a \in E → (x × y)%g a = y (x a).
- -
-Lemma galV E (x : gal_of E) : {in E, (x^-1)%g =1 x^-1%VF}.
- -
-
-
--Definition gal (f : 'AEnd(L)) := Gal (subg _ (coset _ f)).
-Definition gal_sgval x := let: Gal u := x in u.
- -
-Fact gal_sgvalK : cancel gal_sgval Gal.
-Let gal_sgval_inj := can_inj gal_sgvalK.
- -
-Definition gal_eqMixin := CanEqMixin gal_sgvalK.
-Canonical gal_eqType := Eval hnf in EqType gal_of gal_eqMixin.
-Definition gal_choiceMixin := CanChoiceMixin gal_sgvalK.
-Canonical gal_choiceType := Eval hnf in ChoiceType gal_of gal_choiceMixin.
-Definition gal_countMixin := CanCountMixin gal_sgvalK.
-Canonical gal_countType := Eval hnf in CountType gal_of gal_countMixin.
-Definition gal_finMixin := CanFinMixin gal_sgvalK.
-Canonical gal_finType := Eval hnf in FinType gal_of gal_finMixin.
- -
-Definition gal_one := Gal 1%g.
-Definition gal_inv x := Gal (gal_sgval x)^-1.
-Definition gal_mul x y := Gal (gal_sgval x × gal_sgval y).
-Fact gal_oneP : left_id gal_one gal_mul.
- Fact gal_invP : left_inverse gal_one gal_inv gal_mul.
- Fact gal_mulP : associative gal_mul.
- -
-Definition gal_finGroupMixin :=
- FinGroup.Mixin gal_mulP gal_oneP gal_invP.
-Canonical gal_finBaseGroupType :=
- Eval hnf in BaseFinGroupType gal_of gal_finGroupMixin.
-Canonical gal_finGroupType := Eval hnf in FinGroupType gal_invP.
- -
-Coercion gal_repr u : 'AEnd(L) := repr (sgval (gal_sgval u)).
- -
-Fact gal_is_morphism : {in kAEnd 1 (agenv V) &, {morph gal : x y / x × y}%g}.
-Canonical gal_morphism := Morphism gal_is_morphism.
- -
-Lemma gal_reprK : cancel gal_repr gal.
- -
-Lemma gal_repr_inj : injective gal_repr.
- -
-Lemma gal_AEnd x : gal_repr x \in kAEnd 1 (agenv V).
- -
-End gal_of_Definition.
- -
- -
-Lemma gal_eqP E {x y : gal_of E} : reflect {in E, x =1 y} (x == y).
- -
-Lemma galK E (f : 'AEnd(L)) : (f @: E ≤ E)%VS → {in E, gal E f =1 f}.
- -
-Lemma eq_galP E (f g : 'AEnd(L)) :
- (f @: E ≤ E)%VS → (g @: E ≤ E)%VS →
- reflect {in E, f =1 g} (gal E f == gal E g).
- -
-Lemma limg_gal E (x : gal_of E) : (x @: E)%VS = E.
- -
-Lemma memv_gal E (x : gal_of E) a : a \in E → x a \in E.
- -
-Lemma gal_id E a : (1 : gal_of E)%g a = a.
- -
-Lemma galM E (x y : gal_of E) a : a \in E → (x × y)%g a = y (x a).
- -
-Lemma galV E (x : gal_of E) : {in E, (x^-1)%g =1 x^-1%VF}.
- -
-
- Standard mathematical notation for 'Gal(E / K) puts the larger field first.
-
-
-Definition galoisG V U := gal V @* <<kAEnd (U :&: V) V>>.
-Canonical galoisG_group E U := Eval hnf in [group of (galoisG E U)].
- -
-Section Automorphism.
- -
-Lemma gal_cap U V : 'Gal(V / U) = 'Gal(V / U :&: V).
- -
-Lemma gal_kAut K E x : (K ≤ E)%VS → (x \in 'Gal(E / K)) = kAut K E x.
- -
-Lemma gal_kHom K E x : (K ≤ E)%VS → (x \in 'Gal(E / K)) = kHom K E x.
- -
-Lemma kAut_to_gal K E f :
- kAut K E f → {x : gal_of E | x \in 'Gal(E / K) & {in E, f =1 x}}.
- -
-Lemma fixed_gal K E x a :
- (K ≤ E)%VS → x \in 'Gal(E / K) → a \in K → x a = a.
- -
-Lemma fixedPoly_gal K E x p :
- (K ≤ E)%VS → x \in 'Gal(E / K) → p \is a polyOver K → map_poly x p = p.
- -
-Lemma root_minPoly_gal K E x a :
- (K ≤ E)%VS → x \in 'Gal(E / K) → a \in E → root (minPoly K a) (x a).
- -
-End Automorphism.
- -
-Lemma gal_adjoin_eq K a x y :
- x \in 'Gal(<<K; a>> / K) → y \in 'Gal(<<K; a>> / K) →
- (x == y) = (x a == y a).
- -
-Lemma galS K M E : (K ≤ M)%VS → 'Gal(E / M) \subset 'Gal(E / K).
- -
-Lemma gal_conjg K E x : 'Gal(E / K) :^ x = 'Gal(E / x @: K).
- -
-Definition fixedField V (A : {set gal_of V}) :=
- (V :&: \bigcap_(x in A) fixedSpace x)%VS.
- -
-Lemma fixedFieldP E {A : {set gal_of E}} a :
- a \in E → reflect (∀ x, x \in A → x a = a) (a \in fixedField A).
- -
-Lemma mem_fixedFieldP E (A : {set gal_of E}) a :
- a \in fixedField A → a \in E ∧ (∀ x, x \in A → x a = a).
- -
-Fact fixedField_is_aspace E (A : {set gal_of E}) : is_aspace (fixedField A).
-Canonical fixedField_aspace E A : {subfield L} :=
- ASpace (@fixedField_is_aspace E A).
- -
-Lemma fixedField_bound E (A : {set gal_of E}) : (fixedField A ≤ E)%VS.
- -
-Lemma fixedFieldS E (A B : {set gal_of E}) :
- A \subset B → (fixedField B ≤ fixedField A)%VS.
- -
-Lemma galois_connection_subv K E :
- (K ≤ E)%VS → (K ≤ fixedField ('Gal(E / K)))%VS.
- -
-Lemma galois_connection_subset E (A : {set gal_of E}):
- A \subset 'Gal(E / fixedField A).
- -
-Lemma galois_connection K E (A : {set gal_of E}):
- (K ≤ E)%VS → (A \subset 'Gal(E / K)) = (K ≤ fixedField A)%VS.
- -
-Definition galTrace U V a := \sum_(x in 'Gal(V / U)) (x a).
- -
-Definition galNorm U V a := \prod_(x in 'Gal(V / U)) (x a).
- -
-Section TraceAndNormMorphism.
- -
-Variables U V : {vspace L}.
- -
-Fact galTrace_is_additive : additive (galTrace U V).
-Canonical galTrace_additive := Additive galTrace_is_additive.
- -
-Lemma galNorm1 : galNorm U V 1 = 1.
- -
-Lemma galNormM : {morph galNorm U V : a b / a × b}.
- -
-Lemma galNormV : {morph galNorm U V : a / a^-1}.
- -
-Lemma galNormX n : {morph galNorm U V : a / a ^+ n}.
- -
-Lemma galNorm_prod (I : Type) (r : seq I) (P : pred I) (B : I → L) :
- galNorm U V (\prod_(i <- r | P i) B i)
- = \prod_(i <- r | P i) galNorm U V (B i).
- -
-Lemma galNorm0 : galNorm U V 0 = 0.
- -
-Lemma galNorm_eq0 a : (galNorm U V a == 0) = (a == 0).
- -
-End TraceAndNormMorphism.
- -
-Section TraceAndNormField.
- -
-Variables K E : {subfield L}.
- -
-Lemma galTrace_fixedField a :
- a \in E → galTrace K E a \in fixedField 'Gal(E / K).
- -
-Lemma galTrace_gal a x :
- a \in E → x \in 'Gal(E / K) → galTrace K E (x a) = galTrace K E a.
- -
-Lemma galNorm_fixedField a :
- a \in E → galNorm K E a \in fixedField 'Gal(E / K).
- -
-Lemma galNorm_gal a x :
- a \in E → x \in 'Gal(E / K) → galNorm K E (x a) = galNorm K E a.
- -
-End TraceAndNormField.
- -
-Definition normalField U V := [∀ x in kAEndf U, x @: V == V]%VS.
- -
-Lemma normalField_kAut K M E f :
- (K ≤ M ≤ E)%VS → normalField K M → kAut K E f → kAut K M f.
- -
-Lemma normalFieldP K E :
- reflect {in E, ∀ a, exists2 r,
- all (mem E) r & minPoly K a = \prod_(b <- r) ('X - b%:P)}
- (normalField K E).
- -
-Lemma normalFieldf K : normalField K {:L}.
- -
-Lemma normalFieldS K M E : (K ≤ M)%VS → normalField K E → normalField M E.
- -
-Lemma splitting_normalField E K :
- (K ≤ E)%VS →
- reflect (exists2 p, p \is a polyOver K & splittingFieldFor K p E)
- (normalField K E).
- -
-Lemma kHom_to_gal K M E f :
- (K ≤ M ≤ E)%VS → normalField K E → kHom K M f →
- {x | x \in 'Gal(E / K) & {in M, f =1 x}}.
- -
-Lemma normalField_root_minPoly K E a b :
- (K ≤ E)%VS → normalField K E → a \in E → root (minPoly K a) b →
- exists2 x, x \in 'Gal(E / K) & x a = b.
- -
- -
-Lemma normalField_factors K E :
- (K ≤ E)%VS →
- reflect {in E, ∀ a, exists2 r : seq (gal_of E),
- r \subset 'Gal(E / K)
- & minPoly K a = \prod_(x <- r) ('X - (x a)%:P)}
- (normalField K E).
- -
-Definition galois U V := [&& (U ≤ V)%VS, separable U V & normalField U V].
- -
-Lemma galoisS K M E : (K ≤ M ≤ E)%VS → galois K E → galois M E.
- -
-Lemma galois_dim K E : galois K E → \dim_K E = #|'Gal(E / K)|.
- -
-Lemma galois_factors K E :
- (K ≤ E)%VS →
- reflect {in E, ∀ a, ∃ r, let r_a := [seq x a | x : gal_of E <- r] in
- [/\ r \subset 'Gal(E / K), uniq r_a
- & minPoly K a = \prod_(b <- r_a) ('X - b%:P)]}
- (galois K E).
- -
-Lemma splitting_galoisField K E :
- reflect (∃ p, [/\ p \is a polyOver K, separable_poly p
- & splittingFieldFor K p E])
- (galois K E).
- -
-Lemma galois_fixedField K E :
- reflect (fixedField 'Gal(E / K) = K) (galois K E).
- -
-Lemma mem_galTrace K E a : galois K E → a \in E → galTrace K E a \in K.
- -
-Lemma mem_galNorm K E a : galois K E → a \in E → galNorm K E a \in K.
- -
-Lemma gal_independent_contra E (P : pred (gal_of E)) (c_ : gal_of E → L) x :
- P x → c_ x != 0 →
- exists2 a, a \in E & \sum_(y | P y) c_ y × y a != 0.
- -
-Lemma gal_independent E (P : pred (gal_of E)) (c_ : gal_of E → L) :
- (∀ a, a \in E → \sum_(x | P x) c_ x × x a = 0) →
- (∀ x, P x → c_ x = 0).
- -
-Lemma Hilbert's_theorem_90 K E x a :
- generator 'Gal(E / K) x → a \in E →
- reflect (exists2 b, b \in E ∧ b != 0 & a = b / x b) (galNorm K E a == 1).
- -
-Section Matrix.
- -
-Variable (E : {subfield L}) (A : {set gal_of E}).
- -
-Let K := fixedField A.
- -
-Lemma gal_matrix :
- {w : #|A|.-tuple L | {subset w ≤ E} ∧ 0 \notin w &
- [/\ \matrix_(i, j < #|A|) enum_val i (tnth w j) \in unitmx,
- directv (\sum_i K × <[tnth w i]>) &
- group_set A → (\sum_i K × <[tnth w i]>)%VS = E] }.
- -
-End Matrix.
- -
-Lemma dim_fixedField E (G : {group gal_of E}) : #|G| = \dim_(fixedField G) E.
- -
-Lemma dim_fixed_galois K E (G : {group gal_of E}) :
- galois K E → G \subset 'Gal(E / K) →
- \dim_K (fixedField G) = #|'Gal(E / K) : G|.
- -
-Lemma gal_fixedField E (G : {group gal_of E}): 'Gal(E / fixedField G) = G.
- -
-Lemma gal_generated E (A : {set gal_of E}) : 'Gal(E / fixedField A) = <<A>>.
- -
-Lemma fixedField_galois E (A : {set gal_of E}): galois (fixedField A) E.
- -
-Section FundamentalTheoremOfGaloisTheory.
- -
-Variables E K : {subfield L}.
-Hypothesis galKE : galois K E.
- -
-Section IntermediateField.
- -
-Variable M : {subfield L}.
-Hypothesis (sKME : (K ≤ M ≤ E)%VS) (nKM : normalField K M).
- -
-Lemma normalField_galois : galois K M.
- -
-Definition normalField_cast (x : gal_of E) : gal_of M := gal M x.
- -
-Lemma normalField_cast_eq x :
- x \in 'Gal(E / K) → {in M, normalField_cast x =1 x}.
- -
-Lemma normalField_castM :
- {in 'Gal(E / K) &, {morph normalField_cast : x y / (x × y)%g}}.
-Canonical normalField_cast_morphism := Morphism normalField_castM.
- -
-Lemma normalField_ker : 'ker normalField_cast = 'Gal(E / M).
- -
-Lemma normalField_normal : 'Gal(E / M) <| 'Gal(E / K).
- -
-Lemma normalField_img : normalField_cast @* 'Gal(E / K) = 'Gal(M / K).
- -
-Lemma normalField_isom :
- {f : {morphism ('Gal(E / K) / 'Gal(E / M)) >-> gal_of M} |
- isom ('Gal(E / K) / 'Gal (E / M)) 'Gal(M / K) f
- & (∀ A, f @* (A / 'Gal(E / M)) = normalField_cast @* A)
- ∧ {in 'Gal(E / K) & M, ∀ x, f (coset 'Gal (E / M) x) =1 x} }%g.
- -
-Lemma normalField_isog : 'Gal(E / K) / 'Gal(E / M) \isog 'Gal(M / K).
- -
-End IntermediateField.
- -
-Section IntermediateGroup.
- -
-Variable G : {group gal_of E}.
-Hypothesis nsGgalE : G <| 'Gal(E / K).
- -
-Lemma normal_fixedField_galois : galois K (fixedField G).
- -
-End IntermediateGroup.
- -
-End FundamentalTheoremOfGaloisTheory.
- -
-End GaloisTheory.
- -
- -
-Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope.
-Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope.
- -
-
--Canonical galoisG_group E U := Eval hnf in [group of (galoisG E U)].
- -
-Section Automorphism.
- -
-Lemma gal_cap U V : 'Gal(V / U) = 'Gal(V / U :&: V).
- -
-Lemma gal_kAut K E x : (K ≤ E)%VS → (x \in 'Gal(E / K)) = kAut K E x.
- -
-Lemma gal_kHom K E x : (K ≤ E)%VS → (x \in 'Gal(E / K)) = kHom K E x.
- -
-Lemma kAut_to_gal K E f :
- kAut K E f → {x : gal_of E | x \in 'Gal(E / K) & {in E, f =1 x}}.
- -
-Lemma fixed_gal K E x a :
- (K ≤ E)%VS → x \in 'Gal(E / K) → a \in K → x a = a.
- -
-Lemma fixedPoly_gal K E x p :
- (K ≤ E)%VS → x \in 'Gal(E / K) → p \is a polyOver K → map_poly x p = p.
- -
-Lemma root_minPoly_gal K E x a :
- (K ≤ E)%VS → x \in 'Gal(E / K) → a \in E → root (minPoly K a) (x a).
- -
-End Automorphism.
- -
-Lemma gal_adjoin_eq K a x y :
- x \in 'Gal(<<K; a>> / K) → y \in 'Gal(<<K; a>> / K) →
- (x == y) = (x a == y a).
- -
-Lemma galS K M E : (K ≤ M)%VS → 'Gal(E / M) \subset 'Gal(E / K).
- -
-Lemma gal_conjg K E x : 'Gal(E / K) :^ x = 'Gal(E / x @: K).
- -
-Definition fixedField V (A : {set gal_of V}) :=
- (V :&: \bigcap_(x in A) fixedSpace x)%VS.
- -
-Lemma fixedFieldP E {A : {set gal_of E}} a :
- a \in E → reflect (∀ x, x \in A → x a = a) (a \in fixedField A).
- -
-Lemma mem_fixedFieldP E (A : {set gal_of E}) a :
- a \in fixedField A → a \in E ∧ (∀ x, x \in A → x a = a).
- -
-Fact fixedField_is_aspace E (A : {set gal_of E}) : is_aspace (fixedField A).
-Canonical fixedField_aspace E A : {subfield L} :=
- ASpace (@fixedField_is_aspace E A).
- -
-Lemma fixedField_bound E (A : {set gal_of E}) : (fixedField A ≤ E)%VS.
- -
-Lemma fixedFieldS E (A B : {set gal_of E}) :
- A \subset B → (fixedField B ≤ fixedField A)%VS.
- -
-Lemma galois_connection_subv K E :
- (K ≤ E)%VS → (K ≤ fixedField ('Gal(E / K)))%VS.
- -
-Lemma galois_connection_subset E (A : {set gal_of E}):
- A \subset 'Gal(E / fixedField A).
- -
-Lemma galois_connection K E (A : {set gal_of E}):
- (K ≤ E)%VS → (A \subset 'Gal(E / K)) = (K ≤ fixedField A)%VS.
- -
-Definition galTrace U V a := \sum_(x in 'Gal(V / U)) (x a).
- -
-Definition galNorm U V a := \prod_(x in 'Gal(V / U)) (x a).
- -
-Section TraceAndNormMorphism.
- -
-Variables U V : {vspace L}.
- -
-Fact galTrace_is_additive : additive (galTrace U V).
-Canonical galTrace_additive := Additive galTrace_is_additive.
- -
-Lemma galNorm1 : galNorm U V 1 = 1.
- -
-Lemma galNormM : {morph galNorm U V : a b / a × b}.
- -
-Lemma galNormV : {morph galNorm U V : a / a^-1}.
- -
-Lemma galNormX n : {morph galNorm U V : a / a ^+ n}.
- -
-Lemma galNorm_prod (I : Type) (r : seq I) (P : pred I) (B : I → L) :
- galNorm U V (\prod_(i <- r | P i) B i)
- = \prod_(i <- r | P i) galNorm U V (B i).
- -
-Lemma galNorm0 : galNorm U V 0 = 0.
- -
-Lemma galNorm_eq0 a : (galNorm U V a == 0) = (a == 0).
- -
-End TraceAndNormMorphism.
- -
-Section TraceAndNormField.
- -
-Variables K E : {subfield L}.
- -
-Lemma galTrace_fixedField a :
- a \in E → galTrace K E a \in fixedField 'Gal(E / K).
- -
-Lemma galTrace_gal a x :
- a \in E → x \in 'Gal(E / K) → galTrace K E (x a) = galTrace K E a.
- -
-Lemma galNorm_fixedField a :
- a \in E → galNorm K E a \in fixedField 'Gal(E / K).
- -
-Lemma galNorm_gal a x :
- a \in E → x \in 'Gal(E / K) → galNorm K E (x a) = galNorm K E a.
- -
-End TraceAndNormField.
- -
-Definition normalField U V := [∀ x in kAEndf U, x @: V == V]%VS.
- -
-Lemma normalField_kAut K M E f :
- (K ≤ M ≤ E)%VS → normalField K M → kAut K E f → kAut K M f.
- -
-Lemma normalFieldP K E :
- reflect {in E, ∀ a, exists2 r,
- all (mem E) r & minPoly K a = \prod_(b <- r) ('X - b%:P)}
- (normalField K E).
- -
-Lemma normalFieldf K : normalField K {:L}.
- -
-Lemma normalFieldS K M E : (K ≤ M)%VS → normalField K E → normalField M E.
- -
-Lemma splitting_normalField E K :
- (K ≤ E)%VS →
- reflect (exists2 p, p \is a polyOver K & splittingFieldFor K p E)
- (normalField K E).
- -
-Lemma kHom_to_gal K M E f :
- (K ≤ M ≤ E)%VS → normalField K E → kHom K M f →
- {x | x \in 'Gal(E / K) & {in M, f =1 x}}.
- -
-Lemma normalField_root_minPoly K E a b :
- (K ≤ E)%VS → normalField K E → a \in E → root (minPoly K a) b →
- exists2 x, x \in 'Gal(E / K) & x a = b.
- -
- -
-Lemma normalField_factors K E :
- (K ≤ E)%VS →
- reflect {in E, ∀ a, exists2 r : seq (gal_of E),
- r \subset 'Gal(E / K)
- & minPoly K a = \prod_(x <- r) ('X - (x a)%:P)}
- (normalField K E).
- -
-Definition galois U V := [&& (U ≤ V)%VS, separable U V & normalField U V].
- -
-Lemma galoisS K M E : (K ≤ M ≤ E)%VS → galois K E → galois M E.
- -
-Lemma galois_dim K E : galois K E → \dim_K E = #|'Gal(E / K)|.
- -
-Lemma galois_factors K E :
- (K ≤ E)%VS →
- reflect {in E, ∀ a, ∃ r, let r_a := [seq x a | x : gal_of E <- r] in
- [/\ r \subset 'Gal(E / K), uniq r_a
- & minPoly K a = \prod_(b <- r_a) ('X - b%:P)]}
- (galois K E).
- -
-Lemma splitting_galoisField K E :
- reflect (∃ p, [/\ p \is a polyOver K, separable_poly p
- & splittingFieldFor K p E])
- (galois K E).
- -
-Lemma galois_fixedField K E :
- reflect (fixedField 'Gal(E / K) = K) (galois K E).
- -
-Lemma mem_galTrace K E a : galois K E → a \in E → galTrace K E a \in K.
- -
-Lemma mem_galNorm K E a : galois K E → a \in E → galNorm K E a \in K.
- -
-Lemma gal_independent_contra E (P : pred (gal_of E)) (c_ : gal_of E → L) x :
- P x → c_ x != 0 →
- exists2 a, a \in E & \sum_(y | P y) c_ y × y a != 0.
- -
-Lemma gal_independent E (P : pred (gal_of E)) (c_ : gal_of E → L) :
- (∀ a, a \in E → \sum_(x | P x) c_ x × x a = 0) →
- (∀ x, P x → c_ x = 0).
- -
-Lemma Hilbert's_theorem_90 K E x a :
- generator 'Gal(E / K) x → a \in E →
- reflect (exists2 b, b \in E ∧ b != 0 & a = b / x b) (galNorm K E a == 1).
- -
-Section Matrix.
- -
-Variable (E : {subfield L}) (A : {set gal_of E}).
- -
-Let K := fixedField A.
- -
-Lemma gal_matrix :
- {w : #|A|.-tuple L | {subset w ≤ E} ∧ 0 \notin w &
- [/\ \matrix_(i, j < #|A|) enum_val i (tnth w j) \in unitmx,
- directv (\sum_i K × <[tnth w i]>) &
- group_set A → (\sum_i K × <[tnth w i]>)%VS = E] }.
- -
-End Matrix.
- -
-Lemma dim_fixedField E (G : {group gal_of E}) : #|G| = \dim_(fixedField G) E.
- -
-Lemma dim_fixed_galois K E (G : {group gal_of E}) :
- galois K E → G \subset 'Gal(E / K) →
- \dim_K (fixedField G) = #|'Gal(E / K) : G|.
- -
-Lemma gal_fixedField E (G : {group gal_of E}): 'Gal(E / fixedField G) = G.
- -
-Lemma gal_generated E (A : {set gal_of E}) : 'Gal(E / fixedField A) = <<A>>.
- -
-Lemma fixedField_galois E (A : {set gal_of E}): galois (fixedField A) E.
- -
-Section FundamentalTheoremOfGaloisTheory.
- -
-Variables E K : {subfield L}.
-Hypothesis galKE : galois K E.
- -
-Section IntermediateField.
- -
-Variable M : {subfield L}.
-Hypothesis (sKME : (K ≤ M ≤ E)%VS) (nKM : normalField K M).
- -
-Lemma normalField_galois : galois K M.
- -
-Definition normalField_cast (x : gal_of E) : gal_of M := gal M x.
- -
-Lemma normalField_cast_eq x :
- x \in 'Gal(E / K) → {in M, normalField_cast x =1 x}.
- -
-Lemma normalField_castM :
- {in 'Gal(E / K) &, {morph normalField_cast : x y / (x × y)%g}}.
-Canonical normalField_cast_morphism := Morphism normalField_castM.
- -
-Lemma normalField_ker : 'ker normalField_cast = 'Gal(E / M).
- -
-Lemma normalField_normal : 'Gal(E / M) <| 'Gal(E / K).
- -
-Lemma normalField_img : normalField_cast @* 'Gal(E / K) = 'Gal(M / K).
- -
-Lemma normalField_isom :
- {f : {morphism ('Gal(E / K) / 'Gal(E / M)) >-> gal_of M} |
- isom ('Gal(E / K) / 'Gal (E / M)) 'Gal(M / K) f
- & (∀ A, f @* (A / 'Gal(E / M)) = normalField_cast @* A)
- ∧ {in 'Gal(E / K) & M, ∀ x, f (coset 'Gal (E / M) x) =1 x} }%g.
- -
-Lemma normalField_isog : 'Gal(E / K) / 'Gal(E / M) \isog 'Gal(M / K).
- -
-End IntermediateField.
- -
-Section IntermediateGroup.
- -
-Variable G : {group gal_of E}.
-Hypothesis nsGgalE : G <| 'Gal(E / K).
- -
-Lemma normal_fixedField_galois : galois K (fixedField G).
- -
-End IntermediateGroup.
- -
-End FundamentalTheoremOfGaloisTheory.
- -
-End GaloisTheory.
- -
- -
-Notation "''Gal' ( V / U )" := (galoisG V U) : group_scope.
-Notation "''Gal' ( V / U )" := (galoisG_group V U) : Group_scope.
- -
-