:: Artin's Theorem towards the Existence of Algebraic Closures
:: by Christoph Schwarzweller
::
:: Received September 30, 2022
:: Copyright (c) 2022-2025 Association of Mizar Users

:: Preliminaries about bags and multivariate polynomials

theorem Th13e: :: FIELD_11:1

for n, m being Ordinal
for b1, b2 being bag of n st support b1 = {m} & support b2 = {m} holds
( b1 <=' b2 iff b1 . m <= b2 . m )

proof end;

theorem Th13h: :: FIELD_11:2

for n, m being Ordinal
for b1, b2 being bag of n st support b1 = {m} holds
( b2 divides b1 iff ( b2 = EmptyBag n or ( support b2 = {m} & b2 . m <= b1 . m ) ) )

proof end;

theorem Th13f: :: FIELD_11:3

for F being Field
for m, n being Ordinal
for b being bag of n st support b = {m} holds
( len (divisors b) = (b . m) + 1 & ( for k being Nat
for S being finite Subset of n st S = {m} & k in dom (divisors b) holds
(divisors b) . k = (S,(k -' 1)) -bag ) )

proof end;

registration

let n be Ordinal;
let L be non degenerated right_complementable right_unital distributive add-associative right_zeroed doubleLoopStr ;

cluster Polynom-Ring (n,L) -> non degenerated ;

coherence
not Polynom-Ring (n,L) is degenerated

proof end;

end;

theorem ringext: :: FIELD_11:4

for R being non degenerated comRing
for S being comRingExtension of R
for n being Ordinal holds Polynom-Ring (n,S) is comRingExtension of Polynom-Ring (n,R)

proof end;

definition

let R be non degenerated Ring;
let n be Ordinal;
let p be Polynomial of n,R;

func Leading-Term p -> bag of n equals :defLT: :: FIELD_11:def 1
(SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) if p <> 0_ (n,R)
otherwise EmptyBag n;

consistency
for b₁ being bag of n holds verum ;
coherence
( ( p <> 0_ (n,R) implies (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) is bag of n ) & ( not p <> 0_ (n,R) implies EmptyBag n is bag of n ) )

proof end;

end;

:: deftheorem defLT defines Leading-Term FIELD_11:def 1 :
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds
( ( p <> 0_ (n,R) implies Leading-Term p = (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) ) & ( not p <> 0_ (n,R) implies Leading-Term p = EmptyBag n ) );

definition

let R be non degenerated Ring;
let n be Ordinal;
let p be Polynomial of n,R;

func Leading-Coefficient p -> Element of R equals :: FIELD_11:def 2
p . (Leading-Term p);

coherence
p . (Leading-Term p) is Element of R ;

end;

:: deftheorem defines Leading-Coefficient FIELD_11:def 2 :
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds Leading-Coefficient p = p . (Leading-Term p);

definition

let R be non degenerated Ring;
let n be Ordinal;
let p be Polynomial of n,R;

func Leading-Monomial p -> Monomial of n,R equals :: FIELD_11:def 3
Monom ((Leading-Coefficient p),(Leading-Term p));

coherence
Monom ((Leading-Coefficient p),(Leading-Term p)) is Monomial of n,R ;

end;

:: deftheorem defines Leading-Monomial FIELD_11:def 3 :
for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds Leading-Monomial p = Monom ((Leading-Coefficient p),(Leading-Term p));

notation

let R be non degenerated Ring;
let n be Ordinal;
let p be Polynomial of n,R;
synonym LC p for Leading-Coefficient p;
synonym Lt p for Leading-Term p;
synonym LM p for Leading-Monomial p;

end;

theorem YY: :: FIELD_11:5

for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds
( p = 0_ (n,R) iff Support p = {} )

proof end;

theorem Y0: :: FIELD_11:6

for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds
( LC p = 0. R iff p = 0_ (n,R) )

proof end;

theorem LT1: :: FIELD_11:7

for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R
for b being bag of n st b in Support p holds
( b = Lt p iff for b1 being bag of n st b1 in Support p holds
b1 <=' b )

proof end;

theorem YZ: :: FIELD_11:8

for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds Support (LM p) c= Support p

proof end;

theorem Th14x: :: FIELD_11:9

for F being Field
for n being Ordinal
for p being Monomial of n,F holds
( LC p = coefficient p & Lt p = term p )

proof end;

theorem Z2: :: FIELD_11:10

for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds
( Support (LM p) = {} or Support (LM p) = {(Lt p)} )

proof end;

lemY: for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds (LM p) . (Lt p) = LC p

proof end;

theorem Z2a: :: FIELD_11:11

for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds
( LM p = 0_ (n,R) iff p = 0_ (n,R) )

proof end;

W2: for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R
for b being bag of n st b <> Lt p holds
(LM p) . b = 0. R

proof end;

theorem :: FIELD_11:12

for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds
( (LM p) . (Lt p) = LC p & ( for b being bag of n st b <> Lt p holds
(LM p) . b = 0. R ) ) by lemY, W2;

lemZ: for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds Lt (LM p) = Lt p

proof end;

theorem :: FIELD_11:13

for R being non degenerated Ring
for n being Ordinal
for p being Polynomial of n,R holds
( Lt (LM p) = Lt p & LC (LM p) = LC p )

proof end;

theorem T4a: :: FIELD_11:14

for n being Ordinal
for R being non degenerated Ring
for a, b being Element of R holds (a | (n,R)) + (b | (n,R)) = (a + b) | (n,R)

proof end;

theorem T4: :: FIELD_11:15

for n being Ordinal
for R being non degenerated Ring
for a, b being Element of R holds (a | (n,R)) *' (b | (n,R)) = (a * b) | (n,R)

proof end;

:: Extended evaluation of multivariate polynomials

definition

let R, S be non degenerated comRing;
let n be Ordinal;
let p be Polynomial of n,R;
let x be Function of n,S;

func Ext_eval (p,x) -> Element of S means :defeval: :: FIELD_11:def 4
ex y being FinSequence of S st
( it = Sum y & len y = len (SgmX ((BagOrder n),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len y holds
y . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) );

existence
ex b₁ being Element of S ex y being FinSequence of S st
( b₁ = Sum y & len y = len (SgmX ((BagOrder n),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len y holds
y . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) )

proof end;

uniqueness
for b₁, b₂ being Element of S st ex y being FinSequence of S st
( b₁ = Sum y & len y = len (SgmX ((BagOrder n),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len y holds
y . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) & ex y being FinSequence of S st
( b₂ = Sum y & len y = len (SgmX ((BagOrder n),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len y holds
y . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defeval defines Ext_eval FIELD_11:def 4 :
for R, S being non degenerated comRing
for n being Ordinal
for p being Polynomial of n,R
for x being Function of n,S
for b₆ being Element of S holds
( b₆ = Ext_eval (p,x) iff ex y being FinSequence of S st
( b₆ = Sum y & len y = len (SgmX ((BagOrder n),(Support p))) & ( for i being Element of NAT st 1 <= i & i <= len y holds
y . i = (In (((p * (SgmX ((BagOrder n),(Support p)))) . i),S)) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) );

theorem ev0: :: FIELD_11:16

for R, S being non degenerated comRing
for n being Ordinal
for x being Function of n,S holds Ext_eval ((0_ (n,R)),x) = 0. S

proof end;

theorem eval1: :: FIELD_11:17

for R, S being non degenerated comRing
for n being Ordinal
for x being Function of n,S st R is Subring of S holds
Ext_eval ((1_ (n,R)),x) = 1. S

proof end;

Lm6: for n being Ordinal
for R, S being non degenerated comRing
for p, q being Polynomial of n,R
for x being Function of n,S
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b1 being bag of n st b1 <> b holds
q . b1 = p . b1 ) holds
Ext_eval (q,x) = (Ext_eval (p,x)) + ((In ((q . b),S)) * (eval (b,x)))

proof end;

theorem Th11: :: FIELD_11:18

for R, S being non degenerated comRing
for n being Ordinal
for p being Polynomial of n,R
for b being bag of n st Support p = {b} holds
for x being Function of n,S holds Ext_eval (p,x) = (In ((p . b),S)) * (eval (b,x))

proof end;

Lm5: for A, B being Ring st A is Subring of B holds
( In ((0. A),B) = 0. B & In ((1. A),B) = 1. B )

proof end;

Th12: for A, B being Ring
for x1 being Element of A st A is Subring of B holds
In ((- x1),B) = - (In (x1,B))

proof end;

Lm7: for n being Ordinal
for R, S being non degenerated comRing st R is Subring of S holds
for p being Polynomial of n,R st ex b being bag of n st Support p = {b} holds
for q being Polynomial of n,R
for x being Function of n,S holds Ext_eval ((p + q),x) = (Ext_eval (p,x)) + (Ext_eval (q,x))

proof end;

theorem evalpl: :: FIELD_11:19

for R, S being non degenerated comRing
for n being Ordinal
for p, q being Polynomial of n,R
for x being Function of n,S st R is Subring of S holds
Ext_eval ((p + q),x) = (Ext_eval (p,x)) + (Ext_eval (q,x))

proof end;

Lm3: for X being set
for S being Subset of X
for R being Order of X st R is being_linear-order holds
R linearly_orders S

proof end;

Lm8: for R, S being non degenerated comRing st R is Subring of S holds
for n being Ordinal
for p, q being Polynomial of n,R
for b1, b2 being bag of n st Support p = {b1} & Support q = {b2} holds
for x being Function of n,S holds Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))

proof end;

Lm9: for R, S being non degenerated comRing st R is Subring of S holds
for n being Ordinal
for q being Polynomial of n,R st ex b being bag of n st Support q = {b} holds
for p being Polynomial of n,R
for x being Function of n,S holds Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))

proof end;

theorem evalti: :: FIELD_11:20

for R, S being non degenerated comRing
for n being Ordinal
for p, q being Polynomial of n,R
for x being Function of n,S st R is Subring of S holds
Ext_eval ((p *' q),x) = (Ext_eval (p,x)) * (Ext_eval (q,x))

proof end;

ideal2: for R being non degenerated comRing
for S being comRingExtension of R
for n being Ordinal
for P being non empty Subset of (Polynom-Ring (n,R))
for F being LeftLinearCombination of P
for p being Polynomial of n,R st p = Sum F holds
for x being Function of n,S ex G being FinSequence of S st
( len G = len F & Ext_eval (p,x) = Sum G & ( for i being set st i in dom G holds
for q being Polynomial of n,R st q = F . i holds
G . i = Ext_eval (q,x) ) )

proof end;

:: "... To each polynomial f in K[X] we associate a letter X_f and we let
:: S be the set of all such letters X_f (so that S is in bijection with the
:: set of all polynomials in K[X] of degree >= 1). We form the polynomial
:: ring K[S], ..."
:: First a bijection between the set of all polynomials in K[X] of degree >= 1
:: and S = n, where n = card {p in K[X] | deg p > = 1}, is shown to exist.

definition

let F be Field;

func nonConstantPolys F -> non empty Subset of the carrier of (Polynom-Ring F) equals :: FIELD_11:def 5
{ p where p is non constant Element of the carrier of (Polynom-Ring F) : verum } ;

coherence
{ p where p is non constant Element of the carrier of (Polynom-Ring F) : verum } is non empty Subset of the carrier of (Polynom-Ring F)

proof end;

end;

:: deftheorem defines nonConstantPolys FIELD_11:def 5 :
for F being Field holds nonConstantPolys F = { p where p is non constant Element of the carrier of (Polynom-Ring F) : verum } ;

registration

let F be Field;

cluster card (nonConstantPolys F) -> non empty ;

coherence
not card (nonConstantPolys F) is empty ;

end;

registration

let F be Field;

cluster Relation-like nonConstantPolys F -defined card (nonConstantPolys F) -valued Function-like non empty total quasi_total bijective for Element of bool [:(nonConstantPolys F),(card (nonConstantPolys F)):];

existence
ex b₁ being Function of (nonConstantPolys F),(card (nonConstantPolys F)) st b₁ is bijective

proof end;

end;

definition

let F be Field;
let g be Function of (nonConstantPolys F),(card (nonConstantPolys F));
let p be non constant Element of the carrier of (Polynom-Ring F);
:: original: .
redefine func g . p -> Ordinal;
coherence
g . p is Ordinal

proof end;

end;

:: Translation of polynomials from K[X] into K[X1,X2,...] = K[n]:
:: For p in K[X] we have Poly(m,p) = p(Xm) where m is the m-th variable of
:: n = card { p in K[X] | deg p >= 1 }
:: --- if not m in n, then Poly(m,p) is the constant polynomial given by p(0)

definition

let F be Field;
let m be Ordinal;
let p be Polynomial of F;

func Poly (m,p) -> Polynomial of (card (nonConstantPolys F)),F means :defPg: :: FIELD_11:def 6
( it . (EmptyBag (card (nonConstantPolys F))) = p . 0 & ( for b being bag of card (nonConstantPolys F) st support b = {m} holds
it . b = p . (b . m) ) & ( for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
it . b = 0. F ) );

existence
ex b₁ being Polynomial of (card (nonConstantPolys F)),F st
( b₁ . (EmptyBag (card (nonConstantPolys F))) = p . 0 & ( for b being bag of card (nonConstantPolys F) st support b = {m} holds
b₁ . b = p . (b . m) ) & ( for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
b₁ . b = 0. F ) )

proof end;

uniqueness
for b₁, b₂ being Polynomial of (card (nonConstantPolys F)),F st b₁ . (EmptyBag (card (nonConstantPolys F))) = p . 0 & ( for b being bag of card (nonConstantPolys F) st support b = {m} holds
b₁ . b = p . (b . m) ) & ( for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
b₁ . b = 0. F ) & b₂ . (EmptyBag (card (nonConstantPolys F))) = p . 0 & ( for b being bag of card (nonConstantPolys F) st support b = {m} holds
b₂ . b = p . (b . m) ) & ( for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
b₂ . b = 0. F ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defPg defines Poly FIELD_11:def 6 :
for F being Field
for m being Ordinal
for p being Polynomial of F
for b₄ being Polynomial of (card (nonConstantPolys F)),F holds
( b₄ = Poly (m,p) iff ( b₄ . (EmptyBag (card (nonConstantPolys F))) = p . 0 & ( for b being bag of card (nonConstantPolys F) st support b = {m} holds
b₄ . b = p . (b . m) ) & ( for b being bag of card (nonConstantPolys F) st support b <> {} & support b <> {m} holds
b₄ . b = 0. F ) ) );

definition

let F be Field;
let g be bijective Function of (nonConstantPolys F),(card (nonConstantPolys F));

func nonConstantPolys (g,F) -> non empty Subset of (Polynom-Ring ((card (nonConstantPolys F)),F)) equals :: FIELD_11:def 7
{ (Poly ((g . p),p)) where p is non constant Element of the carrier of (Polynom-Ring F) : verum } ;

coherence
{ (Poly ((g . p),p)) where p is non constant Element of the carrier of (Polynom-Ring F) : verum } is non empty Subset of (Polynom-Ring ((card (nonConstantPolys F)),F))

proof end;

end;

:: deftheorem defines nonConstantPolys FIELD_11:def 7 :
for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F)) holds nonConstantPolys (g,F) = { (Poly ((g . p),p)) where p is non constant Element of the carrier of (Polynom-Ring F) : verum } ;

registration

let F be Field;
let m be Ordinal;
let p be Polynomial of F;

cluster Poly (m,(LM p)) -> monomial-like ;

coherence
Poly (m,(LM p)) is monomial-like

proof end;

end;

Th14c: for F being Field
for m being Ordinal
for p being Polynomial of F holds Support (Poly (m,p)) c= {(EmptyBag (card (nonConstantPolys F)))} \/ { b where b is bag of card (nonConstantPolys F) : support b = {m} }

proof end;

Th28: for L being non empty ZeroStr
for a being Element of L holds
( (a | L) . 0 = a & ( for n being Nat st n <> 0 holds
(a | L) . n = 0. L ) )

proof end;

theorem pZero: :: FIELD_11:21

for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F holds
( Poly (m,p) = 0_ ((card (nonConstantPolys F)),F) iff p = 0_. F )

proof end;

theorem XYZbb: :: FIELD_11:22

for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F
for a being Element of F holds
( Poly (m,p) = a | ((card (nonConstantPolys F)),F) iff p = a | F )

proof end;

theorem bij3a: :: FIELD_11:23

for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being non zero Element of the carrier of (Polynom-Ring F) holds
( Support (Poly (m,p)) = {(EmptyBag (card (nonConstantPolys F)))} iff p is constant )

proof end;

lemSet: for o being object
for S being set holds
( not S c= {o} or S = {} or S = {o} )

proof end;

theorem bij3: :: FIELD_11:24

for F being Field
for m1, m2 being Ordinal st m1 in card (nonConstantPolys F) & m2 in card (nonConstantPolys F) holds
for p1, p2 being non constant Polynomial of F st Poly (m1,p1) = Poly (m2,p2) holds
( m1 = m2 & p1 = p2 )

proof end;

theorem ZZZ: :: FIELD_11:25

for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being constant Polynomial of F holds
( Lt (Poly (m,p)) = EmptyBag (card (nonConstantPolys F)) & LC (Poly (m,p)) = p . 0 )

proof end;

theorem XYZaa: :: FIELD_11:26

for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being non constant Polynomial of F holds
( (Lt (Poly (m,p))) . m = deg p & ( for o being Ordinal st o <> m holds
(Lt (Poly (m,p))) . o = 0 ) )

proof end;

XYZa: for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being non constant Polynomial of F holds
( support (Lt (Poly (m,p))) = {m} & (Lt (Poly (m,p))) . m = deg p )

proof end;

Th14b: for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F holds LC (Poly (m,p)) = LC p

proof end;

theorem Th14z: :: FIELD_11:27

for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F holds
( LC (Poly (m,(LM p))) = LC (Poly (m,p)) & Lt (Poly (m,(LM p))) = Lt (Poly (m,p)) )

proof end;

theorem Th14y: :: FIELD_11:28

for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F holds Poly (m,(LM p)) = Monom ((LC (Poly (m,p))),(Lt (Poly (m,p))))

proof end;

theorem :: FIELD_11:29

for F being Field
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F holds LM (Poly (m,p)) = Poly (m,(LM p)) by Th14y;

lemKr3: for F being Field
for m being Ordinal
for a being Element of F holds Poly (m,(a | F)) = a | ((card (nonConstantPolys F)),F)

proof end;

theorem Th14: :: FIELD_11:30

for F being Field
for m being Ordinal
for p, q being Polynomial of F holds Poly (m,(p + q)) = (Poly (m,p)) + (Poly (m,q))

proof end;

theorem Th14xy: :: FIELD_11:31

for F being Field
for m being Ordinal
for p being Polynomial of F holds Poly (m,(- p)) = - (Poly (m,p))

proof end;

theorem Th11: :: FIELD_11:32

for F being Field
for a being non zero Element of F
for i being Nat
for m being Ordinal st m in card (nonConstantPolys F) holds
(Poly (m,(anpoly (a,0)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly (a,i)))

proof end;

theorem Th13a: :: FIELD_11:33

for F being Field
for i being Element of NAT
for m being Ordinal st m in card (nonConstantPolys F) holds
(Poly (m,(anpoly ((1. F),1)))) *' (Poly (m,(anpoly ((1. F),i)))) = Poly (m,(anpoly ((1. F),(i + 1))))

proof end;

theorem Th13: :: FIELD_11:34

for F being Field
for i being Nat
for m being Ordinal st m in card (nonConstantPolys F) holds
(power (Polynom-Ring ((card (nonConstantPolys F)),F))) . ((Poly (m,(anpoly ((1. F),1)))),i) = Poly (m,(anpoly ((1. F),i)))

proof end;

theorem Th12: :: FIELD_11:35

for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for m being Ordinal st m in card (nonConstantPolys F) holds
Poly (m,(anpoly ((LC p),(deg p)))) = LM (Poly (m,p))

proof end;

:: "... and contend that the ideal generated by all the polynomials
:: f(X_f) in K[S] is not the unit ideal. ..."

theorem KrSet: :: FIELD_11:36

for F being Field
for P being finite Subset of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) st p in P holds
p is_with_roots_in E

proof end;

eval0LM: for F being Field
for E being FieldExtension of F
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F
for x being Function of (card (nonConstantPolys F)),E st card (Support (Poly (m,p))) = 1 holds
Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))

proof end;

theorem eval0: :: FIELD_11:37

for F being Field
for E being FieldExtension of F
for m being Ordinal st m in card (nonConstantPolys F) holds
for p being Polynomial of F
for x being Function of (card (nonConstantPolys F)),E holds Ext_eval ((Poly (m,p)),x) = Ext_eval (p,(x /. m))

proof end;

ideal1: for R being non degenerated comRing
for M being non empty Subset of R
for o being object holds
( o in M -Ideal iff ex P being non empty finite Subset of R ex L being LeftLinearCombination of P st
( P c= M & o = Sum L ) )

proof end;

theorem :: FIELD_11:38

for R being non degenerated comRing
for M being non empty Subset of R
for o being object holds
( o in M -Ideal iff ex P being non empty finite Subset of R ex L being LinearCombination of P st
( P c= M & o = Sum L ) )

proof end;

:: "... If it is, then there is a finite combination of elements in our ideal
:: which is equal to 1: g1 * f1(X_f1) + ... + gn * fn(X_fn) = 1 with gi in K[S].
:: For simplicity, write Xi instead of X_fi. ...
:: Let F be a finite extension in which each polynomial f1, ..., fn has a root,
:: say ai is a root of fi in F, for i = 1,..., n. Let ai = 0 for i > n.
:: Substitute ai for Xi in our relation. We get 0 = 1, contradiction. ... "

registration

let F be Field;
let g be bijective Function of (nonConstantPolys F),(card (nonConstantPolys F));

cluster (nonConstantPolys (g,F)) -Ideal -> proper ;

coherence
(nonConstantPolys (g,F)) -Ideal is proper

proof end;

end;

:: "... Let m be a maximal ideal generated by all polynomials f(X_f) in K[S].
:: Then K[S]/m is a field, ..."

definition

let R be non degenerated commutative Ring;
let I be proper Ideal of R;

mode maxIdeal of I -> Ideal of R means :defideal: :: FIELD_11:def 8
( I c= it & it is maximal );

existence
ex b₁ being Ideal of R st
( I c= b₁ & b₁ is maximal )

proof end;

end;

:: deftheorem defideal defines maxIdeal FIELD_11:def 8 :
for R being non degenerated commutative Ring
for I being proper Ideal of R
for b₃ being Ideal of R holds
( b₃ is maxIdeal of I iff ( I c= b₃ & b₃ is maximal ) );

registration

let R be non degenerated commutative Ring;
let I be proper Ideal of R;

cluster -> maximal for maxIdeal of I;

coherence
for b₁ being maxIdeal of I holds b₁ is maximal by defideal;

end;

definition

let F be Field;
let g be bijective Function of (nonConstantPolys F),(card (nonConstantPolys F));
let I be maxIdeal of (nonConstantPolys (g,F)) -Ideal ;

func KroneckerField (F,g,I) -> Field equals :: FIELD_11:def 9
(Polynom-Ring ((card (nonConstantPolys F)),F)) / I;

coherence
(Polynom-Ring ((card (nonConstantPolys F)),F)) / I is Field by RING_1:21;

end;

:: deftheorem defines KroneckerField FIELD_11:def 9 :
for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal holds KroneckerField (F,g,I) = (Polynom-Ring ((card (nonConstantPolys F)),F)) / I;

:: " ... and we have a canonical map sigma: K[S] -> K[S]/m.
:: For any polynomial f in K[X] of degree >= 1, the polynomial sigma(f) has
:: a root in K[S]/m, which is an extension of sigma(K). ..."
:: Embedding F in KroneckerField(F,b,I)

definition

let n be Ordinal;
let R be non degenerated Ring;

func canHom (n,R) -> Function of R,(Polynom-Ring (n,R)) means :defcanhom: :: FIELD_11:def 10
for a being Element of R holds it . a = a | (n,R);

existence
ex b₁ being Function of R,(Polynom-Ring (n,R)) st
for a being Element of R holds b₁ . a = a | (n,R)

proof end;

uniqueness
for b₁, b₂ being Function of R,(Polynom-Ring (n,R)) st ( for a being Element of R holds b₁ . a = a | (n,R) ) & ( for a being Element of R holds b₂ . a = a | (n,R) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem defcanhom defines canHom FIELD_11:def 10 :
for n being Ordinal
for R being non degenerated Ring
for b₃ being Function of R,(Polynom-Ring (n,R)) holds
( b₃ = canHom (n,R) iff for a being Element of R holds b₃ . a = a | (n,R) );

registration

let n be Ordinal;
let R be non degenerated comRing;

cluster canHom (n,R) -> additive unity-preserving multiplicative ;

coherence
( canHom (n,R) is additive & canHom (n,R) is multiplicative & canHom (n,R) is unity-preserving )

proof end;

end;

registration

let n be Ordinal;
let R be non degenerated comRing;

cluster canHom (n,R) -> monomorphism ;

coherence
canHom (n,R) is monomorphism

proof end;

end;

definition

let F be Field;
let g be bijective Function of (nonConstantPolys F),(card (nonConstantPolys F));
let I be maxIdeal of (nonConstantPolys (g,F)) -Ideal ;

func emb (F,I,g) -> Function of F,(KroneckerField (F,g,I)) equals :: FIELD_11:def 11
(canHom I) * (canHom ((card (nonConstantPolys F)),F));

coherence
(canHom I) * (canHom ((card (nonConstantPolys F)),F)) is Function of F,(KroneckerField (F,g,I)) ;

end;

:: deftheorem defines emb FIELD_11:def 11 :
for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal holds emb (F,I,g) = (canHom I) * (canHom ((card (nonConstantPolys F)),F));

registration

let F be Field;
let g be bijective Function of (nonConstantPolys F),(card (nonConstantPolys F));
let I be maxIdeal of (nonConstantPolys (g,F)) -Ideal ;

cluster emb (F,I,g) -> additive unity-preserving multiplicative ;

coherence
( emb (F,I,g) is additive & emb (F,I,g) is multiplicative & emb (F,I,g) is unity-preserving )

proof end;

end;

registration

let F be Field;
let g be bijective Function of (nonConstantPolys F),(card (nonConstantPolys F));
let I be maxIdeal of (nonConstantPolys (g,F)) -Ideal ;

cluster emb (F,I,g) -> monomorphism ;

coherence
emb (F,I,g) is monomorphism ;

end;

registration

let F be Field;
let g be bijective Function of (nonConstantPolys F),(card (nonConstantPolys F));
let I be maxIdeal of (nonConstantPolys (g,F)) -Ideal ;

cluster KroneckerField (F,g,I) -> F -homomorphic F -monomorphic ;

coherence
( KroneckerField (F,g,I) is F -monomorphic & KroneckerField (F,g,I) is F -homomorphic )

proof end;

end;

:: the roots are - analogous to Kronecker's construction - the classes [Xm]

definition

let F be Field;
let m be Ordinal;
let g be bijective Function of (nonConstantPolys F),(card (nonConstantPolys F));
let I be maxIdeal of (nonConstantPolys (g,F)) -Ideal ;

func KrRoot (I,m) -> Element of (KroneckerField (F,g,I)) equals :: FIELD_11:def 12
Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,<%(0. F),(1. F)%>)));

coherence
Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,<%(0. F),(1. F)%>))) is Element of (KroneckerField (F,g,I))

proof end;

end;

:: deftheorem defines KrRoot FIELD_11:def 12 :
for F being Field
for m being Ordinal
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal holds KrRoot (I,m) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,<%(0. F),(1. F)%>)));

theorem TH39: :: FIELD_11:39

for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for a being Element of F holds (emb (F,I,g)) . a = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(a | ((card (nonConstantPolys F)),F)))

proof end;

theorem TH40: :: FIELD_11:40

for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for p being Element of the carrier of (Polynom-Ring F)
for n being Element of NAT holds ((PolyHom (emb (F,I,g))) . p) . n = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),((p . n) | ((card (nonConstantPolys F)),F)))

proof end;

Kr2a: for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for p being constant Element of the carrier of (Polynom-Ring F)
for n being Ordinal holds eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,n))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (n,p)))

proof end;

lemKr2: for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for p being non constant Element of the carrier of (Polynom-Ring F)
for m being Ordinal st m in card (nonConstantPolys F) holds
eval ((LM ((PolyHom (emb (F,I,g))) . p)),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(LM (Poly (m,p))))

proof end;

Kr3: for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for p being non constant Element of the carrier of (Polynom-Ring F)
for m being Ordinal st m in card (nonConstantPolys F) holds
eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,p)))

proof end;

theorem Kr2: :: FIELD_11:41

for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for p being Element of the carrier of (Polynom-Ring F)
for m being Ordinal st m in card (nonConstantPolys F) holds
eval (((PolyHom (emb (F,I,g))) . p),(KrRoot (I,m))) = Class ((EqRel ((Polynom-Ring ((card (nonConstantPolys F)),F)),I)),(Poly (m,p)))

proof end;

theorem Kr1: :: FIELD_11:42

for F being Field
for g being bijective Function of (nonConstantPolys F),(card (nonConstantPolys F))
for I being maxIdeal of (nonConstantPolys (g,F)) -Ideal
for p being non constant Element of the carrier of (Polynom-Ring F) holds KrRoot (I,(g . p)) is_a_root_of (PolyHom (emb (F,I,g))) . p

proof end;

:: "... Using the same set-theoretic argument as in Proposition 2.3, we conclude
:: that there exists an extension E1 of K in which every polynomial f in K[X] of
:: degree >= 1 has a root in E1."

theorem :: FIELD_11:43

for F being Field ex E1 being FieldExtension of F st
for p being non constant Element of the carrier of (Polynom-Ring F) holds p is_with_roots_in E1

proof end;