:: On Roots of Polynomials over K[X]/<p>
:: by Christoph Schwarzweller
::
:: Received March 28, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


notation
let L be non empty ZeroStr ;
let p be Polynomial of L;
synonym LM p for Leading-Monomial p;
end;

theorem Th2: :: FIELD_1:1
for L being non empty ZeroStr
for p being Polynomial of L holds
( deg p is Element of NAT iff p <> 0_. L )
proof end;

definition
let R be non degenerated Ring;
let p be non zero Polynomial of R;
:: original: deg
redefine func deg p -> Element of NAT ;
coherence
deg p is Element of NAT
proof end;
end;

registration
let R be non empty right_complementable right-distributive add-associative right_zeroed doubleLoopStr ;
let f be additive Function of R,R;
reduce f . (0. R) to 0. R;
reducibility
f . (0. R) = 0. R by RING_2:6;
end;

theorem Th3: :: FIELD_1:2
for R being Ring
for I being Ideal of R
for x being Element of (R / I)
for a being Element of R st x = Class ((EqRel (R,I)),a) holds
for n being Nat holds x |^ n = Class ((EqRel (R,I)),(a |^ n))
proof end;

definition
let R be Ring;
let a, b be Element of R;
pred b is_a_irreducible_factor_of a means :: FIELD_1:def 1
( b divides a & b is irreducible );
end;

:: deftheorem defines is_a_irreducible_factor_of FIELD_1:def 1 :
for R being Ring
for a, b being Element of R holds
( b is_a_irreducible_factor_of a iff ( b divides a & b is irreducible ) );

registration
cluster non empty non degenerated V62() left_add-cancelable right_add-cancelable left_complementable right_complementable almost_left_cancelable almost_right_cancelable non almost_left_invertible right-distributive left-distributive right_unital well-unital V111() left_unital Abelian add-associative right_zeroed V128() unital V133() V135() domRing-like V250() V251() V252() V253() K720() -homomorphic factorial for doubleLoopStr ;
existence
ex b1 being domRing st
( not b1 is almost_left_invertible & b1 is factorial ) ;
end;

theorem Th4: :: FIELD_1:3
for R being non almost_left_invertible factorial domRing
for a being non zero NonUnit of R ex b being Element of R st b is_a_irreducible_factor_of a
proof end;

notation
let R be Ring;
let a be Element of R;
let n be Nat;
synonym anpoly (a,n) for seq (n,a);
end;

Lm1: for n being Nat
for R being non degenerated Ring
for a being non zero Element of R holds deg (anpoly (a,n)) = n
proof end;

registration
let R be non degenerated Ring;
let a be non zero Element of R;
let n be Nat;
cluster anpoly (a,n) -> non zero ;
coherence
not anpoly (a,n) is zero
proof end;
end;

registration
let R be Ring;
let a be zero Element of R;
let n be Nat;
cluster anpoly (a,n) -> zero ;
coherence
anpoly (a,n) is zero
proof end;
end;

theorem :: FIELD_1:4
for n being Nat
for R being non degenerated Ring
for a being non zero Element of R holds deg (anpoly (a,n)) = n by Lm1;

theorem :: FIELD_1:5
for n being Nat
for R being non degenerated Ring
for a being Element of R holds LC (anpoly (a,n)) = a
proof end;

theorem :: FIELD_1:6
for R being non degenerated Ring
for n being non zero Nat
for a, x being Element of R holds eval ((anpoly (a,n)),x) = a * (x |^ n)
proof end;

theorem :: FIELD_1:7
for R being non degenerated Ring
for a being Element of R holds anpoly (a,0) = a | R ;

theorem Th9: :: FIELD_1:8
for R being non degenerated Ring
for n being non zero Element of NAT holds anpoly ((1. R),n) = rpoly (n,(0. R))
proof end;

theorem Th10: :: FIELD_1:9
for n being Nat
for R being non degenerated comRing
for a, b being non zero Element of R holds b * (anpoly (a,n)) = anpoly ((a * b),n)
proof end;

theorem Th11: :: FIELD_1:10
for R being non degenerated comRing
for a, b being non zero Element of R
for n, m being Nat holds (anpoly (a,n)) *' (anpoly (b,m)) = anpoly ((a * b),(n + m))
proof end;

theorem Th12: :: FIELD_1:11
for R being non degenerated Ring
for p being non zero Polynomial of R holds LM p = anpoly ((p . (deg p)),(deg p))
proof end;

theorem Th13: :: FIELD_1:12
for n being Nat
for R being non degenerated comRing holds <%(0. R),(1. R)%> `^ n = anpoly ((1. R),n)
proof end;

theorem Th14: :: FIELD_1:13
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for a being Element of R
for n being Nat holds h . (a |^ n) = (h . a) |^ n
proof end;

theorem :: FIELD_1:14
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S holds h . (Sum (<*> the carrier of R)) = 0. S
proof end;

theorem :: FIELD_1:15
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for F being FinSequence of R
for a being Element of R holds h . (Sum (<*a*> ^ F)) = (h . a) + (h . (Sum F))
proof end;

theorem Th17: :: FIELD_1:16
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for F being FinSequence of R
for a being Element of R holds h . (Sum (F ^ <*a*>)) = (h . (Sum F)) + (h . a)
proof end;

theorem :: FIELD_1:17
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for F, G being FinSequence of R holds h . (Sum (F ^ G)) = (h . (Sum F)) + (h . (Sum G))
proof end;

theorem :: FIELD_1:18
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S holds h . (Product (<*> the carrier of R)) = 1. S
proof end;

theorem :: FIELD_1:19
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for F being FinSequence of R
for a being Element of R holds h . (Product (<*a*> ^ F)) = (h . a) * (h . (Product F))
proof end;

theorem :: FIELD_1:20
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for F being FinSequence of R
for a being Element of R holds h . (Product (F ^ <*a*>)) = (h . (Product F)) * (h . a)
proof end;

theorem :: FIELD_1:21
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for F, G being FinSequence of R holds h . (Product (F ^ G)) = (h . (Product F)) * (h . (Product G))
proof end;

definition
let R, S be Ring;
let f be Function of (Polynom-Ring R),(Polynom-Ring S);
let p be Element of the carrier of (Polynom-Ring R);
:: original: .
redefine func f . p -> Element of the carrier of (Polynom-Ring S);
coherence
f . p is Element of the carrier of (Polynom-Ring S)
proof end;
end;

definition
let R be Ring;
let S be R -homomorphic Ring;
let h be additive Function of R,S;
func PolyHom h -> Function of (Polynom-Ring R),(Polynom-Ring S) means :Def2: :: FIELD_1:def 2
 for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (it . f) . i = h . (f . i);
existence
ex b1 being Function of (Polynom-Ring R),(Polynom-Ring S) st
for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (b1 . f) . i = h . (f . i)
proof end;
uniqueness
for b1, b2 being Function of (Polynom-Ring R),(Polynom-Ring S) st ( for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (b1 . f) . i = h . (f . i) ) & ( for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (b2 . f) . i = h . (f . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines PolyHom FIELD_1:def 2 :
for R being Ring
for S being b1 -homomorphic Ring
for h being additive Function of R,S
for b4 being Function of (Polynom-Ring R),(Polynom-Ring S) holds
( b4 = PolyHom h iff for f being Element of the carrier of (Polynom-Ring R)
for i being Nat holds (b4 . f) . i = h . (f . i) );

registration
let R be Ring;
let S be R -homomorphic Ring;
let h be Homomorphism of R,S;
cluster PolyHom h -> additive unity-preserving multiplicative ;
coherence
( PolyHom h is additive & PolyHom h is multiplicative & PolyHom h is unity-preserving )
proof end;
end;

theorem Th23: :: FIELD_1:22
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S holds (PolyHom h) . (0_. R) = 0_. S
proof end;

theorem :: FIELD_1:23
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S holds (PolyHom h) . (1_. R) = 1_. S
proof end;

theorem :: FIELD_1:24
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p, q being Element of the carrier of (Polynom-Ring R) holds (PolyHom h) . (p + q) = ((PolyHom h) . p) + ((PolyHom h) . q) by VECTSP_1:def 20;

theorem :: FIELD_1:25
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p, q being Element of the carrier of (Polynom-Ring R) holds (PolyHom h) . (p * q) = ((PolyHom h) . p) * ((PolyHom h) . q) by GROUP_6:def 6;

theorem Th27: :: FIELD_1:26
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for b being Element of R holds (PolyHom h) . (b * p) = (h . b) * ((PolyHom h) . p)
proof end;

Lm2: for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds len ((PolyHom h) . p) <= len p
proof end;

Lm3: for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) st len p <> 0 holds
( len ((PolyHom h) . p) = len p iff h . (p . ((len p) -' 1)) <> 0. S )
proof end;

Lm4: for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p, L being Element of the carrier of (Polynom-Ring R) st L = LM p holds
for a being Element of R holds h . (eval ((LM p),a)) = eval (((PolyHom h) . L),(h . a))
proof end;

theorem Th28: :: FIELD_1:27
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R holds h . (eval (p,a)) = eval (((PolyHom h) . p),(h . a))
proof end;

:: RING_5:7 is required domRing
theorem :: FIELD_1:28
for R being domRing
for S being b1 -homomorphic domRing
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for b, x being Element of R holds h . (eval ((b * p),x)) = (h . b) * (eval (((PolyHom h) . p),(h . x)))
proof end;

registration
let R be Ring;
cluster non empty left_add-cancelable right_add-cancelable left_complementable right_complementable right-distributive left-distributive right_unital well-unital V111() left_unital Abelian add-associative right_zeroed V128() unital V133() V250() V251() V252() V253() R -homomorphic K720() -homomorphic K720() -homomorphic R -monomorphic for doubleLoopStr ;
existence
ex b1 being Ring st
( b1 is R -homomorphic & b1 is R -monomorphic )
proof end;
cluster non empty left_add-cancelable right_add-cancelable left_complementable right_complementable right-distributive left-distributive right_unital well-unital V111() left_unital Abelian add-associative right_zeroed V128() unital V133() V250() V251() V252() V253() R -homomorphic K720() -homomorphic K720() -homomorphic R -isomorphic for doubleLoopStr ;
existence
ex b1 being Ring st
( b1 is R -homomorphic & b1 is R -isomorphic )
proof end;
end;

registration
let R be Ring;
cluster non empty right_complementable well-unital V111() Abelian add-associative right_zeroed V133() R -monomorphic -> R -homomorphic for doubleLoopStr ;
coherence
for b1 being Ring st b1 is R -monomorphic holds
b1 is R -homomorphic ;
end;

registration
let R be Ring;
let S be R -homomorphic R -monomorphic Ring;
let h be Monomorphism of R,S;
cluster PolyHom h -> monomorphism ;
coherence
PolyHom h is RingMonomorphism
proof end;
end;

registration
let R be Ring;
let S be R -homomorphic R -isomorphic Ring;
let h be Isomorphism of R,S;
cluster PolyHom h -> isomorphism ;
coherence
PolyHom h is RingIsomorphism
proof end;
end;

theorem :: FIELD_1:29
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds deg ((PolyHom h) . p) <= deg p by Lm2, XREAL_1:6;

theorem :: FIELD_1:30
for R being non degenerated Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being non zero Element of the carrier of (Polynom-Ring R) holds
( deg ((PolyHom h) . p) = deg p iff h . (LC p) <> 0. S )
proof end;

theorem Th32: :: FIELD_1:31
for R being Ring
for S being b1 -homomorphic b1 -monomorphic Ring
for h being Monomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds deg ((PolyHom h) . p) = deg p
proof end;

theorem Th33: :: FIELD_1:32
for R being Ring
for S being b1 -homomorphic b1 -monomorphic Ring
for h being Monomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds LM ((PolyHom h) . p) = (PolyHom h) . (LM p)
proof end;

theorem Th34: :: FIELD_1:33
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R st a is_a_root_of p holds
h . a is_a_root_of (PolyHom h) . p
proof end;

theorem Th35: :: FIELD_1:34
for R being Ring
for S being b1 -homomorphic b1 -monomorphic Ring
for h being Monomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for a being Element of R holds
( a is_a_root_of p iff h . a is_a_root_of (PolyHom h) . p )
proof end;

theorem Th36: :: FIELD_1:35
for R being Ring
for S being b1 -homomorphic b1 -isomorphic Ring
for h being Isomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R)
for b being Element of S holds
( b is_a_root_of (PolyHom h) . p iff ex a being Element of R st
( a is_a_root_of p & h . a = b ) )
proof end;

theorem Th37: :: FIELD_1:36
for R being Ring
for S being b1 -homomorphic Ring
for h being Homomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds Roots p c= { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }
proof end;

theorem :: FIELD_1:37
for R being Ring
for S being b1 -homomorphic b1 -monomorphic Ring
for h being Monomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds Roots p = { a where a is Element of R : h . a in Roots ((PolyHom h) . p) }
proof end;

theorem Th39: :: FIELD_1:38
for R being Ring
for S being b1 -homomorphic b1 -isomorphic Ring
for h being Isomorphism of R,S
for p being Element of the carrier of (Polynom-Ring R) holds Roots ((PolyHom h) . p) = { (h . a) where a is Element of R : a in Roots p }
proof end;

definition
let F be Field;
let p be irreducible Element of the carrier of (Polynom-Ring F);
func KroneckerField (F,p) -> Field equals :: FIELD_1:def 3
(Polynom-Ring F) / ({p} -Ideal);
coherence
(Polynom-Ring F) / ({p} -Ideal) is Field ;
end;

:: deftheorem defines KroneckerField FIELD_1:def 3 :
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds KroneckerField (F,p) = (Polynom-Ring F) / ({p} -Ideal);

definition
let F be Field;
let p be irreducible Element of the carrier of (Polynom-Ring F);
func emb p -> Function of F,(KroneckerField (F,p)) equals :: FIELD_1:def 4
(canHom ({p} -Ideal)) * (canHom F);
coherence
(canHom ({p} -Ideal)) * (canHom F) is Function of F,(KroneckerField (F,p)) ;
end;

:: deftheorem defines emb FIELD_1:def 4 :
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds emb p = (canHom ({p} -Ideal)) * (canHom F);

registration
let F be Field;
let p be irreducible Element of the carrier of (Polynom-Ring F);
cluster emb p -> additive unity-preserving multiplicative ;
coherence
( emb p is additive & emb p is multiplicative & emb p is unity-preserving ) ;
end;

registration
let F be Field;
let p be irreducible Element of the carrier of (Polynom-Ring F);
cluster emb p -> monomorphism ;
coherence
emb p is RingMonomorphism ;
end;

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

definition
let F be Field;
let p be irreducible Element of the carrier of (Polynom-Ring F);
let f be Element of the carrier of (Polynom-Ring F);
func emb (f,p) -> Element of the carrier of (Polynom-Ring (KroneckerField (F,p))) equals :: FIELD_1:def 5
(PolyHom (emb p)) . f;
coherence
(PolyHom (emb p)) . f is Element of the carrier of (Polynom-Ring (KroneckerField (F,p))) ;
end;

:: deftheorem defines emb FIELD_1:def 5 :
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for f being Element of the carrier of (Polynom-Ring F) holds emb (f,p) = (PolyHom (emb p)) . f;

definition
let F be Field;
let p be irreducible Element of the carrier of (Polynom-Ring F);
func KrRoot p -> Element of (KroneckerField (F,p)) equals :: FIELD_1:def 6
 Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),<%(0. F),(1. F)%>);
coherence
Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),<%(0. F),(1. F)%>) is Element of (KroneckerField (F,p))
proof end;
end;

:: deftheorem defines KrRoot FIELD_1:def 6 :
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds KrRoot p = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),<%(0. F),(1. F)%>);

theorem Th40: :: FIELD_1:39
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for a being Element of F holds (emb p) . a = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(a | F))
proof end;

theorem Th41: :: FIELD_1:40
for n being Nat
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for f being Element of the carrier of (Polynom-Ring F) holds (emb (f,p)) . n = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),((f . n) | F))
proof end;

Lm5: for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for f being Element of the carrier of (Polynom-Ring F) holds eval ((LM (emb (f,p))),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),(LM f))
proof end;

theorem Th42: :: FIELD_1:41
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F)
for f being Element of the carrier of (Polynom-Ring F) holds eval ((emb (f,p)),(KrRoot p)) = Class ((EqRel ((Polynom-Ring F),({p} -Ideal))),f)
proof end;

theorem Th43: :: FIELD_1:42
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) holds KrRoot p is_a_root_of emb (p,p)
proof end;

theorem :: FIELD_1:43
for F being Field
for f being Element of the carrier of (Polynom-Ring F) st not f is constant holds
ex p being irreducible Element of the carrier of (Polynom-Ring F) st emb (f,p) is with_roots
proof end;

theorem Th45: :: FIELD_1:44
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) st emb p is isomorphism holds
p is with_roots
proof end;

theorem :: FIELD_1:45
for F being Field
for p being irreducible Element of the carrier of (Polynom-Ring F) st not p is with_roots holds
not emb p is isomorphism by Th45;