let F be Field; for E being F -finite FieldExtension of F st ( for K being FieldExtension of E
for h being F -fixing Monomorphism of E,K holds h is Automorphism of E ) holds
E is F -normal
let E be F -finite FieldExtension of F; ( ( for K being FieldExtension of E
for h being F -fixing Monomorphism of E,K holds h is Automorphism of E ) implies E is F -normal )
assume AS:
for K being FieldExtension of E
for h being F -fixing Monomorphism of E,K holds h is Automorphism of E
; E is F -normal
consider T being finite F -algebraic Subset of E such that
A:
E == FAdj (F,T)
by FIELD_7:37;
B:
doubleLoopStr(# the carrier of E, the addF of E, the multF of E, the OneF of E, the ZeroF of E #) = doubleLoopStr(# the carrier of (FAdj (F,T)), the addF of (FAdj (F,T)), the multF of (FAdj (F,T)), the OneF of (FAdj (F,T)), the ZeroF of (FAdj (F,T)) #)
by A, FIELD_7:def 1;
now for a being Element of E holds MinPoly (a,F) splits_in Elet a be
Element of
E;
MinPoly (a,F) splits_in Eset T1 =
T \/ {a};
reconsider T1 =
T \/ {a} as non
empty finite F -algebraic Subset of
E ;
Z:
E == FAdj (
F,
T1)
by A, B, lemNor31;
set M =
{ (MinPoly (a,F)) where a is Element of T1 : verum } ;
a in {a}
by TARSKI:def 1;
then H:
a in T1
by XBOOLE_0:def 3;
then E:
MinPoly (
a,
F)
in { (MinPoly (a,F)) where a is Element of T1 : verum }
;
then reconsider M =
{ (MinPoly (a,F)) where a is Element of T1 : verum } as non
empty Subset of the
carrier of
(Polynom-Ring F) by E, TARSKI:def 3;
defpred S1[
object ,
object ]
means ex
a being
Element of
T1 st
(
a = $1 & $2
= MinPoly (
a,
F) );
E1:
for
a being
Element of
T1 ex
y being
Element of
M st
S1[
a,
y]
consider f being
Function of
T1,
M such that E2:
for
a being
Element of
T1 holds
S1[
a,
f . a]
from FUNCT_2:sch 3(E1);
E3:
dom f = T1
by FUNCT_2:def 1;
rng f = M
then reconsider M =
M as non
empty finite Subset of the
carrier of
(Polynom-Ring F) ;
(
rng (canFS M) c= M &
M c= the
carrier of
(Polynom-Ring F) )
by FINSEQ_1:def 4;
then
(
len (canFS M) = card M &
rng (canFS M) c= the
carrier of
(Polynom-Ring F) )
by FINSEQ_1:93;
then reconsider G =
canFS M as non
empty FinSequence of the
carrier of
(Polynom-Ring F) by FINSEQ_1:def 4;
reconsider p =
Product G as
Element of the
carrier of
(Polynom-Ring F) ;
F:
ex
i being
Element of
dom G st
G . i = MinPoly (
a,
F)
not
Product G is
constant
then reconsider pF =
Product G as non
constant Element of the
carrier of
(Polynom-Ring F) ;
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring E)
by FIELD_4:10;
then reconsider p =
pF as
Element of the
carrier of
(Polynom-Ring E) ;
(
deg pF > 0 &
deg pF = deg p )
by FIELD_4:20, RING_4:def 4;
then reconsider p =
p as non
constant Element of the
carrier of
(Polynom-Ring E) by RING_4:def 4;
L1:
for
u being
Element of
T1 ex
i being
Element of
dom G st
G . i = MinPoly (
u,
F)
L2:
(
p = MinPoly (
a,
F) or ex
q being non
zero Polynomial of
F st
p = (MinPoly (a,F)) *' q )
proof
assume
p <> MinPoly (
a,
F)
;
ex q being non zero Polynomial of F st p = (MinPoly (a,F)) *' q
set x = the
Element of
T;
consider j being
Element of
dom G such that K1:
G . j = MinPoly (
a,
F)
by H, L1;
dom G = Seg (len G)
by FINSEQ_1:def 3;
then
( 1
<= j &
j <= len G )
by FINSEQ_1:1;
then
G = ((G | (j -' 1)) ^ <*(G . j)*>) ^ (G /^ j)
by FINSEQ_5:84;
then K2:
Product G =
(Product ((G | (j -' 1)) ^ <*(G . j)*>)) * (Product (G /^ j))
by GROUP_4:5
.=
((Product (G | (j -' 1))) * (Product <*(G . j)*>)) * (Product (G /^ j))
by GROUP_4:5
.=
((Product <*(G . j)*>) * (Product (G | (j -' 1)))) * (Product (G /^ j))
by GROUP_1:def 12
.=
(Product <*(G . j)*>) * ((Product (G | (j -' 1))) * (Product (G /^ j)))
by GROUP_1:def 3
;
reconsider r1 =
Product (G | (j -' 1)),
r2 =
Product (G /^ j) as
Polynomial of
F by POLYNOM3:def 10;
K3:
r1 *' r2 = (Product (G | (j -' 1))) * (Product (G /^ j))
by POLYNOM3:def 10;
Product <*(G . j)*> = MinPoly (
a,
F)
by K1, GROUP_4:9;
then K4:
p = (MinPoly (a,F)) *' (r1 *' r2)
by K2, K3, POLYNOM3:def 10;
then
r1 *' r2 is non
zero Polynomial of
F
;
hence
ex
q being non
zero Polynomial of
F st
p = (MinPoly (a,F)) *' q
by K4;
verum
end; L3:
for
u being
Element of
T1 holds
u in Roots p
deg (MinPoly (a,F)) > 0
by RING_4:def 4;
then L4:
MinPoly (
a,
F) is non
constant Polynomial of
F
by RATFUNC1:def 2;
set U = the
SplittingField of
p;
reconsider U = the
SplittingField of
p as
E -extending FieldExtension of
F ;
E is
Subfield of
U
by FIELD_4:7;
then
the
carrier of
E c= the
carrier of
U
by EC_PF_1:def 1;
then
T1 c= the
carrier of
U
;
then reconsider T2 =
T1 as
Subset of
U ;
G0:
MinPoly (
a,
F)
splits_in U
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring (FAdj (F,{a})))
by FIELD_4:10;
then reconsider pa =
p as
Element of the
carrier of
(Polynom-Ring (FAdj (F,{a}))) ;
E is
FieldExtension of
FAdj (
F,
{a})
by FIELD_4:7;
then
(
deg p > 0 &
deg pa = deg p )
by FIELD_4:20, RING_4:def 4;
then reconsider pa =
pa as non
constant Element of the
carrier of
(Polynom-Ring (FAdj (F,{a}))) by RING_4:def 4;
G1:
U is
SplittingField of
pa
proof
reconsider E1 =
E as
FieldExtension of
FAdj (
F,
{a})
by FIELD_4:7;
reconsider T2 =
T as
Subset of
E1 ;
P0:
FAdj (
F,
T1)
= FAdj (
(FAdj (F,{a})),
T2)
by FIELD_7:35;
now for x being Element of E1 st x in T2 holds
x is FAdj (F,{a}) -algebraic let x be
Element of
E1;
( x in T2 implies x is FAdj (F,{a}) -algebraic )assume
x in T2
;
x is FAdj (F,{a}) -algebraic consider p being non
zero Polynomial of
F such that H:
Ext_eval (
p,
x)
= 0. E
by FIELD_6:43;
reconsider p1 =
p as
Polynomial of
(FAdj (F,{a})) by FIELD_4:8;
p <> 0_. F
;
then
p1 <> 0_. (FAdj (F,{a}))
by FIELD_4:12;
then reconsider p1 =
p1 as non
zero Polynomial of
(FAdj (F,{a})) by UPROOTS:def 5;
(
p is
Element of the
carrier of
(Polynom-Ring F) &
p1 is
Element of the
carrier of
(Polynom-Ring (FAdj (F,{a}))) )
by POLYNOM3:def 10;
then
Ext_eval (
p1,
x)
= 0. E
by H, FIELD_7:15;
hence
x is
FAdj (
F,
{a})
-algebraic
by FIELD_6:43;
verum end;
then P1:
T is
FAdj (
F,
{a})
-algebraic Subset of
E1
by FIELD_7:def 12;
T c= T1
by XBOOLE_1:7;
then
(
T c= Roots p &
Roots p c= Roots (
U,
p) )
by L3, FIELD_4:28;
then
T c= Roots (
U,
p)
;
hence
U is
SplittingField of
pa
by Z, P0, P1, lemNor32;
verum
end; now for o being object st o in Roots (U,(MinPoly (a,F))) holds
o in the carrier of Elet o be
object ;
( o in Roots (U,(MinPoly (a,F))) implies o in the carrier of E )assume LL:
o in Roots (
U,
(MinPoly (a,F)))
;
o in the carrier of Ethen reconsider b =
o as
Element of
U ;
Roots (
U,
(MinPoly (a,F)))
= { x where x is Element of U : x is_a_root_of MinPoly (a,F),U }
by FIELD_4:def 4;
then consider c being
Element of
U such that LK:
(
c = b &
c is_a_root_of MinPoly (
a,
F),
U )
by LL;
the
carrier of
(Polynom-Ring F) c= the
carrier of
(Polynom-Ring (FAdj (F,{b})))
by FIELD_4:10;
then reconsider pb =
pF as
Element of the
carrier of
(Polynom-Ring (FAdj (F,{b}))) ;
(
deg pF > 0 &
deg pb = deg pF )
by FIELD_4:20, RING_4:def 4;
then reconsider pb =
pb as non
constant Element of the
carrier of
(Polynom-Ring (FAdj (F,{b}))) by RING_4:def 4;
G2:
U is
SplittingField of
pb
proof
G0:
U is
FieldExtension of
FAdj (
F,
{b})
by FIELD_4:7;
reconsider U1 =
U as
FieldExtension of
FAdj (
F,
{b})
by FIELD_4:7;
p splits_in U
by FIELD_8:def 1;
then consider x being non
zero Element of
U,
r being
Ppoly of
U such that G3:
p = x * r
by FIELD_4:def 5;
G4:
pb splits_in U
by G3, FIELD_4:def 5;
GG:
Roots (
U1,
pb)
= Roots (
U,
p)
by lemNor3z;
L6:
FAdj (
F,
T2)
== FAdj (
F,
T1)
by lemh1;
now for V being FieldExtension of FAdj (F,{b}) st pb splits_in V & V is Subfield of U holds
V == Ulet V be
FieldExtension of
FAdj (
F,
{b});
( pb splits_in V & V is Subfield of U implies V == U )assume G5:
(
pb splits_in V &
V is
Subfield of
U )
;
V == Uthen consider y being non
zero Element of
V,
s being
Ppoly of
V such that K2:
pb = y * s
by FIELD_4:def 5;
G9:
U is
V -extending
by G5, FIELD_4:7;
G6:
p splits_in V
by K2, FIELD_4:def 5;
GH:
Roots (
U1,
pb)
c= the
carrier of
V
by G9, G4, G5, FIELD_8:27;
F is
Subfield of
V
by FIELD_4:7;
then G8:
FAdj (
F,
(Roots (U,p))) is
Subfield of
V
by G5, GG, GH, FIELD_6:37;
Roots p c= Roots (
U,
p)
by FIELD_4:28;
then
T1 c= Roots (
U,
p)
by L3;
then
FAdj (
F,
T2) is
Subfield of
FAdj (
F,
(Roots (U,p)))
by FIELD_7:10;
then
FAdj (
F,
T2) is
Subfield of
V
by G8, EC_PF_1:5;
then
V is
FieldExtension of
FAdj (
F,
T2)
by FIELD_4:7;
then
V is
FieldExtension of
E
by FIELD_12:37, L6, Z, helpb;
hence
V == U
by G5, G6, FIELD_8:def 1;
verum end;
hence
U is
SplittingField of
pb
by G0, G3, FIELD_4:def 5, FIELD_8:def 1;
verum
end;
id F is
isomorphism
;
then reconsider F1 =
F as
F -homomorphic F -isomorphic Field by RING_2:def 4, RING_3:def 4;
reconsider U1 =
U as
FieldExtension of
F1 ;
reconsider b1 =
b as
Element of
U1 ;
reconsider f =
id F as
Isomorphism of
F,
F1 ;
G3:
Ext_eval (
(MinPoly (a,F)),
a)
= 0. E
by FIELD_6:51;
G4:
Ext_eval (
((PolyHom f) . (MinPoly (a,F))),
b1) =
Ext_eval (
(MinPoly (a,F)),
b1)
by K1
.=
0. U1
by LK, FIELD_4:def 2
;
then G5:
(
Psi (
a,
b1,
f,
(MinPoly (a,F))) is
f -extending &
Psi (
a,
b1,
f,
(MinPoly (a,F))) is
isomorphism )
by G3, FIELD_8:55;
then reconsider Fb =
FAdj (
F,
{b}) as
FAdj (
F,
{a})
-homomorphic FAdj (
F,
{a})
-isomorphic Field by RING_2:def 4, RING_3:def 4;
reconsider i =
Psi (
a,
b1,
f,
(MinPoly (a,F))) as
Isomorphism of
(FAdj (F,{a})),
Fb by G5;
(PolyHom i) . pa = (PolyHom f) . pF
then reconsider U1 =
U1 as
SplittingField of
(PolyHom i) . pa by K1, G2;
reconsider U =
U as
SplittingField of
pa by G1;
consider h being
Function of
U,
U1 such that G6:
(
h is
i -extending &
h is
isomorphism )
by FIELD_8:57;
G7:
(
h is
additive &
h is
multiplicative &
h is
unity-preserving )
by G6;
reconsider U =
U as
FieldExtension of
E ;
reconsider h =
h as
Function of
U,
U ;
E is
Subfield of
U
by FIELD_4:7;
then
the
carrier of
E c= the
carrier of
U
by EC_PF_1:def 1;
then reconsider g =
h | the
carrier of
E as
Function of
E,
U by FUNCT_2:32;
(
g is
additive &
g is
multiplicative &
g is
unity-preserving )
then reconsider g =
g as
Monomorphism of
E,
U ;
then
g is
F -fixing
by FIELD_8:def 2;
then reconsider g =
g as
Automorphism of
E by AS;
g . a = b
proof
(
a in {a} &
{a} is
Subset of
(FAdj (F,{a})) )
by TARSKI:def 1, FIELD_6:35;
then reconsider c =
a as
Element of
(FAdj (F,{a})) ;
thus g . a =
h . c
by FUNCT_1:49
.=
(Psi (a,b1,f,(MinPoly (a,F)))) . c
by G6, FIELD_8:def 6
.=
b
by G3, G4, lemNor3e
;
verum
end; hence
o in the
carrier of
E
;
verum end; then
Roots (
U,
(MinPoly (a,F)))
c= the
carrier of
E
;
hence
MinPoly (
a,
F)
splits_in E
by G0, FIELD_8:27;
verum end;
hence
E is F -normal
by lemmin; verum