:: 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

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;

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

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;

ex b_{1} being Field st

( b_{1} is F -homomorphic & b_{1} is F -monomorphic & b_{1} is F -isomorphic )

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

( b

proof end;

registration

let R be Ring;

for b_{1} being R -isomorphic Ring holds

( b_{1} is R -homomorphic & b_{1} is R -monomorphic )
;

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

( b

registration

let R be Ring;

let S be R -homomorphic Ring;

coherence

Polynom-Ring S is Polynom-Ring R -homomorphic

end;
let S be R -homomorphic Ring;

coherence

Polynom-Ring S is Polynom-Ring R -homomorphic

proof end;

registration

let F1 be Field;

let F2 be F1 -homomorphic F1 -isomorphic Field;

coherence

Polynom-Ring F2 is Polynom-Ring F1 -isomorphic

end;
let F2 be F1 -homomorphic F1 -isomorphic Field;

coherence

Polynom-Ring F2 is Polynom-Ring F1 -isomorphic

proof 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

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_{3} -extending FieldExtension of F

for a being Element of U holds Ext_eval (q,a) = Ext_eval (p,a)

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

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)

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

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 )

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

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

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

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_{1} -homomorphic Ring

for h being Homomorphism of R,S

for a being Element of R holds (PolyHom h) . (a | R) = (h . a) | S

for S being b

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_{1} -homomorphic b_{1} -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 )

for F2 being b

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_{1} -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

for E being FieldExtension of F

for a being b

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_{1} -homomorphic b_{1} -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)

for F2 being b

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);

coherence

for b_{1} being Element of the carrier of (Polynom-Ring F2) st b_{1} = (PolyHom h) . p holds

b_{1} is constant

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

coherence

for b

b

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 non constant Element of the carrier of (Polynom-Ring F1);

coherence

for b_{1} being Element of the carrier of (Polynom-Ring F2) st b_{1} = (PolyHom h) . p holds

not b_{1} is constant

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

coherence

for b

not b

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 irreducible Element of the carrier of (Polynom-Ring F1);

coherence

for b_{1} being Element of the carrier of (Polynom-Ring F2) st b_{1} = (PolyHom h) . p holds

b_{1} is irreducible

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

coherence

for b

b

proof end;

lemma6a: for F1 being Field

for p being non constant Element of the carrier of (Polynom-Ring F1)

for F2 being b

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_{1} -isomorphic Field

for h being Isomorphism of F1,F2 holds

( p splits_in F1 iff (PolyHom h) . p splits_in F2 )

for p being non constant Element of the carrier of (Polynom-Ring F1)

for F2 being b

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_{3} -extending FieldExtension of F holds Roots (E,p) c= Roots (U,p)

for p being Element of the carrier of (Polynom-Ring F)

for E being FieldExtension of F

for U being b

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

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

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) ) )

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) ) )

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 :: 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;

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 )

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

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

( 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_{3} -extending FieldExtension of F st p splits_in E holds

( p splits_in U iff Roots (E,p) c= the carrier of U )

for p being non constant Element of the carrier of (Polynom-Ring F)

for U being FieldExtension of F

for E being b

( 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_{3} -extending FieldExtension of F st p splits_in E holds

( p splits_in U iff Roots (E,p) c= Roots (U,p) )

for p being non constant Element of the carrier of (Polynom-Ring F)

for U being FieldExtension of F

for E being b

( 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_{3} -extending FieldExtension of F st p splits_in E holds

( p splits_in U iff Roots (E,p) = Roots (U,p) )

for p being non constant Element of the carrier of (Polynom-Ring F)

for U being FieldExtension of F

for E being b

( 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)))

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);

ex b_{1} being FieldExtension of F st

( p splits_in b_{1} & ( for E being FieldExtension of F st p splits_in E & E is Subfield of b_{1} holds

E == b_{1} ) )

end;
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 ( p splits_in it & ( for E being FieldExtension of F st p splits_in E & E is Subfield of it holds

E == it ) );

ex b

( p splits_in b

E == b

proof 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_{3} being FieldExtension of F holds

( b_{3} is SplittingField of p iff ( p splits_in b_{3} & ( for E being FieldExtension of F st p splits_in E & E is Subfield of b_{3} holds

E == b_{3} ) ) );

for F being Field

for p being non constant Element of the carrier of (Polynom-Ring F)

for b

( b

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

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

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

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)))

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);

ex b_{1} being SplittingField of p st b_{1} is strict

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

proof end;

registration

let F be Field;

let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

for b_{1} being SplittingField of p holds b_{1} is F -finite

end;
let p be non constant Element of the carrier of (Polynom-Ring F);

coherence

for b

proof end;

registration

let R be Ring;

ex b_{1} being Function of R,R st b_{1} is isomorphism

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

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

:: 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 );

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 )

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_{2} -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)) )

for E1 being FieldExtension of F

for E2 being b

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_{2} -extending FieldExtension of F

for h being Function of E1,E2 st h is E -fixing holds

h is F -fixing

for E being FieldExtension of F

for E1, E2 being b

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;

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

( h is R -fixing & h is additive & h is multiplicative & h is unity-preserving );

:: 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 ) );

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 ) );

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 ) );

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;

ex b_{1} being Automorphism of S st b_{1} is R -fixing

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

proof 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_{1} -fixing Monomorphism of S

for a being Element of S holds

( a in Roots (S,p) iff h . a in Roots (S,p) )

for S being RingExtension of R

for p being Element of the carrier of (Polynom-Ring R)

for h being b

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_{1} -fixing Monomorphism of S holds h | (Roots (S,p)) is Permutation of (Roots (S,p))

for S being domRingExtension of R

for p being non zero Element of the carrier of (Polynom-Ring R)

for h being b

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;

end;
let S1 be RingExtension of R1;

let h1 be Function of R1,R2;

let h2 be Function of S1,S2;

:: 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 );

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 )

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;

for b_{1} being Automorphism of S st b_{1} is R -fixing holds

b_{1} is id R -extending
;

for b_{1} being Automorphism of S st b_{1} is id R -extending holds

b_{1} is R -fixing

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

b

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

b

proof 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_{3} -extending FieldExtension of F1

for K2 being b_{4} -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

for E1 being FieldExtension of F1

for E2 being FieldExtension of F2

for K1 being b

for K2 being b

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;

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

ex i being Function of E1,E2 st i is F -isomorphism ;

:: 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 );

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: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

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

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_{1} -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) )

for E1 being b

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;

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

ex g being Function of S1,S2 st

( g = h & g is R -isomorphism );

:: 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 ) );

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_{1} -algebraic Element of E holds

( 0. (FAdj (F,{a})) = Ext_eval ((0_. F),a) & 1. (FAdj (F,{a})) = Ext_eval ((1_. F),a) )

for E being FieldExtension of F

for a being b

( 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_{1} -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) )

for E being FieldExtension of F

for a being b

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_{1} -algebraic Element of E

for x being Element of F holds x = Ext_eval ((x | F),a)

for E being FieldExtension of F

for a being b

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}))

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}))

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_{1} -homomorphic b_{1} -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_{1} -algebraic Element of E1

for b being b_{2} -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)

for F2 being b

for h being Isomorphism of F1,F2

for E1 being FieldExtension of F1

for E2 being FieldExtension of F2

for a being b

for b being b

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_{1} -homomorphic b_{1} -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_{1} -algebraic Element of E1

for b being b_{2} -algebraic Element of E2 st Ext_eval (((PolyHom h) . (MinPoly (a,F1))),b) = 0. E2 holds

(PolyHom h) . (MinPoly (a,F1)) = MinPoly (b,F2)

for F2 being b

for h being Isomorphism of F1,F2

for E1 being FieldExtension of F1

for E2 being FieldExtension of F2

for a being b

for b being b

(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

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;

{ [(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}))

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

{ [(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;

:: deftheorem defines Phi FIELD_8:def 9 :

for F being Field

for E being FieldExtension of F

for a, b being b_{1} -algebraic Element of E holds Phi (a,b) = { [(Ext_eval (p,a)),(Ext_eval (p,b))] where p is Polynomial of F : verum } ;

for F being Field

for E being FieldExtension of F

for a, b being b

registration

let F be Field;

let E be FieldExtension of F;

let a, b be F -algebraic Element of E;

coherence

Phi (a,b) is quasi_total

end;
let E be FieldExtension of F;

let a, b be F -algebraic Element of E;

coherence

Phi (a,b) is quasi_total

proof end;

theorem :: FIELD_8:54

for F being Field

for E being FieldExtension of F

for a, b being b_{1} -algebraic Element of E holds

( Phi (a,b) is F -isomorphism iff MinPoly (a,F) = MinPoly (b,F) )

for E being FieldExtension of F

for a, b being b

( 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 ) ;

ex b_{1} being Function of (FAdj (F1,{a})),(FAdj (F2,{b})) st

for r being Element of the carrier of (Polynom-Ring F1) holds b_{1} . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b)

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

b_{1} = b_{2}

end;
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 for r being Element of the carrier of (Polynom-Ring F1) holds it . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b);

ex b

for r being Element of the carrier of (Polynom-Ring F1) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem psi defines Psi FIELD_8:def 10 :

for F1 being Field

for F2 being b_{1} -homomorphic b_{1} -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_{9} being Function of (FAdj (F1,{a})),(FAdj (F2,{b})) holds

( b_{9} = Psi (a,b,h,p) iff for r being Element of the carrier of (Polynom-Ring F1) holds b_{9} . (Ext_eval (r,a)) = Ext_eval (((PolyHom h) . r),b) );

for F1 being Field

for F2 being b

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

( b

theorem unique1: :: FIELD_8:55

for F1 being Field

for F2 being b_{1} -homomorphic b_{1} -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 )

for F2 being b

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

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_{1} -homomorphic b_{1} -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 )

for F2 being b

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

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;