:: Field Extensions and {K}ronecker's Construction
:: by Christoph Schwarzweller
::
:: Received August 29, 2019
:: 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;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital V113() left_unital Abelian add-associative right_zeroed V131() unital associative V201() V202() V203() V204() INT.Ring -homomorphic INT.Ring -homomorphic R -extending for doubleLoopStr ;
existence
ex b1 being Ring st b1 is R -extending
proof end;
end;

registration
let R be comRing;
cluster non empty left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable right-distributive left-distributive right_unital well-unital V113() left_unital Abelian add-associative right_zeroed V131() unital associative commutative V201() V202() V203() V204() INT.Ring -homomorphic R -extending for doubleLoopStr ;
existence
ex b1 being comRing st b1 is R -extending
proof end;
end;

registration
let R be domRing;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable right-distributive left-distributive right_unital well-unital V113() left_unital Abelian add-associative right_zeroed V131() unital associative commutative domRing-like V201() V202() V203() V204() INT.Ring -homomorphic R -extending for doubleLoopStr ;
existence
ex b1 being domRing st b1 is R -extending
proof end;
end;

registration
let F be Field;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital V113() left_unital Abelian add-associative right_zeroed V131() unital associative commutative domRing-like V201() V202() V203() V204() PID V239() Euclidian INT.Ring -homomorphic factorial F -extending for doubleLoopStr ;
existence
ex b1 being Field st b1 is F -extending
proof end;
end;

definition
let R be Ring;
mode RingExtension of R is R -extending Ring;
end;

definition
let R be comRing;
mode comRingExtension of R is R -extending comRing;
end;

definition
let R be domRing;
mode domRingExtension of R is R -extending domRing;
end;

definition
let F be Field;
mode FieldExtension of F is F -extending Field;
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
cluster F_Complex -> F_Real -extending ;
coherence
F_Complex is F_Real -extending by RING_3:43, RING_3:48;
end;

registration
cluster F_Real -> F_Rat -extending ;
coherence
F_Real is F_Rat -extending by RING_3:43, GAUSSINT:14;
end;

registration
cluster F_Rat -> INT.Ring -extending ;
coherence
F_Rat is INT.Ring -extending by RING_3:47;
end;

registration
let R be Ring;
let S be RingExtension of R;
cluster non empty right_complementable well-unital V113() Abelian add-associative right_zeroed associative S -extending -> R -extending for doubleLoopStr ;
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;
cluster non empty right_complementable well-unital V113() Abelian add-associative right_zeroed associative commutative S -extending -> R -extending for doubleLoopStr ;
coherence
for b1 being comRingExtension of S holds b1 is R -extending ;
end;

registration
let R be domRing;
let S be domRingExtension of R;
cluster non empty non degenerated right_complementable well-unital V113() Abelian add-associative right_zeroed associative commutative domRing-like S -extending -> R -extending for doubleLoopStr ;
coherence
for b1 being domRingExtension of S holds b1 is R -extending ;
end;

registration
let F be Field;
let E be FieldExtension of F;
cluster non empty non degenerated right_complementable almost_left_invertible well-unital V113() Abelian add-associative right_zeroed associative commutative E -extending -> F -extending for doubleLoopStr ;
coherence
for b1 being FieldExtension of E holds b1 is F -extending ;
end;

registration
let R be non degenerated Ring;
cluster non empty right_complementable well-unital V113() Abelian add-associative right_zeroed associative R -extending -> non degenerated for doubleLoopStr ;
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 (Polynom-Ring R) c= the carrier of (Polynom-Ring S)
proof end;

theorem Th7: :: FIELD_4:11
for R, S being Ring st S is RingExtension of R holds
0. (Polynom-Ring S) = 0. (Polynom-Ring R)
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. (Polynom-Ring S) = 1. (Polynom-Ring R)
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 (Polynom-Ring R) = the addF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)
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 (Polynom-Ring R) = the multF of (Polynom-Ring S) || the carrier of (Polynom-Ring R)
proof end;

registration
let R be Ring;
let S be RingExtension of R;
cluster Polynom-Ring S -> Polynom-Ring R -extending ;
coherence
Polynom-Ring S is Polynom-Ring R -extending
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 (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S) 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 (Polynom-Ring R)
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 (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S)
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 (Polynom-Ring R)
for q being Element of the carrier of (Polynom-Ring S)
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 (Polynom-Ring R);
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 (Polynom-Ring R)
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 (Polynom-Ring R);
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 (Polynom-Ring R) 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 (Polynom-Ring R);
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 (Polynom-Ring R) 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 (Polynom-Ring R) 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;
cluster VecSp (S,R) -> right_complementable strict Abelian add-associative right_zeroed ;
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;
cluster VecSp (S,R) -> strict vector-distributive scalar-distributive scalar-associative scalar-unital ;
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;
cluster non empty non degenerated non trivial left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable almost_left_cancelable almost_right_cancelable almost_cancelable almost_left_invertible almost_right_invertible almost_invertible right-distributive left-distributive right_unital well-unital V113() left_unital Abelian add-associative right_zeroed V131() unital associative commutative domRing-like V201() V202() V203() V204() PID V239() Euclidian INT.Ring -homomorphic factorial F -extending F -finite for doubleLoopStr ;
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 (Polynom-Ring F);
cluster the carrier of (Polynom-Ring p) -> F -polynomial-membered ;
coherence
the carrier of (Polynom-Ring p) is F -polynomial-membered
proof end;
cluster Polynom-Ring p -> F -polynomial-membered ;
coherence
Polynom-Ring p is F -polynomial-membered ;
end;

definition
let F be Field;
let p be irreducible Element of the carrier of (Polynom-Ring F);
func KroneckerIso p -> Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)) means :Def8: :: FIELD_4:def 9
 for q being Element of the carrier of (Polynom-Ring p) holds it . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q);
existence
ex b1 being Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)) st
for q being Element of the carrier of (Polynom-Ring p) holds b1 . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q)
proof end;
uniqueness
for b1, b2 being Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)) st ( for q being Element of the carrier of (Polynom-Ring p) holds b1 . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) ) & ( for q being Element of the carrier of (Polynom-Ring p) holds b2 . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),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 (Polynom-Ring F)
for b3 being Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)) holds
( b3 = KroneckerIso p iff for q being Element of the carrier of (Polynom-Ring p) holds b3 . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) );

Lm6: for L being Ring
for a being Element of (Polynom-Ring L)
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 (Polynom-Ring L)
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 (Polynom-Ring F)
for a being Element of (Polynom-Ring p) holds a in the carrier of (Polynom-Ring F)
proof end;

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

Lm10: for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for a, b being Element of the carrier of (Polynom-Ring F)
for q, r being Element of (Polynom-Ring p) 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 (Polynom-Ring F);
cluster KroneckerIso p -> one-to-one onto additive unity-preserving multiplicative ;
coherence
( KroneckerIso p is additive & KroneckerIso p is multiplicative & KroneckerIso p is unity-preserving & KroneckerIso p is one-to-one & KroneckerIso p is onto )
proof end;
end;

registration
let F be Field;
let p be irreducible Element of the carrier of (Polynom-Ring F);
cluster KroneckerField (F,p) -> Polynom-Ring p -homomorphic Polynom-Ring p -monomorphic Polynom-Ring p -isomorphic ;
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;
cluster Polynom-Ring p -> KroneckerField (F,p) -homomorphic KroneckerField (F,p) -monomorphic KroneckerField (F,p) -isomorphic ;
coherence
( Polynom-Ring p is KroneckerField (F,p) -homomorphic & Polynom-Ring p is KroneckerField (F,p) -monomorphic & Polynom-Ring p is KroneckerField (F,p) -isomorphic )
proof end;
cluster Polynom-Ring p -> F -homomorphic F -monomorphic ;
coherence
( Polynom-Ring p is F -homomorphic & Polynom-Ring p is F -monomorphic ) ;
end;

Lm11: for F being polynomial_disjoint Field
for p being irreducible Element of the carrier of (Polynom-Ring F) 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 (Polynom-Ring F) ex E being FieldExtension of F st f is_with_roots_in E
proof end;