:: Field Extensions and {K}ronecker's Construction
:: by Christoph Schwarzweller
::
:: Copyright (c) 2019-2021 Association of Mizar Users

Th1: for R being Ring holds R is Subring of R
by LIOUVIL2:18;

theorem :: FIELD_4:1
for K being Field holds K is Subfield of K
proof end;

registration
let R be non degenerated Ring;
cluster -> non degenerated for Subring of R;
coherence
for b1 being Subring of R holds not b1 is degenerated
proof end;
end;

registration
let R be comRing;
cluster -> commutative for Subring of R;
coherence
for b1 being Subring of R holds b1 is commutative
proof end;
end;

registration
let R be domRing;
cluster -> domRing-like for Subring of R;
coherence
for b1 being Subring of R holds b1 is domRing-like
proof end;
end;

theorem Th2: :: FIELD_4:2
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
Sum F = Sum G
proof end;

definition
let R, S be Ring;
attr S is R -extending means :Def1: :: FIELD_4:def 1
R is Subring of S;
end;

:: deftheorem Def1 defines -extending FIELD_4:def 1 :
for R, S being Ring holds
( S is R -extending iff R is Subring of S );

registration
let R be Ring;
existence
ex b1 being Ring st b1 is R -extending
proof end;
end;

registration
let R be comRing;
existence
ex b1 being comRing st b1 is R -extending
proof end;
end;

registration
let R be domRing;
existence
ex b1 being domRing st b1 is R -extending
proof end;
end;

registration
let F be Field;
existence
ex b1 being Field st b1 is F -extending
proof end;
end;

definition end;

definition end;

definition end;

definition end;

theorem :: FIELD_4:3
for R being Ring holds R is RingExtension of R
proof end;

theorem :: FIELD_4:4
for R being comRing holds R is comRingExtension of R
proof end;

theorem :: FIELD_4:5
for R being domRing holds R is domRingExtension of R
proof end;

theorem Th3: :: FIELD_4:6
for F being Field holds F is FieldExtension of F
proof end;

theorem Th4: :: FIELD_4:7
for F, E being Field holds
( E is FieldExtension of F iff F is Subfield of E )
proof end;

registration
coherence by ;
end;

registration
coherence by ;
end;

registration
coherence by RING_3:47;
end;

registration
let R be Ring;
let S be RingExtension of R;
coherence
for b1 being RingExtension of S holds b1 is R -extending
proof end;
end;

registration
let R be comRing;
let S be comRingExtension of R;
coherence
for b1 being comRingExtension of S holds b1 is R -extending
;
end;

registration
let R be domRing;
let S be domRingExtension of R;
coherence
for b1 being domRingExtension of S holds b1 is R -extending
;
end;

registration
let F be Field;
let E be FieldExtension of F;
coherence
for b1 being FieldExtension of E holds b1 is F -extending
;
end;

registration
let R be non degenerated Ring;
coherence
for b1 being RingExtension of R holds not b1 is degenerated
proof end;
end;

theorem Th5: :: FIELD_4:8
for R being Ring
for S being RingExtension of R
for p being Polynomial of R holds p is Polynomial of S
proof end;

theorem :: FIELD_4:9
for S being Ring
for R being Subring of S
for p being Polynomial of R holds p is Polynomial of S
proof end;

theorem Th6: :: FIELD_4:10
for R being Ring
for S being RingExtension of R holds the carrier of () c= the carrier of ()
proof end;

theorem Th7: :: FIELD_4:11
for R, S being Ring st S is RingExtension of R holds
0. () = 0. ()
proof end;

theorem Th8: :: FIELD_4:12
for R, S being Ring st S is RingExtension of R holds
0_. S = 0_. R
proof end;

theorem Th9: :: FIELD_4:13
for R, S being Ring st S is RingExtension of R holds
1. () = 1. ()
proof end;

theorem :: FIELD_4:14
for R being Ring
for S being RingExtension of R holds 1_. S = 1_. R
proof end;

theorem Th10: :: FIELD_4:15
for R being Ring
for S being RingExtension of R
for p, q being Polynomial of R
for p1, q1 being Polynomial of S st p = p1 & q = q1 holds
p + q = p1 + q1
proof end;

theorem Th11: :: FIELD_4:16
for R being Ring
for S being RingExtension of R holds the addF of () = the addF of () || the carrier of ()
proof end;

theorem Th12: :: FIELD_4:17
for R being Ring
for S being RingExtension of R
for p, q being Polynomial of R
for p1, q1 being Polynomial of S st p = p1 & q = q1 holds
p *' q = p1 *' q1
proof end;

theorem Th13: :: FIELD_4:18
for R, S being Ring st S is RingExtension of R holds
the multF of () = the multF of () || the carrier of ()
proof end;

registration
let R be Ring;
let S be RingExtension of R;
coherence
proof end;
end;

theorem :: FIELD_4:19
for R being Ring
for S being RingExtension of R holds Polynom-Ring S is RingExtension of Polynom-Ring R ;

theorem :: FIELD_4:20
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of ()
for q being Element of the carrier of () st p = q holds
deg p = deg q
proof end;

Lm2: for R being Ring
for S being RingExtension of R
for a being Element of R
for b being Element of S st a = b holds
- a = - b

proof end;

theorem :: FIELD_4:21
for R being non degenerated Ring
for S being RingExtension of R
for a being Element of R
for b being Element of S st a = b holds
rpoly (1,a) = rpoly (1,b)
proof end;

theorem :: FIELD_4:22
for R, S being Ring
for a being Element of S st S is RingExtension of R holds
Ext_eval ((0_. R),a) = 0. S by ALGNUM_1:13;

theorem :: FIELD_4:23
for R being non degenerated Ring
for S being RingExtension of R
for a being Element of S holds Ext_eval ((1_. R),a) = 1. S
proof end;

theorem :: FIELD_4:24
for R being Ring
for S being RingExtension of R
for a being Element of S
for p, q being Polynomial of R holds Ext_eval ((p + q),a) = (Ext_eval (p,a)) + (Ext_eval (q,a))
proof end;

theorem :: FIELD_4:25
for R being comRing
for S being comRingExtension of R
for a being Element of S
for p, q being Polynomial of R holds Ext_eval ((p *' q),a) = (Ext_eval (p,a)) * (Ext_eval (q,a))
proof end;

Th14: for R being Ring
for S being RingExtension of R
for p being Element of the carrier of ()
for a being Element of R
for b being Element of S st b = a holds
Ext_eval (p,b) = eval (p,a)

proof end;

theorem Th15: :: FIELD_4:26
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of ()
for q being Element of the carrier of ()
for a being Element of S st p = q holds
Ext_eval (p,a) = eval (q,a)
proof end;

theorem :: FIELD_4:27
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of ()
for q being Element of the carrier of ()
for a being Element of R
for b being Element of S st q = p & b = a holds
eval (q,b) = eval (p,a)
proof end;

definition
let R be Ring;
let S be RingExtension of R;
let p be Element of the carrier of ();
let a be Element of S;
pred a is_a_root_of p,S means :: FIELD_4:def 2
Ext_eval (p,a) = 0. S;
end;

:: deftheorem defines is_a_root_of FIELD_4:def 2 :
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of ()
for a being Element of S holds
( a is_a_root_of p,S iff Ext_eval (p,a) = 0. S );

definition
let R be Ring;
let S be RingExtension of R;
let p be Element of the carrier of ();
pred p is_with_roots_in S means :: FIELD_4:def 3
ex a being Element of S st a is_a_root_of p,S;
end;

:: deftheorem defines is_with_roots_in FIELD_4:def 3 :
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of () holds
( p is_with_roots_in S iff ex a being Element of S st a is_a_root_of p,S );

definition
let R be Ring;
let S be RingExtension of R;
let p be Element of the carrier of ();
func Roots (S,p) -> Subset of S equals :: FIELD_4:def 4
{ a where a is Element of S : a is_a_root_of p,S } ;
coherence
{ a where a is Element of S : a is_a_root_of p,S } is Subset of S
proof end;
end;

:: deftheorem defines Roots FIELD_4:def 4 :
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of () holds Roots (S,p) = { a where a is Element of S : a is_a_root_of p,S } ;

theorem :: FIELD_4:28
for R being Ring
for S being RingExtension of R
for p being Element of the carrier of () holds Roots p c= Roots (S,p)
proof end;

::: changed Element of the carrier of Polynom-Ring R -> Polynomial R
definition
let R be Ring;
let S be non degenerated Ring;
let p be Polynomial of R;
pred p splits_in S means :: FIELD_4:def 5
ex a being non zero Element of S ex q being Ppoly of S st p = a * q;
end;

:: deftheorem defines splits_in FIELD_4:def 5 :
for R being Ring
for S being non degenerated Ring
for p being Polynomial of R holds
( p splits_in S iff ex a being non zero Element of S ex q being Ppoly of S st p = a * q );

::: changed Element of the carrier of Polynom-Ring R -> Polynomial R
theorem :: FIELD_4:29
for F being Field
for p being Polynomial of F st deg p = 1 holds
p splits_in F
proof end;

definition
let R be Ring;
let S be RingExtension of R;
func VecSp (S,R) -> strict ModuleStr over R means :Def5: :: FIELD_4:def 6
( the carrier of it = the carrier of S & the addF of it = the addF of S & the ZeroF of it = 0. S & the lmult of it = the multF of S | [: the carrier of R, the carrier of S:] );
existence
ex b1 being strict ModuleStr over R st
( the carrier of b1 = the carrier of S & the addF of b1 = the addF of S & the ZeroF of b1 = 0. S & the lmult of b1 = the multF of S | [: the carrier of R, the carrier of S:] )
proof end;
uniqueness
for b1, b2 being strict ModuleStr over R st the carrier of b1 = the carrier of S & the addF of b1 = the addF of S & the ZeroF of b1 = 0. S & the lmult of b1 = the multF of S | [: the carrier of R, the carrier of S:] & the carrier of b2 = the carrier of S & the addF of b2 = the addF of S & the ZeroF of b2 = 0. S & the lmult of b2 = the multF of S | [: the carrier of R, the carrier of S:] holds
b1 = b2
;
end;

:: deftheorem Def5 defines VecSp FIELD_4:def 6 :
for R being Ring
for S being RingExtension of R
for b3 being strict ModuleStr over R holds
( b3 = VecSp (S,R) iff ( the carrier of b3 = the carrier of S & the addF of b3 = the addF of S & the ZeroF of b3 = 0. S & the lmult of b3 = the multF of S | [: the carrier of R, the carrier of S:] ) );

registration
let R be Ring;
let S be RingExtension of R;
cluster VecSp (S,R) -> non empty strict ;
coherence
not VecSp (S,R) is empty
proof end;
end;

registration
let R be Ring;
let S be RingExtension of R;
coherence
( VecSp (S,R) is Abelian & VecSp (S,R) is add-associative & VecSp (S,R) is right_zeroed & VecSp (S,R) is right_complementable )
proof end;
end;

Lm3: for R being Ring
for E being RingExtension of R
for a, b being Element of E
for s being Element of R
for v being Element of (VecSp (E,R)) st a = s & b = v holds
a * b = s * v

proof end;

Lm4: for R being Ring
for E being RingExtension of R
for a, b being Element of E
for x, y being Element of R st a = x & b = y holds
a + b = x + y

proof end;

Lm5: for R being Ring
for E being RingExtension of R
for a, b being Element of E
for x, y being Element of R st a = x & b = y holds
a * b = x * y

proof end;

registration
let R be Ring;
let S be RingExtension of R;
coherence
( VecSp (S,R) is scalar-distributive & VecSp (S,R) is scalar-associative & VecSp (S,R) is scalar-unital & VecSp (S,R) is vector-distributive )
proof end;
end;

theorem :: FIELD_4:30
for R being Ring
for S being RingExtension of R holds VecSp (S,R) is VectSp of R ;

definition
let F be Field;
let E be FieldExtension of F;
func deg (E,F) -> Integer equals :Def6: :: FIELD_4:def 7
dim (VecSp (E,F)) if VecSp (E,F) is finite-dimensional
otherwise - 1;
coherence
( ( VecSp (E,F) is finite-dimensional implies dim (VecSp (E,F)) is Integer ) & ( not VecSp (E,F) is finite-dimensional implies - 1 is Integer ) )
;
consistency
for b1 being Integer holds verum
;
end;

:: deftheorem Def6 defines deg FIELD_4:def 7 :
for F being Field
for E being FieldExtension of F holds
( ( VecSp (E,F) is finite-dimensional implies deg (E,F) = dim (VecSp (E,F)) ) & ( not VecSp (E,F) is finite-dimensional implies deg (E,F) = - 1 ) );

registration
let F be Field;
let E be FieldExtension of F;
cluster deg (E,F) -> dim-like ;
coherence
deg (E,F) is dim-like
proof end;
end;

definition
let F be Field;
let E be FieldExtension of F;
attr E is F -finite means :Def7: :: FIELD_4:def 8
VecSp (E,F) is finite-dimensional ;
end;

:: deftheorem Def7 defines -finite FIELD_4:def 8 :
for F being Field
for E being FieldExtension of F holds
( E is F -finite iff VecSp (E,F) is finite-dimensional );

registration
let F be Field;
existence
ex b1 being FieldExtension of F st b1 is F -finite
proof end;
end;

registration
let F be Field;
let E be F -finite FieldExtension of F;
cluster deg (E,F) -> natural ;
coherence
deg (E,F) is natural
proof end;
end;

registration
let F be Field;
let p be non constant Element of the carrier of ();
cluster the carrier of () -> F -polynomial-membered ;
coherence
the carrier of () is F -polynomial-membered
proof end;
coherence ;
end;

definition
let F be Field;
let p be irreducible Element of the carrier of ();
func KroneckerIso p -> Function of the carrier of (), the carrier of (KroneckerField (F,p)) means :Def8: :: FIELD_4:def 9
for q being Element of the carrier of () holds it . q = Class ((EqRel ((),())),q);
existence
ex b1 being Function of the carrier of (), the carrier of (KroneckerField (F,p)) st
for q being Element of the carrier of () holds b1 . q = Class ((EqRel ((),())),q)
proof end;
uniqueness
for b1, b2 being Function of the carrier of (), the carrier of (KroneckerField (F,p)) st ( for q being Element of the carrier of () holds b1 . q = Class ((EqRel ((),())),q) ) & ( for q being Element of the carrier of () holds b2 . q = Class ((EqRel ((),())),q) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines KroneckerIso FIELD_4:def 9 :
for F being Field
for p being irreducible Element of the carrier of ()
for b3 being Function of the carrier of (), the carrier of (KroneckerField (F,p)) holds
( b3 = KroneckerIso p iff for q being Element of the carrier of () holds b3 . q = Class ((EqRel ((),())),q) );

Lm6: for L being Ring
for a being Element of ()
for p being Polynomial of L st a = p holds
- a = - p

proof end;

Lm7: for L being Ring
for a, b being Element of ()
for p, q being Polynomial of L st a = p & b = q holds
a - b = p - q

proof end;

Lm8: for F being Field
for p being irreducible Element of the carrier of ()
for a being Element of () holds a in the carrier of ()

proof end;

Lm9: for F being Field
for p being irreducible Element of the carrier of ()
for a being Element of the carrier of ()
for q being Element of () st a = q holds
- a = - q

proof end;

Lm10: for F being Field
for p being irreducible Element of the carrier of ()
for a, b being Element of the carrier of ()
for q, r being Element of () st a = q & b = r holds
a - b = q - r

proof end;

registration
let F be Field;
let p be irreducible Element of the carrier of ();
coherence
proof end;
end;

registration
let F be Field;
let p be irreducible Element of the carrier of ();
coherence
( KroneckerField (F,p) is Polynom-Ring p -homomorphic & KroneckerField (F,p) is Polynom-Ring p -monomorphic & KroneckerField (F,p) is Polynom-Ring p -isomorphic )
proof end;
coherence
proof end;
coherence ;
end;

Lm11: for F being polynomial_disjoint Field
for p being irreducible Element of the carrier of () ex E being FieldExtension of F st p is_with_roots_in E

proof end;

theorem :: FIELD_4:31
for F being polynomial_disjoint Field
for f being non constant Element of the carrier of () ex E being FieldExtension of F st f is_with_roots_in E
proof end;