:: Splitting Fields
:: by Christoph Schwarzweller
::
:: Received June 30, 2021
:: Copyright (c) 2021 Association of Mizar Users


theorem DZIW: :: FIELD_8:1
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 end;

poly0: for R being Ring
for 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 end;

theorem poly1: :: FIELD_8:2
for R being Ring
for p being Polynomial of R
for a being Element of R holds a * p = (a | R) *' p
proof end;

theorem hcon2: :: FIELD_8:3
for R being Ring
for a being Element of R holds LC (a | R) = a
proof end;

Th14: for A, B being Ring
for F being FinSequence of A
for G being FinSequence of B st A is Subring of B & F = G holds
In ((Product F),B) = Product G

proof end;

theorem u5: :: FIELD_8:4
for R being Ring
for 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 end;

registration
let F be Field;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable left_complementable right_complementable almost_left_cancelable almost_right_cancelable almost_left_invertible almost_right_invertible V116() V117() V118() V123() right-distributive left-distributive right_unital well-unital V140() left_unital unital V151() V153() domRing-like V251() V252() V253() V254() PID F -homomorphic K712() -homomorphic factorial F -monomorphic F -isomorphic for doubleLoopStr ;
existence
ex b1 being Field st
( b1 is F -homomorphic & b1 is F -monomorphic & b1 is F -isomorphic )
proof end;
end;

registration
let R be Ring;
cluster non empty right_complementable V116() V117() V118() well-unital V140() V151() R -isomorphic -> R -homomorphic R -monomorphic R -isomorphic for doubleLoopStr ;
coherence
for b1 being R -isomorphic Ring holds
( b1 is R -homomorphic & b1 is R -monomorphic )
;
end;

registration
let R be Ring;
let S be R -homomorphic Ring;
cluster Polynom-Ring S -> Polynom-Ring R -homomorphic ;
coherence
Polynom-Ring S is Polynom-Ring R -homomorphic
proof end;
end;

registration
let F1 be Field;
let F2 be F1 -homomorphic F1 -isomorphic Field;
cluster Polynom-Ring F2 -> Polynom-Ring F1 -isomorphic ;
coherence
Polynom-Ring F2 is Polynom-Ring F1 -isomorphic
proof end;
end;

theorem lemma2e: :: FIELD_8:5
for R being non degenerated Ring
for 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 end;

theorem lemma7b: :: FIELD_8:6
for F being Field
for p being Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for q being Element of the carrier of (Polynom-Ring E) st p = q holds
for U being b3 -extending FieldExtension of F
for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)
proof end;

theorem m4spl: :: FIELD_8:7
for R being Ring
for 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 holds
for T1 being RingExtension of S
for T2 being RingExtension of R st T1 = T2 holds
Roots (T2,p) = Roots (T1,q)
proof end;

theorem lemppoly: :: FIELD_8:8
for R being domRing
for F being non empty FinSequence of (Polynom-Ring R)
for p being Polynomial of R st p = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) holds
deg p = len F
proof end;

theorem lemppolspl2: :: FIELD_8:9
for F being Field
for 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 end;

lemppolspl: for F being Field
for p being Ppoly of F holds p splits_in F

proof 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 end;

theorem lemppolspl3a: :: FIELD_8:10
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 end;

theorem lemppolspl3: :: FIELD_8:11
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 end;

theorem lemppolspl1: :: FIELD_8:12
for F being Field
for p, q being Polynomial of F st p splits_in F & q splits_in F holds
p *' q splits_in F
proof end;

theorem hcon: :: FIELD_8:13
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for a being Element of R holds (PolyHom h) . (a | R) = (h . a) | S
proof end;

theorem uu0: :: FIELD_8:14
for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic 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 end;

theorem uu4: :: FIELD_8:15
for F being Field
for E being FieldExtension of F
for a being b1 -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 end;

theorem uu5: :: FIELD_8:16
for F1 being Field
for F2 being b1 -homomorphic b1 -monomorphic 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 end;

registration
let F1 be Field;
let F2 be F1 -homomorphic F1 -isomorphic 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
for b1 being Element of the carrier of (Polynom-Ring F2) st b1 = (PolyHom h) . p holds
b1 is constant
proof end;
end;

registration
let F1 be Field;
let 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);
cluster (PolyHom h) . p -> non constant for Element of the carrier of (Polynom-Ring F2);
coherence
for b1 being Element of the carrier of (Polynom-Ring F2) st b1 = (PolyHom h) . p holds
not b1 is constant
proof end;
end;

registration
let F1 be Field;
let F2 be F1 -homomorphic F1 -isomorphic 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
for b1 being Element of the carrier of (Polynom-Ring F2) st b1 = (PolyHom h) . p holds
b1 is irreducible
proof end;
end;

lemma6a: for F1 being Field
for p being non constant Element of the carrier of (Polynom-Ring F1)
for F2 being b1 -isomorphic Field
for h being Isomorphism of F1,F2 st p splits_in F1 holds
(PolyHom h) . p splits_in F2

proof end;

theorem :: FIELD_8:17
for F1 being Field
for p being non constant Element of the carrier of (Polynom-Ring F1)
for F2 being b1 -isomorphic Field
for h being Isomorphism of F1,F2 holds
( p splits_in F1 iff (PolyHom h) . p splits_in F2 )
proof end;

theorem lemma7: :: FIELD_8:18
for F being Field
for p being Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for U being b3 -extending FieldExtension of F holds Roots (E,p) c= Roots (U,p)
proof end;

lemmapp: for F being Field
for E being FieldExtension of F
for p being Ppoly of F holds p is Ppoly of E

proof end;

theorem :: FIELD_8:19
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for E being FieldExtension of F
for U being FieldExtension of E st p splits_in E holds
p splits_in U
proof end;

theorem lemma2y: :: FIELD_8:20
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 holds
ex a being Element of F st G . i = rpoly (1,a) ) holds
G is Factorization of Product G
proof end;

theorem lemma2z: :: FIELD_8:21
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 holds
ex a being Element of F st G1 . i = rpoly (1,a) ) & ( for i being Nat st i in dom G2 holds
ex a being Element of F st G2 . i = rpoly (1,a) ) & Product G1 = Product G2 holds
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 end;

theorem lemma2u: :: FIELD_8:22
for F being Field
for 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 holds
ex a being Element of F st G1 . i = rpoly (1,a) ) holds
for G2 being non empty FinSequence of (Polynom-Ring E) st ( for i being Nat st i in dom G2 holds
ex a being Element of E st G2 . i = rpoly (1,a) ) & Product G1 = Product G2 holds
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 end;

theorem u6: :: FIELD_8:23
for F being Field
for p being Ppoly of F
for a being Element of F holds LC (a * p) = a
proof end;

theorem :: FIELD_8:24
for F being Field
for E being FieldExtension of F
for p being Ppoly of F holds p is Ppoly of E by lemmapp;

theorem lemma2d: :: FIELD_8:25
for F being Field
for E being FieldExtension of F
for a being non zero Element of F
for 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 end;

theorem u8: :: FIELD_8:26
for F being Field
for 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 holds
ex a being Element of F st G . i = rpoly (1,a) ) holds
Product G is Ppoly of F
proof end;

lemma2: for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for U being FieldExtension of F
for E being b3 -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 end;

theorem lemma6: :: FIELD_8:27
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for U being FieldExtension of F
for E being b3 -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff Roots (E,p) c= the carrier of U )
proof end;

theorem lemma3: :: FIELD_8:28
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for U being FieldExtension of F
for E being b3 -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff Roots (E,p) c= Roots (U,p) )
proof end;

theorem :: FIELD_8:29
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for U being FieldExtension of F
for E being b3 -extending FieldExtension of F st p splits_in E holds
( p splits_in U iff Roots (E,p) = Roots (U,p) )
proof end;

theorem lemma5: :: FIELD_8:30
for F being Field
for 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 end;

definition
let F be Field;
let p be non constant Element of the carrier of (Polynom-Ring F);
mode SplittingField of p -> FieldExtension of F means :defspl: :: FIELD_8:def 1
( p splits_in it & ( for E being FieldExtension of F st p splits_in E & E is Subfield of it holds
E == it ) );
existence
ex b1 being FieldExtension of F st
( p splits_in b1 & ( for E being FieldExtension of F st p splits_in E & E is Subfield of b1 holds
E == b1 ) )
proof end;
end;

:: deftheorem defspl defines SplittingField FIELD_8:def 1 :
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for b3 being FieldExtension of F holds
( b3 is SplittingField of p iff ( p splits_in b3 & ( for E being FieldExtension of F st p splits_in E & E is Subfield of b3 holds
E == b3 ) ) );

theorem :: FIELD_8:31
for F being Field
for 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 end;

theorem spl0: :: FIELD_8:32
for F being Field
for 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 end;

theorem spl1: :: FIELD_8:33
for F being Field
for 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 end;

theorem XX: :: FIELD_8:34
for F being Field
for 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 end;

registration
let F be Field;
let p be non constant Element of the carrier of (Polynom-Ring F);
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable left_complementable right_complementable almost_left_cancelable almost_right_cancelable almost_left_invertible almost_right_invertible strict V116() V117() V118() V123() right-distributive left-distributive right_unital well-unital V140() left_unital unital V151() V153() domRing-like V251() V252() V253() V254() PID Polynom-Ring F -homomorphic factorial F -extending for SplittingField of p;
existence
ex b1 being SplittingField of p st b1 is strict
proof 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
for b1 being SplittingField of p holds b1 is F -finite
proof end;
end;

registration
let R be Ring;
cluster V1() V4( the carrier of R) V5( the carrier of R) Function-like non empty total quasi_total isomorphism for Element of bool [: the carrier of R, the carrier of R:];
existence
ex b1 being Function of R,R st b1 is isomorphism
proof end;
end;

definition
let R be Ring;
mode Homomorphism of R is additive unity-preserving multiplicative 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;
let S1 be RingExtension of R;
let h be Function of S1,S2;
attr h is R -fixing means :deffix: :: FIELD_8:def 2
for a being Element of R holds h . a = a;
end;

:: deftheorem deffix defines -fixing FIELD_8:def 2 :
for R, S2 being Ring
for S1 being RingExtension of R
for h being Function of S1,S2 holds
( h is R -fixing iff for a being Element of R holds h . a = a );

theorem e0: :: FIELD_8:35
for R, S2 being Ring
for S1 being RingExtension of R
for h being Function of S1,S2 holds
( h is R -fixing iff h | R = id R )
proof end;

theorem lintrans: :: FIELD_8:36
for F being Field
for E1 being FieldExtension of F
for E2 being b2 -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 end;

theorem :: FIELD_8:37
for F being Field
for E being FieldExtension of F
for E1, E2 being b2 -extending FieldExtension of F
for h being Function of E1,E2 st h is E -fixing holds
h is F -fixing
proof end;

definition
let R be Ring;
let S1, S2 be RingExtension of R;
let h be Function of S1,S2;
attr h is R -homomorphism means :: FIELD_8:def 3
( h is R -fixing & h is additive & h is multiplicative & h is unity-preserving );
attr h is R -monomorphism means :: FIELD_8:def 4
( h is R -fixing & h is monomorphism );
attr h is R -isomorphism means :deffixiso: :: FIELD_8:def 5
( h is R -fixing & h is isomorphism );
end;

:: deftheorem defines -homomorphism FIELD_8:def 3 :
for R being Ring
for S1, S2 being RingExtension of R
for h being Function of S1,S2 holds
( h is R -homomorphism iff ( h is R -fixing & h is additive & h is multiplicative & h is unity-preserving ) );

:: deftheorem defines -monomorphism FIELD_8:def 4 :
for R being Ring
for S1, S2 being RingExtension of R
for h being Function of S1,S2 holds
( h is R -monomorphism iff ( h is R -fixing & h is monomorphism ) );

:: deftheorem deffixiso defines -isomorphism FIELD_8:def 5 :
for R being Ring
for S1, S2 being RingExtension of R
for h being Function of S1,S2 holds
( h is R -isomorphism iff ( h is R -fixing & h is isomorphism ) );

registration
let R be Ring;
let S be RingExtension of R;
cluster V1() V4( the carrier of S) V5( the carrier of S) Function-like one-to-one non empty total quasi_total onto bijective additive unity-preserving RingHomomorphism RingMonomorphism RingEpimorphism RingIsomorphism endomorphism multiplicative R -fixing for Element of bool [: the carrier of S, the carrier of S:];
existence
ex b1 being Automorphism of S st b1 is R -fixing
proof end;
end;

theorem prm: :: FIELD_8:38
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of (Polynom-Ring R)
for h being b1 -fixing Monomorphism of S
for a being Element of S holds
( a in Roots (S,p) iff h . a in Roots (S,p) )
proof end;

theorem :: FIELD_8:39
for R being domRing
for S being domRingExtension of R
for p being non zero Element of the carrier of (Polynom-Ring R)
for h being b1 -fixing Monomorphism of S holds h | (Roots (S,p)) is Permutation of (Roots (S,p))
proof end;

definition
let R1, R2, S2 be Ring;
let S1 be RingExtension of R1;
let h1 be Function of R1,R2;
let h2 be Function of S1,S2;
attr h2 is h1 -extending means :: FIELD_8:def 6
for a being Element of R1 holds h2 . a = h1 . a;
end;

:: deftheorem defines -extending FIELD_8:def 6 :
for R1, R2, S2 being Ring
for S1 being RingExtension of R1
for h1 being Function of R1,R2
for h2 being Function of S1,S2 holds
( h2 is h1 -extending iff for a being Element of R1 holds h2 . a = h1 . a );

theorem e1: :: FIELD_8:40
for R1, R2, S2 being Ring
for S1 being RingExtension of R1
for h1 being Function of R1,R2
for h2 being Function of S1,S2 holds
( h2 is h1 -extending iff h2 | R1 = h1 )
proof end;

registration
let R be Ring;
let S be RingExtension of R;
cluster Function-like quasi_total RingIsomorphism R -fixing -> id R -extending for Element of bool [: the carrier of S, the carrier of S:];
coherence
for b1 being Automorphism of S st b1 is R -fixing holds
b1 is id R -extending
;
cluster Function-like quasi_total RingIsomorphism id R -extending -> R -fixing for Element of bool [: the carrier of S, the carrier of S:];
coherence
for b1 being Automorphism of S st b1 is id R -extending holds
b1 is R -fixing
proof end;
end;

theorem e1a: :: FIELD_8:41
for F1, F2 being Field
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for K1 being b3 -extending FieldExtension of F1
for K2 being b4 -extending FieldExtension of F2
for h1 being Function of F1,F2
for h2 being Function of E1,E2
for h3 being Function of K1,K2 st h2 is h1 -extending & h3 is h2 -extending holds
h3 is h1 -extending
proof end;

definition
let F be Field;
let E1, E2 be FieldExtension of F;
pred E1,E2 are_isomorphic_over F means :: FIELD_8:def 7
ex i being Function of E1,E2 st i is F -isomorphism ;
end;

:: deftheorem defines are_isomorphic_over FIELD_8:def 7 :
for F being Field
for E1, E2 being FieldExtension of F holds
( E1,E2 are_isomorphic_over F iff ex i being Function of E1,E2 st i is F -isomorphism );

theorem :: FIELD_8:42
for F being Field
for E being FieldExtension of F holds E,E are_isomorphic_over F
proof end;

theorem :: FIELD_8:43
for F being Field
for E1, E2 being FieldExtension of F st E1,E2 are_isomorphic_over F holds
E2,E1 are_isomorphic_over F
proof end;

theorem :: FIELD_8:44
for F being Field
for 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 end;

theorem :: FIELD_8:45
for F being Field
for E1 being b1 -finite FieldExtension of F
for E2 being FieldExtension of F st E1,E2 are_isomorphic_over F holds
( E2 is F -finite & deg (E1,F) = deg (E2,F) )
proof end;

definition
let R be Ring;
let S1, S2 be RingExtension of R;
let h be Relation of the carrier of S1, the carrier of S2;
attr h is R -isomorphism means :: FIELD_8:def 8
ex g being Function of S1,S2 st
( g = h & g is R -isomorphism );
end;

:: deftheorem defines -isomorphism FIELD_8:def 8 :
for R being Ring
for S1, S2 being RingExtension of R
for h being Relation of the carrier of S1, the carrier of S2 holds
( h is R -isomorphism iff ex g being Function of S1,S2 st
( g = h & g is R -isomorphism ) );

theorem u1: :: FIELD_8:46
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E holds
( 0. (FAdj (F,{a})) = Ext_eval ((0_. F),a) & 1. (FAdj (F,{a})) = Ext_eval ((1_. F),a) )
proof end;

theorem u2: :: FIELD_8:47
for F being Field
for E being FieldExtension of F
for a being b1 -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 end;

theorem u3: :: FIELD_8:48
for F being Field
for E being FieldExtension of F
for a being b1 -algebraic Element of E
for x being Element of F holds x = Ext_eval ((x | F),a)
proof end;

theorem u10: :: FIELD_8:49
for F being Field
for 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 end;

theorem :: FIELD_8:50
for F being Field
for 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 end;

theorem x1000: :: FIELD_8:51
for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being b1 -algebraic Element of E1
for b being b2 -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 end;

theorem :: FIELD_8:52
for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being b1 -algebraic Element of E1
for b being b2 -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 end;

theorem splift: :: FIELD_8:53
for F1 being Field
for p1 being non constant Element of the carrier of (Polynom-Ring F1)
for F2 being FieldExtension of F1
for 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 end;

definition
let F be Field;
let 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 :: FIELD_8:def 9
{ [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } ;
coherence
{ [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } is Relation of the carrier of (FAdj (F,{a})), the carrier of (FAdj (F,{b}))
proof end;
end;

:: deftheorem defines Phi FIELD_8:def 9 :
for F being Field
for E being FieldExtension of F
for a, b being b1 -algebraic Element of E holds Phi (a,b) = { [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } ;

registration
let F be Field;
let E be FieldExtension of F;
let a, b be F -algebraic Element of E;
cluster Phi (a,b) -> quasi_total ;
coherence
Phi (a,b) is quasi_total
proof end;
end;

theorem :: FIELD_8:54
for F being Field
for E being FieldExtension of F
for a, b being b1 -algebraic Element of E holds
( Phi (a,b) is F -isomorphism iff MinPoly (a,F) = MinPoly (b,F) )
proof end;

definition
let F1 be Field;
let F2 be F1 -homomorphic F1 -isomorphic Field;
let h be Isomorphism of F1,F2;
let E1 be FieldExtension of F1;
let E2 be FieldExtension of F2;
let a be Element of E1;
let 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: :: FIELD_8:def 10
for r being Element of the carrier of (Polynom-Ring F1) holds it . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b);
existence
ex b1 being Function of (FAdj (F1,{a})),(FAdj (F2,{b})) st
for r being Element of the carrier of (Polynom-Ring F1) holds b1 . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b)
proof end;
uniqueness
for b1, b2 being Function of (FAdj (F1,{a})),(FAdj (F2,{b})) st ( for r being Element of the carrier of (Polynom-Ring F1) holds b1 . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) ) & ( for r being Element of the carrier of (Polynom-Ring F1) holds b2 . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) ) holds
b1 = b2
proof end;
end;

:: deftheorem psi defines Psi FIELD_8:def 10 :
for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
for b9 being Function of (FAdj (F1,{a})),(FAdj (F2,{b})) holds
( b9 = Psi (a,b,h,p) iff for r being Element of the carrier of (Polynom-Ring F1) holds b9 . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) );

theorem unique1: :: FIELD_8:55
for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being Element of E1
for b being Element of E2
for p being irreducible Element of the carrier of (Polynom-Ring F1) st Ext_eval (p,a) = 0. E1 & Ext_eval (((PolyHom h) . p),b) = 0. E2 holds
( Psi (a,b,h,p) is h -extending & Psi (a,b,h,p) is isomorphism )
proof end;

theorem :: FIELD_8:56
for F being Field
for 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 end;

unique20: for F1, F2 being Field st F1 is Subfield of F2 & F2 is Subfield of F1 holds
for f being Function of F1,F2 st f = id F1 holds
f is isomorphism

proof end;

theorem unique2: :: FIELD_8:57
for F1 being Field
for F2 being b1 -homomorphic b1 -isomorphic Field
for h being Isomorphism of F1,F2
for p being non constant Element of the carrier of (Polynom-Ring F1)
for E1 being SplittingField of p
for E2 being SplittingField of (PolyHom h) . p ex f being Function of E1,E2 st
( f is h -extending & f is isomorphism )
proof 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 end;

theorem :: FIELD_8:58
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 end;