:: Splitting Fields
:: by Christoph Schwarzweller
::
:: Received June 30, 2021
:: Copyright (c) 2021-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, VECTSP_1, ALGSTR_0, TARSKI, CAT_1, STRUCT_0, SUBSET_1,
SUPINF_2, QC_LANG1, NAT_1, MESFUNC1, REALSET1, C0SP1, FUNCT_4, CARD_3,
POLYNOM1, POLYNOM2, POLYNOM3, FUNCSDOM, CATALG_1, EC_PF_1, HURWITZ,
FINSEQ_1, FINSEQ_3, MOD_4, RANKNULL, FUNCT_1, GLIB_000, RELAT_1, CARD_1,
IDEAL_1, GCD_1, GROUP_6, XBOOLE_0, NUMBERS, MSSUBFAM, POLYNOM5, GROUP_1,
ZFMISC_1, FUNCT_7, GROUP_4, QUOFIELD, FDIFF_1, VECTSP10, YELLOW_8,
RATFUNC1, RING_2, RING_3, FUNCT_2, ALGNUM_1, RING_5, FIELD_4, WELLORD1,
VECTSP_2, RLVECT_5, XXREAL_0, XCMPLX_0, FIELD_6, FOMODEL1, ARYTM_1,
FIELD_1, PARTFUN1, ORDINAL4, FIELD_8;
notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, RELSET_1, PARTFUN1, REALSET1,
ORDINAL1,
FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_3, ZFMISC_1, MATRLIN2, NAT_D, NUMBERS,
CARD_1, XCMPLX_0, XXREAL_0, NAT_1, VFUNCT_1, FUNCT_7, IDEAL_1, ALGSEQ_1,
GCD_1, QUOFIELD, STRUCT_0, POLYNOM3, POLYNOM4, POLYNOM5, GROUP_1,
GROUP_4, GROUP_6, MOD_4, VECTSP10, ALGSTR_0, VECTSP_1, VECTSP_2,
VECTSP_9, RANKNULL, RLVECT_1, MATRLIN, HURWITZ, RINGCAT1, C0SP1, EC_PF_1,
RATFUNC1, RING_2, RING_3, RING_4, RING_5, ALGNUM_1, FIELD_1, FIELD_4,
FIELD_6, FIELD_7;
constructors POLYNOM4, RELSET_1, ABIAN, NAT_D, VFUNCT_1, RATFUNC1, GCD_1,
REALSET1, RINGCAT1, RING_3, ALGSEQ_1, VECTSP_9, MATRLIN2, GROUP_4,
ALGNUM_1, RING_5, FIELD_6, FIELD_7, WSIERP_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, FINSET_1,
FUNCT_2, SUBSET_1, RLVECT_1, QUOFIELD, FUNCT_1, CARD_1, RATFUNC1,
RELAT_1, MOD_4, RINGCAT1, FINSEQ_1, RING_2, RING_3, RING_4, RING_5,
VFUNCT_1, REALSET1, POLYNOM3, POLYNOM5, GROUP_6, FIELD_1, FIELD_4,
GRCAT_1, FIELD_6, FIELD_7;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities BINOP_1, REALSET1, STRUCT_0, ALGSTR_0, POLYNOM3, MATRLIN2,
FINSEQ_1, VECTSP_1;
definitions TARSKI;
expansions STRUCT_0, GROUP_1, VECTSP_1, TARSKI, GROUP_6, QUOFIELD, FINSEQ_1,
FUNCT_1, FUNCT_2, FIELD_7;
theorems GROUP_1, VECTSP_2, RLVECT_1, NORMSP_1, C0SP1, SUBSET_1, PARTFUN1,
FUNCT_2, TARSKI, FUNCT_1, RELAT_1, EC_PF_1, RING_3, XREAL_0, XTUPLE_0,
BHSP_1, XXREAL_0, VECTSP10, RATFUNC1, POLYNOM5, UPROOTS, RING_4, RING_5,
NAT_1, HURWITZ, XREAL_1, XBOOLE_0, FUNCT_7, NIVEN, RING_2, FUNCOP_1,
POLYNOM3, ALGNUM_1, MOD_2, ZFMISC_1, XBOOLE_1, FINSEQ_1, POLYNOM4,
VECTSP_1, STRUCT_0, ORDINAL1, GROUP_6, VECTSP12, FINSEQ_4, GROUP_4,
NAT_2, POLYNOM2, FINSEQ_3, CARD_2, FIELD_1, FIELD_2, FIELD_4, FIELD_5,
FIELD_6, FIELD_7;
schemes NAT_1, FUNCT_2;
begin :: Preliminaries
theorem DZIW:
for R being Ring
for p being Polynomial of R
for q being Element of the carrier of Polynom-Ring R
st p = q holds -p = -q
proof
let R be Ring; let p be Polynomial of R;
let q be Element of the carrier of Polynom-Ring R;
assume AS: p = q;
reconsider r = -p as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
now let n be Element of NAT;
thus (p + -p).n = p.n + (-p).n by NORMSP_1:def 2
.= p.n + -(p.n) by BHSP_1:44
.= (0_.(R)).n by RLVECT_1:5;
end;
then p + -p = 0_.(R);
then q + r = 0_.(R) by AS,POLYNOM3:def 10;
then q + r = 0.(Polynom-Ring R) by POLYNOM3:def 10;
hence thesis by RLVECT_1:6;
end;
poly0:
for R being Ring,
a being Element of R
holds (a|R).0 = a & for n being Element of NAT st n <> 0 holds (a|R).n = 0.R
proof
let L be Ring, a be Element of L;
H: a|L = 0_.(L) +* (0,a) by RING_4:def 5;
0 in dom 0_.(L);
hence (a|L).0 = a by H,FUNCT_7:31;
let n be Nat;
now assume n <> 0;
hence (a|L).n = (0_.(L)).n by H,FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
hence thesis;
end;
theorem poly1:
for R being Ring,
p being Polynomial of R
for a being Element of R holds a * p = (a|R) *' p
proof
let R be Ring, p be Polynomial of R; let a be Element of R;
set q = (a|R) *' p;
A: now let x be object;
assume x in dom(a * p);
then reconsider i = x as Element of NAT;
consider F being FinSequence of the carrier of R such that
A1: len F = i+1 & q.i = Sum F &
for k being Element of NAT st k in dom F
holds F.k = (a|R).(k-'1) * p.(i+1-'k) by POLYNOM3:def 9;
A2: now let k be Element of NAT;
assume A3: k in dom F & k <> 1; then
k in Seg(i+1) by A1,FINSEQ_1:def 3; then
1 <= k <= i + 1 by FINSEQ_1:1; then
A6: k -' 1 = k - 1 by XREAL_1:233;
A4: k - 1 <> 0 by A3;
thus F/.k = F.k by A3,PARTFUN1:def 6
.= (a|R).(k-'1) * p.(i+1-'k) by A1,A3
.= 0.R * p.(i+1-'k) by A6,A4,poly0
.= 0.R;
end;
I: i+1-'1 = i+1-1 by NAT_1:11,XREAL_1:233;
1 <= i + 1 by NAT_1:11; then
1 in Seg(i+1); then
A3: 1 in dom F by A1,FINSEQ_1:def 3; then
A4: F.1 = (a|R).(1-'1) * p.(i+1-'1) by A1
.= (a|R).0 * p.(i+1-'1) by NAT_2:8
.= a * p.i by I,poly0;
Sum F = F/.1 by A2,A3,POLYNOM2:3 .= F.1 by A3,PARTFUN1:def 6;
hence (a * p).x = q.x by A4,A1,POLYNOM5:def 4;
end;
dom(a * p) = NAT by FUNCT_2:def 1 .= dom q by FUNCT_2:def 1;
hence thesis by A;
end;
theorem hcon2:
for R being Ring
for a being Element of R holds LC(a|R) = a
proof
let R be Ring; let a be Element of R;
H: 0 - 1 < 0 & 1 - 1 >= 0;
per cases;
suppose A: a = 0.R;
then B: a|R = 0_.(R) by RING_4:13;
then len(a|R) = 0 by POLYNOM4:3;
then len(a|R) -' 1 = 0 by H,XREAL_0:def 2;
then LC(a|R) = (a|R).0 by RATFUNC1:def 6;
hence thesis by A,B;
end;
suppose a <> 0.R;
then A: deg(a|R) = 0 by RING_4:21;
deg(a|R) = len(a|R) - 1 by HURWITZ:def 2;
then len(a|R) -' 1 = 0 by A,XREAL_0:def 2;
then LC(a|R) = (a|R).0 by RATFUNC1:def 6;
hence thesis by poly0;
end;
end;
Th14: for A,B being Ring
for F be FinSequence of A,
G be FinSequence of B
st A is Subring of B & F = G holds In(Product F,B) = Product G
proof
let A,B be Ring, F be FinSequence of A, G be FinSequence of B;
assume
A0: A is Subring of B;
defpred P[Nat] means
for F being FinSequence of A, G being FinSequence of B
st len F = $1 & F = G holds In(Product F,B) = Product G;
P1: P[0]
proof
let F be FinSequence of A,
G be FinSequence of B;
assume
A1: len F = 0 & F = G; then
A2: F = <*>the carrier of A;
A3: G = <*>the carrier of B by A1;
In(Product F,B) = In(1_A,B) by A2,GROUP_4:8
.= In(1_B,B) by A0,C0SP1:def 3
.= Product G by A3,GROUP_4:8;
hence thesis;
end;
P2: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
assume
A4: P[n];
let F be FinSequence of A,
G be FinSequence of B;
assume
A5: len F = n+1 & F = G;
reconsider F0 = F| n as FinSequence of A;
n+1 in Seg (n+1) by FINSEQ_1:4; then
A6: n+1 in dom F by A5,FINSEQ_1:def 3;
rng F c= the carrier of A by FINSEQ_1:def 4; then
reconsider af = F.(n+1) as Element of A by A6,FUNCT_1:3;
B: F = F0^<*af*> by A5,FINSEQ_3:55;
reconsider G0 = G| n as FinSequence of B;
n+1 in Seg (n+1) by FINSEQ_1:4; then
A10: n+1 in dom G by A5,FINSEQ_1:def 3;
rng G c= the carrier of B by FINSEQ_1:def 4; then
reconsider bf = G.(n+1) as Element of B by A10,FUNCT_1:3;
A11: len F0 = n & F0 = G0 by FINSEQ_1:59,A5,NAT_1:11;
G = G0^<*bf*> by A5,FINSEQ_3:55; then
Product G = Product G0 * bf by GROUP_4:6
.= In(Product F0,B) * In(af,B) by A5,A4,A11
.= In(Product F0 * af,B) by A0,ALGNUM_1:9
.= In(Product F,B) by B,GROUP_4:6;
hence thesis;
end;
for n being Nat holds P[n] from NAT_1:sch 2(P1,P2);
hence thesis;
end;
theorem u5:
for R being Ring, S being Subring of R
for F being FinSequence of R
for G being FinSequence of S st F = G holds Product F = Product G
proof
let R be Ring, S be Subring of R; let F be FinSequence of R;
let G be FinSequence of S;
assume AS: F = G;
the carrier of S c= the carrier of R by C0SP1:def 3;
then In(Product G,R) = Product G by SUBSET_1:def 8;
hence thesis by AS,Th14;
end;
registration
let F be Field;
cluster F-homomorphic F-monomorphic F-isomorphic for Field;
existence
proof
take F;
id F is RingHomomorphism;
hence F is F-homomorphic by RING_2:def 4;
id F is RingHomomorphism monomorphism;
hence F is F-monomorphic by RING_3:def 3;
id F is isomorphism;
hence F is F-isomorphic by RING_3:def 4;
end;
end;
registration
let R be Ring;
cluster -> R-homomorphic R-monomorphic for R-isomorphic Ring;
coherence;
end;
registration
let R be Ring;
let S be R-homomorphic Ring;
cluster Polynom-Ring S -> (Polynom-Ring R)-homomorphic;
coherence
proof
set h = the Homomorphism of R,S;
PolyHom h is Homomorphism of (Polynom-Ring R),Polynom-Ring S;
hence thesis by RING_2:def 4;
end;
end;
registration
let F1 be Field,
F2 be F1-isomorphic F1-homomorphic Field;
cluster Polynom-Ring F2 -> (Polynom-Ring F1)-isomorphic;
coherence
proof
set h = the Isomorphism of F1,F2;
PolyHom h is isomorphism;
hence thesis by RING_3:def 4;
end;
end;
begin :: More on Polynomials
theorem lemma2e:
for R being non degenerated Ring,
S being RingExtension of R
for p being Polynomial of R
for q being Polynomial of S st p = q holds LC p = LC q
proof
let R be non degenerated Ring, S be RingExtension of R;
let p be Polynomial of R; let q be Polynomial of S;
assume A: p = q;
H: R is Subring of S by FIELD_4:def 1;
per cases;
suppose C: p = 0_.(R);
D: LC p = p.(len p -'1) by RATFUNC1:def 6
.= 0.S by C,H,C0SP1:def 3;
E: q = 0_.(S) by A,C,FIELD_4:12;
thus LC q = q.(len q -'1) by RATFUNC1:def 6 .= LC p by D,E;
end;
suppose F: p <> 0_.(R); then
C: p is non zero by UPROOTS:def 5;
D: now assume q is zero; then
q = 0_.(S) by UPROOTS:def 5 .= 0_.(R) by FIELD_4:12;
hence contradiction by A,F;
end;
E: p is Element of the carrier of Polynom-Ring R &
q is Element of the carrier of Polynom-Ring S by POLYNOM3:def 10;
thus LC p = p.(deg p) by C,FIELD_6:2
.= q.(deg q) by A,E,FIELD_4:20
.= LC q by D,FIELD_6:2;
end;
end;
theorem lemma7b:
for F being Field,
p being Element of the carrier of Polynom-Ring F
for E being FieldExtension of F,
q being Element of the carrier of Polynom-Ring E st p = q
for U being E-extending FieldExtension of F,
a being Element of U
holds Ext_eval(q,a) = Ext_eval(p,a)
proof
let F be Field,
p be Element of the carrier of Polynom-Ring F;
let E be FieldExtension of F,
q be Element of the carrier of Polynom-Ring E;
assume AS2: p = q;
let U be E-extending FieldExtension of F; let a be Element of U;
consider Fp being FinSequence of U such that
A: Ext_eval(p,a) = Sum Fp & len Fp = len p &
for n being Element of NAT st n in dom Fp holds
Fp.n = In(p.(n-'1),U) * (power U).(a,n-'1) by ALGNUM_1:def 1;
consider Fq being FinSequence of U such that
B: Ext_eval(q,a) = Sum Fq & len Fq = len q &
for n being Element of NAT st n in dom Fq holds
Fq.n = In(q.(n-'1),U) * (power U).(a,n-'1) by ALGNUM_1:def 1;
len p - 1 = deg p by HURWITZ:def 2
.= deg q by AS2,FIELD_4:20
.= len q -1 by HURWITZ:def 2; then
D: dom Fp = Seg(len Fq) by A,B,FINSEQ_1:def 3 .= dom Fq by FINSEQ_1:def 3;
now let n be Nat;
assume F: n in dom Fq;
hence Fq.n = In(q.(n-'1),U) * (power U).(a,n-'1) by B
.= Fp.n by AS2,A,D,F;
end;
then Fp = Fq by D;
hence thesis by A,B;
end;
theorem m4spl:
for R being Ring,
S being RingExtension of R
for p being Element of the carrier of Polynom-Ring R
for q being Element of the carrier of Polynom-Ring S st p = q
for T1 being RingExtension of S,
T2 being RingExtension of R
st T1 = T2 holds Roots(T2,p) = Roots(T1,q)
proof
let R be Ring, S be RingExtension of R;
let p be Element of the carrier of Polynom-Ring R;
let q be Element of the carrier of Polynom-Ring S;
assume AS1: p = q;
let T1 be RingExtension of S, T2 be RingExtension of R;
assume AS2: T1 = T2;
the carrier of Polynom-Ring S c= the carrier of Polynom-Ring T1
by FIELD_4:10; then
reconsider q1 = q as Element of the carrier of Polynom-Ring T1;
the carrier of Polynom-Ring R c= the carrier of Polynom-Ring T2
by FIELD_4:10; then
reconsider p1 = p as Element of the carrier of Polynom-Ring T2;
thus Roots(T2,p) = Roots(p1) by FIELD_7:13
.= Roots(T1,q) by AS1,AS2,FIELD_7:13;
end;
theorem lemppoly:
for R being domRing,
F being non empty FinSequence of Polynom-Ring R,
p being Polynomial of R
st p = Product F &
(for i being Nat st i in dom F ex a being Element of R st F.i = rpoly(1,a))
holds deg p = len F
proof
let R be domRing, F be non empty FinSequence of Polynom-Ring R,
p be Polynomial of R;
assume AS: p = Product F &
(for i being Nat st i in dom F ex a being Element of R st F.i = rpoly(1,a));
defpred P[Nat] means
for F being non empty FinSequence of Polynom-Ring R
for p being Polynomial of R st len F = $1 & p = Product F &
(for i being Nat st i in dom F ex a being Element of R st F.i = rpoly(1,a))
holds deg p = len F;
IA: P[0];
IS: now let k be Nat;
assume IV: P[k];
per cases;
suppose S: k = 0;
now let F be non empty FinSequence of Polynom-Ring R,
p being Polynomial of R;
assume A: len F = 1 & p = Product F &
(for i being Nat st i in dom F
ex a being Element of R st F.i = rpoly(1,a));
then 1 in Seg(len F);
then 1 in dom F by FINSEQ_1:def 3;
then consider a being Element of R such that A0: F.1 = rpoly(1,a) by A;
reconsider q = rpoly(1,a) as Element of Polynom-Ring R
by POLYNOM3:def 10;
F = <*q*> by A0,A,FINSEQ_1:40;
then q = p by A,GROUP_4:9;
hence deg p = 1 by HURWITZ:27;
end;
hence P[k+1] by S;
end;
suppose S: k > 0;
now let F be non empty FinSequence of Polynom-Ring R,
p being Polynomial of R;
assume A: len F = k + 1 & p = Product F &
(for i being Nat st i in dom F
ex a being Element of R st F.i = rpoly(1,a));
consider G being FinSequence, y being object such that
B2: F = G^<*y*> by FINSEQ_1:46;
B2a: rng G c= rng F by B2,FINSEQ_1:29;
B2b: rng F c= the carrier of Polynom-Ring R by FINSEQ_1:def 4;
then reconsider G as FinSequence of Polynom-Ring R
by B2a,XBOOLE_1:1,FINSEQ_1:def 4;
reconsider q = Product G as Polynomial of R by POLYNOM3:def 10;
B3: len F = len G + len<*y*> by B2,FINSEQ_1:22
.= len G + 1 by FINSEQ_1:39; then
reconsider G as non empty FinSequence of Polynom-Ring R by S,A;
C: dom G c= dom F by B2,FINSEQ_1:26;
now let i be Nat;
assume C0: i in dom G;
then G.i = F.i by B2,FINSEQ_1:def 7;
hence ex a being Element of R st G.i = rpoly(1,a) by C,C0,A;
end;
then F: deg q = k by IV,B3,A;
rng<*y*> = {y} by FINSEQ_1:39;
then G5: y in rng<*y*> by TARSKI:def 1;
rng<*y*> c= rng F by B2,FINSEQ_1:30;
then reconsider y as Element of Polynom-Ring R by G5,B2b;
dom<*y*> = {1} by FINSEQ_1:2,FINSEQ_1:def 8;
then 1 in dom<*y*> by TARSKI:def 1;
then B6: F.(k+1) = <*y*>.1 by B2,B3,A,FINSEQ_1:def 7
.= y;
dom F = Seg(k+1) by A,FINSEQ_1:def 3;
then consider a being Element of R such that
B9: y = rpoly(1,a) by A,B6,FINSEQ_1:4;
B10: p = (Product G) * y by A,B2,GROUP_4:6
.= q *' rpoly(1,a) by B9,POLYNOM3:def 10;
q <> 0_.(R) & rpoly(1,a) <> 0_.(R) by F,HURWITZ:20;
hence deg p = deg q + deg rpoly(1,a) by B10,HURWITZ:23
.= k + 1 by F,HURWITZ:27;
end;
hence P[k+1];
end;
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
thus thesis by I,AS;
end;
theorem lemppolspl2:
for F being Field,
p being Polynomial of F
for a being non zero Element of F
holds a * p splits_in F iff p splits_in F
proof
let F be Field, p be Polynomial of F; let a be non zero Element of F;
X: now assume p splits_in F; then
consider b being non zero Element of F, q being Ppoly of F such that
A: p = b * q by FIELD_4:def 5;
a * p = (a * b) * q by A,RING_4:11;
hence a * p splits_in F by FIELD_4:def 5;
end;
now assume a * p splits_in F; then
consider b being non zero Element of F, q being Ppoly of F such that
A: a * p = b * q by FIELD_4:def 5;
a" <> 0.F & b <> 0.F by VECTSP_2:13; then
B: a" * b is non zero by VECTSP_2:def 1;
a <> 0.F; then
a" * a = 1.F by VECTSP_1:def 10; then
p = (a" * a) * p
.= a" * (a * p) by RING_4:11
.= (a" * b) * q by A,RING_4:11;
hence p splits_in F by B,FIELD_4:def 5;
end;
hence thesis by X;
end;
lemppolspl:
for F being Field, p being Ppoly of F holds p splits_in F
proof
let F be Field, p be Ppoly of F;
p = 1.F * p;
hence thesis by FIELD_4:def 5;
end;
lemppolspl3b:
for F being Field
for p being non constant monic Polynomial of F
for a being Element of F
st rpoly(1,a) *' p is Ppoly of F holds p is Ppoly of F
proof
let F be Field; let p be non constant monic Polynomial of F;
let a be Element of F;
assume rpoly(1,a) *' p is Ppoly of F; then
consider G being non empty
FinSequence of the carrier of Polynom-Ring F such that
A1: rpoly(1,a) *' p = Product G & for i being Nat st i in dom G
ex a being Element of F st G.i = rpoly(1,a) by RING_5:def 4;
eval(rpoly(1,a),a) = a - a by HURWITZ:29 .= 0.F by RLVECT_1:15; then
0.F = eval(rpoly(1,a),a) * eval(p,a)
.= eval(rpoly(1,a) *' p,a) by POLYNOM4:24; then
consider i being Nat such that
A2: i in dom G & G.i = rpoly(1,a) by A1,RATFUNC1:12;
set H = Del(G,i);
consider m being Nat such that
A3: len G = m + 1 & len Del(G,i) = m by A2,FINSEQ_3:104;
A4: rpoly(1,a) <> 0_.(F) & p <> 0_.(F);
now assume H is empty;
then 1 = deg(rpoly(1,a) *' p) by A1,A3,lemppoly
.= deg rpoly(1,a) + deg p by A4,HURWITZ:23
.= 1 + deg p by HURWITZ:27;
hence contradiction by RATFUNC1:def 2;
end; then
reconsider H as non empty
FinSequence of the carrier of Polynom-Ring F by FINSEQ_3:105;
reconsider q = Product H as Polynomial of F by POLYNOM3:def 10;
now let j be Nat;
assume B1: j in dom H;
B2: dom H = Seg m & dom G = Seg(m+1) by A3,FINSEQ_1:def 3; then
dom H c= dom G by FINSEQ_1:5,NAT_1:11; then
consider b being Element of F such that
B3: G.j = rpoly(1,b) by A1,B1;
B4: 1 <= j & j <= m by B1,B2,FINSEQ_1:1;
per cases;
suppose j < i;
hence ex b being Element of F st H.j = rpoly(1,b) by B3,FINSEQ_3:110;
end;
suppose j >= i; then
B5: H.j = G.(j+1) by A2,A3,B4,FINSEQ_3:111;
1 <= j + 1 & j + 1 <= m + 1 by NAT_1:11,B4,XREAL_1:6; then
j + 1 in dom G by B2;
hence ex b being Element of F st H.j = rpoly(1,b) by A1,B5;
end;
end; then
reconsider q as Ppoly of F by RING_5:def 4;
A4: G/.i = rpoly(1,a) by A2,PARTFUN1:def 6;
rpoly(1,a) *' p = (G/.i) * (Product H) by A1,A2,RATFUNC1:3
.= rpoly(1,a) *' q by A4,POLYNOM3:def 10;
hence thesis by RATFUNC1:7;
end;
theorem lemppolspl3a:
for F being Field
for p being non constant monic Polynomial of F
for q being non zero Polynomial of F
st p *' q is Ppoly of F holds p is Ppoly of F
proof
let F be Field;
let p be non constant monic Polynomial of F;
let q be non zero Polynomial of F;
assume AS: p *' q is Ppoly of F;
p <> 0_.(F) & q <> 0_.(F); then
A1: deg(p*'q) = deg p + deg q by HURWITZ:23;
deg p > 0 by RATFUNC1:def 2; then
A: deg(p*'q) >= 1 + 0 by A1,NAT_1:14;
defpred P[Nat] means
for p being non constant monic Polynomial of F
for q being non zero Polynomial of F
st deg(p*'q) = $1 & p*'q is Ppoly of F holds p is Ppoly of F;
now let p be non constant monic Polynomial of F;
let q be non zero Polynomial of F;
assume B: deg(p*'q) = 1 & p*'q is Ppoly of F;
p <> 0_.(F) & q <> 0_.(F); then
deg(p*'q) = deg p + deg q by HURWITZ:23; then
B1: deg p <= deg(p*'q) by NAT_1:12;
deg p > 0 by RATFUNC1:def 2; then
deg p >= deg(p*'q) by B,NAT_1:14; then
consider x,z being Element of F such that
A3: x <> 0.F & p = x * rpoly(1,z) by B,B1,XXREAL_0:1,HURWITZ:28;
x * LC rpoly(1,z) = LC(x * rpoly(1,z)) by RING_5:5
.= 1.F by A3,RATFUNC1:def 7;
then x * 1.F = 1.F by RATFUNC1:def 7;
hence p is Ppoly of F by A3,RING_5:51;
end; then
IA: P[1];
IS: now let k be Nat;
assume BB: 1 <= k;
assume IV: P[k];
now let p be non constant monic Polynomial of F;
let q be non zero Polynomial of F;
assume B: deg(p*'q) = k+1 & p*'q is Ppoly of F; then
LC p = 1.F & LC(p*'q) = 1.F by RATFUNC1:def 7; then
B0: 1.F = 1.F * LC(q) by NIVEN:46; then
B0a: q is monic by RATFUNC1:def 7;
consider a being Element of F such that
B1: a is_a_root_of (p*'q) by B,POLYNOM5:def 8;
0.F = eval(p*'q,a) by B1,POLYNOM5:def 7
.= eval(p,a) * eval(q,a) by POLYNOM4:24; then
per cases by VECTSP_2:def 1;
suppose eval(q,a) = 0.F; then
consider s being Polynomial of F such that
B2: q = rpoly(1,a) *' s by HURWITZ:33,POLYNOM5:def 7;
B3: s is non zero by B2;
B6: s <> 0_.(F) & p <> 0_.(F) by B2; then
deg q = deg rpoly(1,a) + deg s by B2,HURWITZ:23
.= 1 + deg s by HURWITZ:27; then
B4: deg(p*'s) = deg p + (deg q - 1) by B6,HURWITZ:23
.= (deg p + deg q) - 1
.= deg(p*'q) - 1 by B6,HURWITZ:23
.= k by B;
1.F = LC rpoly(1,a) * LC s by B0,B2,NIVEN:46
.= 1.F * LC s by RING_5:9; then
s is monic by RATFUNC1:def 7; then
B5: p *' s is non constant monic by BB,B4,RATFUNC1:def 2;
p *' q = rpoly(1,a) *' (p *' s) by B2,POLYNOM3:33; then
p *' s is Ppoly of F by B,B5,lemppolspl3b;
hence p is Ppoly of F by B3,B4,IV;
end;
suppose eval(p,a) = 0.F; then
consider s being Polynomial of F such that
B2: p = rpoly(1,a) *' s by POLYNOM5:def 7,HURWITZ:33;
reconsider s as non zero Polynomial of F by B2;
B6: s <> 0_.(F); then
deg p = deg rpoly(1,a) + deg s by B2,HURWITZ:23
.= 1 + deg s by HURWITZ:27; then
B4: deg(q*'s) = deg q + (deg p - 1) by B6,HURWITZ:23
.= (deg p + deg q) - 1
.= deg(p*'q) - 1 by B6,HURWITZ:23
.= k by B;
B5: p *' q = rpoly(1,a) *' (s *' q) by B2,POLYNOM3:33;
B7b: 1.F = LC p by RATFUNC1:def 7
.= LC rpoly(1,a) * LC s by B2,NIVEN:46
.= 1.F * LC s by RING_5:9; then
B7a: s is monic by RATFUNC1:def 7;
reconsider s1 = s as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
per cases;
suppose K: deg s >= 1; then
B8a: s is non constant by RATFUNC1:def 2;
deg(s *' q) = deg s + deg q by B6,HURWITZ:23; then
s *' q is non constant by K,RATFUNC1:def 2; then
s *' q is Ppoly of F by B,B5,B7a,B0a,lemppolspl3b; then
B9: s is Ppoly of F by B4,B7a,B8a,IV;
rpoly(1,a) is Ppoly of F by RING_5:51;
hence p is Ppoly of F by B9,B2,RING_5:52;
end;
suppose deg s < 1; then
deg s = 0 by NAT_1:14; then
consider b being Element of F such that
B8: s1 = b|F by RING_4:def 4,RING_4:20;
B9: s = b * 1_.(F) by B8,RING_4:16; then
LC s = b * LC 1_.(F) by RING_5:5
.= b * 1.F by RATFUNC1:def 7;
hence p is Ppoly of F by B7b,B9,B2,RING_5:51;
end;
end;
end;
hence P[k+1];
end;
for i being Nat st 1 <= i holds P[i] from NAT_1:sch 8(IA,IS);
hence thesis by A,AS;
end;
theorem lemppolspl3:
for F being Field
for p being non constant Polynomial of F
for q being non zero Polynomial of F
st p *' q splits_in F holds p splits_in F
proof
let F be Field;
let p be non constant Polynomial of F;
let q be non zero Polynomial of F;
assume p *' q splits_in F; then
consider a being non zero Element of F, u being Ppoly of F such that
A: p *' q = a * u by FIELD_4:def 5;
set b = (LC p) * a";
B: LC p <> 0.F & a" <> 0.F by VECTSP_2:13;
C2: p is Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
not deg p <= 0 by RATFUNC1:def 2; then
C1: len p - 1 > 0 by HURWITZ:def 2; then
len p <> 0; then
len(NormPolynomial p) = len p by POLYNOM5:57; then
deg(NormPolynomial p) > 0 by C1,HURWITZ:def 2; then
NormPolynomial p is non constant monic by RATFUNC1:def 2; then
C: (LC p)" * p is non constant monic by C2,RING_4:23;
D: b is non zero by B,VECTSP_2:def 1;
E: (LC p)" is non zero by VECTSP_2:13; then
F: (LC p)" * (LC p) = 1.F by VECTSP_1:def 10;
a" <> 0.F by VECTSP_2:13; then
a" * a = 1.F by VECTSP_1:def 10; then
u = (a" * a) * u
.= a" * (p *' q) by A,RING_4:11
.= ((LC p)" * (LC p)) * (p *' (a" * q)) by F,RING_4:10
.= (LC p)" * ((LC p) * (p *' (a" * q))) by RING_4:11
.= ((LC p)") * (p *' ((LC p) * (a" * q))) by RING_4:10
.= ((LC p)") * (p *' (b * q)) by RING_4:11
.= ((LC p)" * p) *' (b * q) by RING_4:10; then
(LC p)" * p is Ppoly of F by D,C,lemppolspl3a;
hence thesis by E,lemppolspl2,lemppolspl;
end;
theorem lemppolspl1:
for F being Field,
p,q being Polynomial of F
st p splits_in F & q splits_in F holds p *' q splits_in F
proof
let F be Field, p,q be Polynomial of F;
assume AS: p splits_in F & q splits_in F; then
consider b being non zero Element of F, u being Ppoly of F such that
A: p = b * u by FIELD_4:def 5;
consider c being non zero Element of F, v being Ppoly of F such that
B: q = c * v by AS,FIELD_4:def 5;
D: u *' v is Ppoly of F by RING_5:52;
p *' q = c * ((b * u) *' v) by A,B,RING_4:10
.= c * (b * (u *' v)) by RING_4:10
.= (c * b) * (u*' v) by RING_4:11
.= (b * c) * (u*' v) by GROUP_1:def 12;
hence thesis by D,FIELD_4:def 5;
end;
theorem hcon:
for R being Ring,
S being R-homomorphic Ring
for h being Homomorphism of R,S
for a being Element of R holds (PolyHom h).(a|R) = (h.a)|S
proof
let R be Ring, S be R-homomorphic Ring;
let h be Homomorphism of R,S; let a be Element of R;
reconsider g = a|R as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
now let i be Element of NAT;
per cases;
suppose A: i <> 0;
thus ((PolyHom h).g).i = h.(g.i) by FIELD_1:def 2
.= h.(0.R) by A,poly0
.= 0.S by RING_2:6
.= ((h.a)|S).i by A,poly0;
end;
suppose B: i = 0;
thus ((PolyHom h).g).i = h.(g.i) by FIELD_1:def 2
.= h.a by B,poly0
.= ((h.a)|S).i by B,poly0;
end;
end;
hence thesis by FUNCT_2:63;
end;
theorem uu0:
for F1 being Field,
F2 being F1-isomorphic F1-homomorphic Field
for h being Isomorphism of F1,F2
for p,q being Element of the carrier of Polynom-Ring F1
holds p divides q iff (PolyHom h).p divides (PolyHom h).q
proof
let F1 be Field, F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let p,q be Element of the carrier of Polynom-Ring F1;
A: now assume AS: p divides q;
reconsider pp = p, qq = q as Polynomial of F1;
consider rr being Polynomial of F1 such that
B: pp *' rr = qq by AS,RING_4:1;
reconsider r = rr as Element of the carrier of Polynom-Ring F1
by POLYNOM3:def 10;
p * r = q by B,POLYNOM3:def 10; then
C: (PolyHom h).q = (PolyHom h).p * (PolyHom h).r by FIELD_1:25;
reconsider pe = (PolyHom h).p, qe = (PolyHom h).q, re = (PolyHom h).r
as Polynomial of F2;
qe = pe *' re by C,POLYNOM3:def 10;
hence (PolyHom h).p divides (PolyHom h).q by RING_4:1;
end;
reconsider f = (PolyHom h)" as
Isomorphism of Polynom-Ring F2,Polynom-Ring F1 by RING_3:73;
now assume AS: (PolyHom h).p divides (PolyHom h).q;
reconsider pp = (PolyHom h).p, qq = (PolyHom h).q as Polynomial of F2;
consider rr being Polynomial of F2 such that
B: pp *' rr = qq by AS,RING_4:1;
reconsider r = rr as Element of the carrier of Polynom-Ring F2
by POLYNOM3:def 10;
(PolyHom h).p * r = (PolyHom h).q by B,POLYNOM3:def 10; then
C: f.((PolyHom h).p) * f.r = f.((PolyHom h).q) by GROUP_6:def 6;
D: f.((PolyHom h).p) = p & f.((PolyHom h).q) = q by FUNCT_2:26;
reconsider pe = p, qe = q, re = f.r as Polynomial of F1;
qe = pe *' re by C,D,POLYNOM3:def 10;
hence p divides q by RING_4:1;
end;
hence thesis by A;
end;
theorem uu4:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for p being irreducible Element of the carrier of Polynom-Ring F
st Ext_eval(p,a) = 0.E holds MinPoly(a,F) = NormPolynomial p
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E;
let p be irreducible Element of the carrier of Polynom-Ring F;
set q = NormPolynomial p;
assume Ext_eval(p,a) = 0.E;
then Ext_eval(q,a) = 0.E by FIELD_6:25;
hence thesis by RING_4:28,FIELD_6:52;
end;
theorem uu5:
for F1 being Field,
F2 being F1-monomorphic F1-homomorphic Field
for h being Monomorphism of F1,F2
for p being Element of the carrier of Polynom-Ring F1
holds NormPolynomial((PolyHom h).p) = (PolyHom h).(NormPolynomial p)
proof
let F1 be Field, F2 be F1-monomorphic F1-homomorphic Field;
let h be Monomorphism of F1,F2;
let p be Element of the carrier of Polynom-Ring F1;
set q = NormPolynomial((PolyHom h).p), pp = (PolyHom h).p,
r = (PolyHom h).(NormPolynomial p);
per cases;
suppose p is zero; then
A: p = 0_.(F1) by UPROOTS:def 5; then
NormPolynomial p = 0_.(F1) by RING_4:22; then
B: (PolyHom h).(NormPolynomial p) = 0_.(F2) by FIELD_1:22;
pp = 0_.(F2) by A,FIELD_1:22;
hence thesis by B,RING_4:22;
end;
suppose p is non zero; then
LC p is non zero; then
B: p.(len p-'1) <> 0.F1 by RATFUNC1:def 6;
deg pp = deg p by FIELD_1:31; then
deg p = len pp - 1 by HURWITZ:def 2; then
A: len p - 1 = len pp - 1 by HURWITZ:def 2;
now let n be Nat;
reconsider i = n as Element of NAT by ORDINAL1:def 12;
pp.i = h.(p.i) by FIELD_1:def 2; then
q.i = (h.(p.i)) / pp.(len p-'1) by A,POLYNOM5:def 11
.= h.(p.i) * (h.(p.(len p-'1)))" by FIELD_1:def 2
.= h.(p.i) * h.((p.(len p-'1))") by B,FIELD_2:6
.= h.( (p.i) / p.(len p-'1) ) by GROUP_6:def 6
.= h.( (NormPolynomial p).i ) by POLYNOM5:def 11
.= r.i by FIELD_1:def 2;
hence q.n = r.n;
end;
hence thesis;
end;
end;
registration
let F1 be Field,
F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let p be constant Element of the carrier of Polynom-Ring F1;
cluster (PolyHom h).p -> constant for
Element of the carrier of Polynom-Ring F2;
coherence
proof
let q be Element of the carrier of Polynom-Ring F2 such that
A: q = (PolyHom h).p;
B: deg p <= 0 by RING_4:def 4;
deg q = deg p by A,FIELD_1:31;
hence q is constant by B,RING_4:def 4;
end;
end;
registration
let F1 be Field,
F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let p be non constant Element of the carrier of Polynom-Ring F1;
cluster (PolyHom h).p -> non constant for
Element of the carrier of Polynom-Ring F2;
coherence
proof
let q be Element of the carrier of Polynom-Ring F2 such that
A: q = (PolyHom h).p;
B: deg p > 0 by RING_4:def 4;
deg q = deg p by A,FIELD_1:31;
hence q is non constant by B,RING_4:def 4;
end;
end;
registration
let F1 be Field,
F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let p be irreducible Element of the carrier of Polynom-Ring F1;
cluster (PolyHom h).p -> irreducible for
Element of the carrier of Polynom-Ring F2;
coherence
proof
set q = (PolyHom h).p;
h" is Isomorphism of F2,F1 by RING_3:73; then
reconsider F1i = F1 as F2-isomorphic F2-homomorphic Field
by RING_3:def 4,RING_2:def 4;
reconsider hi = h" as Isomorphism of F2,F1i by RING_3:73;
H: (PolyHom hi).((PolyHom h).p) = p
proof
now let i be Nat;
((PolyHom h).p).i = h.(p.i) by FIELD_1:def 2;
hence ((PolyHom hi).((PolyHom h).p)).i
= hi.(h.(p.i)) by FIELD_1:def 2
.= p.i by FUNCT_2:26;
end;
hence thesis;
end;
now assume q is reducible; then
per cases by RING_4:41;
suppose q = 0_.(F2);
hence contradiction;
end;
suppose q is Unit of Polynom-Ring F2;
hence contradiction;
end;
suppose ex r being Element of the carrier of Polynom-Ring F2
st r divides q & 1 <= deg r & deg r < deg q; then
consider r being Element of the carrier of Polynom-Ring F2 such that
A: r divides q & 1 <= deg r & deg r < deg q;
C: deg r = deg (PolyHom hi).r by FIELD_1:31;
D: 1 <= deg (PolyHom hi).r by A,FIELD_1:31;
deg (PolyHom hi).r < deg p by A,C,FIELD_1:31;
hence contradiction by H,A,uu0,D,RING_4:40;
end;
end;
hence thesis;
end;
end;
lemma6a:
for F1 being Field,
p being non constant Element of the carrier of Polynom-Ring F1
for F2 being F1-isomorphic Field
for h being Isomorphism of F1,F2
holds p splits_in F1 implies (PolyHom h).p splits_in F2
proof
let F1 be Field,
p be non constant Element of the carrier of Polynom-Ring F1;
let F2 be F1-isomorphic Field; let h be Isomorphism of F1,F2;
assume AS: p splits_in F1;
defpred P[Nat] means
for p being Element of the carrier of Polynom-Ring F1
st deg p = $1 & p splits_in F1 holds (PolyHom h).p splits_in F2;
IA: P[1]
proof
now let p being Element of the carrier of Polynom-Ring F1;
assume deg p = 1 & p splits_in F1;
then deg (PolyHom h).p = 1 by FIELD_1:31;
hence (PolyHom h).p splits_in F2 by FIELD_4:29;
end;
hence thesis;
end;
IS: now let k be Nat;
assume 1 <= k;
assume IV: P[k];
now let p being Element of the carrier of Polynom-Ring F1;
assume AS3: deg p = k + 1 & p splits_in F1; then
consider a being non zero Element of F1,
q being Ppoly of F1 such that
A1: p = a * q by FIELD_4:def 5;
reconsider qq = q as Element of the carrier of Polynom-Ring F1
by POLYNOM3:def 10;
consider G being non empty FinSequence of Polynom-Ring F1 such that
A2: q = Product G & for i being Nat st i in dom G
ex a being Element of F1 st G.i = rpoly(1,a)
by RING_5:def 4;
deg q = k + 1 by AS3,A1,RING_5:4; then
A3: len G = k + 1 by A2,lemppoly;
consider H being FinSequence, y being object such that
B2: G = H^<*y*> by FINSEQ_1:46;
B2a: rng H c= rng G by B2,FINSEQ_1:29;
B2b: rng G c= the carrier of Polynom-Ring F1 by FINSEQ_1:def 4;
then reconsider H as FinSequence of Polynom-Ring F1
by B2a,XBOOLE_1:1,FINSEQ_1:def 4;
B3: len G = len H + len <*y*> by B2,FINSEQ_1:22
.= len H + 1 by FINSEQ_1:39;
rng<*y*> = {y} by FINSEQ_1:39;
then G5: y in rng<*y*> by TARSKI:def 1;
rng<*y*> c= rng G by B2,FINSEQ_1:30; then
reconsider y as Element of the carrier of Polynom-Ring F1 by G5,B2b;
dom<*y*> = {1} by FINSEQ_1:2,FINSEQ_1:def 8;
then 1 in dom<*y*> by TARSKI:def 1;
then B6: G.(k+1) = <*y*>.1 by B2,B3,A3,FINSEQ_1:def 7
.= y;
dom G = Seg(k+1) by A3,FINSEQ_1:def 3;
then consider b being Element of F1 such that
B9: y = rpoly(1,b) by A2,B6,FINSEQ_1:4;
deg y = 1 by B9,HURWITZ:27; then
deg (PolyHom h).y = 1 by FIELD_1:31; then
Y: (PolyHom h).y splits_in F2 by FIELD_4:29;
per cases;
suppose H is empty;
then G = <*y*> by B2,FINSEQ_1:34;
then q = rpoly(1,b) by B9,A2,GROUP_4:9;
then deg q = 1 by HURWITZ:27;
then deg p = 1 by A1,RING_5:4;
then deg (PolyHom h).p = 1 by FIELD_1:31;
hence (PolyHom h).p splits_in F2 by FIELD_4:29;
end;
suppose H is non empty; then
reconsider H as non empty FinSequence of Polynom-Ring F1;
reconsider q1 = Product H as Element of the carrier of Polynom-Ring F1;
C: dom H c= dom G by B2,FINSEQ_1:26;
D: now let i be Nat;
assume C0: i in dom H;
then H.i = G.i by B2,FINSEQ_1:def 7;
hence ex a being Element of F1 st H.i = rpoly(1,a) by C,C0,A2;
end;
then reconsider q1p = q1 as Ppoly of F1 by RING_5:def 4;
E: q1p splits_in F1 by lemppolspl;
deg q1 = k by A3,B3,D,lemppoly; then
F: (PolyHom h).q1 splits_in F2 by E,IV;
now assume h.a = 0.F2;
then h.a = h.(0.F1) by RING_2:6;
hence contradiction by FUNCT_2:19;
end; then
reconsider ha = h.a as non zero Element of F2 by STRUCT_0:def 12;
reconsider q1h = (PolyHom h).q1, yh = (PolyHom h).y as
Polynomial of F2;
I: q1h *' yh = (PolyHom h).q1 * (PolyHom h).y by POLYNOM3:def 10
.= (PolyHom h).(q1*y) by FIELD_1:25
.= (PolyHom h).q by A2,B2,GROUP_4:6;
q1h *' yh splits_in F2 by Y,F,lemppolspl1;
then ha * (PolyHom h).qq splits_in F2 by I,lemppolspl2;
hence (PolyHom h).p splits_in F2 by A1,FIELD_1:26;
end;
end;
hence P[k+1];
end;
I: for k being Nat st 1 <= k holds P[k] from NAT_1:sch 8(IA,IS);
consider n being Nat such that H: n = deg p;
n > 0 by H,RING_4:def 4;
then n >= 1 by NAT_1:14;
hence thesis by AS,H,I;
end;
theorem
for F1 being Field,
p being non constant Element of the carrier of Polynom-Ring F1
for F2 being F1-isomorphic Field
for h being Isomorphism of F1,F2
holds p splits_in F1 iff (PolyHom h).p splits_in F2
proof
let F1 be Field,
p be non constant Element of the carrier of Polynom-Ring F1;
let F2 be F1-isomorphic Field; let h be Isomorphism of F1,F2;
now assume AS: (PolyHom h).p splits_in F2;
h" is Isomorphism of F2,F1 by RING_3:73; then
reconsider F1a = F1 as F2-isomorphic F2-homomorphic Field
by RING_3:def 4,RING_2:def 4;
reconsider g = h" as Isomorphism of F2,F1a by RING_3:73;
now let i be Element of NAT;
thus ((PolyHom g).((PolyHom h).p)).i
= g.(((PolyHom h).p).i) by FIELD_1:def 2
.= g.(h.(p.i)) by FIELD_1:def 2
.= p.i by FUNCT_2:26;
end;
then (PolyHom g).((PolyHom h).p) = p;
hence p splits_in F1 by AS,lemma6a;
end;
hence thesis by lemma6a;
end;
theorem lemma7:
for F being Field,
p being Element of the carrier of Polynom-Ring F
for E being FieldExtension of F,
U being E-extending FieldExtension of F
holds Roots(E,p) c= Roots(U,p)
proof
let F be Field,
p be Element of the carrier of Polynom-Ring F;
let E be FieldExtension of F, U be E-extending FieldExtension of F;
E is Subfield of U by FIELD_4:7; then
H: the carrier of E c= the carrier of U & 0.E = 0.U by EC_PF_1:def 1;
now let o be object;
assume o in Roots(E,p); then
o in {a where a is Element of E : a is_a_root_of p,E} by FIELD_4:def 4;
then consider a being Element of E such that
A: o = a & a is_a_root_of p,E;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E
by FIELD_4:10; then
reconsider p1 = p as Element of the carrier of (Polynom-Ring E);
reconsider U1 = U as FieldExtension of E;
reconsider b = a as Element of U by H;
Ext_eval(p,b) = Ext_eval(p,a) by FIELD_7:14
.= 0.U by H,A,FIELD_4:def 2;
then b is_a_root_of p,U by FIELD_4:def 2; then
a in {a where a is Element of U : a is_a_root_of p,U};
hence o in Roots(U,p) by A,FIELD_4:def 4;
end;
hence thesis;
end;
lemmapp:
for F being Field,
E being FieldExtension of F
for p being Ppoly of F holds p is Ppoly of E
proof
let F be Field, E be FieldExtension of F; let p be Ppoly of F;
F is Subfield of E by FIELD_4:7; then
H1: the carrier of F c= the carrier of E by EC_PF_1:def 1;
set PF = Polynom-Ring F, PE = Polynom-Ring E;
consider G being non empty FinSequence of Polynom-Ring F such that
H2: p = Product G &
for i being Nat st i in dom G ex a being Element of F st G.i = rpoly(1,a)
by RING_5:def 4;
defpred P[Nat] means
for G being non empty FinSequence of Polynom-Ring F st len G = $1 &
for i being Nat st i in dom G ex a being Element of F st G.i = rpoly(1,a)
holds Product G is Ppoly of E;
IA: P[0];
IS: now let k be Nat;
assume IV: P[k];
now let G be non empty FinSequence of Polynom-Ring F;
assume A: len G = k+1 & for i being Nat st i in dom G
ex a being Element of F st G.i = rpoly(1,a);
per cases;
suppose S: k = 0;
then 1 in Seg(len G) by A;
then 1 in dom G by FINSEQ_1:def 3;
then consider a being Element of F such that A0: G.1 = rpoly(1,a) by A;
reconsider b = a as Element of E by H1;
H: G = <*rpoly(1,a)*> by A0,A,S,FINSEQ_1:40;
rpoly(1,a) is Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
then Product G = rpoly(1,a) by H,GROUP_4:9 .= rpoly(1,b) by FIELD_4:21;
hence Product G is Ppoly of E by RING_5:51;
end;
suppose S: k > 0;
consider H being FinSequence, y being object such that
B2: G = H^<*y*> by FINSEQ_1:46;
B2a: rng H c= rng G by B2,FINSEQ_1:29;
B2b: rng G c= the carrier of Polynom-Ring F by FINSEQ_1:def 4;
then reconsider H as FinSequence of Polynom-Ring F
by B2a,XBOOLE_1:1,FINSEQ_1:def 4;
B3: len G = len H + len <*y*> by B2,FINSEQ_1:22
.= len H + 1 by FINSEQ_1:39; then
reconsider H as non empty FinSequence of Polynom-Ring F by S,A;
reconsider q = Product H as Polynomial of F by POLYNOM3:def 10;
C: dom H c= dom G by B2,FINSEQ_1:26;
now let i be Nat;
assume C0: i in dom H;
then H.i = G.i by B2,FINSEQ_1:def 7;
hence ex a being Element of F st H.i = rpoly(1,a) by C,C0,A;
end;
then reconsider q1 = Product H as Ppoly of E by B3,A,IV;
rng<*y*> = {y} by FINSEQ_1:39;
then G5: y in rng<*y*> by TARSKI:def 1;
rng<*y*> c= rng G by B2,FINSEQ_1:30;
then reconsider y as Element of Polynom-Ring F by G5,B2b;
dom<*y*> = {1} by FINSEQ_1:2,FINSEQ_1:def 8;
then 1 in dom<*y*> by TARSKI:def 1;
then B6: G.(k+1) = <*y*>.1 by B2,B3,A,FINSEQ_1:def 7
.= y;
dom G = Seg(k+1) by A,FINSEQ_1:def 3;
then consider a being Element of F such that
B9: y = rpoly(1,a) by A,B6,FINSEQ_1:4;
reconsider b = a as Element of E by H1;
reconsider y1 = rpoly(1,b) as Element of PE by POLYNOM3:def 10;
B8: rpoly(1,b) = rpoly(1,a) by FIELD_4:21;
B7: rpoly(1,b) is Ppoly of E by RING_5:51;
Product G = (Product H) * y by B2,GROUP_4:6
.= q *' rpoly(1,a) by B9,POLYNOM3:def 10
.= q1 *' rpoly(1,b) by B8,FIELD_4:17;
hence Product G is Ppoly of E by B7,RING_5:52;
end;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that J: len G = n;
thus thesis by I,J,H2;
end;
theorem
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for E being FieldExtension of F
for U being FieldExtension of E holds p splits_in E implies p splits_in U
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
let E be FieldExtension of F;
let U be FieldExtension of E;
assume p splits_in E; then
consider a being non zero Element of E, q being Ppoly of E such that
A: p = a * q by FIELD_4:def 5;
B: 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 b = a as Element of U;
a <> 0.E & 0.U = 0.E by B,EC_PF_1:def 1; then
reconsider b as non zero Element of U by STRUCT_0:def 12;
reconsider r = q as Ppoly of U by lemmapp;
C: b|U = a|E by FIELD_6:23;
b * r = (b|U) *' r by poly1
.= (a|E) *' q by C,FIELD_4:17
.= a * q by poly1;
hence thesis by A,FIELD_4:def 5;
end;
begin :: More on Products of Linear Polynomials
theorem lemma2y:
for F being Field
for G being non empty FinSequence of the carrier of Polynom-Ring F
st for i being Nat st i in dom G
ex a being Element of F st G.i = rpoly(1,a)
holds G is Factorization of (Product G)
proof
let F be Field;
let G be non empty FinSequence of the carrier of Polynom-Ring F;
assume A: for i being Nat st i in dom G
ex a being Element of F st G.i = rpoly(1,a);
C:now let i be Element of dom G;
consider a being Element of F such that B: G.i = rpoly(1,a) by A;
deg rpoly(1,a) = 1 by HURWITZ:27;
hence G.i is irreducible by B,RING_4:42;
end;
then B: G is_a_factorization_of (Product G) by RING_2:def 11;
(Product G) is factorizable by C,RING_2:def 11,RING_2:def 12;
hence thesis by B,RING_2:def 13;
end;
theorem lemma2z:
for F being Field
for G1,G2 being non empty FinSequence of Polynom-Ring F
st (for i being Nat st i in dom G1
ex a being Element of F st G1.i = rpoly(1,a)) &
(for i being Nat st i in dom G2
ex a being Element of F st G2.i = rpoly(1,a)) &
Product G1 = Product G2
for a being Element of F holds
(ex i being Nat st i in dom G1 & G1.i = rpoly(1,a)) iff
(ex i being Nat st i in dom G2 & G2.i = rpoly(1,a))
proof
let F be Field;
let G1,G2 be non empty FinSequence of Polynom-Ring F;
assume AS: (for i being Nat st i in dom G1
ex a being Element of F st G1.i = rpoly(1,a)) &
(for i being Nat st i in dom G2
ex a being Element of F st G2.i = rpoly(1,a)) &
Product G1 = Product G2;
let a be Element of F;
Product G1 is Polynomial of F by POLYNOM3:def 10; then
reconsider p1 = Product G1 as Ppoly of F by AS,RING_5:def 4;
Product G1 <> 0_.(F) by AS,RATFUNC1:11; then
A: Product G1 is non zero by POLYNOM3:def 10;
deg p1 <> 0 by RATFUNC1:def 2; then
B: Product G1 is NonUnit of Polynom-Ring F by RING_4:37;
G1 is Factorization of (Product G1) &
G2 is Factorization of (Product G1) by AS,lemma2y; then
consider B being Function of dom G1, dom G2 such that
C: B is bijective &
for i being Element of dom G1 holds G2.(B.i) is_associated_to G1.i
by A,B,RING_2:def 14;
X: now assume
ex i being Nat st i in dom G1 & G1.i = rpoly(1,a); then
consider i being Nat such that
X1: i in dom G1 & G1.i = rpoly(1,a);
reconsider i as Element of dom G1 by X1;
consider j being Element of dom G1 such that
X2: G2.(B.i) is_associated_to G1.i by C;
consider b being Element of F such that
X3: G2.(B.i) = rpoly(1,b) by AS;
reconsider p1 = G1.i, p2 = G2.(B.i) as
Element of the carrier of Polynom-Ring F;
thus ex i being Nat st i in dom G2 & G2.i = rpoly(1,a)
by X1,X2,X3,RING_4:30;
end;
now assume
ex i being Nat st i in dom G2 & G2.i = rpoly(1,a); then
consider i being Nat such that
X1: i in dom G2 & G2.i = rpoly(1,a);
reconsider i as Element of dom G2 by X1;
X2: B is one-to-one onto by C;
reconsider C = B" as Function of dom G2, dom G1 by X2,FUNCT_2:25;
C.i in dom G1; then
reconsider j = (B").i as Element of dom G1;
X3: G2.(B.j) is_associated_to G1.j by C;
consider b being Element of F such that
X4: G1.j = rpoly(1,b) by AS;
reconsider p1 = G1.j, p2 = G2.i as
Element of the carrier of Polynom-Ring F;
i = B.j by X2,FUNCT_1:35;
hence ex i being Nat st i in dom G1 & G1.i = rpoly(1,a)
by X1,X4,X3,RING_4:30;
end;
hence thesis by X;
end;
theorem lemma2u:
for F being Field,
E being FieldExtension of F
for G1 being non empty FinSequence of Polynom-Ring F
st for i being Nat st i in dom G1
ex a being Element of F st G1.i = rpoly(1,a)
for G2 being non empty FinSequence of Polynom-Ring E
st for i being Nat st i in dom G2
ex a being Element of E st G2.i = rpoly(1,a)
holds Product G1 = Product G2 implies
for a being Element of E holds
(ex i being Nat st i in dom G1 & G1.i = rpoly(1,a)) iff
(ex i being Nat st i in dom G2 & G2.i = rpoly(1,a))
proof
let F be Field, E be FieldExtension of F;
let G1 be non empty FinSequence of Polynom-Ring F;
assume AS1: for i being Nat st i in dom G1
ex a being Element of F st G1.i = rpoly(1,a);
let G2 be non empty FinSequence of Polynom-Ring E;
assume AS2: for i being Nat st i in dom G2
ex a being Element of E st G2.i = rpoly(1,a);
assume AS3: Product G1 = Product G2;
H: Polynom-Ring F is Subring of Polynom-Ring E by FIELD_4:def 1;
reconsider p = Product G2 as Polynomial of E by POLYNOM3:def 10;
now let o be object;
assume o in rng G1; then
consider i being object such that
H1: i in dom G1 & G1.i = o by FUNCT_1:def 3;
reconsider i as Nat by H1;
consider a being Element of F such that H2: G1.i = rpoly(1,a) by H1,AS1;
F is Subring of E by FIELD_4:def 1;
then the carrier of F c= the carrier of E by C0SP1:def 3;
then reconsider b = a as Element of E;
rpoly(1,a) = rpoly(1,b) by FIELD_4:21;
hence o in the carrier of Polynom-Ring E by H1,H2,POLYNOM3:def 10;
end;
then rng G1 c= the carrier of Polynom-Ring E; then
reconsider G1a = G1 as non empty FinSequence of Polynom-Ring E
by FINSEQ_1:def 4;
AS4: now let i be Nat;
assume i in dom G1a; then
consider a being Element of F such that L: G1.i = rpoly(1,a) by AS1;
F is Subring of E by FIELD_4:def 1;
then the carrier of F c= the carrier of E by C0SP1:def 3;
then reconsider b = a as Element of E;
rpoly(1,a) = rpoly(1,b) by FIELD_4:21;
hence ex a being Element of E st G1a.i = rpoly(1,a) by L;
end;
Product G1a = Product G2 by AS3,H,u5;
hence thesis by AS2,AS4,lemma2z;
end;
theorem u6:
for F being Field
for p being Ppoly of F
for a being Element of F holds LC(a * p) = a
proof
let F be Field; let q be Ppoly of F; let a be Element of F;
thus LC(a * q) = a * LC q by RING_5:5 .= a * 1.F by RING_5:50 .= a;
end;
theorem
for F being Field,
E being FieldExtension of F
for p being Ppoly of F holds p is Ppoly of E by lemmapp;
theorem lemma2d:
for F being Field,
E being FieldExtension of F
for a being non zero Element of F,
b being non zero Element of E
for p being Ppoly of F
for q being Ppoly of E st a * p = b * q holds a = b & p = q
proof
let F be Field, E be FieldExtension of F;
let a be non zero Element of F, b be non zero Element of E;
let p be Ppoly of F; let q be Ppoly of E;
assume AS: a * p = b * q;
thus T: b = b * 1.E
.= b * LC(q) by RING_5:50
.= LC(b * q) by RATFUNC1:18
.= LC(a * p) by AS,lemma2e
.= a * LC(p) by RATFUNC1:18
.= a * 1.F by RING_5:50
.= a;
F is Subfield of E by FIELD_4:7; then
the carrier of F c= the carrier of E by EC_PF_1:def 1; then
reconsider a1 = a as Element of E;
reconsider q1 = p as Ppoly of E by lemmapp;
a1|E = a|F by FIELD_6:23; then
(a1|E) *' q1 = (a|F) *' p by FIELD_4:17 .= a * p by poly1; then
(a1|E) *' q1 = (b|E) *' q by AS,poly1;
hence thesis by T,RATFUNC1:7;
end;
theorem u8:
for F being Field,
E being FieldExtension of F
for G being non empty FinSequence of the carrier of Polynom-Ring E
st for i being Nat st i in dom G ex a being Element of F st G.i = rpoly(1,a)
holds (Product G) is Ppoly of F
proof
let F be Field, E be FieldExtension of F;
let G be non empty FinSequence of the carrier of Polynom-Ring E;
assume AS: for i being Nat st i in dom G
ex a being Element of F st G.i = rpoly(1,a);
F is Subfield of E by FIELD_4:7; then
H1: the carrier of F c= the carrier of E by EC_PF_1:def 1;
defpred P[Nat] means
for G being non empty FinSequence of Polynom-Ring E st len G = $1 &
for i being Nat st i in dom G ex a being Element of F st G.i = rpoly(1,a)
holds Product G is Ppoly of F;
IA: P[0];
IS: now let k be Nat;
assume IV: P[k];
now let G be non empty FinSequence of Polynom-Ring E;
assume A: len G = k+1 & for i being Nat st i in dom G
ex a being Element of F st G.i = rpoly(1,a);
per cases;
suppose S: k = 0;
then 1 in Seg(len G) by A;
then 1 in dom G by FINSEQ_1:def 3;
then consider a being Element of F such that A0: G.1 = rpoly(1,a) by A;
H: G = <*rpoly(1,a)*> by A0,A,S,FINSEQ_1:40;
reconsider b = a as Element of E by H1;
rpoly(1,a) = rpoly(1,b) by FIELD_4:21; then
rpoly(1,a) is Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
then Product G = rpoly(1,a) by H,GROUP_4:9;
hence Product G is Ppoly of F by RING_5:51;
end;
suppose S: k > 0;
consider H being FinSequence, y being object such that
B2: G = H^<*y*> by FINSEQ_1:46;
B2a: rng H c= rng G by B2,FINSEQ_1:29;
B2b: rng G c= the carrier of Polynom-Ring E by FINSEQ_1:def 4;
then reconsider H as FinSequence of Polynom-Ring E
by B2a,XBOOLE_1:1,FINSEQ_1:def 4;
B3: len G = len H + len <*y*> by B2,FINSEQ_1:22
.= len H + 1 by FINSEQ_1:39; then
reconsider H as non empty FinSequence of Polynom-Ring E by S,A;
reconsider q = Product H as Polynomial of E by POLYNOM3:def 10;
C: dom H c= dom G by B2,FINSEQ_1:26;
now let i be Nat;
assume C0: i in dom H;
then H.i = G.i by B2,FINSEQ_1:def 7;
hence ex a being Element of F st H.i = rpoly(1,a) by C,C0,A;
end;
then reconsider q1 = Product H as Ppoly of F by B3,A,IV;
rng<*y*> = {y} by FINSEQ_1:39;
then G5: y in rng<*y*> by TARSKI:def 1;
rng<*y*> c= rng G by B2,FINSEQ_1:30;
then reconsider y as Element of Polynom-Ring E by G5,B2b;
dom<*y*> = {1} by FINSEQ_1:2,FINSEQ_1:def 8;
then 1 in dom<*y*> by TARSKI:def 1;
then B6: G.(k+1) = <*y*>.1 by B2,B3,A,FINSEQ_1:def 7
.= y;
dom G = Seg(k+1) by A,FINSEQ_1:def 3;
then consider a being Element of F such that
B9: y = rpoly(1,a) by A,B6,FINSEQ_1:4;
reconsider b = a as Element of E by H1;
reconsider y1 = rpoly(1,b) as Element of Polynom-Ring E
by POLYNOM3:def 10;
B8: rpoly(1,b) = rpoly(1,a) by FIELD_4:21;
B7: rpoly(1,a) is Ppoly of F by RING_5:51;
Product G = (Product H) * y by B2,GROUP_4:6
.= q *' rpoly(1,b) by B8,B9,POLYNOM3:def 10
.= q1 *' rpoly(1,a) by B8,FIELD_4:17;
hence Product G is Ppoly of F by B7,RING_5:52;
end;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that J: len G = n;
thus thesis by I,J,AS;
end;
begin :: Existence of Splitting Fields
lemma2:
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for U being FieldExtension of F
for E being U-extending FieldExtension of F st p splits_in E
holds p splits_in U iff
for a being Element of E st a is_a_root_of p,E holds a in U
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
let U be FieldExtension of F;
let E be U-extending FieldExtension of F;
assume p splits_in E; then
consider aE being non zero Element of E, qE being Ppoly of E such that
B: p = aE * qE by FIELD_4:def 5;
reconsider aqE = aE * qE as Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
consider GE being non empty FinSequence of the carrier of Polynom-Ring E
such that
C: qE = Product GE &
for i being Nat st i in dom GE ex a being Element of E st GE.i = rpoly(1,a)
by RING_5:def 4;
D: now let x be Element of E;
assume x is_a_root_of p,E; then
0.E = Ext_eval(p,x) by FIELD_4:def 2
.= eval(aqE,x) by B,FIELD_4:26
.= aE * eval(qE,x) by POLYNOM5:30; then
eval(qE,x) = 0.E by VECTSP_2:def 1;
hence ex i being Nat st i in dom GE & GE.i = rpoly(1,x) by C,RATFUNC1:12;
end;
U is Subfield of E by FIELD_4:7; then
H1: the carrier of U c= the carrier of E by EC_PF_1:def 1;
reconsider p0 = p as Element of the carrier of Polynom-Ring F;
p is Polynomial of E by FIELD_4:8; then
reconsider p1 = p as Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
A: now assume p splits_in U; then
consider a being non zero Element of U, q being Ppoly of U such that
A1: p = a * q by FIELD_4:def 5;
consider GU being non empty FinSequence of the carrier of Polynom-Ring U
such that
A4: q = Product GU &
for i being Nat st i in dom GU ex a being Element of U
st GU.i = rpoly(1,a) by RING_5:def 4;
reconsider q1 = q as Ppoly of E by lemmapp;
reconsider b = a as Element of E by H1;
A2: U is Subfield of E by FIELD_4:7;
now let x be Element of E;
assume x is_a_root_of p,E; then
consider j being Nat such that
B3: j in dom GE & GE.j = rpoly(1,x) by D;
qE = q by A1,B,lemma2d; then
consider i being Nat such that
G: i in dom GU & GU.i = rpoly(1,x) by B3,A4,C,lemma2u;
reconsider v = rpoly(1,x) as Element of the carrier of Polynom-Ring U
by G,PARTFUN1:4;
U is Subring of E by A2,FIELD_5:12; then
-v.0 = -rpoly(1,x).0 by FIELD_6:17
.= --(power(E).(x,1+0)) by HURWITZ:25
.= --(power(E).(x,0) * x) by GROUP_1:def 7
.= --(1_E * x) by GROUP_1:def 7
.= x;
hence x in the carrier of U;
end;
hence for a being Element of E st a is_a_root_of p,E holds a in U;
end;
X: aE*qE is Element of the carrier of Polynom-Ring E &
p is Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
now assume AS: for a being Element of E st a is_a_root_of p,E holds a in U;
now let i be Nat;
assume E: i in dom GE; then
consider c being Element of E such that F: GE.i = rpoly(1,c) by C;
eval(qE,c) = 0.E by E,F,C,RATFUNC1:12; then
eval(aE*qE,c) = aE * 0.E by RING_5:7; then
Ext_eval(p,c) = 0.E by X,B,FIELD_4:26; then
c in U by AS,FIELD_4:def 2; then
reconsider b = c as Element of U;
rpoly(1,c) = rpoly(1,b) by FIELD_4:21;
hence ex b being Element of U st GE.i = rpoly(1,b) by F;
end;
then reconsider qU = qE as Ppoly of U by C,u8;
I3: aE = LC(aE*qE) by u6 .= LC p by B,lemma2e;
U is Subring of E by FIELD_4:def 1; then
I4: 0.U = 0.E by C0SP1:def 3;
F is Subring of U by FIELD_4:def 1;
then the carrier of F c= the carrier of U by C0SP1:def 3;
then reconsider aU = aE as non zero Element of U by I3,I4,STRUCT_0:def 12;
I2: aU|U = aE|E by FIELD_6:23;
aU * qU = (aU|U) *' qU by poly1
.= (aE|E) *' qE by I2,FIELD_4:17
.= aE * qE by poly1;
hence p splits_in U by B,FIELD_4:def 5;
end;
hence thesis by A;
end;
theorem lemma6:
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for U being FieldExtension of F
for E being U-extending FieldExtension of F st p splits_in E
holds p splits_in U iff Roots(E,p) c= the carrier of U
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
let U being FieldExtension of F;
let E being U-extending FieldExtension of F;
assume AS: p splits_in E;
A: now assume A1: p splits_in U;
now let o be object;
assume o in Roots(E,p); then o in
{a where a is Element of E : a is_a_root_of p,E} by FIELD_4:def 4;
then consider a being Element of E such that
A2: o = a & a is_a_root_of p,E;
a in U by AS,A1,A2,lemma2;
hence o in the carrier of U by A2;
end;
hence Roots(E,p) c= the carrier of U;
end;
now assume B1: Roots(E,p) c= the carrier of U;
now let a be Element of E;
assume a is_a_root_of p,E;
then a in {a where a is Element of E : a is_a_root_of p,E};
then a in Roots(E,p) by FIELD_4:def 4;
hence a in U by B1;
end;
hence p splits_in U by AS,lemma2;
end;
hence thesis by A;
end;
theorem lemma3:
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for U being FieldExtension of F
for E being U-extending FieldExtension of F st p splits_in E
holds p splits_in U iff Roots(E,p) c= Roots(U,p)
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
let U being FieldExtension of F;
let E being U-extending FieldExtension of F;
assume AS: p splits_in E;
H: U is Subfield of E by FIELD_4:7;
A: now assume A1: p splits_in U;
now let o be object;
assume o in Roots(E,p); then o in
{a where a is Element of E : a is_a_root_of p,E} by FIELD_4:def 4;
then consider a being Element of E such that
A2: o = a & a is_a_root_of p,E;
a in U by AS,A1,A2,lemma2; then
reconsider b = a as Element of U;
Ext_eval(p,b) = Ext_eval(p,a) by FIELD_7:14
.= 0.E by A2,FIELD_4:def 2
.= 0.U by H,EC_PF_1:def 1; then
b is_a_root_of p,U by FIELD_4:def 2; then
b in {a where a is Element of U : a is_a_root_of p,U};
hence o in Roots(U,p) by A2,FIELD_4:def 4;
end;
hence Roots(E,p) c= Roots(U,p);
end;
now assume Roots(E,p) c= Roots(U,p);
then Roots(E,p) c= the carrier of U by XBOOLE_1:1;
hence p splits_in U by AS,lemma6;
end;
hence thesis by A;
end;
theorem
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for U being FieldExtension of F
for E being U-extending FieldExtension of F st p splits_in E
holds p splits_in U iff Roots(E,p) = Roots(U,p)
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
let U being FieldExtension of F;
let E being U-extending FieldExtension of F;
assume AS: p splits_in E;
now assume p splits_in U; then
B: Roots(E,p) c= Roots(U,p) by AS,lemma3;
Roots(U,p) c= Roots(E,p) by lemma7;
hence Roots(E,p) = Roots(U,p) by B,XBOOLE_0:def 10;
end;
hence thesis by AS,lemma3;
end;
theorem lemma5:
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for E being FieldExtension of F
st p splits_in E holds p splits_in FAdj(F,Roots(E,p))
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
let E be FieldExtension of F;
assume A: p splits_in E;
set K = FAdj(F,Roots(E,p));
B: E is K-extending by FIELD_4:7;
Roots(E,p) is Subset of K by FIELD_6:35;
hence thesis by A,B,lemma6;
end;
definition
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
mode SplittingField of p -> FieldExtension of F means :defspl:
p splits_in it &
for E being FieldExtension of F
st p splits_in E & E is Subfield of it holds E == it;
existence
proof
consider E being FieldExtension of F such that
A: p splits_in E by FIELD_5:31;
take K = FAdj(F,Roots(E,p));
thus p splits_in K by A,lemma5;
now let U be FieldExtension of F;
assume B: p splits_in U & U is Subfield of K;
C: U is Subfield of E by B,EC_PF_1:5; then
C1: E is FieldExtension of U by FIELD_4:7;
D: F is Subfield of U by FIELD_4:7;
E: Roots(U,p) c= Roots(E,p) by C1,lemma7;
Roots(E,p) c= Roots(U,p) by C1,A,B,lemma3; then
Roots(E,p) is Subset of U by E,XBOOLE_0:def 10;
hence U == K by B,D,C,FIELD_6:37;
end;
hence thesis;
end;
end;
theorem
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
ex E being FieldExtension of F st E is SplittingField of p
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
set E = the SplittingField of p;
take E;
thus thesis;
end;
theorem spl0:
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
ex E being FieldExtension of F
st FAdj(F,Roots(E,p)) is SplittingField of p
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
consider E being FieldExtension of F such that
A: p splits_in E by FIELD_5:31;
take E;
set K = FAdj(F,Roots(E,p));
thus p splits_in K by A,lemma5;
now let U be FieldExtension of F;
assume B: U is Subfield of K & p splits_in U;
C: U is Subfield of E by B,EC_PF_1:5; then
C1: E is FieldExtension of U by FIELD_4:7;
D: F is Subfield of U by FIELD_4:7;
E: Roots(U,p) c= Roots(E,p) by C1,lemma7;
Roots(E,p) c= Roots(U,p) by C1,A,B,lemma3; then
Roots(E,p) is Subset of U by E,XBOOLE_0:def 10;
hence K is Subfield of U by D,C,FIELD_6:37;
end;
hence thesis;
end;
theorem spl1:
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for E being FieldExtension of F st p splits_in E
holds FAdj(F,Roots(E,p)) is SplittingField of p
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
let E be FieldExtension of F;
assume AS: p splits_in E;
set K = FAdj(F,Roots(E,p));
thus p splits_in K by AS,lemma5;
now let U be FieldExtension of F;
assume B: U is Subfield of K & p splits_in U;
C: U is Subfield of E by B,EC_PF_1:5; then
C1: E is FieldExtension of U by FIELD_4:7;
D: F is Subfield of U by FIELD_4:7;
E: Roots(U,p) c= Roots(E,p) by C1,lemma7;
Roots(E,p) c= Roots(U,p) by C1,AS,B,lemma3; then
Roots(E,p) is Subset of U by E,XBOOLE_0:def 10;
hence K is Subfield of U by D,C,FIELD_6:37;
end;
hence thesis;
end;
theorem XX:
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
for E being SplittingField of p
holds E == FAdj(F,Roots(E,p))
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
let E be SplittingField of p;
set K = FAdj(F,Roots(E,p));
p splits_in E by defspl; then
K is SplittingField of p by spl1; then
p splits_in K by defspl;
hence thesis by defspl;
end;
registration
let F be Field;
let p be non constant Element of the carrier of Polynom-Ring F;
cluster strict for SplittingField of p;
existence
proof
consider E being FieldExtension of F such that
A: FAdj(F,Roots(E,p)) is SplittingField of p by spl0;
thus thesis by A;
end;
end;
registration
let F be Field;
let p be non constant Element of the carrier of Polynom-Ring F;
cluster -> F-finite for SplittingField of p;
coherence
proof
let E be SplittingField of p;
E == FAdj(F,Roots(E,p)) by XX;
hence thesis by FIELD_7:37;
end;
end;
begin :: Fixing and Extending Automorphisms
registration
let R be Ring;
cluster isomorphism for Function of R,R;
existence
proof
take id R;
thus thesis;
end;
end;
definition
let R be Ring;
mode Homomorphism of R is
additive multiplicative unity-preserving Function of R,R;
mode Monomorphism of R is monomorphism Function of R,R;
mode Automorphism of R is isomorphism Function of R,R;
end;
definition
let R,S2 be Ring,
S1 be RingExtension of R;
let h be Function of S1,S2;
attr h is R-fixing means :deffix:
for a being Element of R holds h.a = a;
end;
theorem e0:
for R,S2 being Ring,
S1 being RingExtension of R
for h being Function of S1,S2 holds h is R-fixing iff h|R = id R
proof
let R,S2 be Ring, S1 be RingExtension of R;
let h be Function of S1,S2;
H: R is Subring of S1 by FIELD_4:def 1;
A: now assume AS: h is R-fixing;
A0: dom h = the carrier of S1 by FUNCT_2:def 1;
the carrier of R c= the carrier of S1 by H,C0SP1:def 3; then
A1: dom(id R) = dom h /\ (the carrier of R) by A0,XBOOLE_1:28;
now let x be object;
assume x in dom(id R);
then reconsider a = x as Element of R;
h.a = a by AS;
hence (id R).x = h.x;
end;
hence h|R = id R by A1,FUNCT_1:46;
end;
now assume AS: h|R = id R;
now let a be Element of R;
thus h.a = (h|(the carrier of R)).a by FUNCT_1:49
.= a by AS;
end;
hence h is R-fixing;
end;
hence thesis by A;
end;
theorem lintrans:
for F being Field,
E1 being FieldExtension of F,
E2 being E1-homomorphic FieldExtension of F
for h being Homomorphism of E1,E2
holds h is F-fixing iff
h is linear-transformation of VecSp(E1,F),VecSp(E2,F)
proof
let F be Field, E1 be FieldExtension of F,
E2 be E1-homomorphic FieldExtension of F;
let h be Homomorphism of E1,E2;
G: now assume AS: h is F-fixing;
H: dom h = the carrier of E1 by FUNCT_2:def 1
.= the carrier of VecSp(E1,F) by FIELD_4:def 6;
rng h c= the carrier of E2 by RELAT_1:def 19; then
rng h c= the carrier of VecSp(E2,F) by FIELD_4:def 6; then
reconsider f = h as Function of VecSp(E1,F),VecSp(E2,F) by H,FUNCT_2:2;
now let x,y be Element of VecSp(E1,F);
reconsider a = x, b = y as Element of E1 by FIELD_4:def 6;
H: x + y = a + b by FIELD_4:def 6;
thus f.(x+y) = h.a + h.b by H,VECTSP_1:def 20
.= f.x + f.y by FIELD_4:def 6;
end; then
A: f is additive;
now let a be Scalar of F, x be Vector of VecSp(E1,F);
reconsider v = x as Element of E1 by FIELD_4:def 6;
F is Subring of E1 by FIELD_4:def 1; then
the carrier of F c= the carrier of E1 by C0SP1:def 3; then
reconsider u1 = a as Element of E1;
F is Subring of E2 by FIELD_4:def 1; then
the carrier of F c= the carrier of E2 by C0SP1:def 3; then
reconsider u2 = a as Element of E2;
I: [u1,v] in [:the carrier of F,the carrier of E1:] by ZFMISC_1:def 2;
H: a * x = (the multF of E1)|[:the carrier of F,the carrier of E1:].(u1,v)
by FIELD_4:def 6
.= u1 * v by I,FUNCT_1:49;
J: [u2,h.v] in [:the carrier of F,the carrier of E2:] by ZFMISC_1:def 2;
thus f.(a*x)
= h.u1 * h.v by H,GROUP_6:def 6
.= u2 * h.v by AS
.= (the multF of E2)|[:the carrier of F,the carrier of E2:].(u2,h.v)
by J,FUNCT_1:49
.= a * f.x by FIELD_4:def 6;
end;
hence h is linear-transformation of VecSp(E1,F),VecSp(E2,F)
by A,MOD_2:def 2;
end;
set V1 = VecSp(E1,F), V2 = VecSp(E2,F);
now assume h is linear-transformation of VecSp(E1,F),VecSp(E2,F); then
reconsider h1 = h as linear-transformation of VecSp(E1,F),VecSp(E2,F);
A: the carrier of E1 = the carrier of VecSp(E1,F) by FIELD_4:def 6;
reconsider 1V = 1.E1 as Element of VecSp(E1,F) by FIELD_4:def 6;
now let a be Element of F;
F is Subfield of E1 by FIELD_4:7; then
B: the carrier of F c= the carrier of E1 &
the multF of F = (the multF of E1) || the carrier of F &
1.F = 1.E1 by EC_PF_1:def 1;
F is Subfield of E2 by FIELD_4:7; then
the carrier of F c= the carrier of E2 by EC_PF_1:def 1;
then reconsider a2 = a as Element of E2;
reconsider aV = a as Element of VecSp(E1,F) by A,B;
D: [a,1.F] in [:the carrier of F,the carrier of E1:] by B,ZFMISC_1:def 2;
E: [a,1.F] in [:the carrier of F,the carrier of F:] by ZFMISC_1:def 2;
F: (the multF of F).(a,1.F)
= (the multF of E1).(a,1.F) by B,E,FUNCT_1:49
.= ((the multF of E1)|[:the carrier of F,the carrier of E1:]).(a,1.F)
by D,FUNCT_1:49
.= (the lmult of V1).(a,1V) by B,FIELD_4:def 6;
I: [a,1.E2] in [:the carrier of F,the carrier of E2:] by ZFMISC_1:def 2;
G: h1.1V = h.(1_E1) .= 1_E2 by GROUP_1:def 13;
J: (the lmult of V2).(a,1.E2)
= ((the multF of E2)|[:the carrier of F,the carrier of E2:]).(a,1.E2)
by FIELD_4:def 6
.= (the multF of E2).(a2,1.E2) by I,FUNCT_1:49;
h.(a * 1.F) = h1.(a * 1V) by F
.= a * h1.1V by MOD_2:def 2
.= a2 * 1.E2 by J,G;
hence h.a = a;
end;
hence h is F-fixing;
end;
hence thesis by G;
end;
theorem
for F being Field,
E being FieldExtension of F
for E1 being E-extending FieldExtension of F,
E2 being E-extending FieldExtension of F
for h being Function of E1,E2 holds h is E-fixing implies h is F-fixing
proof
let F be Field, E be FieldExtension of F;
let E1 be E-extending FieldExtension of F,
E2 be E-extending FieldExtension of F;
let h be Function of E1,E2;
assume AS: h is E-fixing;
now let a be Element of F;
thus h.a = h.(@(a,E)) by FIELD_7:def 4
.= @(a,E) by AS
.= a by FIELD_7:def 4;
end;
hence thesis;
end;
definition
let R be Ring,
S1,S2 be RingExtension of R;
let h be Function of S1,S2;
attr h is R-homomorphism means
h is R-fixing additive multiplicative unity-preserving;
attr h is R-monomorphism means
h is R-fixing monomorphism;
attr h is R-isomorphism means :deffixiso:
h is R-fixing isomorphism;
end;
registration
let R be Ring;
let S be RingExtension of R;
cluster R-fixing for Automorphism of S;
existence
proof
reconsider h = id S as Automorphism of S;
take h;
now let a be Element of R;
R is Subring of S by FIELD_4:def 1; then
the carrier of R c= the carrier of S by C0SP1:def 3;
then reconsider a1 = a as Element of S;
h.a1 = a1;
hence h.a = a;
end;
hence thesis;
end;
end;
theorem prm:
for R being Ring,
S being RingExtension of R
for p being Element of the carrier of Polynom-Ring R
for h being R-fixing Monomorphism of S
for a being Element of S holds a in Roots(S,p) iff h.a in Roots(S,p)
proof
let F be Ring, E be RingExtension of F;
let p be Element of the carrier of Polynom-Ring F;
let h be F-fixing Monomorphism of E;
let a be Element of E;
h is monomorphism; then
reconsider E1 = E as E-monomorphic E-homomorphic Ring
by RING_2:def 4,RING_3:def 3;
reconsider h1 = h as Monomorphism of E,E1;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of Polynom-Ring E;
now let i be Element of NAT;
thus p.i = h1.(p.i) by deffix .= ((PolyHom h1).p1).i by FIELD_1:def 2;
end;
then H: (PolyHom h1).p1 = p1;
A: now assume a in Roots(E,p);
then a in Roots p1 by FIELD_7:13;
then a is_a_root_of p1 by POLYNOM5:def 10;
then h1.a is_a_root_of (PolyHom h1).p1 by FIELD_1:34;
then h.a in Roots p1 by H,POLYNOM5:def 10;
hence h.a in Roots(E,p) by FIELD_7:13;
end;
now assume h.a in Roots(E,p);
then A0: h.a in Roots (PolyHom h1).p1 by H,FIELD_7:13;
Roots p1 = {a where a is Element of E : h1.a in Roots (PolyHom h1).p1}
by FIELD_1:37;
then a in Roots p1 by A0;
hence a in Roots(E,p) by FIELD_7:13;
end;
hence thesis by A;
end;
theorem
for R being domRing,
S being domRingExtension of R
for p being non zero Element of the carrier of Polynom-Ring R
for h being R-fixing Monomorphism of S
holds h|Roots(S,p) is Permutation of Roots(S,p)
proof
let R be domRing, S be domRingExtension of R;
let p be non zero Element of the carrier of Polynom-Ring R;
let h be R-fixing Monomorphism of S;
set N = Roots(S,p);
reconsider g = h|Roots(S,p) as Function of N,S by FUNCT_2:32;
C: dom g = Roots(S,p) by FUNCT_2:def 1;
now let o be object;
assume o in rng g; then
consider b being object such that
B1: b in dom g & o = g.b by FUNCT_1:def 3;
reconsider b as Element of S by C,B1;
h.b in Roots(S,p) by B1,prm;
hence o in Roots(S,p) by B1,FUNCT_1:47;
end;
then rng g c= Roots(S,p);
then reconsider g as Function of N,N by C,FUNCT_2:2;
E: card Roots(S,p) = card Roots(S,p);
A: g is one-to-one by FUNCT_1:52; then
g is onto by E,FINSEQ_4:63;
hence thesis by A;
end;
definition
let R1,R2,S2 be Ring,
S1 be RingExtension of R1;
let h1 be Function of R1,R2, h2 be Function of S1,S2;
attr h2 is h1-extending means
for a being Element of R1 holds h2.a = h1.a;
end;
theorem e1:
for R1,R2,S2 being Ring,
S1 being RingExtension of R1
for h1 being Function of R1,R2, h2 being Function of S1,S2
holds h2 is h1-extending iff h2|R1 = h1
proof
let R1,R2,S2 be Ring, S1 be RingExtension of R1;
let h1 be Function of R1,R2, h2 be Function of S1,S2;
H: R1 is Subring of S1 by FIELD_4:def 1;
now assume AS: h2 is h1-extending;
A0: dom h2 = the carrier of S1 &
dom h1 = the carrier of R1 by FUNCT_2:def 1;
the carrier of R1 c= the carrier of S1 by H,C0SP1:def 3; then
A1: dom h1 = dom h2 /\ (the carrier of R1) by A0,XBOOLE_1:28;
for x being object st x in dom h1 holds h2.x = h1.x by AS;
hence h2|R1 = h1 by A1,FUNCT_1:46;
end;
hence thesis by FUNCT_1:49;
end;
registration
let R be Ring;
let S be RingExtension of R;
cluster R-fixing -> (id R)-extending for Automorphism of S;
coherence;
cluster (id R)-extending -> R-fixing for Automorphism of S;
coherence
proof
let h be Automorphism of S;
assume h is (id R)-extending;
then h|R = id R by e1;
hence h is R-fixing by e0;
end;
end;
theorem e1a:
for F1,F2 being Field,
E1 being FieldExtension of F1, E2 being FieldExtension of F2
for K1 being E1-extending FieldExtension of F1,
K2 being E2-extending FieldExtension of F2
for h1 being Function of F1,F2, h2 being Function of E1,E2,
h3 being Function of K1,K2
st h2 is h1-extending & h3 is h2-extending holds h3 is h1-extending
proof
let F1,F2 be Field,
E1 be FieldExtension of F1, E2 be FieldExtension of F2;
let K1 be E1-extending FieldExtension of F1,
K2 be E2-extending FieldExtension of F2;
let h1 be Function of F1,F2, h2 be Function of E1,E2,
h3 be Function of K1,K2;
assume AS: h2 is h1-extending & h3 is h2-extending;
now let a be Element of F1;
thus h3.a = h3.@(a,E1) by FIELD_7:def 4
.= h2.@(a,E1) by AS
.= h2.a by FIELD_7:def 4
.= h1.a by AS;
end;
hence thesis;
end;
definition
let F be Field;
let E1,E2 be FieldExtension of F;
pred E1,E2 are_isomorphic_over F means
ex i being Function of E1,E2 st i is F-isomorphism;
end;
theorem
for F being Field,
E being FieldExtension of F holds E,E are_isomorphic_over F
proof
let F be Field, E be FieldExtension of F;
now let a be Element of F;
F is Subring of E by FIELD_4:def 1;
then the carrier of F c= the carrier of E by C0SP1:def 3;
hence (id E).a = a by FUNCT_1:18;
end;
then id E is F-fixing;
then id E is F-isomorphism;
hence thesis;
end;
theorem
for F being Field,
E1,E2 being FieldExtension of F
st E1,E2 are_isomorphic_over F holds E2,E1 are_isomorphic_over F
proof
let F be Field, E1,E2 be FieldExtension of F;
F is Subring of E1 by FIELD_4:def 1; then
H1: the carrier of F c= the carrier of E1 by C0SP1:def 3;
assume E1,E2 are_isomorphic_over F; then
consider f being Function of E1,E2 such that A: f is F-isomorphism;
B: f is F-fixing isomorphism by A;
C: f is one-to-one & f is onto & rng f = the carrier of E2 by A,FUNCT_2:def 3;
then reconsider g = f" as Function of E2,E1 by FUNCT_2:25;
now let a be Element of F;
H2: dom f = the carrier of E1 by FUNCT_2:def 1;
H3: a in the carrier of E1 by H1;
thus g.a = g.(f.a) by B .= a by H2,H3,A,FUNCT_1:34;
end;
then D: g is F-fixing;
H4: f is additive multiplicative unity-preserving by A;
H5: g is additive
proof
now let a,b be Element of E2;
consider x being object such that
A2: x in the carrier of E1 & a = f.x by C,FUNCT_2:11;
reconsider x as Element of E1 by A2;
consider y being object such that
A3: y in the carrier of E1 & b = f.y by C,FUNCT_2:11;
reconsider y as Element of E1 by A3;
thus g.a + g.b = x + g.(f.y) by A2,A3,A,FUNCT_2:26
.= x + y by A,FUNCT_2:26
.= g.(f.(x+y)) by A,FUNCT_2:26
.= g.(a+b) by H4,A2,A3;
end;
hence thesis;
end;
H6: g is multiplicative
proof
now let a,b be Element of E2;
consider x being object such that
A2: x in the carrier of E1 & a = f.x by C,FUNCT_2:11;
reconsider x as Element of E1 by A2;
consider y being object such that
A3: y in the carrier of E1 & b = f.y by C,FUNCT_2:11;
reconsider y as Element of E1 by A3;
thus g.a * g.b = x * g.(f.y) by A,A2,A3,FUNCT_2:26
.= x * y by A,FUNCT_2:26
.= g.(f.(x*y)) by A,FUNCT_2:26
.= g.(a*b) by H4,A2,A3;
end;
hence thesis;
end;
F: g is unity-preserving by H4,FUNCT_2:26;
now let x be object;
H7: now assume H8: x in rng g;
rng g c= the carrier of E1 by RELAT_1:def 19;
hence x in the carrier of E1 by H8;
end;
now assume x in the carrier of E1;
then reconsider x1 = x as Element of E1;
f.x1 in the carrier of E2;
then A9: f.x1 in dom g by FUNCT_2:def 1;
g.(f.x1) = x1 by A,FUNCT_2:26;
hence x in rng g by A9,FUNCT_1:def 3;
end;
hence x in rng g iff x in the carrier of E1 by H7;
end;
then g is onto by TARSKI:2;
then g is F-isomorphism by D,F,H5,H6;
hence E2,E1 are_isomorphic_over F;
end;
theorem
for F being Field,
E1,E2,E3 being FieldExtension of F
st E1,E2 are_isomorphic_over F & E2,E3 are_isomorphic_over F
holds E1,E3 are_isomorphic_over F
proof
let F be Field, E1,E2,E3 be FieldExtension of F;
assume AS: E1,E2 are_isomorphic_over F & E2,E3 are_isomorphic_over F;
consider f being Function of E1,E2 such that A: f is F-isomorphism by AS;
consider g being Function of E2,E3 such that B: g is F-isomorphism by AS;
C: f is F-fixing isomorphism by A;
D: f is one-to-one & f is onto & rng f = the carrier of E2 by A,FUNCT_2:def 3;
E: g is F-fixing isomorphism by B;
F: g is one-to-one & g is onto & rng g = the carrier of E3 by B,FUNCT_2:def 3;
H0: dom(g * f) = the carrier of E1
proof
H1: for o being object st o in dom(g*f) holds o in the carrier of E1;
now let o be object;
assume H2: o in the carrier of E1; then
reconsider x = o as Element of E1;
o in dom f & f.x in the carrier of E2 by H2,FUNCT_2:def 1;
then o in dom f & f.o in dom g by FUNCT_2:def 1;
hence o in dom(g*f) by FUNCT_1:11;
end;
hence thesis by H1,TARSKI:2;
end;
rng(g * f) = the carrier of E3 by D,F,FUNCT_2:14; then
reconsider h = g * f as Function of E1,E3 by H0,FUNCT_2:2;
K: h is onto by D,F,FUNCT_2:14;
h is F-fixing
proof
F is Subring of E1 by FIELD_4:def 1; then
H3: the carrier of F c= the carrier of E1 by C0SP1:def 3;
now let a be Element of F;
thus h.a = g.(f.a) by H0,H3,FUNCT_1:12 .= g.a by C .= a by E;
end;
hence thesis;
end;
then h is F-isomorphism by A,B,K;
hence thesis;
end;
theorem
for F being Field,
E1 being F-finite FieldExtension of F,
E2 being FieldExtension of F
st E1,E2 are_isomorphic_over F holds E2 is F-finite & deg(E1,F) = deg(E2,F)
proof
let F be Field, E1 be F-finite FieldExtension of F,
E2 being FieldExtension of F;
assume E1,E2 are_isomorphic_over F; then
consider h being Function of E1,E2 such that A: h is F-isomorphism;
H: the carrier of VecSp(E1,F) = the carrier of E1 &
the carrier of VecSp(E2,F) = the carrier of E2 by FIELD_4:def 6;
reconsider E = E2 as E1-homomorphic FieldExtension of F by A,RING_2:def 4;
reconsider h as Homomorphism of E1,E by A;
reconsider i = h as linear-transformation of VecSp(E1,F),VecSp(E,F)
by A,lintrans;
C: VecSp(E1,F) is finite-dimensional by FIELD_4:def 8;
i is bijective by H,A; then
D: VecSp(E2,F) is finite-dimensional &
dim(VecSp(E1,F)) = dim(VecSp(E2,F)) by C,VECTSP12:4;
hence E2 is F-finite by FIELD_4:def 8;
thus deg(E1,F) = dim(VecSp(E2,F)) by D,FIELD_4:def 7
.= deg(E2,F) by D,FIELD_4:def 7;
end;
begin :: Some More Preliminaries
definition
let R be Ring,
S1,S2 be RingExtension of R;
let h be Relation of the carrier of S1,the carrier of S2;
attr h is R-risomorphism means
ex g being Function of S1,S2 st g = h & g is R-isomorphism;
end;
theorem u1:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
holds 0.FAdj(F,{a}) = Ext_eval(0_.F,a) & 1.FAdj(F,{a}) = Ext_eval(1_.F,a)
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E;
H: F is Subring of E by FIELD_4:def 1;
thus 0.FAdj(F,{a}) = 0.E by FIELD_6:def 6
.= Ext_eval(0_.F,a) by ALGNUM_1:13;
thus 1.FAdj(F,{a}) = 1.E by FIELD_6:def 6
.= Ext_eval(1_.F,a) by H,ALGNUM_1:14;
end;
theorem u2:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for x,y being Element of FAdj(F,{a})
for p,q being Polynomial of F st x = Ext_eval(p,a) & y = Ext_eval(q,a)
holds x + y = Ext_eval(p+q,a) & x * y = Ext_eval(p*'q,a)
proof
let F be Field, E be FieldExtension of F; let a be F-algebraic Element of E;
let x,y be Element of FAdj(F,{a}); let p,q be Polynomial of F;
assume AS: x = Ext_eval(p,a) & y = Ext_eval(q,a);
H0: F is Subring of E by FIELD_4:def 1;
x in the carrier of FAdj(F,{a}); then
H1: x in carrierFA({a}) by FIELD_6:def 6;
y in the carrier of FAdj(F,{a}); then
y in carrierFA({a}) by FIELD_6:def 6; then
H2: [x,y] in [:carrierFA({a}),carrierFA({a}):] by H1,ZFMISC_1:def 2;
thus x + y = ((the addF of E)||carrierFA({a})).(x,y) by FIELD_6:def 6
.= Ext_eval(p,a) + Ext_eval(q,a) by AS,H2,FUNCT_1:49
.= Ext_eval(p+q,a) by H0,ALGNUM_1:15;
thus x * y = ((the multF of E)||carrierFA({a})).(x,y) by FIELD_6:def 6
.= Ext_eval(p,a) * Ext_eval(q,a) by AS,H2,FUNCT_1:49
.= Ext_eval(p*'q,a) by H0,ALGNUM_1:20;
end;
theorem u3:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for x being Element of F holds x = Ext_eval(x|F,a)
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E; let x be Element of F;
thus Ext_eval(x|F,a) = LC(x|F) by FIELD_6:28 .= x by RING_5:6;
end;
theorem u10:
for F being Field,
E being FieldExtension of F
for a being Element of E
holds hom_Ext_eval(a,F) is Function of (Polynom-Ring F),RAdj(F,{a})
proof
let F be Field, E be FieldExtension of F; let a be Element of E;
reconsider E1 = E as (Polynom-Ring F)-homomorphic Field;
reconsider f = hom_Ext_eval(a,F) as Homomorphism of (Polynom-Ring F),E1;
RAdj(F,{a}) = Image f by FIELD_6:44;
then rng f = the carrier of RAdj(F,{a}) by RING_2:def 6;
hence thesis by FUNCT_2:6;
end;
theorem
for F being Field,
E being FieldExtension of F
for a being Element of E
holds hom_Ext_eval(a,F) is Function of (Polynom-Ring F),FAdj(F,{a})
proof
let F be Field, E be FieldExtension of F; let a be Element of E;
RAdj(F,{a}) is Subring of FAdj(F,{a}) by FIELD_6:39; then
A: the carrier of RAdj(F,{a}) c= the carrier of FAdj(F,{a}) by C0SP1:def 3;
hom_Ext_eval(a,F) is Function of (Polynom-Ring F),RAdj(F,{a}) by u10;
hence thesis by A,FUNCT_2:7;
end;
theorem x1000:
for F1 being Field,
F2 being F1-isomorphic F1-homomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1, E2 being FieldExtension of F2
for a being F1-algebraic Element of E1, b being F2-algebraic 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 (PolyHom h).MinPoly(a,F1) = MinPoly(b,F2)
proof
let F1 be Field, F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let E1 be FieldExtension of F1, E2 being FieldExtension of F2;
let a be F1-algebraic Element of E1, b being F2-algebraic Element of E2;
let p be irreducible Element of the carrier of Polynom-Ring F1;
assume AS: Ext_eval(p,a) = 0.E1 & Ext_eval((PolyHom h).p,b) = 0.E2;
hence MinPoly(b,F2) = NormPolynomial (PolyHom h).p by uu4
.= (PolyHom h).(NormPolynomial p) by uu5
.= (PolyHom h).MinPoly(a,F1) by AS,uu4;
end;
theorem
for F1 being Field,
F2 being F1-isomorphic F1-homomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1, E2 being FieldExtension of F2
for a being F1-algebraic Element of E1, b being F2-algebraic Element of E2
st Ext_eval((PolyHom h).MinPoly(a,F1),b) = 0.E2
holds (PolyHom h).MinPoly(a,F1) = MinPoly(b,F2)
proof
let F1 be Field, F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let E1 be FieldExtension of F1, E2 being FieldExtension of F2;
let a be F1-algebraic Element of E1, b being F2-algebraic Element of E2;
set p = MinPoly(a,F1);
A: Ext_eval(p,a) = 0.E1 by FIELD_6:51;
assume Ext_eval((PolyHom h).MinPoly(a,F1),b) = 0.E2;
hence MinPoly(b,F2) = NormPolynomial (PolyHom h).p by uu4
.= (PolyHom h).(NormPolynomial p) by uu5
.= (PolyHom h).MinPoly(a,F1) by A,uu4;
end;
theorem splift:
for F1 being Field,
p1 being non constant Element of the carrier of Polynom-Ring F1
for F2 being FieldExtension of F1,
p2 being non constant Element of the carrier of Polynom-Ring F2
for E being SplittingField of p1
st p2 = p1 & E is F2-extending holds E is SplittingField of p2
proof
let F1 be Field,
p1 be non constant Element of the carrier of Polynom-Ring F1;
let F2 be FieldExtension of F1,
p2 be non constant Element of the carrier of Polynom-Ring F2;
let E be SplittingField of p1;
assume AS: p2 = p1 & E is F2-extending;
p1 splits_in E by defspl; then
consider a being non zero Element of E, q being Ppoly of E such that
A: p1 = a * q by FIELD_4:def 5;
now let K be FieldExtension of F2;
assume C: p2 splits_in K & K is Subfield of E; then
consider a being non zero Element of K, q being Ppoly of K such that
D: p2 = a * q by FIELD_4:def 5;
p1 splits_in K by D,AS,FIELD_4:def 5;
hence K == E by C,defspl;
end;
hence thesis by A,AS,FIELD_4:def 5,defspl;
end;
begin :: Uniqueness of Splitting Fields
definition
let F be Field,
E be FieldExtension of F;
let a,b be F-algebraic Element of E;
func Phi(a,b) -> Relation of the carrier of FAdj(F,{a}),
the carrier of FAdj(F,{b}) equals
the set of all [Ext_eval(p,a),Ext_eval(p,b)] where p is Polynomial of F;
coherence
proof
set M = the set of all [Ext_eval(p,a),Ext_eval(p,b)]
where p is Polynomial of F;
H: FAdj(F,{a}) = RAdj(F,{a}) by FIELD_6:56;
I: FAdj(F,{b}) = RAdj(F,{b}) by FIELD_6:56;
now let o be object;
assume o in M; then
consider p being Polynomial of F such that
A: o = [Ext_eval(p,a),Ext_eval(p,b)];
Ext_eval(p,a) in the set of all Ext_eval(p,a) where p is Polynomial of F;
then B: Ext_eval(p,a) in the carrier of FAdj(F,{a}) by H,FIELD_6:45;
Ext_eval(p,b) in the set of all Ext_eval(p,b) where p is Polynomial of F;
then Ext_eval(p,b) in the carrier of FAdj(F,{b}) by I,FIELD_6:45;
hence o in [:the carrier of FAdj(F,{a}),
the carrier of FAdj(F,{b}):] by A,B,ZFMISC_1:def 2;
end;
then M c= [:the carrier of FAdj(F,{a}),the carrier of FAdj(F,{b}):];
hence thesis;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let a,b be F-algebraic Element of E;
cluster Phi(a,b) -> quasi_total;
coherence
proof
H: FAdj(F,{a}) = RAdj(F,{a}) by FIELD_6:56;
A: for o being object st o in dom Phi(a,b)
holds o in the carrier of FAdj(F,{a});
now let o be object;
assume o in the carrier of FAdj(F,{a}); then
o in the set of all Ext_eval(p,a) where p is Polynomial of F
by H,FIELD_6:45; then
consider p being Polynomial of F such that
A: o = Ext_eval(p,a);
ex y being object st [o,y] in Phi(a,b)
proof
take y = Ext_eval(p,b);
thus thesis by A;
end;
hence o in dom Phi(a,b) by XTUPLE_0:def 12;
end;
then dom Phi(a,b) = the carrier of FAdj(F,{a}) by A,TARSKI:2;
hence thesis by FUNCT_2:def 1;
end;
end;
theorem
for F being Field,
E being FieldExtension of F
for a,b being F-algebraic Element of E
holds Phi(a,b) is F-risomorphism iff MinPoly(a,F) = MinPoly(b,F)
proof
let F be Field, E be FieldExtension of F;
let a,b be F-algebraic Element of E;
set Fa = FAdj(F,{a}), Fb = FAdj(F,{b});
I1: FAdj(F,{a}) = RAdj(F,{a}) by FIELD_6:56;
I2: FAdj(F,{b}) = RAdj(F,{b}) by FIELD_6:56;
I4: F is Subring of E by FIELD_4:def 1;
A: now assume AS: MinPoly(a,F) = MinPoly(b,F);
now let x,y1,y2 be object;
assume A1: [x,y1] in Phi(a,b) & [x,y2] in Phi(a,b); then
consider p being Polynomial of F such that
A2: [x,y1] = [Ext_eval(p,a),Ext_eval(p,b)];
A3: x = Ext_eval(p,a) & y1 = Ext_eval(p,b) by A2,XTUPLE_0:1;
consider q being Polynomial of F such that
A4: [x,y2] = [Ext_eval(q,a),Ext_eval(q,b)] by A1;
A5: x = Ext_eval(q,a) & y2 = Ext_eval(q,b) by A4,XTUPLE_0:1;
A6: for r being Polynomial of F holds
Ext_eval(r,a) = 0.E implies Ext_eval(r,b) = 0.E
proof
let r be Polynomial of F;
A8: r is Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
assume Ext_eval(r,a) = 0.E; then
MinPoly(b,F) divides r by AS,A8,FIELD_6:53;
hence Ext_eval(r,b) = 0.E by A8,FIELD_6:53;
end;
Ext_eval(p,a) = Ext_eval(q,a) by A2,XTUPLE_0:1,A5; then
0.E = Ext_eval(p,a) - Ext_eval(q,a) by RLVECT_1:15
.= Ext_eval(p-q,a) by FIELD_6:27; then
0.E = Ext_eval(p-q,b) by A6
.= Ext_eval(p,b) - Ext_eval(q,b) by FIELD_6:27;
hence y1 = y2 by A5,A3,RLVECT_1:21;
end; then
reconsider g = Phi(a,b) as Function of
the carrier of FAdj(F,{a}),the carrier of FAdj(F,{b}) by FUNCT_1:def 1;
H: now let p be Polynomial of F;
[Ext_eval(p,a),Ext_eval(p,b)] in Phi(a,b);
hence g.Ext_eval(p,a) = Ext_eval(p,b) by FUNCT_1:1;
end;
I: g.(1.Fa) = g.Ext_eval(1_.F,a) by u1
.= Ext_eval(1_.F,b) by H
.= 1.Fb by u1;
now let x,y be Element of FAdj(F,{a});
x in the carrier of FAdj(F,{a}); then
x in the set of all Ext_eval(p,a) where p is Polynomial of F
by I1,FIELD_6:45; then
consider p being Polynomial of F such that A1: x = Ext_eval(p,a);
y in the carrier of FAdj(F,{a}); then
y in the set of all Ext_eval(p,a) where p is Polynomial of F
by I1,FIELD_6:45; then
consider q being Polynomial of F such that A2: y = Ext_eval(q,a);
B: g.x = Ext_eval(p,b) & g.y = Ext_eval(q,b) by A1,A2,H;
g.x in the carrier of FAdj(F,{b}) &
g.y in the carrier of FAdj(F,{b}); then
g.x in carrierFA({b}) & g.y in carrierFA({b}) by FIELD_6:def 6; then
C: [g.x,g.y] in [:carrierFA({b}),carrierFA({b}):] by ZFMISC_1:def 2;
x * y = Ext_eval(p*'q,a) by A1,A2,u2;
hence g.(x*y) = Ext_eval(p*'q,b) by H
.= Ext_eval(p,b) * Ext_eval(q,b) by I4,ALGNUM_1:20
.= ((the multF of E)||carrierFA({b})).(g.x,g.y)
by B,C,FUNCT_1:49
.= g.x * g.y by FIELD_6:def 6;
end; then
B: g is multiplicative;
now let x,y be Element of FAdj(F,{a});
x in the carrier of FAdj(F,{a}); then
x in the set of all Ext_eval(p,a) where p is Polynomial of F
by I1,FIELD_6:45; then
consider p being Polynomial of F such that A1: x = Ext_eval(p,a);
y in the carrier of FAdj(F,{a}); then
y in the set of all Ext_eval(p,a) where p is Polynomial of F
by I1,FIELD_6:45; then
consider q being Polynomial of F such that A2: y = Ext_eval(q,a);
B: g.x = Ext_eval(p,b) & g.y = Ext_eval(q,b) by A1,A2,H;
g.x in the carrier of FAdj(F,{b}) &
g.y in the carrier of FAdj(F,{b}); then
g.x in carrierFA({b}) & g.y in carrierFA({b}) by FIELD_6:def 6; then
C: [g.x,g.y] in [:carrierFA({b}),carrierFA({b}):] by ZFMISC_1:def 2;
x + y = Ext_eval(p+q,a) by A1,A2,u2;
hence g.(x+y) = Ext_eval(p+q,b) by H
.= Ext_eval(p,b) + Ext_eval(q,b) by I4,ALGNUM_1:15
.= ((the addF of E)||carrierFA({b})).(g.x,g.y)
by B,C,FUNCT_1:49
.= g.x + g.y by FIELD_6:def 6;
end; then
g is additive; then
D: g is monomorphism by I,B,RING_2:11;
X: g is onto
proof
E1: now let o be object;
assume E2: o in rng g;
rng g c= the carrier of FAdj(F,{b}) by RELAT_1:def 19;
hence o in the carrier of FAdj(F,{b}) by E2;
end;
now let o be object;
assume o in the carrier of FAdj(F,{b});
then o in the set of all Ext_eval(p,b) where p is Polynomial of F
by I2,FIELD_6:45;
then consider p being Polynomial of F such that
E2: o = Ext_eval(p,b);
Ext_eval(p,a) in
the set of all Ext_eval(p,a) where p is Polynomial of F;
then Ext_eval(p,a) in the carrier of FAdj(F,{a}) by I1,FIELD_6:45;
then E3: Ext_eval(p,a) in dom g by FUNCT_2:def 1;
g.Ext_eval(p,a) = o by E2,H;
hence o in rng g by E3,FUNCT_1:def 3;
end;
hence thesis by E1,TARSKI:2;
end;
now let x be Element of F;
x = Ext_eval(x|F,a) by u3;
then g.x = Ext_eval(x|F,b) by H;
hence g.x = x by u3;
end;
then g is F-fixing;
hence Phi(a,b) is F-risomorphism by X,D,deffixiso;
end;
now assume Phi(a,b) is F-risomorphism; then
consider g being Function of Fa,Fb such that
B1: g = Phi(a,b) & g is F-isomorphism;
set h = g * hom_Ext_eval(a,F);
rng hom_Ext_eval(a,F) c= dom g
proof
let o be object;
assume B2: o in rng hom_Ext_eval(a,F);
reconsider E1 = E as (Polynom-Ring F)-homomorphic Field;
reconsider f = hom_Ext_eval(a,F) as Homomorphism of (Polynom-Ring F),E1;
RAdj(F,{a}) = Image f by FIELD_6:44; then
B3: rng f = the carrier of RAdj(F,{a}) by RING_2:def 6;
RAdj(F,{a}) is Subring of FAdj(F,{a}) by FIELD_6:39; then
the carrier of RAdj(F,{a}) c= the carrier of FAdj(F,{a}) by C0SP1:def 3;
then o in the carrier of FAdj(F,{a}) by B2,B3;
hence o in dom g by FUNCT_2:def 1;
end; then
C1: dom h = dom hom_Ext_eval(a,F) by RELAT_1:27
.= the carrier of Polynom-Ring F by FUNCT_2:def 1;
CX: now let p be Polynomial of F;
[Ext_eval(p,a),Ext_eval(p,b)] in Phi(a,b);
hence g.Ext_eval(p,a) = Ext_eval(p,b) by B1,FUNCT_1:1;
end;
C0: now let x be object;
assume C2: x in dom h; then
reconsider p = x as Polynomial of F by POLYNOM3:def 10;
thus h.x = g.(hom_Ext_eval(a,F).p) by C2,FUNCT_1:12
.= g.Ext_eval(p,a) by ALGNUM_1:def 11
.= Ext_eval(p,b) by CX
.= hom_Ext_eval(b,F).x by ALGNUM_1:def 11;
end;
B2: g * hom_Ext_eval(a,F) = hom_Ext_eval(b,F) by C0,C1,FUNCT_2:def 1;
then reconsider h as Function of (Polynom-Ring F),E;
B7: ker g = {0.Fa} & g.(0.Fa) = 0.Fb
proof
B8: g is isomorphism by B1; then
reconsider Fb1 = Fb as Fa-monomorphic Field by RING_3:def 3;
reconsider g1 = g as Monomorphism of Fa,Fb1 by B8;
ker g1 = {0.Fa} by RING_2:12;
hence ker g = {0.Fa};
g1.(0.Fa) = 0.Fb by RING_2:6;
hence thesis;
end;
ker h = ker hom_Ext_eval(a,F)
proof
D: now let o be object;
assume o in ker h; then
o in {v where v is Element of Polynom-Ring F : h.v = 0.E}
by VECTSP10:def 9; then
consider p being Element of Polynom-Ring F such that
D1: o = p & h.p = 0.E;
D2: g.(hom_Ext_eval(a,F).p) = 0.E by C1,D1,FUNCT_1:12
.= 0.Fb by FIELD_6:def 6;
hom_Ext_eval(a,F).p is Element of Fa
proof
reconsider E1 = E as (Polynom-Ring F)-homomorphic Field;
reconsider f = hom_Ext_eval(a,F) as Homomorphism of (Polynom-Ring F),E1;
RAdj(F,{a}) = Image f by FIELD_6:44; then
B3: rng f = the carrier of RAdj(F,{a}) by RING_2:def 6;
RAdj(F,{a}) is Subring of FAdj(F,{a}) by FIELD_6:39; then
B4: the carrier of RAdj(F,{a}) c=
the carrier of FAdj(F,{a}) by C0SP1:def 3;
dom hom_Ext_eval(a,F) = the carrier of Polynom-Ring F by FUNCT_2:def 1;
hence thesis by B3,B4,FUNCT_1:3;
end; then
hom_Ext_eval(a,F).p in
{v where v is Element of Fa : g.v = 0.Fb} by D2;
then hom_Ext_eval(a,F).p in ker g by VECTSP10:def 9; then
hom_Ext_eval(a,F).p = 0.Fa by B7,TARSKI:def 1
.= 0.E by FIELD_6:def 6; then
p in {v where v is Element of Polynom-Ring F :
hom_Ext_eval(a,F).v = 0.E};
hence o in ker hom_Ext_eval(a,F) by D1,VECTSP10:def 9;
end;
now let o be object;
assume D1: o in ker hom_Ext_eval(a,F);
ker hom_Ext_eval(a,F) = {v where v is Element of Polynom-Ring F :
hom_Ext_eval(a,F).v = 0.E} by VECTSP10:def 9;
then consider p being Element of Polynom-Ring F such that
D2: o = p & hom_Ext_eval(a,F).p = 0.E by D1;
dom hom_Ext_eval(a,F) = the carrier of Polynom-Ring F by FUNCT_2:def 1;
then D3: h.p = g.(hom_Ext_eval(a,F).p) by FUNCT_1:13
.= g.(0.Fa) by D2,FIELD_6:def 6
.= 0.E by B7,FIELD_6:def 6;
ker h = {v where v is Element of Polynom-Ring F : h.v = 0.E}
by VECTSP10:def 9;
hence o in ker h by D2,D3;
end;
hence thesis by D,TARSKI:2;
end; then
ker hom_Ext_eval(a,F) = {MinPoly(b,F)}-Ideal by B2,FIELD_6:50;
hence MinPoly(a,F) = MinPoly(b,F) by FIELD_6:50;
end;
hence thesis by A;
end;
definition
let F1 be Field,
F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let E1 be FieldExtension of F1, E2 be FieldExtension of F2;
let a be Element of E1, b be Element of E2;
let p be irreducible Element of the carrier of Polynom-Ring F1;
assume AS:Ext_eval(p,a) = 0.E1 & Ext_eval((PolyHom h).p,b) = 0.E2;
func Psi(a,b,h,p) -> Function of FAdj(F1,{a}),FAdj(F2,{b}) means :psi:
for r being Element of the carrier of Polynom-Ring F1
holds it.Ext_eval(r,a) = Ext_eval((PolyHom h).r,b);
existence
proof
set C1 = the carrier of FAdj(F1,{a}), C2 = the carrier of FAdj(F2,{b});
reconsider 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})
= the set of all Ext_eval(p,a) where p is Polynomial of F1 by FIELD_6:45;
reconsider b as F2-algebraic Element of E2 by AS,FIELD_6:43;
H4: FAdj(F2,{b}) = RAdj(F2,{b}) by FIELD_6:56;
H5: the carrier of RAdj(F2,{b})
= the set of all Ext_eval(p,b) where p is Polynomial of F2 by FIELD_6:45;
defpred P[object,object] means
for r being Element of the carrier of Polynom-Ring F1
st $1 = Ext_eval(r,a) holds $2 = Ext_eval((PolyHom h).r,b);
H6: now let r be Element of the carrier of Polynom-Ring F1;
X: (PolyHom h).MinPoly(a,F1) = MinPoly(b,F2) by AS,x1000;
assume Ext_eval(r,a) = 0.E1; then
MinPoly(b,F2) divides (PolyHom h).r by X,uu0,FIELD_6:53;
hence Ext_eval((PolyHom h).r,b) = 0.E2 by FIELD_6:53;
end;
H7: now let r1,r2 be Element of the carrier of Polynom-Ring F1;
reconsider r1p = r1, r2p = r2 as Polynomial of F1;
reconsider r = r1 - r2 as Element of the carrier of Polynom-Ring F1;
reconsider rp = r as Polynomial of F1;
X: (PolyHom h).(r1-r2) = (PolyHom h).r1 - (PolyHom h).r2 by RING_2:8;
reconsider q = (PolyHom h).r,
q1 = (PolyHom h).r1, q2 = (PolyHom h).r2
as Polynomial of F2;
H9: -q2 = -(PolyHom h).r2 by DZIW;
H8: q1 - q2 = q by X,H9,POLYNOM3:def 10;
-r2p = -r2 by DZIW; then
H10: r1 - r2 = r1p - r2p by POLYNOM3:def 10;
assume Ext_eval(r1,a) = Ext_eval(r2,a); then
0.E1 = Ext_eval(r1p,a) - Ext_eval(r2p,a) by RLVECT_1:15
.= Ext_eval(r,a) by H10,FIELD_6:27; then
0.E2 = Ext_eval((PolyHom h).r,b) by H6
.= Ext_eval((PolyHom h).r1,b) - Ext_eval((PolyHom h).r2,b)
by H8,FIELD_6:27;
hence Ext_eval((PolyHom h).r1,b) = Ext_eval((PolyHom h).r2,b)
by RLVECT_1:21;
end;
A1: now let x be object;
assume x in C1;
then consider r being Polynomial of F1 such that
H8: x = Ext_eval(r,a) by H1,H2;
reconsider r as Element of the carrier of Polynom-Ring F1
by POLYNOM3:def 10;
thus ex y being object st y in C2 & P[x,y]
proof
take y = Ext_eval((PolyHom h).r,b);
thus y in C2 by H4,H5;
thus thesis by H7,H8;
end;
end;
consider f being Function of C1,C2 such that
A: for x being object st x in C1 holds P[x,f.x] from FUNCT_2:sch 1(A1);
now let r being Element of the carrier of Polynom-Ring F1;
Ext_eval(r,a) in C1 by H1,H2;
hence f.Ext_eval(r,a) = Ext_eval((PolyHom h).r,b) by A;
end;
hence thesis;
end;
uniqueness
proof
let F,G be Function of FAdj(F1,{a}),FAdj(F2,{b});
assume that
A1: for r being Element of the carrier of Polynom-Ring F1
holds F.Ext_eval(r,a) = Ext_eval((PolyHom h).r,b) and
A2: for r being Element of the carrier of Polynom-Ring F1
holds G.Ext_eval(r,a) = Ext_eval((PolyHom h).r,b);
now let o be object;
assume A3: o in the carrier of FAdj(F1,{a});
A4: FAdj(F1,{a}) = RAdj(F1,{a}) by AS,FIELD_6:43,FIELD_6:56;
the carrier of RAdj(F1,{a})
= the set of all Ext_eval(p,a) where p is Polynomial of F1 by FIELD_6:45;
then consider r being Polynomial of F1 such that
A5: o = Ext_eval(r,a) by A3,A4;
reconsider r as Element of the carrier of Polynom-Ring F1 by POLYNOM3:def 10;
F.Ext_eval(r,a) = Ext_eval((PolyHom h).r,b) by A1 .= G.Ext_eval(r,a) by A2;
hence F.o = G.o by A5;
end;
hence F = G;
end;
end;
theorem unique1:
for F1 being Field,
F2 being F1-isomorphic F1-homomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1, E2 being FieldExtension of F2
for a being Element of E1, 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 isomorphism
proof
let F1 be Field, F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let E1 be FieldExtension of F1, E2 being FieldExtension of F2;
let a be Element of E1, b being Element of E2;
let p be irreducible Element of the carrier of Polynom-Ring F1;
assume AS: Ext_eval(p,a) = 0.E1 & Ext_eval((PolyHom h).p,b) = 0.E2;
set f = Psi(a,b,h,p);
set C1 = the carrier of FAdj(F1,{a}), C2 = the carrier of FAdj(F2,{b});
reconsider 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})
= the set of all Ext_eval(p,a) where p is Polynomial of F1 by FIELD_6:45;
reconsider b as F2-algebraic Element of E2 by AS,FIELD_6:43;
now let x be Element of F1;
reconsider 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 f.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;
end;
hence f is h-extending;
set F1a = FAdj(F1,{a}), F2b = FAdj(F2,{b});
reconsider f as Function of F1a,F2b;
A: f.(1.F1a) = 1.F2b
proof
F1 is Subfield of F1a & F2 is Subfield of F2b by FIELD_6:36; then
A0: 1.F1a = 1.F1 & 1.F2b = 1.F2 by EC_PF_1:def 1;
A1: 1_.F1a = 1_.F1 by FIELD_4:14;
A2: (PolyHom h).(1_.F1a)
= (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.F2b)|F2b by A0,FIELD_6:23
.= 1_.F2b by RING_4:14;
reconsider r = 1_.F1a as Element of the carrier of Polynom-Ring F1
by A1,POLYNOM3:def 10;
thus f.(1.F1a) = 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.F2b by u1;
end;
B: now let x,y be Element of F1a;
x in the set of all Ext_eval(p,a) where p is Polynomial of F1 by H1,H2;
then consider r1 being Polynomial of F1 such that
B1: x = Ext_eval(r1,a);
y in the set of all Ext_eval(p,a) where p is Polynomial of F1 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;
end;
C: now let x,y be Element of F1a;
x in the set of all Ext_eval(p,a) where p is Polynomial of F1 by H1,H2;
then consider r1 being Polynomial of F1 such that
B1: x = Ext_eval(r1,a);
y in the set of all Ext_eval(p,a) where p is Polynomial of F1 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;
end;
D: f is onto
proof
E1: now let o be object;
assume E2: o in rng f;
rng f c= the carrier of F2b by RELAT_1:def 19;
hence o in the carrier of F2b by E2;
end;
I2: FAdj(F1,{a}) = RAdj(F1,{a}) & FAdj(F2,{b}) = RAdj(F2,{b})
by FIELD_6:56;
now let o be object;
assume o in the carrier of F2b;
then o in the set of all Ext_eval(p,b) where p is Polynomial of F2
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 as Element of the carrier of Polynom-Ring F1 by E3;
Ext_eval(ph,a) in the set of all Ext_eval(p,a)
where p is Polynomial of F1; then
Ext_eval(ph,a) in the carrier of F1a 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;
end;
hence thesis by E1,TARSKI:2;
end;
f is additive multiplicative unity-preserving by A,B,C;
hence thesis by D;
end;
theorem
for F being Field,
E being FieldExtension of F
for p being irreducible Element of the carrier of Polynom-Ring F
for a,b being Element of E
st a is_a_root_of p,E & b is_a_root_of p,E
holds FAdj(F,{a}),FAdj(F,{b}) are_isomorphic
proof
let F1 be Field, E1 be FieldExtension of F1;
let p be irreducible Element of the carrier of Polynom-Ring F1;
let a,b be Element of E1;
assume a is_a_root_of p,E1 & b is_a_root_of p,E1; then
B: Ext_eval(p,a) = 0.E1 & Ext_eval(p,b) = 0.E1 by FIELD_4:def 2; then
reconsider a1 = a as F1-algebraic Element of E1 by FIELD_6:43;
id F1 is isomorphism; then
reconsider F2 = F1 as F1-isomorphic Field by RING_3:def 4;
reconsider E2 = E1 as FieldExtension of F2;
reconsider h = id F1 as Isomorphism of F1,F2;
reconsider b1 = b as F2-algebraic Element of E2 by B,FIELD_6:43;
now let i be Element of NAT;
thus ((PolyHom h).p).i = h.(p.i) by FIELD_1:def 2 .= p.i;
end; then
(PolyHom h).p = p; then
Psi(a1,b1,h,p) is h-extending isomorphism by B,unique1;
hence thesis;
end;
unique20:
for F1,F2 being Field
st F1 is Subfield of F2 & F2 is Subfield of F1
for f being Function of F1,F2 st f = id F1 holds f is isomorphism
proof
let F1,F2 be Field;
assume AS1: F1 is Subfield of F2 & F2 is Subfield of F1;
let f be Function of F1,F2;
assume AS2: f = id F1;
the carrier of F1 c= the carrier of F2 &
the carrier of F2 c= the carrier of F1 by AS1,EC_PF_1:def 1; then
A: the carrier of F2 = the carrier of F1 by TARSKI:2;
C: the addF of F1
= (the addF of F2) || the carrier of F1 by AS1,EC_PF_1:def 1
.= the addF of F2 by A;
D: the multF of F1
= (the multF of F2) || the carrier of F1 by AS1,EC_PF_1:def 1
.= the multF of F2 by A;
f is additive multiplicative unity-preserving by C,D,AS2,AS1,EC_PF_1:def 1;
hence thesis by A,AS2;
end;
theorem unique2:
for F1 being Field,
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,
E2 being SplittingField of (PolyHom h).p
ex f being Function of E1,E2 st f is h-extending isomorphism
proof
let F1 be Field, F2 be F1-homomorphic F1-isomorphic Field;
let h be Isomorphism of F1,F2;
let p be non constant Element of the carrier of Polynom-Ring F1;
let E1 be SplittingField of p, E2 be SplittingField of (PolyHom h).p;
defpred P[Nat] means
for F1 being Field, 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,
E2 being SplittingField of (PolyHom h).p
st card( Roots(E1,p) \ the carrier of F1 ) = $1
ex f being Function of E1,E2 st f is h-extending isomorphism;
II: now let k be Nat;
assume IV: for j being Nat st j < k holds P[j];
per cases;
suppose S: k = 0;
now let F1 be Field, F2 be F1-homomorphic F1-isomorphic Field;
let h be Isomorphism of F1,F2;
let p be non constant Element of the carrier of Polynom-Ring F1;
let E1 be SplittingField of p, E2 be SplittingField of (PolyHom h).p;
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; 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;
now let a be Element of E1;
a in dom idF1; then
K4: (h*idF1).a = h.(idF1.a) by FUNCT_1:13 .= h.a;
reconsider aF = a as Element of F1 by A1;
reconsider ha = h.aF as Element of F2;
a in the carrier of F1 by A1; then
a in dom idF1 & idF1.a in dom h by FUNCT_2:def 1; then
a in dom(h*idF1) by FUNCT_1:11;
hence f.a = idF2.(h.a) by K4,FUNCT_1:13 .= ha .= h.a;
end;
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 isomorphism by K6,K5,K4;
end;
hence P[k] by S;
end;
suppose S: k > 0;
now let F1 be Field, F2 be F1-homomorphic F1-isomorphic Field;
let h be Isomorphism of F1,F2;
let p be non constant Element of the carrier of Polynom-Ring F1;
let E1 be SplittingField of p, E2 be SplittingField of (PolyHom h).p;
assume AS: card( Roots(E1,p) \ the carrier of F1 ) = k;
set a = the Element of Roots(E1,p) \ the carrier of F1;
Roots(E1,p) \ the carrier of F1 <> {} by AS,S; then
A1: a in Roots(E1,p) & not a in the carrier of F1 by XBOOLE_0:def 5; then
reconsider a 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 as F1-algebraic Element of E1;
set r = MinPoly(a,F1);
consider u being Polynomial of F1 such that
A3: r *' 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 = r * y by A3,POLYNOM3:def 10;
reconsider rh = (PolyHom h).r, yh = (PolyHom h).y as Polynomial of F2;
A6: (PolyHom h).p = (PolyHom h).r * (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: rhE2 is non constant by RING_4:def 4,RATFUNC1:def 2;
yh <> 0_.(F2) by A6; then
yhE2 <> 0_.(E2) by FIELD_4:12; then
A7a: yhE2 is non 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, 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(r,a) = 0.E1 by FIELD_6:51;
reconsider b as F2-algebraic Element of E2;
K: Psi(a,b,h,r) is h-extending isomorphism by K1,A22,unique1;
set F1a = FAdj(F1,{a});
reconsider F2b = FAdj(F2,{b}) as F1a-homomorphic
F1a-isomorphic Field by K,RING_2:def 4,RING_3:def 4;
reconsider g = Psi(a,b,h,r) as Isomorphism of F1a,F2b by K;
reconsider E1a = E1 as FieldExtension of F1a 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 F1a
by FIELD_4:10; then
reconsider f = p as Element of the carrier of Polynom-Ring F1a;
deg f = deg p & deg p > 0 by FIELD_4:20,RING_4:def 4; then
reconsider f as non constant
Element of the carrier of Polynom-Ring F1a by RING_4:def 4;
reconsider E1a as SplittingField of f by splift;
reconsider aa = a as Element of E1a;
(PolyHom g).f = (PolyHom h).p
proof
now let i be Nat;
thus ((PolyHom g).f).i = g.(f.i) by FIELD_1:def 2
.= h.(p.i) by K .= ((PolyHom h).p).i by FIELD_1:def 2;
end;
hence thesis;
end; then
reconsider 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 F1a by K7,K8,XBOOLE_0:def 5;
Roots(E1a,f) \ the carrier of F1a c= Roots(E1a,f) \ the carrier of F1
proof
now let o be object;
assume L: o in Roots(E1a,f) \ the carrier of F1a;
F1 is Subfield of F1a by FIELD_4:7; then
the carrier of F1 c= the carrier of F1a 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;
end;
hence thesis;
end;
then Roots(E1a,f) \ the carrier of F1a c<
Roots(E1a,f) \ the carrier of F1 by K4,K5,XBOOLE_0:def 8;
then L2: card(Roots(E1a,f) \ the carrier of F1a) <
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 isomorphism by IV,L2;
reconsider h1 as Function of E1,E2;
thus ex f being Function of E1,E2
st f is h-extending isomorphism by L1,K,e1a;
end;
hence P[k];
end;
end;
I: for k being Nat holds P[k] from NAT_1:sch 4(II);
consider n being Nat such that H: card( Roots(E1,p) \ the carrier of F1 ) = n;
thus thesis by H,I;
end;
unique3:
for F being Field
for p being non constant Element of the carrier of Polynom-Ring F
for E1,E2 being SplittingField of p
ex h being Function of E1,E2 st h is F-isomorphism
proof
let F1 be Field;
let p be non constant Element of the carrier of Polynom-Ring F1;
let E1,E be SplittingField of p;
id F1 is isomorphism; then
reconsider F2 = F1 as F1-homomorphic F1-isomorphic Field
by RING_2:def 4,RING_3:def 4;
reconsider h = id F1 as Isomorphism of F1,F2;
now let i be Element of NAT;
thus ((PolyHom h).p).i = h.(p.i) by FIELD_1:def 2 .= p.i;
end; then
(PolyHom h).p = p; then
reconsider E2 = E as SplittingField of (PolyHom h).p;
consider f being Function of E1,E2 such that
B: f is h-extending isomorphism by unique2;
reconsider f as Function of E1,E;
take f;
now let a be Element of F1;
thus f.a = h.a by B .= a;
end;
then f is F1-fixing;
hence thesis by B;
end;
theorem
for F being Field
for p being non constant Element of the carrier of Polynom-Ring F
for E1,E2 being SplittingField of p holds E1,E2 are_isomorphic_over F
proof
let F be Field;
let p be non constant Element of the carrier of Polynom-Ring F;
let E1,E2 be SplittingField of p;
consider f being Function of E1,E2 such that
A: f is F-isomorphism by unique3;
thus thesis by A;
end;