let F1 be Field; for F2 being F1 -homomorphic F1 -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let F2 be F1 -homomorphic F1 -isomorphic Field; for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let h be Isomorphism of F1,F2; for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let E1 be FieldExtension of F1; for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let E2 be FieldExtension of F2; for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let a be Element of E1; for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let b be Element of E2; for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
let p be irreducible Element of the carrier of (Polynom-Ring F1); ( Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 implies ( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism ) )
assume AS:
( Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 )
; ( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
set f = Psi (a,b,h,p);
set C1 = the carrier of (FAdj (F1,{a}));
set C2 = the carrier of (FAdj (F2,{b}));
reconsider a = a as F1 -algebraic Element of E1 by AS, FIELD_6:43;
H1:
FAdj (F1,{a}) = RAdj (F1,{a})
by FIELD_6:56;
H2:
the carrier of (RAdj (F1,{a})) = { (Ext_eval (p,a)) where p is Polynomial of F1 : verum }
by FIELD_6:45;
reconsider b = b as F2 -algebraic Element of E2 by AS, FIELD_6:43;
now for x being Element of F1 holds (Psi (a,b,h,p)) . x = h . xlet x be
Element of
F1;
(Psi (a,b,h,p)) . x = h . xreconsider g1 =
x | F1 as
Element of the
carrier of
(Polynom-Ring F1) by POLYNOM3:def 10;
H6:
the
carrier of
(Polynom-Ring F2) c= the
carrier of
(Polynom-Ring E2)
by FIELD_4:10;
(h . x) | F2 is
Element of the
carrier of
(Polynom-Ring F2)
by POLYNOM3:def 10;
then reconsider g2 =
(h . x) | F2 as
Element of the
carrier of
(Polynom-Ring E2) by H6;
x = Ext_eval (
(x | F1),
a)
by u3;
hence (Psi (a,b,h,p)) . x =
Ext_eval (
((PolyHom h) . g1),
b)
by AS, psi
.=
Ext_eval (
((h . x) | F2),
b)
by hcon
.=
LC ((h . x) | F2)
by FIELD_6:28
.=
h . x
by hcon2
;
verum end;
hence
Psi (a,b,h,p) is h -extending
; Psi (a,b,h,p) is isomorphism
set F1a = FAdj (F1,{a});
set F2b = FAdj (F2,{b});
reconsider f = Psi (a,b,h,p) as Function of (FAdj (F1,{a})),(FAdj (F2,{b})) ;
A:
f . (1. (FAdj (F1,{a}))) = 1. (FAdj (F2,{b}))
proof
(
F1 is
Subfield of
FAdj (
F1,
{a}) &
F2 is
Subfield of
FAdj (
F2,
{b}) )
by FIELD_6:36;
then A0:
(
1. (FAdj (F1,{a})) = 1. F1 &
1. (FAdj (F2,{b})) = 1. F2 )
by EC_PF_1:def 1;
A1:
1_. (FAdj (F1,{a})) = 1_. F1
by FIELD_4:14;
A2:
(PolyHom h) . (1_. (FAdj (F1,{a}))) =
(PolyHom h) . (1_. F1)
by FIELD_4:14
.=
(PolyHom h) . ((1. F1) | F1)
by RING_4:14
.=
(h . (1_ F1)) | F2
by hcon
.=
(1_ F2) | F2
by GROUP_1:def 13
.=
(1. (FAdj (F2,{b}))) | (FAdj (F2,{b}))
by A0, FIELD_6:23
.=
1_. (FAdj (F2,{b}))
by RING_4:14
;
reconsider r =
1_. (FAdj (F1,{a})) as
Element of the
carrier of
(Polynom-Ring F1) by A1, POLYNOM3:def 10;
thus f . (1. (FAdj (F1,{a}))) =
f . (Ext_eval (r,a))
by A1, u1
.=
Ext_eval (
((PolyHom h) . r),
b)
by AS, psi
.=
Ext_eval (
(1_. F2),
b)
by A2, FIELD_4:14
.=
1. (FAdj (F2,{b}))
by u1
;
verum
end;
B:
now for x, y being Element of (FAdj (F1,{a})) holds f . (x * y) = (f . x) * (f . y)let x,
y be
Element of
(FAdj (F1,{a}));
f . (x * y) = (f . x) * (f . y)
x in { (Ext_eval (p,a)) where p is Polynomial of F1 : verum }
by H1, H2;
then consider r1 being
Polynomial of
F1 such that B1:
x = Ext_eval (
r1,
a)
;
y in { (Ext_eval (p,a)) where p is Polynomial of F1 : verum }
by H1, H2;
then consider r2 being
Polynomial of
F1 such that B2:
y = Ext_eval (
r2,
a)
;
reconsider q1 =
r1,
q2 =
r2 as
Element of the
carrier of
(Polynom-Ring F1) by POLYNOM3:def 10;
B3:
q1 * q2 = r1 *' r2
by POLYNOM3:def 10;
reconsider g1 =
(PolyHom h) . q1,
g2 =
(PolyHom h) . q2 as
Polynomial of
F2 ;
B4:
g1 *' g2 = ((PolyHom h) . q1) * ((PolyHom h) . q2)
by POLYNOM3:def 10;
B5:
(
f . x = Ext_eval (
g1,
b) &
f . y = Ext_eval (
g2,
b) )
by B1, B2, AS, psi;
thus f . (x * y) =
f . (Ext_eval ((r1 *' r2),a))
by u2, B1, B2
.=
Ext_eval (
((PolyHom h) . (q1 * q2)),
b)
by B3, AS, psi
.=
Ext_eval (
(g1 *' g2),
b)
by B4, FIELD_1:25
.=
(f . x) * (f . y)
by u2, B5
;
verum end;
C:
now for x, y being Element of (FAdj (F1,{a})) holds f . (x + y) = (f . x) + (f . y)let x,
y be
Element of
(FAdj (F1,{a}));
f . (x + y) = (f . x) + (f . y)
x in { (Ext_eval (p,a)) where p is Polynomial of F1 : verum }
by H1, H2;
then consider r1 being
Polynomial of
F1 such that B1:
x = Ext_eval (
r1,
a)
;
y in { (Ext_eval (p,a)) where p is Polynomial of F1 : verum }
by H1, H2;
then consider r2 being
Polynomial of
F1 such that B2:
y = Ext_eval (
r2,
a)
;
reconsider q1 =
r1,
q2 =
r2 as
Element of the
carrier of
(Polynom-Ring F1) by POLYNOM3:def 10;
reconsider q =
q1 + q2 as
Element of the
carrier of
(Polynom-Ring F1) ;
B3:
q1 + q2 = r1 + r2
by POLYNOM3:def 10;
reconsider g1 =
(PolyHom h) . q1,
g2 =
(PolyHom h) . q2 as
Polynomial of
F2 ;
B4:
g1 + g2 =
((PolyHom h) . q1) + ((PolyHom h) . q2)
by POLYNOM3:def 10
.=
(PolyHom h) . (q1 + q2)
by FIELD_1:24
;
B5:
(
f . x = Ext_eval (
g1,
b) &
f . y = Ext_eval (
g2,
b) )
by B1, B2, AS, psi;
thus f . (x + y) =
f . (Ext_eval ((r1 + r2),a))
by u2, B1, B2
.=
Ext_eval (
((PolyHom h) . q),
b)
by B3, AS, psi
.=
(f . x) + (f . y)
by u2, B4, B5
;
verum end;
D:
f is onto
proof
I2:
(
FAdj (
F1,
{a})
= RAdj (
F1,
{a}) &
FAdj (
F2,
{b})
= RAdj (
F2,
{b}) )
by FIELD_6:56;
now for o being object st o in the carrier of (FAdj (F2,{b})) holds
o in rng flet o be
object ;
( o in the carrier of (FAdj (F2,{b})) implies o in rng f )assume
o in the
carrier of
(FAdj (F2,{b}))
;
o in rng fthen
o in { (Ext_eval (p,b)) where p is Polynomial of F2 : verum }
by I2, FIELD_6:45;
then consider p being
Polynomial of
F2 such that E2:
o = Ext_eval (
p,
b)
;
PolyHom h is
onto
;
then
p in rng (PolyHom h)
by POLYNOM3:def 10;
then consider ph being
object such that E3:
(
ph in dom (PolyHom h) &
(PolyHom h) . ph = p )
by FUNCT_1:def 3;
reconsider ph =
ph as
Element of the
carrier of
(Polynom-Ring F1) by E3;
Ext_eval (
ph,
a)
in { (Ext_eval (p,a)) where p is Polynomial of F1 : verum }
;
then
Ext_eval (
ph,
a)
in the
carrier of
(FAdj (F1,{a}))
by I2, FIELD_6:45;
then E4:
Ext_eval (
ph,
a)
in dom f
by FUNCT_2:def 1;
f . (Ext_eval (ph,a)) = o
by E2, E3, AS, psi;
hence
o in rng f
by E4, FUNCT_1:def 3;
verum end;
hence
f is
onto
by E1, TARSKI:2;
verum
end;
( f is additive & f is multiplicative & f is unity-preserving )
by A, B, C;
hence
Psi (a,b,h,p) is isomorphism
by D; verum