let F1 be Field; for F2 being F1 -homomorphic F1 -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let F2 be F1 -homomorphic F1 -isomorphic Field; for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let h be Isomorphism of F1,F2; for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let p be non constant Element of the carrier of (Polynom-Ring F1); for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let E1 be SplittingField of p; for E2 being SplittingField of (PolyHom h) . p ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
let E2 be SplittingField of (PolyHom h) . p; ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
defpred S1[ Nat] means for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = $1 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism );
II:
now for k being Nat st ( for j being Nat st j < k holds
S1[j] ) holds
S1[k]let k be
Nat;
( ( for j being Nat st j < k holds
S1[j] ) implies S1[b1] )assume IV:
for
j being
Nat st
j < k holds
S1[
j]
;
S1[b1]per cases
( k = 0 or k > 0 )
;
suppose S:
k = 0
;
S1[b1]now for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = 0 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )let F1 be
Field;
for F2 being F1 -homomorphic F1 -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = 0 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )let F2 be
F1 -homomorphic F1 -isomorphic Field;
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = 0 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )let h be
Isomorphism of
F1,
F2;
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = 0 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )let p be non
constant Element of the
carrier of
(Polynom-Ring F1);
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = 0 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )let E1 be
SplittingField of
p;
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = 0 holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )let E2 be
SplittingField of
(PolyHom h) . p;
( card ((Roots (E1,p)) \ the carrier of F1) = 0 implies ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism ) )H0:
(
p splits_in E1 &
(PolyHom h) . p splits_in E2 )
by defspl;
H1:
(
F1 is
FieldExtension of
F1 &
F2 is
FieldExtension of
F2 )
by FIELD_4:6;
H2:
(
F1 is
Subfield of
E1 &
F2 is
Subfield of
E2 )
by FIELD_4:7;
assume
card ((Roots (E1,p)) \ the carrier of F1) = 0
;
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )then
(Roots (E1,p)) \ the
carrier of
F1 = {}
;
then
Roots (
E1,
p)
c= the
carrier of
F1
by XBOOLE_1:37;
then A0:
p splits_in F1
by H0, H1, lemma6;
then A1:
F1 == E1
by H1, H2, defspl;
then reconsider idF1 =
id E1 as
Function of
E1,
F1 ;
(PolyHom h) . p splits_in F2
by A0, lemma6a;
then A2:
F2 == E2
by H1, H2, defspl;
then reconsider idF2 =
id F2 as
Function of
F2,
E2 ;
reconsider hidF1 =
h * idF1 as
Function of
E1,
F2 by FUNCT_2:13;
h * idF1 is
Function of
E1,
F2
by FUNCT_2:13;
then reconsider f =
idF2 * (h * idF1) as
Function of
E1,
E2 by FUNCT_2:13;
then K4:
f is
h -extending
by A1;
K5:
(
idF1 is
isomorphism &
idF2 is
isomorphism )
by A1, A2, unique20;
then K6:
hidF1 is
linear
;
hidF1 is
onto
by A1, FUNCT_2:27;
then
f is
onto
by A2, FUNCT_2:27;
hence
ex
f being
Function of
E1,
E2 st
(
f is
h -extending &
f is
isomorphism )
by K6, K5, K4;
verum end; hence
S1[
k]
by S;
verum suppose S:
k > 0
;
S1[b1]now for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = k holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )let F1 be
Field;
for F2 being F1 -homomorphic F1 -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = k holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )let F2 be
F1 -homomorphic F1 -isomorphic Field;
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = k holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )let h be
Isomorphism of
F1,
F2;
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = k holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )let p be non
constant Element of the
carrier of
(Polynom-Ring F1);
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = k holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )let E1 be
SplittingField of
p;
for E2 being SplittingField of (PolyHom h) . p st card ((Roots (E1,p)) \ the carrier of F1) = k holds
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )let E2 be
SplittingField of
(PolyHom h) . p;
( card ((Roots (E1,p)) \ the carrier of F1) = k implies ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism ) )assume AS:
card ((Roots (E1,p)) \ the carrier of F1) = k
;
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )set a = the
Element of
(Roots (E1,p)) \ the
carrier of
F1;
(Roots (E1,p)) \ the
carrier of
F1 <> {}
by AS, S;
then A1:
( the
Element of
(Roots (E1,p)) \ the
carrier of
F1 in Roots (
E1,
p) & not the
Element of
(Roots (E1,p)) \ the
carrier of
F1 in the
carrier of
F1 )
by XBOOLE_0:def 5;
then reconsider a = the
Element of
(Roots (E1,p)) \ the
carrier of
F1 as
Element of
E1 ;
Roots (
E1,
p)
= { b where b is Element of E1 : b is_a_root_of p,E1 }
by FIELD_4:def 4;
then consider j being
Element of
E1 such that J:
(
j = a &
j is_a_root_of p,
E1 )
by A1;
A2:
Ext_eval (
p,
a)
= 0. E1
by J, FIELD_4:def 2;
reconsider a =
a as
F1 -algebraic Element of
E1 ;
set r =
MinPoly (
a,
F1);
consider u being
Polynomial of
F1 such that A3:
(MinPoly (a,F1)) *' u = p
by A2, FIELD_6:53, RING_4:1;
reconsider y =
u as
Element of the
carrier of
(Polynom-Ring F1) by POLYNOM3:def 10;
A4:
p = (MinPoly (a,F1)) * y
by A3, POLYNOM3:def 10;
reconsider rh =
(PolyHom h) . (MinPoly (a,F1)),
yh =
(PolyHom h) . y as
Polynomial of
F2 ;
A6:
(PolyHom h) . p =
((PolyHom h) . (MinPoly (a,F1))) * ((PolyHom h) . y)
by A4, FIELD_1:25
.=
rh *' yh
by POLYNOM3:def 10
;
reconsider rhE2 =
rh,
yhE2 =
yh as
Polynomial of
E2 by FIELD_4:8;
(
rhE2 is
Element of the
carrier of
(Polynom-Ring E2) &
rh is
Element of the
carrier of
(Polynom-Ring F2) )
by POLYNOM3:def 10;
then
deg rhE2 = deg rh
by FIELD_4:20;
then A5a:
not
rhE2 is
constant
by RING_4:def 4, RATFUNC1:def 2;
yh <> 0_. F2
by A6;
then
yhE2 <> 0_. E2
by FIELD_4:12;
then A7a:
not
yhE2 is
zero
by UPROOTS:def 5;
A100:
rh *' yh = rhE2 *' yhE2
by FIELD_4:17;
rh *' yh splits_in E2
by A6, defspl;
then
ex
x being non
zero Element of
E2 ex
qx being
Ppoly of
E2 st
rh *' yh = x * qx
by FIELD_4:def 5;
then
rhE2 splits_in E2
by A5a, A7a, A100, FIELD_4:def 5, lemppolspl3;
then consider rhr being non
zero Element of
E2,
qrh being
Ppoly of
E2 such that A9:
rh = rhr * qrh
by FIELD_4:def 5;
consider b being
Element of
E2 such that A11:
b is_a_root_of rhr * qrh
by POLYNOM5:def 8;
A12:
rhr * qrh is
Element of the
carrier of
(Polynom-Ring E2)
by POLYNOM3:def 10;
eval (
(rhr * qrh),
b)
= 0. E2
by A11, POLYNOM5:def 7;
then K1:
Ext_eval (
rh,
b)
= 0. E2
by A9, A12, FIELD_4:26;
A22:
Ext_eval (
(MinPoly (a,F1)),
a)
= 0. E1
by FIELD_6:51;
reconsider b =
b as
F2 -algebraic Element of
E2 ;
K:
(
Psi (
a,
b,
h,
(MinPoly (a,F1))) is
h -extending &
Psi (
a,
b,
h,
(MinPoly (a,F1))) is
isomorphism )
by K1, A22, unique1;
set F1a =
FAdj (
F1,
{a});
reconsider F2b =
FAdj (
F2,
{b}) as
FAdj (
F1,
{a})
-homomorphic FAdj (
F1,
{a})
-isomorphic Field by K, RING_2:def 4, RING_3:def 4;
reconsider g =
Psi (
a,
b,
h,
(MinPoly (a,F1))) as
Isomorphism of
(FAdj (F1,{a})),
F2b by K;
reconsider E1a =
E1 as
FieldExtension of
FAdj (
F1,
{a})
by FIELD_4:7;
reconsider E2a =
E2 as
FieldExtension of
F2b by FIELD_4:7;
the
carrier of
(Polynom-Ring F1) c= the
carrier of
(Polynom-Ring (FAdj (F1,{a})))
by FIELD_4:10;
then reconsider f =
p as
Element of the
carrier of
(Polynom-Ring (FAdj (F1,{a}))) ;
(
deg f = deg p &
deg p > 0 )
by FIELD_4:20, RING_4:def 4;
then reconsider f =
f as non
constant Element of the
carrier of
(Polynom-Ring (FAdj (F1,{a}))) by RING_4:def 4;
reconsider E1a =
E1a as
SplittingField of
f by splift;
reconsider aa =
a as
Element of
E1a ;
(PolyHom g) . f = (PolyHom h) . p
then reconsider E2a =
E2a as
SplittingField of
(PolyHom g) . f by splift;
K8:
{a} is
Subset of
(FAdj (F1,{a}))
by FIELD_6:35;
K7:
a in {a}
by TARSKI:def 1;
Ext_eval (
f,
aa)
= 0. E1a
by A2, lemma7b;
then
aa is_a_root_of f,
E1a
by FIELD_4:def 2;
then
a in { x where x is Element of E1a : x is_a_root_of f,E1a }
;
then K6:
a in Roots (
E1a,
f)
by FIELD_4:def 4;
K4:
a in (Roots (E1a,f)) \ the
carrier of
F1
by A1, K6, XBOOLE_0:def 5;
K5:
not
a in (Roots (E1a,f)) \ the
carrier of
(FAdj (F1,{a}))
by K7, K8, XBOOLE_0:def 5;
(Roots (E1a,f)) \ the
carrier of
(FAdj (F1,{a})) c= (Roots (E1a,f)) \ the
carrier of
F1
proof
now for o being object st o in (Roots (E1a,f)) \ the carrier of (FAdj (F1,{a})) holds
o in (Roots (E1a,f)) \ the carrier of F1let o be
object ;
( o in (Roots (E1a,f)) \ the carrier of (FAdj (F1,{a})) implies o in (Roots (E1a,f)) \ the carrier of F1 )assume L:
o in (Roots (E1a,f)) \ the
carrier of
(FAdj (F1,{a}))
;
o in (Roots (E1a,f)) \ the carrier of F1
F1 is
Subfield of
FAdj (
F1,
{a})
by FIELD_4:7;
then
the
carrier of
F1 c= the
carrier of
(FAdj (F1,{a}))
by EC_PF_1:def 1;
then
(
o in Roots (
E1a,
f) & not
o in the
carrier of
F1 )
by L, XBOOLE_0:def 5;
hence
o in (Roots (E1a,f)) \ the
carrier of
F1
by XBOOLE_0:def 5;
verum end;
hence
(Roots (E1a,f)) \ the
carrier of
(FAdj (F1,{a})) c= (Roots (E1a,f)) \ the
carrier of
F1
;
verum
end; then
(Roots (E1a,f)) \ the
carrier of
(FAdj (F1,{a})) c< (Roots (E1a,f)) \ the
carrier of
F1
by K4, K5, XBOOLE_0:def 8;
then L2:
card ((Roots (E1a,f)) \ the carrier of (FAdj (F1,{a}))) < card ((Roots (E1a,f)) \ the carrier of F1)
by CARD_2:48;
card ((Roots (E1a,f)) \ the carrier of F1) = k
by AS, m4spl;
then consider h1 being
Function of
E1a,
E2a such that L1:
(
h1 is
g -extending &
h1 is
isomorphism )
by IV, L2;
reconsider h1 =
h1 as
Function of
E1,
E2 ;
thus
ex
f being
Function of
E1,
E2 st
(
f is
h -extending &
f is
isomorphism )
by L1, K, e1a;
verum end; hence
S1[
k]
;
verum end;
I:
for k being Nat holds S1[k]
from NAT_1:sch 4(II);
consider n being Nat such that
H:
card ((Roots (E1,p)) \ the carrier of F1) = n
;
thus
ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
by H, I; verum