:: 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 b₁ being Field st
( b₁ is F -homomorphic & b₁ is F -monomorphic & b₁ 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 b₁ being R -isomorphic Ring holds
( b₁ is R -homomorphic & b₁ 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 b₃ -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 b₁ -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 b₁ -homomorphic b₁ -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 b₁ -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 b₁ -homomorphic b₁ -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 b₁ being Element of the carrier of (Polynom-Ring F2) st b₁ = (PolyHom h) . p holds
b₁ 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 b₁ being Element of the carrier of (Polynom-Ring F2) st b₁ = (PolyHom h) . p holds
not b₁ 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 b₁ being Element of the carrier of (Polynom-Ring F2) st b₁ = (PolyHom h) . p holds
b₁ 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 b₁ -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 b₁ -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 b₃ -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 b₃ -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 b₃ -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 b₃ -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 b₃ -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 b₁ being FieldExtension of F st
( p splits_in b₁ & ( for E being FieldExtension of F st p splits_in E & E is Subfield of b₁ holds
E == b₁ ) )

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 b₃ being FieldExtension of F holds
( b₃ is SplittingField of p iff ( p splits_in b₃ & ( for E being FieldExtension of F st p splits_in E & E is Subfield of b₃ holds
E == b₃ ) ) );

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 b₁ being SplittingField of p st b₁ 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 b₁ being SplittingField of p holds b₁ 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 b₁ being Function of R,R st b₁ 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 b₂ -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 b₂ -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 b₁ being Automorphism of S st b₁ 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 b₁ -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 b₁ -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 b₁ being Automorphism of S st b₁ is R -fixing holds
b₁ 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 b₁ being Automorphism of S st b₁ is id R -extending holds
b₁ 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 b₃ -extending FieldExtension of F1
for K2 being b₄ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -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 b₁ -homomorphic b₁ -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being b₁ -algebraic Element of E1
for b being b₂ -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 b₁ -homomorphic b₁ -isomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1
for E2 being FieldExtension of F2
for a being b₁ -algebraic Element of E1
for b being b₂ -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 b₁ -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 b₁ -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 b₁ being Function of (FAdj (F1,{a})),(FAdj (F2,{b})) st
for r being Element of the carrier of (Polynom-Ring F1) holds b₁ . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b)

proof end;

uniqueness
for b₁, b₂ being Function of (FAdj (F1,{a})),(FAdj (F2,{b})) st ( for r being Element of the carrier of (Polynom-Ring F1) holds b₁ . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) ) & ( for r being Element of the carrier of (Polynom-Ring F1) holds b₂ . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem psi defines Psi FIELD_8:def 10 :
for F1 being Field
for F2 being b₁ -homomorphic b₁ -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 b₉ being Function of (FAdj (F1,{a})),(FAdj (F2,{b})) holds
( b₉ = Psi (a,b,h,p) iff for r being Element of the carrier of (Polynom-Ring F1) holds b₉ . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) );

theorem unique1: :: FIELD_8:55

for F1 being Field
for F2 being b₁ -homomorphic b₁ -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 b₁ -homomorphic b₁ -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;