:: Renamings and a Condition-free Formalization of {K}ronecker's Construction
:: by Christoph Schwarzweller
::
:: 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
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;
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 () = the carrier of ()

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;
existence
ex b1 being Polynomial of R st b1 is linear
proof end;
existence
not for b1 being Polynomial of R holds b1 is linear
proof end;
existence
ex b1 being Element of the carrier of () st b1 is linear
proof end;
existence
not for b1 being Element of the carrier of () 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;
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 ();
coherence
for b1 being Element of the carrier of () 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 ();
coherence
for b1 being Element of the carrier of () 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 () holds F, Polynom-Ring p are_disjoint

proof end;

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

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

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

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

definition
let F be polynomial_disjoint Field;
let p be irreducible Element of the carrier of ();
func KrRootP p -> Element of (embField ()) equals :: FIELD_5:def 3
(((emb_iso ()) ") * (() ")) . ();
coherence
(((emb_iso ()) ") * (() ")) . () is Element of (embField ())
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 () holds KrRootP p = (((emb_iso ()) ") * (() ")) . ();

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

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

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

theorem polyd1: :: FIELD_5:20
for F being Field
for p being linear Element of the carrier of () holds
( () / (),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 () 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 () holds
( embField () 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 ()
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)) / ()) = {}

proof end;

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

registration
let n be Prime;
let p be irreducible Element of the carrier of (Polynom-Ring (Z/ n));
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 ;
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)) / () are_disjoint
proof end;

theorem :: FIELD_5:25
for p being non constant Element of the carrier of holds F_Rat , / () are_disjoint
proof end;

registration
let n be Prime;
let p be irreducible Element of the carrier of (Polynom-Ring (Z/ n));
coherence
proof end;
end;

registration
let p be irreducible Element of the carrier of ;
coherence
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 () 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 () holds a <> p );

registration end;

registration
let n be non trivial Nat;
coherence
proof end;
end;

registration
coherence
for b1 being Ring st b1 is strong_polynomial_disjoint holds
b1 is polynomial_disjoint
proof end;
end;

registration
existence
ex b1 being Field st b1 is strong_polynomial_disjoint
proof end;
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 ()
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;
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;
coherence
proof end;
end;

registration
let F be Field;
let Z be set ;
let r be Renaming of the carrier of F,Z;
coherence
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 (),F;
coherence
r " is Function of (),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 () 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 () 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 () ex E being FieldExtension of F st f splits_in E
proof end;