let F be polynomial_disjoint Field; :: thesis: for p being irreducible Element of the carrier of () ex E being FieldExtension of F st p is_with_roots_in E
let p be irreducible Element of the carrier of (); :: thesis: ex E being FieldExtension of F st p is_with_roots_in E
A1: now :: thesis: ( not F, Polynom-Ring p are_disjoint implies for a being Element of the carrier of F /\ the carrier of () holds contradiction )
assume not F, Polynom-Ring p are_disjoint ; :: thesis: for a being Element of the carrier of F /\ the carrier of () holds contradiction
then A2: ([#] F) /\ ([#] ()) <> {} by FIELD_2:def 1;
let a be Element of the carrier of F /\ the carrier of (); :: thesis: contradiction
A3: ( a in the carrier of F & a in the carrier of () ) by ;
the carrier of () = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;
then consider q being Polynomial of F such that
A4: ( a = q & deg q < deg p ) by A3;
a in the carrier of () by ;
then a in ([#] F) /\ ([#] ()) by ;
hence contradiction by FIELD_3:def 3; :: thesis: verum
end;
reconsider KroneckerIsop = () " as Isomorphism of (KroneckerField (F,p)),() by RING_3:73;
set h = KroneckerIsop * (emb p);
reconsider h = KroneckerIsop * (emb p) as Function of F,() by FUNCT_2:13;
( h is linear & h is one-to-one ) by RINGCAT1:1;
then reconsider h = h as Monomorphism of F,() ;
reconsider E = embField h as Field by ;
emb_iso h is onto by ;
then reconsider embisoh = () " as Function of (),E by FUNCT_2:25;
A5: ( emb_iso h is linear & emb_iso h is one-to-one & emb_iso h is onto ) by ;
then reconsider P = Polynom-Ring p as E -isomorphic Field by RING_3:def 4;
reconsider embisoh = embisoh as Isomorphism of P,E by ;
set iso = embisoh * KroneckerIsop;
set u = KrRoot p;
reconsider iso = embisoh * KroneckerIsop as Function of (KroneckerField (F,p)),E by FUNCT_2:13;
A6: iso is RingHomomorphism by RINGCAT1:1;
then reconsider E = E as KroneckerField (F,p) -homomorphic Field by RING_2:def 4;
reconsider iso = iso as Homomorphism of (KroneckerField (F,p)),E by A6;
KrRoot p is_a_root_of emb (p,p) by FIELD_1:42;
then A7: eval (((PolyHom iso) . (emb (p,p))),(iso . ())) = 0. E by ;
F is Subfield of E by FIELD_2:17;
then reconsider E = E as FieldExtension of F by Th4;
take E ; :: thesis:
reconsider a = iso . () as Element of E ;
(PolyHom iso) . (emb (p,p)) = p
proof
set g = (PolyHom iso) . (emb (p,p));
A8: KroneckerField (F,p) = () / () by FIELD_1:def 3;
A9: for a being Element of F holds h . a = a | F
proof
let a be Element of F; :: thesis: h . a = a | F
dom (emb p) = the carrier of F by FUNCT_2:def 1;
then A10: h . a = KroneckerIsop . ((emb p) . a) by FUNCT_1:13
.= KroneckerIsop . (Class ((EqRel ((),())),(a | F))) by FIELD_1:39 ;
A11: the carrier of () = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;
( deg (a | F) <= 0 & deg p > 0 ) by ;
then a | F in the carrier of () by A11;
then reconsider b1 = a | F as Element of () ;
A12: dom () = the carrier of () by FUNCT_2:def 1;
(KroneckerIso p) . b1 = Class ((EqRel ((),())),b1) by Def8;
hence h . a = a | F by ; :: thesis: verum
end;
A13: for a being Element of F holds iso . ((emb p) . a) = a
proof
let a be Element of F; :: thesis: iso . ((emb p) . a) = a
rng () = the carrier of (KroneckerField (F,p)) by FUNCT_2:def 3;
then A14: dom KroneckerIsop = the carrier of (KroneckerField (F,p)) by FUNCT_1:33;
reconsider b = a | F as Element of the carrier of () by POLYNOM3:def 10;
A15: the carrier of () = { q where q is Polynomial of F : deg q < deg p } by RING_4:def 8;
( deg (a | F) <= 0 & deg p > 0 ) by ;
then a | F in the carrier of () by A15;
then reconsider b1 = a | F as Element of () ;
reconsider v = Class ((EqRel ((),())),b) as Element of (KroneckerField (F,p)) by ;
A16: (KroneckerIso p) . b1 = Class ((EqRel ((),())),b1) by Def8;
A17: dom () = the carrier of () by FUNCT_2:def 1;
the carrier of () = carr h by FIELD_2:def 7
.= (([#] ()) \ (rng h)) \/ ([#] F) by FIELD_2:def 2 ;
then reconsider a1 = a as Element of () by XBOOLE_0:def 3;
a in F ;
then A18: () . a1 = h . a by FIELD_2:def 8
.= a | F by A9 ;
A19: dom () = the carrier of () by FUNCT_2:def 1;
thus iso . ((emb p) . a) = iso . v by FIELD_1:39
.= embisoh . (KroneckerIsop . v) by
.= embisoh . b by
.= a by ; :: thesis: verum
end;
now :: thesis: for x being object st x in NAT holds
((PolyHom iso) . (emb (p,p))) . x = p . x
let x be object ; :: thesis: ( x in NAT implies ((PolyHom iso) . (emb (p,p))) . x = p . x )
assume x in NAT ; :: thesis: ((PolyHom iso) . (emb (p,p))) . x = p . x
then reconsider i = x as Element of NAT ;
((PolyHom iso) . (emb (p,p))) . i = iso . ((emb (p,p)) . i) by FIELD_1:def 2
.= iso . (Class ((EqRel ((),())),((p . i) | F))) by FIELD_1:40
.= iso . ((emb p) . (p . i)) by FIELD_1:39 ;
hence ((PolyHom iso) . (emb (p,p))) . x = p . x by A13; :: thesis: verum
end;
hence (PolyHom iso) . (emb (p,p)) = p ; :: thesis: verum
end;
then a is_a_root_of p,E by ;
hence p is_with_roots_in E ; :: thesis: verum