From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/mathcomp.field.galois.html | 505 ++++++++++++++++----------------
1 file changed, 253 insertions(+), 252 deletions(-)
(limited to 'docs/htmldoc/mathcomp.field.galois.html')
diff --git a/docs/htmldoc/mathcomp.field.galois.html b/docs/htmldoc/mathcomp.field.galois.html
index 5b28ffb..76c8ddc 100644
--- a/docs/htmldoc/mathcomp.field.galois.html
+++ b/docs/htmldoc/mathcomp.field.galois.html
@@ -21,7 +21,6 @@
@@ -85,13 +84,13 @@
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.
+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.
+Lemma splittingFieldForS (K M E : {subfield L}) p :
+ (K ≤ M)%VS → (M ≤ E)%VS →
+ splittingFieldFor K p E → splittingFieldFor M p E.
End SplittingFieldFor.
@@ -101,164 +100,164 @@
Variables (F : fieldType) (L : fieldExtType F).
-Implicit Types (U V : {vspace L}) (K E : {subfield L}) (f g : 'End(L)).
+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.
+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}]
+ 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 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 kHom1 U V : kHom U V \1.
-Lemma k1HomE V f : kHom 1 V f = ahom_in V f.
+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 kHom_lrmorphism (f : 'End(L)) : reflect (lrmorphism f) (kHom 1 {:L} f).
-Lemma k1AHom V (f : 'AEnd(L)) : kHom 1 V 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.
+ 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 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 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.
+ (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.
+ (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_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_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).
+ 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].
+ 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 →
+ 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 →
+ (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).
+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]).
+ 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].
+Lemma kHomExtendE z : kHomExtend z = (map_poly f (Fadjoin_poly E x z)).[y].
-Hypotheses (sKE : (K ≤ E)%VS) (homKf : kHom K E f).
+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_id z : z \in E → kHomExtend z = f z.
-Lemma kHomExtend_val : kHomExtend x = y.
+Lemma kHomExtend_val : kHomExtend x = y.
Lemma kHomExtend_poly p :
- p \in polyOver E → kHomExtend p.[x] = (map_poly f p).[y].
+ p \in polyOver E → kHomExtend p.[x] = (map_poly f p).[y].
-Lemma kHomExtendP : kHom K <<E; x>> kHomExtend.
+Lemma kHomExtendP : kHom K <<E; x>> kHomExtend.
End kHomExtend.
-Definition kAut U V f := kHom U V f && (f @: V == V)%VS.
+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 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 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 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 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 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 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 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_kHomf K f : kHom K {:L} f → kHom K {:L} f^-1.
-Lemma inv_is_ahom (f : 'AEnd(L)) : ahom_in {: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.
+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).
+ 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 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}}.
+ (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.
+Notation "f ^-1" := (inv_ahom f) : lrfun_scope.
@@ -276,44 +275,44 @@
Definition axiom (L : fieldExtType F) :=
- exists2 p : {poly L}, p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}.
+ 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)}.
+ Class {base : FieldExt.class_of F L; _ : axiom (FieldExt.Pack _ base)}.
-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).
+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 T.
+Definition clone c of phant_id class c := @Pack phF T c.
-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 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 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.
+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.
@@ -358,14 +357,14 @@
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)
+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)
+Notation "[ 'splittingFieldType' F 'of' L ]" :=
+ (@clone _ (Phant F) L _ _ id)
(at level 0, format "[ 'splittingFieldType' F 'of' L ]") : form_scope.
@@ -375,8 +374,8 @@
Lemma normal_field_splitting (F : fieldType) (L : fieldExtType F) :
- (∀ (K : {subfield L}) x,
- ∃ r, minPoly K x == \prod_(y <- r) ('X - y%:P)) →
+ (∀ (K : {subfield L}) x,
+ ∃ r, minPoly K x == \prod_(y <- r) ('X - y%:P)) →
SplittingField.axiom L.
@@ -384,7 +383,7 @@
Canonical regular_splittingFieldType (F : fieldType) :=
- SplittingFieldType F F^o (regular_splittingAxiom F).
+ SplittingFieldType F F^o (regular_splittingAxiom F).
Section SplittingFieldTheory.
@@ -393,15 +392,15 @@
Variables (F : fieldType) (L : splittingFieldType F).
-Implicit Types (U V W : {vspace L}).
-Implicit Types (K M E : {subfield L}).
+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}}.
+ {p : {poly L} | p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}}.
Fact fieldOver_splitting E : SplittingField.axiom (fieldOver_fieldExtType E).
@@ -409,14 +408,14 @@
SplittingFieldType (subvs_of E) (fieldOver E) (fieldOver_splitting E).
-Lemma enum_AEnd : {kAutL : seq 'AEnd(L) | ∀ f, f \in kAutL}.
+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).
+ ∃ 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}}.
+Lemma kHom_to_AEnd K E f : kHom K E f → {g : 'AEnd(L) | {in E, f =1 val g}}.
End SplittingFieldTheory.
@@ -435,19 +434,19 @@
Variables (F : fieldType) (L : splittingFieldType F).
-Implicit Types (U V W : {vspace L}) (K M E : {subfield L}).
+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.
+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)].
+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)].
+Canonical AEnd_finType := Eval hnf in FinType 'AEnd(L) AEnd_finMixin.
+Canonical AEnd_subFinType := Eval hnf in [subFinType of 'AEnd(L)].
@@ -456,43 +455,43 @@
the group operation is the categorical composition operation
@@ -522,7 +521,7 @@
Section gal_of_Definition.
-Variable V : {vspace L}.
+Variable V : {vspace L}.
@@ -532,13 +531,13 @@
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)).
+
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.
+
Fact gal_sgvalK :
cancel gal_sgval Gal.
+
Let gal_sgval_inj :=
can_inj gal_sgvalK.
Definition gal_eqMixin :=
CanEqMixin gal_sgvalK.
@@ -552,11 +551,11 @@
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_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 :=
@@ -566,20 +565,20 @@
Canonical gal_finGroupType :=
Eval hnf in FinGroupType gal_invP.
-
Coercion gal_repr u :
'AEnd(L) :=
repr (
sgval (
gal_sgval u)).
+
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}.
+
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_reprK :
cancel gal_repr gal.
-
Lemma gal_repr_inj :
injective gal_repr.
+
Lemma gal_repr_inj :
injective gal_repr.
-
Lemma gal_AEnd x :
gal_repr x \in kAEnd 1 (
agenv V).
+
Lemma gal_AEnd x :
gal_repr x \in kAEnd 1 (
agenv V).
End gal_of_Definition.
@@ -587,30 +586,30 @@
-
Lemma gal_eqP E {
x y :
gal_of E} :
reflect {in E, x =1 y} (
x == y).
+
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 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 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 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 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 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 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}.
+
Lemma galV E (
x :
gal_of E) :
{in E, (
x^-1)%
g =1 x^-1%
VF}.
-
Definition galoisG V U :=
gal V @* <<kAEnd (
U :&: V)
V>>.
-
Canonical galoisG_group E U :=
Eval hnf in [group of (galoisG E U)].
+
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_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_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 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}}.
+
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.
+ (
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.
+ (
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).
+ (
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).
+
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 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).
+
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.
+
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 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).
+
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} :=
+
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 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 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.
+ (
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_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.
+
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 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).
+
Definition galNorm U V a :=
\prod_(x in 'Gal(V / U)) (x a).
Section TraceAndNormMorphism.
-
Variables U V :
{vspace L}.
+
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 galNorm1 :
galNorm U V 1
= 1.
-
Lemma galNormM :
{morph galNorm U V : a b / a × b}.
+
Lemma galNormM :
{morph galNorm U V : a b / a × b}.
-
Lemma galNormV :
{morph galNorm U V : a / a^-1}.
+
Lemma galNormV :
{morph galNorm U V : a / a^-1}.
-
Lemma galNormX n :
{morph galNorm U V : a / a ^+ n}.
+
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 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 galNorm0 :
galNorm U V 0
= 0.
-
Lemma galNorm_eq0 a :
(galNorm U V a == 0
) = (a == 0
).
+
Lemma galNorm_eq0 a :
(galNorm U V a == 0
) = (a == 0
).
End TraceAndNormMorphism.
@@ -746,169 +745,169 @@
Section TraceAndNormField.
-
Variables K E :
{subfield L}.
+
Variables K E :
{subfield L}.
Lemma galTrace_fixedField a :
-
a \in E → galTrace K E a \in fixedField 'Gal(E / K).
+
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.
+
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).
+
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.
+
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.
+
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.
+ (
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)}
+
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 normalFieldf K :
normalField K {:L}.
-
Lemma normalFieldS K M E : (
K ≤ M)%
VS → normalField K E → normalField M E.
+
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)
+ (
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}}.
+ (
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.
+ (
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)}
+ (
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].
+
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 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_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)]}
+ (
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])
+
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).
+
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_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 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_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 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).
+
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}).
+
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] }.
+
{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_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 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_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 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.
+
Lemma fixedField_galois E (
A :
{set gal_of E}):
galois (
fixedField A)
E.
Section FundamentalTheoremOfGaloisTheory.
-
Variables E K :
{subfield L}.
+
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).
+
Variable M :
{subfield L}.
+
Hypothesis (
sKME : (
K ≤ M ≤ E)%
VS) (
nKM :
normalField K M).
Lemma normalField_galois :
galois K M.
@@ -918,31 +917,31 @@
Lemma normalField_cast_eq x :
-
x \in 'Gal(E / K) → {in M, normalField_cast x =1 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}}.
+
{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_ker :
'ker normalField_cast = 'Gal(E / M).
-
Lemma normalField_normal :
'Gal(E / M) <| 'Gal(E / K).
+
Lemma normalField_normal :
'Gal(E / M) <| 'Gal(E / K).
-
Lemma normalField_img :
normalField_cast @* 'Gal(E / K) = 'Gal(M / 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.
+
{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).
+
Lemma normalField_isog :
'Gal(E / K) / 'Gal(E / M) \isog 'Gal(M / K).
End IntermediateField.
@@ -951,8 +950,8 @@
Section IntermediateGroup.
-
Variable G :
{group gal_of E}.
-
Hypothesis nsGgalE :
G <| 'Gal(E / K).
+
Variable G :
{group gal_of E}.
+
Hypothesis nsGgalE :
G <| 'Gal(E / K).
Lemma normal_fixedField_galois :
galois K (
fixedField G).
@@ -967,8 +966,10 @@
End GaloisTheory.
-
Notation "''Gal' ( V / U )" := (
galoisG V U) :
group_scope.
-
Notation "''Gal' ( V / U )" := (
galoisG_group V U) :
Group_scope.
+
+
+
Notation "''Gal' ( V / U )" := (
galoisG V U) :
group_scope.
+
Notation "''Gal' ( V / U )" := (
galoisG_group V U) :
Group_scope.