:: Renamings and a Condition-free Formalization of {K}ronecker's Construction
:: by Christoph Schwarzweller
::
:: Received May 19, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users


theorem :: FIELD_5:1
for X, Y being set st Y c= X holds
(X \ Y) \/ Y = X
proof end;

theorem th0a: :: FIELD_5:2
for n, m being Nat holds
( n +` m = n + m & n *` m = n * m )
proof end;

theorem th0k: :: FIELD_5:3
for n, m being Nat holds
( ( n c= m implies n <= m ) & ( n <= m implies n c= m ) & ( n in m implies n < m ) & ( n < m implies n in m ) )
proof end;

theorem th0e: :: FIELD_5:4
for n being Nat holds exp (2,n) = 2 |^ n
proof end;

theorem th0n: :: FIELD_5:5
for n being Nat st n >= 3 holds
n + n < 2 |^ n
proof end;

theorem th0b: :: FIELD_5:6
for n being Nat st n >= 3 holds
n +` n in exp (2,n)
proof end;

theorem :: FIELD_5:7
NAT meets bool NAT
proof end;

theorem th1: :: FIELD_5:8
for X being set holds
not for o being object holds o in X
proof end;

theorem thre: :: FIELD_5:9
for X being set ex Y being set st
( card X c= card Y & X /\ Y = {} )
proof end;

theorem thre1: :: FIELD_5:10
for X, Y being set st card X c= card Y holds
ex Z being set st
( Z c= Y & card Z = card X )
proof end;

theorem :: FIELD_5:11
for X being set ex Y being set st
( card X = card Y & X /\ Y = {} )
proof end;

theorem pr1: :: FIELD_5:12
for E being Field
for F being Subfield of E holds F is Subring of E
proof end;

theorem :: FIELD_5:13
for F being Field
for R being Subring of F holds
( R is Subfield of F iff R is Field )
proof end;

registration
let F be Field;
let E be FieldExtension of F;
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 Abelian add-associative right_zeroed V115() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like V217() V278() V279() V280() V281() PID Euclidian INT.Ring -homomorphic factorial F -extending E -extending for doubleLoopStr ;
existence
ex b1 being FieldExtension of F st b1 is E -extending
proof end;
end;

notation
let F be Field;
let E be FieldExtension of F;
antonym F -infinite E for F -finite ;
end;

theorem sp: :: FIELD_5:14
for F being Field
for E being FieldExtension of F
for K being b2 -extending FieldExtension of F holds VecSp (E,F) is Subspace of VecSp (K,F)
proof end;

theorem :: FIELD_5:15
for F being Field
for E being FieldExtension of F
for K being b2 -extending FieldExtension of F holds
( K is F -infinite or ( E is F -finite & deg (E,F) <= deg (K,F) ) )
proof end;

theorem divmod: :: FIELD_5:16
for F being Field
for p being Polynomial of F
for q being non zero Polynomial of F holds deg (p mod q) < deg q
proof end;

lempk: for F, K being Field st the carrier of F = the carrier of K & 0. F = 0. K holds
the carrier of (Polynom-Ring F) = the carrier of (Polynom-Ring K)
proof end;

definition
let R be Ring;
let p be Polynomial of R;
attr p is linear means :defl: :: FIELD_5:def 1
 deg p = 1;
end;

:: deftheorem defl defines linear FIELD_5:def 1 :
for R being Ring
for p being Polynomial of R holds
( p is linear iff deg p = 1 );

registration
let R be non degenerated Ring;
cluster non empty Relation-like omega -defined the carrier of R -valued Function-like V27( omega ) quasi_total finite-Support linear for Element of bool [:omega, the carrier of R:];
existence
ex b1 being Polynomial of R st b1 is linear
proof end;
cluster non empty Relation-like omega -defined the carrier of R -valued Function-like V27( omega ) quasi_total finite-Support non linear for Element of bool [:omega, the carrier of R:];
existence
not for b1 being Polynomial of R holds b1 is linear
proof end;
cluster non empty Relation-like omega -defined the carrier of R -valued Function-like V27( omega ) quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support linear for Element of the carrier of (Polynom-Ring R);
existence
ex b1 being Element of the carrier of (Polynom-Ring R) st b1 is linear
proof end;
cluster non empty Relation-like omega -defined the carrier of R -valued Function-like V27( omega ) quasi_total left_add-cancelable right_add-cancelable add-cancelable left_complementable right_complementable complementable finite-Support non linear for Element of the carrier of (Polynom-Ring R);
existence
not for b1 being Element of the carrier of (Polynom-Ring R) holds b1 is linear
proof end;
end;

registration
let R be non degenerated Ring;
cluster Function-like quasi_total finite-Support zero -> non linear for Element of bool [:omega, the carrier of R:];
coherence
for b1 being Polynomial of R st b1 is zero holds
not b1 is linear
proof end;
cluster Function-like quasi_total finite-Support constant -> non linear for Element of bool [:omega, the carrier of R:];
coherence
for b1 being Polynomial of R st b1 is constant holds
not b1 is linear by RATFUNC1:def 2;
end;

registration
let F be Field;
cluster Function-like quasi_total finite-Support linear -> with_roots for Element of bool [:omega, the carrier of F:];
coherence
for b1 being Polynomial of F st b1 is linear holds
b1 is with_roots
proof end;
end;

registration
let F be Field;
cluster linear -> irreducible for Element of the carrier of (Polynom-Ring F);
coherence
for b1 being Element of the carrier of (Polynom-Ring F) st b1 is linear holds
b1 is irreducible by RING_4:44;
end;

registration
let F be Field;
cluster with_roots non linear -> reducible for Element of the carrier of (Polynom-Ring F);
coherence
for b1 being Element of the carrier of (Polynom-Ring F) st not b1 is linear & b1 is with_roots holds
b1 is reducible
proof end;
end;

registration
let R be domRing;
let p be linear Polynomial of R;
let q be non constant Polynomial of R;
cluster p *' q -> non linear ;
coherence
not p *' q is linear
proof end;
end;

registration
let F be Field;
let p be linear Polynomial of F;
let q be non constant Polynomial of F;
cluster p *' q -> with_roots ;
coherence
p *' q is with_roots ;
end;

lemdis: for F being polynomial_disjoint Field
for p being non constant Element of the carrier of (Polynom-Ring F) holds F, Polynom-Ring p are_disjoint
proof end;

definition
let F be Field;
let p be non constant Element of the carrier of (Polynom-Ring F);
func canHomP p -> Function of F,(Polynom-Ring p) means :defch: :: FIELD_5:def 2
 for a being Element of F holds it . a = a | F;
existence
ex b1 being Function of F,(Polynom-Ring p) st
for a being Element of F holds b1 . a = a | F
proof end;
uniqueness
for b1, b2 being Function of F,(Polynom-Ring p) st ( for a being Element of F holds b1 . a = a | F ) & ( for a being Element of F holds b2 . a = a | F ) holds
b1 = b2
proof end;
end;

:: deftheorem defch defines canHomP FIELD_5:def 2 :
for F being Field
for p being non constant Element of the carrier of (Polynom-Ring F)
for b3 being Function of F,(Polynom-Ring p) holds
( b3 = canHomP p iff for a being Element of F holds b3 . a = a | F );

registration
let F be Field;
let p be non constant Element of the carrier of (Polynom-Ring F);
cluster canHomP p -> one-to-one additive unity-preserving multiplicative ;
coherence
( canHomP p is additive & canHomP p is multiplicative & canHomP p is unity-preserving & canHomP p is one-to-one )
proof end;
end;

registration
let F be Field;
let p be non constant Element of the carrier of (Polynom-Ring F);
cluster Polynom-Ring p -> F -homomorphic F -monomorphic ;
coherence
( Polynom-Ring p is F -homomorphic & Polynom-Ring p is F -monomorphic )
proof end;
end;

registration
let F be polynomial_disjoint Field;
let p be irreducible Element of the carrier of (Polynom-Ring F);
cluster embField (canHomP p) -> right_complementable almost_left_invertible add-associative distributive associative ;
coherence
( embField (canHomP p) is add-associative & embField (canHomP p) is right_complementable & embField (canHomP p) is associative & embField (canHomP p) is distributive & embField (canHomP p) is almost_left_invertible ) by lemdis, FIELD_2:12;
end;

registration
let F be polynomial_disjoint Field;
let p be irreducible Element of the carrier of (Polynom-Ring F);
cluster embField (canHomP p) -> F -extending ;
coherence
embField (canHomP p) is F -extending
proof end;
end;

definition
let F be polynomial_disjoint Field;
let p be irreducible Element of the carrier of (Polynom-Ring F);
func KrRootP p -> Element of (embField (canHomP p)) equals :: FIELD_5:def 3
(((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p);
coherence
(((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p) is Element of (embField (canHomP p))
proof end;
end;

:: deftheorem defines KrRootP FIELD_5:def 3 :
for F being polynomial_disjoint Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds KrRootP p = (((emb_iso (canHomP p)) ") * ((KroneckerIso p) ")) . (KrRoot p);

theorem :: FIELD_5:17
for F being polynomial_disjoint Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds Ext_eval (p,(KrRootP p)) = 0. F
proof end;

theorem polyd: :: FIELD_5:18
for F being Field
for p being linear Element of the carrier of (Polynom-Ring F) holds
( Polynom-Ring p,F are_isomorphic & the carrier of (embField (canHomP p)) = the carrier of F )
proof end;

theorem :: FIELD_5:19
for F being strict Field
for p being linear Element of the carrier of (Polynom-Ring F) holds embField (canHomP p) = F
proof end;

theorem polyd1: :: FIELD_5:20
for F being Field
for p being linear Element of the carrier of (Polynom-Ring F) holds
( (Polynom-Ring F) / ({p} -Ideal),F are_isomorphic & the carrier of (embField (emb p)) = the carrier of F )
proof end;

theorem :: FIELD_5:21
for F being strict Field
for p being linear Element of the carrier of (Polynom-Ring F) holds embField (emb p) = F
proof end;

theorem :: FIELD_5:22
for F being polynomial_disjoint Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds
( embField (canHomP p) is polynomial_disjoint iff p is linear )
proof end;

theorem :: FIELD_5:23
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being polynomial_disjoint Field st E = embField (emb p) holds
F is polynomial_disjoint
proof end;

Disj1: for n being non trivial Nat
for p being Element of the carrier of (Polynom-Ring (Z/ n)) holds the carrier of (Z/ n) /\ the carrier of ((Polynom-Ring (Z/ n)) / ({p} -Ideal)) = {}
proof end;

Disj2: for p being Element of the carrier of (Polynom-Ring F_Rat) holds the carrier of F_Rat /\ the carrier of ((Polynom-Ring F_Rat) / ({p} -Ideal)) = {}
proof end;

registration
let n be Prime;
let p be irreducible Element of the carrier of (Polynom-Ring (Z/ n));
cluster embField (emb p) -> right_complementable almost_left_invertible add-associative distributive associative ;
coherence
( embField (emb p) is add-associative & embField (emb p) is right_complementable & embField (emb p) is associative & embField (emb p) is distributive & embField (emb p) is almost_left_invertible )
proof end;
end;

registration
let p be irreducible Element of the carrier of (Polynom-Ring F_Rat);
cluster embField (emb p) -> right_complementable almost_left_invertible add-associative distributive associative ;
coherence
( embField (emb p) is add-associative & embField (emb p) is right_complementable & embField (emb p) is associative & embField (emb p) is distributive & embField (emb p) is almost_left_invertible )
proof end;
end;

theorem :: FIELD_5:24
for n being Prime
for p being non constant Element of the carrier of (Polynom-Ring (Z/ n)) holds Z/ n,(Polynom-Ring (Z/ n)) / ({p} -Ideal) are_disjoint
proof end;

theorem :: FIELD_5:25
for p being non constant Element of the carrier of (Polynom-Ring F_Rat) holds F_Rat ,(Polynom-Ring F_Rat) / ({p} -Ideal) are_disjoint
proof end;

registration
let n be Prime;
let p be irreducible Element of the carrier of (Polynom-Ring (Z/ n));
cluster embField (emb p) -> polynomial_disjoint ;
coherence
embField (emb p) is polynomial_disjoint
proof end;
end;

registration
let p be irreducible Element of the carrier of (Polynom-Ring F_Rat);
cluster embField (emb p) -> polynomial_disjoint ;
coherence
embField (emb p) is polynomial_disjoint
proof end;
end;

definition
let R be Ring;
attr R is strong_polynomial_disjoint means :dspd: :: FIELD_5:def 4
 for a being Element of R
for S being Ring
for p being Element of the carrier of (Polynom-Ring S) holds a <> p;
end;

:: deftheorem dspd defines strong_polynomial_disjoint FIELD_5:def 4 :
for R being Ring holds
( R is strong_polynomial_disjoint iff for a being Element of R
for S being Ring
for p being Element of the carrier of (Polynom-Ring S) holds a <> p );

registration
cluster INT.Ring -> strong_polynomial_disjoint ;
coherence
INT.Ring is strong_polynomial_disjoint by FIELD_3:25;
cluster F_Rat -> strong_polynomial_disjoint ;
coherence
F_Rat is strong_polynomial_disjoint by FIELD_3:25;
cluster F_Real -> strong_polynomial_disjoint ;
coherence
F_Real is strong_polynomial_disjoint by FIELD_3:26;
end;

registration
let n be non trivial Nat;
cluster INT.Ring n -> strong_polynomial_disjoint ;
coherence
Z/ n is strong_polynomial_disjoint
proof end;
end;

registration
cluster non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative strong_polynomial_disjoint -> polynomial_disjoint for doubleLoopStr ;
coherence
for b1 being Ring st b1 is strong_polynomial_disjoint holds
b1 is polynomial_disjoint
proof end;
end;

registration
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 Abelian add-associative right_zeroed V115() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like V217() V278() V279() V280() V281() PID Euclidian INT.Ring -homomorphic factorial strong_polynomial_disjoint for doubleLoopStr ;
existence
ex b1 being Field st b1 is strong_polynomial_disjoint
proof end;
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 Abelian add-associative right_zeroed V115() right-distributive left-distributive right_unital well-unital distributive left_unital unital associative commutative domRing-like V217() V278() V279() V280() V281() PID Euclidian INT.Ring -homomorphic factorial non strong_polynomial_disjoint for doubleLoopStr ;
existence
not for b1 being Field holds b1 is strong_polynomial_disjoint
proof end;
end;

theorem :: FIELD_5:26
for F being strong_polynomial_disjoint Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for E being Field st E = embField (emb p) holds
E is strong_polynomial_disjoint
proof end;

definition
let X be non empty set ;
let Z be set ;
mode Renaming of X,Z -> Function means :defr: :: FIELD_5:def 5
( dom it = X & it is one-to-one & (rng it) /\ (X \/ Z) = {} );
existence
ex b1 being Function st
( dom b1 = X & b1 is one-to-one & (rng b1) /\ (X \/ Z) = {} )
proof end;
end;

:: deftheorem defr defines Renaming FIELD_5:def 5 :
for X being non empty set
for Z being set
for b3 being Function holds
( b3 is Renaming of X,Z iff ( dom b3 = X & b3 is one-to-one & (rng b3) /\ (X \/ Z) = {} ) );

registration
let X be non empty set ;
let Z be set ;
let r be Renaming of X,Z;
cluster dom r -> non empty ;
coherence
not dom r is empty by defr;
cluster rng r -> non empty ;
coherence
not rng r is empty
proof end;
end;

registration
let X be non empty set ;
let Z be set ;
cluster -> X -defined one-to-one for Renaming of X,Z;
coherence
for b1 being Renaming of X,Z holds
( b1 is X -defined & b1 is one-to-one )
proof end;
end;

definition
let X be non empty set ;
let Z be set ;
let r be Renaming of X,Z;
:: original: "
redefine func r " -> Function of (rng r),X;
coherence
r " is Function of (rng r),X
proof end;
end;

theorem lemonto: :: FIELD_5:27
for X being non empty set
for Z being set
for r being Renaming of X,Z holds r " is onto
proof end;

definition
let F be Field;
let Z be set ;
let r be Renaming of the carrier of F,Z;
func ren_add r -> BinOp of (rng r) means :defra: :: FIELD_5:def 6
 for a, b being Element of rng r holds it . (a,b) = r . (((r ") . a) + ((r ") . b));
existence
ex b1 being BinOp of (rng r) st
for a, b being Element of rng r holds b1 . (a,b) = r . (((r ") . a) + ((r ") . b))
proof end;
uniqueness
for b1, b2 being BinOp of (rng r) st ( for a, b being Element of rng r holds b1 . (a,b) = r . (((r ") . a) + ((r ") . b)) ) & ( for a, b being Element of rng r holds b2 . (a,b) = r . (((r ") . a) + ((r ") . b)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defra defines ren_add FIELD_5:def 6 :
for F being Field
for Z being set
for r being Renaming of the carrier of F,Z
for b4 being BinOp of (rng r) holds
( b4 = ren_add r iff for a, b being Element of rng r holds b4 . (a,b) = r . (((r ") . a) + ((r ") . b)) );

definition
let F be Field;
let Z be set ;
let r be Renaming of the carrier of F,Z;
func ren_mult r -> BinOp of (rng r) means :defrm: :: FIELD_5:def 7
 for a, b being Element of rng r holds it . (a,b) = r . (((r ") . a) * ((r ") . b));
existence
ex b1 being BinOp of (rng r) st
for a, b being Element of rng r holds b1 . (a,b) = r . (((r ") . a) * ((r ") . b))
proof end;
uniqueness
for b1, b2 being BinOp of (rng r) st ( for a, b being Element of rng r holds b1 . (a,b) = r . (((r ") . a) * ((r ") . b)) ) & ( for a, b being Element of rng r holds b2 . (a,b) = r . (((r ") . a) * ((r ") . b)) ) holds
b1 = b2
proof end;
end;

:: deftheorem defrm defines ren_mult FIELD_5:def 7 :
for F being Field
for Z being set
for r being Renaming of the carrier of F,Z
for b4 being BinOp of (rng r) holds
( b4 = ren_mult r iff for a, b being Element of rng r holds b4 . (a,b) = r . (((r ") . a) * ((r ") . b)) );

definition
let F be Field;
let Z be set ;
let r be Renaming of the carrier of F,Z;
func RenField r -> strict doubleLoopStr means :defrf: :: FIELD_5:def 8
( the carrier of it = rng r & the addF of it = ren_add r & the multF of it = ren_mult r & the OneF of it = r . (1. F) & the ZeroF of it = r . (0. F) );
existence
ex b1 being strict doubleLoopStr st
( the carrier of b1 = rng r & the addF of b1 = ren_add r & the multF of b1 = ren_mult r & the OneF of b1 = r . (1. F) & the ZeroF of b1 = r . (0. F) )
proof end;
uniqueness
for b1, b2 being strict doubleLoopStr st the carrier of b1 = rng r & the addF of b1 = ren_add r & the multF of b1 = ren_mult r & the OneF of b1 = r . (1. F) & the ZeroF of b1 = r . (0. F) & the carrier of b2 = rng r & the addF of b2 = ren_add r & the multF of b2 = ren_mult r & the OneF of b2 = r . (1. F) & the ZeroF of b2 = r . (0. F) holds
b1 = b2 ;
end;

:: deftheorem defrf defines RenField FIELD_5:def 8 :
for F being Field
for Z being set
for r being Renaming of the carrier of F,Z
for b4 being strict doubleLoopStr holds
( b4 = RenField r iff ( the carrier of b4 = rng r & the addF of b4 = ren_add r & the multF of b4 = ren_mult r & the OneF of b4 = r . (1. F) & the ZeroF of b4 = r . (0. F) ) );

registration
let F be Field;
let Z be set ;
let r be Renaming of the carrier of F,Z;
cluster RenField r -> non degenerated strict ;
coherence
not RenField r is degenerated
proof end;
end;

registration
let F be Field;
let Z be set ;
let r be Renaming of the carrier of F,Z;
cluster RenField r -> right_complementable strict Abelian add-associative right_zeroed ;
coherence
( RenField r is Abelian & RenField r is add-associative & RenField r is right_zeroed & RenField r is right_complementable )
proof end;
end;

registration
let F be Field;
let Z be set ;
let r be Renaming of the carrier of F,Z;
cluster RenField r -> almost_left_invertible strict well-unital distributive associative commutative ;
coherence
( RenField r is commutative & RenField r is associative & RenField r is well-unital & RenField r is distributive & RenField r is almost_left_invertible )
proof end;
end;

definition
let F be Field;
let Z be set ;
let r be Renaming of the carrier of F,Z;
:: original: "
redefine func r " -> Function of (RenField r),F;
coherence
r " is Function of (RenField r),F
proof end;
end;

theorem thiso: :: FIELD_5:28
for F being Field
for Z being set
for r being Renaming of the carrier of F,Z holds
( r " is additive & r " is multiplicative & r " is unity-preserving & r " is one-to-one & r " is onto )
proof end;

theorem thisofield: :: FIELD_5:29
for F being Field
for Z being set ex E being Field st
( E,F are_isomorphic & the carrier of E /\ ( the carrier of F \/ Z) = {} )
proof end;

kron: for F being 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 main: :: FIELD_5:30
for F being 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;

theorem :: FIELD_5:31
for F being Field
for f being non constant Element of the carrier of (Polynom-Ring F) ex E being FieldExtension of F st f splits_in E
proof end;