:: 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 b₁ being Subring of R holds not b₁ is degenerated

proof end;

end;

registration

let R be comRing;

cluster -> commutative for Subring of R;

coherence
for b₁ being Subring of R holds b₁ is commutative

proof end;

end;

registration

let R be domRing;

cluster -> domRing-like for Subring of R;

coherence
for b₁ being Subring of R holds b₁ 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 b₁ being Ring st b₁ 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 b₁ being comRing st b₁ 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 b₁ being domRing st b₁ 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 b₁ being Field st b₁ 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 b₁ being RingExtension of S holds b₁ 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 b₁ being comRingExtension of S holds b₁ 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 b₁ being domRingExtension of S holds b₁ 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 b₁ being FieldExtension of E holds b₁ 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 b₁ being RingExtension of R holds not b₁ 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 b₁ being strict ModuleStr over R st
( the carrier of b₁ = the carrier of S & the addF of b₁ = the addF of S & the ZeroF of b₁ = 0. S & the lmult of b₁ = the multF of S | [: the carrier of R, the carrier of S:] )

proof end;

uniqueness
for b₁, b₂ being strict ModuleStr over R st the carrier of b₁ = the carrier of S & the addF of b₁ = the addF of S & the ZeroF of b₁ = 0. S & the lmult of b₁ = the multF of S | [: the carrier of R, the carrier of S:] & the carrier of b₂ = the carrier of S & the addF of b₂ = the addF of S & the ZeroF of b₂ = 0. S & the lmult of b₂ = the multF of S | [: the carrier of R, the carrier of S:] holds
b₁ = b₂ ;

end;

:: deftheorem Def5 defines VecSp FIELD_4:def 6 :
for R being Ring
for S being RingExtension of R
for b₃ being strict ModuleStr over R holds
( b₃ = VecSp (S,R) iff ( the carrier of b₃ = the carrier of S & the addF of b₃ = the addF of S & the ZeroF of b₃ = 0. S & the lmult of b₃ = 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 b₁ 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 b₁ being FieldExtension of F st b₁ 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 b₁ 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 b₁ . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q)

proof end;

uniqueness
for b₁, b₂ 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 b₁ . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) ) & ( for q being Element of the carrier of (Polynom-Ring p) holds b₂ . q = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),q) ) holds
b₁ = b₂

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 b₃ being Function of the carrier of (Polynom-Ring p), the carrier of (KroneckerField (F,p)) holds
( b₃ = KroneckerIso p iff for q being Element of the carrier of (Polynom-Ring p) holds b₃ . 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;