let F be polynomial_disjoint Field; for p being irreducible Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st p is_with_roots_in E
let p be irreducible Element of the carrier of (Polynom-Ring F); ex E being FieldExtension of F st p is_with_roots_in E
reconsider KroneckerIsop = (KroneckerIso p) " as Isomorphism of (KroneckerField (F,p)),(Polynom-Ring p) by RING_3:73;
set h = KroneckerIsop * (emb p);
reconsider h = KroneckerIsop * (emb p) as Function of F,(Polynom-Ring p) by FUNCT_2:13;
( h is linear & h is one-to-one )
by RINGCAT1:1;
then reconsider h = h as Monomorphism of F,(Polynom-Ring p) ;
reconsider E = embField h as Field by A1, FIELD_2:12;
emb_iso h is onto
by A1, FIELD_2:15;
then reconsider embisoh = (emb_iso h) " as Function of (Polynom-Ring p),E by FUNCT_2:25;
A5:
( emb_iso h is linear & emb_iso h is one-to-one & emb_iso h is onto )
by A1, FIELD_2:13, FIELD_2:14, FIELD_2:15;
then reconsider P = Polynom-Ring p as E -isomorphic Field by RING_3:def 4;
reconsider embisoh = embisoh as Isomorphism of P,E by A5, RING_3:73;
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 . (KrRoot p))) = 0. E
by FIELD_1:33, POLYNOM5:def 7;
F is Subfield of E
by FIELD_2:17;
then reconsider E = E as FieldExtension of F by Th4;
take
E
; p is_with_roots_in E
reconsider a = iso . (KrRoot p) as Element of E ;
(PolyHom iso) . (emb (p,p)) = p
proof
set g =
(PolyHom iso) . (emb (p,p));
A8:
KroneckerField (
F,
p)
= (Polynom-Ring F) / ({p} -Ideal)
by FIELD_1:def 3;
A9:
for
a being
Element of
F holds
h . a = a | F
A13:
for
a being
Element of
F holds
iso . ((emb p) . a) = a
proof
let a be
Element of
F;
iso . ((emb p) . a) = a
rng (KroneckerIso p) = 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
(Polynom-Ring F) by POLYNOM3:def 10;
A15:
the
carrier of
(Polynom-Ring p) = { q where q is Polynomial of F : deg q < deg p }
by RING_4:def 8;
(
deg (a | F) <= 0 &
deg p > 0 )
by RATFUNC1:def 2, RING_4:def 4;
then
a | F in the
carrier of
(Polynom-Ring p)
by A15;
then reconsider b1 =
a | F as
Element of
(Polynom-Ring p) ;
reconsider v =
Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
b) as
Element of
(KroneckerField (F,p)) by A8, RING_1:12;
A16:
(KroneckerIso p) . b1 = Class (
(EqRel ((Polynom-Ring F),({p} -Ideal))),
b1)
by Def8;
A17:
dom (KroneckerIso p) = the
carrier of
(Polynom-Ring p)
by FUNCT_2:def 1;
the
carrier of
(embField h) =
carr h
by FIELD_2:def 7
.=
(([#] (Polynom-Ring p)) \ (rng h)) \/ ([#] F)
by FIELD_2:def 2
;
then reconsider a1 =
a as
Element of
(embField h) by XBOOLE_0:def 3;
a in F
;
then A18:
(emb_iso h) . a1 =
h . a
by FIELD_2:def 8
.=
a | F
by A9
;
A19:
dom (emb_iso h) = the
carrier of
(embField h)
by FUNCT_2:def 1;
thus iso . ((emb p) . a) =
iso . v
by FIELD_1:39
.=
embisoh . (KroneckerIsop . v)
by A14, FUNCT_1:13
.=
embisoh . b
by A16, A17, FUNCT_1:32
.=
a
by A18, A19, FUNCT_1:32
;
verum
end;
hence
(PolyHom iso) . (emb (p,p)) = p
;
verum
end;
then
a is_a_root_of p,E
by A7, Th15;
hence
p is_with_roots_in E
; verum