:: Some Algebraic Properties of Polynomial Rings
:: by Christoph Schwarzweller , Artur Korni{\l}owicz and Agnieszka Rowinska-Schwarzweller
::
:: Received June 30, 2016
:: Copyright (c) 2016-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_3, POLYNOM1, ARYTM_1, FUNCT_1, TARSKI, POLYNOM3, RELAT_1,
RLVECT_1, FINSEQ_1, GCD_1, ALGSEQ_1, REALSET1, FINSET_1, CARD_3, FDIFF_1,
FUNCT_4, ALGSTR_0, INT_1, WELLORD1, YELLOW_8, HURWITZ, ZFMISC_1,
XBOOLE_0, FUNCT_2, LATTICES, VECTSP10, XCMPLX_0, VECTSP_1, VECTSP_2,
MSALIMIT, STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, NUMBERS, CARD_1, MESFUNC1,
XXREAL_0, RATFUNC1, FUNCSDOM, GROUP_1, INT_2, INT_3, CAT_1, PARTFUN1,
POLYNOM2, POLYNOM5, QUOFIELD, BINOP_1, MSSUBFAM, MOD_4, IDEAL_1, RING_2,
WAYBEL_6, RING_3, RING_4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1,
ORDINAL1, FUNCT_2, QUOFIELD, BINOP_1, FINSEQ_1, REALSET1, FINSET_1,
VFUNCT_1, FUNCT_7, NORMSP_1, ALGSEQ_1, XCMPLX_0, XXREAL_0, NAT_D, INT_1,
INT_3, NUMBERS, STRUCT_0, MOD_4, GCD_1, ALGSTR_0, GROUP_1, GROUP_6,
RLVECT_1, VECTSP_1, VECTSP_2, VECTSP10, POLYNOM1, POLYNOM3, POLYNOM4,
POLYNOM5, HURWITZ, RATFUNC1, IDEAL_1, RINGCAT1, RING_1, RING_2, RING_3;
constructors POLYNOM4, POLYNOM5, HURWITZ, FUNCT_4, RELSET_1, RINGCAT1,
FUNCT_7, NAT_D, VFUNCT_1, RATFUNC1, GCD_1, REALSET1, FVSUM_1, RING_3,
ALGSEQ_1, BINOP_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0,
NAT_1, INT_1, MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, POLYNOM3, POLYNOM4,
POLYNOM5, FUNCT_2, ALGSTR_0, NAT_2, RLVECT_1, INT_3, CARD_1, RING_3,
VFUNCT_1, FINSET_1, RATFUNC1, RING_2, RING_1, REALSET1, MOD_4;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions STRUCT_0, VECTSP_1, GROUP_1, ALGSEQ_1, GROUP_6, RINGCAT1;
equalities STRUCT_0, HURWITZ, INT_3, POLYNOM3, REALSET1, ALGSTR_0, BINOP_1,
RATFUNC1;
expansions STRUCT_0, ALGSTR_0, TARSKI, GCD_1;
theorems GROUP_1, VECTSP_1, NAT_1, FUNCT_1, FUNCT_2, XREAL_1, INT_1, POLYNOM4,
FUNCT_7, ALGSEQ_1, NORMSP_1, TARSKI, POLYNOM3, FUNCOP_1, RING_2, RING_1,
POLYNOM1, POLYNOM5, XXREAL_0, FINSEQ_1, NAT_D, CARD_1, ORDINAL1,
RLVECT_1, POLYNOM2, PARTFUN1, HURWITZ, REALSET1, STRUCT_0, IDEAL_1,
RATFUNC1, GCD_1, RING_3, RINGCAT1, QUOFIELD, ALGSTR_0, ZFMISC_1,
VECTSP10, UPROOTS;
schemes NAT_1, FUNCT_2, BINOP_1;
begin :: Preliminaries
definition
let R be non empty doubleLoopStr,
a be Element of R;
redefine func {a} -> Subset of R; :: redefines { (TARSKI, definition)
coherence
proof
now let x be object;
assume x in {a};
then x = a by TARSKI:def 1;
hence x in the carrier of R;
end;
hence thesis by TARSKI:def 3;
end;
end;
registration
cluster almost_left_invertible commutative -> almost_right_invertible for Ring;
coherence
proof
let R be Ring;
assume AS: R is almost_left_invertible commutative;
now let x be Element of R;
assume x <> 0.R;
then x is left_invertible by AS;
then consider y being Element of R such that A1: y*x = 1.R;
x * y = 1.R by A1,AS,GROUP_1:def 12;
hence x is right_invertible;
end;
hence thesis;
end;
cluster almost_right_invertible commutative -> almost_left_invertible for Ring;
coherence
proof
let R be Ring;
assume AS: R is almost_right_invertible commutative;
now let x be Element of R;
assume x <> 0.R;
then x is right_invertible by AS;
then consider y being Element of R such that A1: x*y = 1.R;
y * x = 1.R by A1,AS,GROUP_1:def 12;
hence x is left_invertible;
end;
hence thesis;
end;
cluster almost_left_cancelable commutative -> almost_right_cancelable for Ring;
coherence
proof
let R be Ring;
assume AS: R is almost_left_cancelable commutative;
now let x be Element of R;
assume x <> 0.R;
then AS1: x is left_mult-cancelable by AS;
now let y,z be Element of R;
assume y * x = z * x;
then x * y = z * x by AS,GROUP_1:def 12 .= x * z by AS,GROUP_1:def 12;
hence y = z by AS1;
end;
hence x is right_mult-cancelable;
end;
hence thesis;
end;
cluster almost_right_cancelable commutative -> almost_left_cancelable for Ring;
coherence
proof
let R be Ring;
assume AS: R is almost_right_cancelable commutative;
now let x be Element of R;
assume x <> 0.R;
then AS1: x is right_mult-cancelable by AS;
now let y,z be Element of R;
assume x * y = x * z;
then y * x = x * z by AS,GROUP_1:def 12 .= z * x by AS,GROUP_1:def 12;
hence y = z by AS1;
end;
hence x is left_mult-cancelable;
end;
hence thesis;
end;
end;
definition
let L be non empty ZeroStr;
let X be set;
attr X is L-polynomial-membered means :polymem:
for p being object st p in X holds p is Polynomial of L;
end;
definition
let L be non empty ZeroStr;
let X be 1-sorted;
attr X is L-polynomial-membered means :polymem1:
the carrier of X is L-polynomial-membered;
end;
registration
let L be non empty ZeroStr;
cluster non empty L-polynomial-membered for set;
existence
proof
take s = {0_.(L)};
thus s is non empty;
thus s is L-polynomial-membered by TARSKI:def 1;
end;
end;
registration
let L be non empty ZeroStr;
cluster non empty L-polynomial-membered for 1-sorted;
existence
proof
take 1-sorted(#the non empty L-polynomial-membered set#);
thus thesis;
end;
end;
registration
let L be non empty ZeroStr;
let X be non empty L-polynomial-membered 1-sorted;
cluster the carrier of X -> L-polynomial-membered;
coherence by polymem1;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
non empty doubleLoopStr;
cluster Polynom-Ring L -> L-polynomial-membered;
coherence
proof
thus the carrier of Polynom-Ring L is L-polynomial-membered by POLYNOM3:def 10;
end;
end;
definition
let L be non empty ZeroStr;
let X be non empty L-polynomial-membered set;
redefine mode Element of X -> Polynomial of L; :: redefines Element (SUBSET_1, definition)
coherence by polymem;
end;
lm: now let L be add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr,
a be Element of Polynom-Ring L,p be Polynomial of L;
reconsider x = -p as Element of Polynom-Ring L by POLYNOM3:def 10;
assume a = p;
then a + x = p - p by POLYNOM3:def 10
.= 0_.(L) by POLYNOM3:29
.= 0.(Polynom-Ring(L)) by POLYNOM3:def 10;
then a = - x by RLVECT_1:6;
hence - a = -p;
end;
registration
let R be Ring;
cluster zero for Element of the carrier of Polynom-Ring R;
existence
proof
take 0_.(R);
thus thesis by POLYNOM3:def 10;
end;
cluster zero for Element of Polynom-Ring R;
existence
proof
take 0.(Polynom-Ring R);
thus thesis;
end;
cluster zero for Polynomial of R;
existence
proof
take 0_.(R);
thus thesis;
end;
end;
registration
let R be non degenerated Ring;
cluster non zero for Element of the carrier of Polynom-Ring R;
existence
proof
take 1_.(R);
thus thesis by POLYNOM3:def 10;
end;
cluster non zero for Element of Polynom-Ring R;
existence
proof
take 1.(Polynom-Ring R);
thus thesis;
end;
end;
T8a: for L being add-associative right_zeroed right_complementable
distributive non trivial doubleLoopStr,
p being Element of the carrier of Polynom-Ring L
holds deg p is Element of NAT iff p <> 0.Polynom-Ring L
proof
let L be add-associative right_zeroed right_complementable
distributive non trivial doubleLoopStr;
let p be Element of the carrier of Polynom-Ring L;
set R = Polynom-Ring L;
reconsider pp = p as Polynomial of L;
A: now assume deg p is Element of NAT;
then p <> 0_.(L) by HURWITZ:20;
hence p <> 0.R by POLYNOM3:def 10;
end;
now assume p <> 0.R;
then p <> 0_.(L) by POLYNOM3:def 10;
then len p <> 0 by POLYNOM4:5;
then len p + 1 > 0 + 1 by XREAL_1:6;
then len p >= 1 by NAT_1:13;
then len p - 1 >= 1 - 1 by XREAL_1:9;
hence deg p is Element of NAT by INT_1:3;
end;
hence thesis by A;
end;
T8b: for L being non empty ZeroStr, p being Polynomial of L
holds deg p is Element of NAT iff p <> 0_.(L)
proof
let L be non empty ZeroStr;let p be Polynomial of L;
now assume p <> 0_.(L);
then len p <> 0 by POLYNOM4:5;
then len p + 1 > 0 + 1 by XREAL_1:6;
then len p >= 1 by NAT_1:13;
then len p - 1 >= 1 - 1 by XREAL_1:9;
hence deg(p) is Element of NAT by INT_1:3;
end;
hence thesis by HURWITZ:20;
end;
definition
let L be add-associative right_zeroed right_complementable distributive
non empty doubleLoopStr;
let p,q be Polynomial of L;
pred p divides q means
ex a,b being Element of Polynom-Ring L st a = p & b = q & a divides b;
end;
theorem T2:
for L being add-associative right_zeroed right_complementable distributive
non empty doubleLoopStr
for p,q be Polynomial of L
holds p divides q iff ex r being Polynomial of L st p *' r = q
proof
let L be add-associative right_zeroed right_complementable distributive
non empty doubleLoopStr;
let p,q be Polynomial of L;
X: now assume p divides q;
then consider a,b being Element of Polynom-Ring L such that
B: a = p & b = q & a divides b;
consider u being Element of Polynom-Ring L such that
C: a * u = b by B;
reconsider z = u as Polynomial of L by POLYNOM3:def 10;
q = p *' z by B,C,POLYNOM3:def 10;
hence ex r being Polynomial of L st p *' r = q;
end;
now assume ex r being Polynomial of L st p *' r = q;
then consider r being Polynomial of L such that
H: q = p *' r;
reconsider a=p,b=q,u=r as Element of Polynom-Ring L by POLYNOM3:def 10;
b = a * u by H,POLYNOM3:def 10;
then a divides b;
hence p divides q;
end;
hence thesis by X;
end;
theorem div1:
for F being Field,
p,q being Polynomial of F st deg p < deg q holds p mod q = p
proof
let F be Field, p,q be Polynomial of F;
assume A1: deg p < deg q;
0_.(F) = 0.Polynom-Ring(F) by POLYNOM3:def 10; then
H: -(0_.(F)) = - 0.Polynom-Ring(F) by lm .= 0.Polynom-Ring(F);
A0: now assume A0: q = 0_.(F);
then deg p < - 1 by A1,HURWITZ:20;
hence contradiction by A0,A1,T8b;
end;
p = 0_.(F) + p by POLYNOM3:28 .= ((0_.(F)) *' q) + p by POLYNOM3:34;
hence p mod q = p - (0_.(F)) *' q by A0,A1,HURWITZ:def 5
.= p - 0_.(F) by POLYNOM3:34
.= p + 0_.(F) by H,POLYNOM3:def 10
.= p by POLYNOM3:28;
end;
div0: for F being Field, p,q being Polynomial of F
st q divides p holds (p div q) *' q = p
proof
let F be Field, p,q be Polynomial of F;
assume q divides p;
then consider r being Polynomial of F such that A2: q *' r = p by T2;
per cases;
suppose A3: q = 0_.(F);
thus (p div q) *' q = 0_.(F) by A3,POLYNOM3:34
.= p by A2,A3,POLYNOM3:34;
end;
suppose A3: q <> 0_.(F);
A4: p = q *' r + 0_.(F) by A2,POLYNOM3:28;
deg 0_.(F) = -1 by HURWITZ:20;
then deg 0_.(F) < deg q by T8b,A3;
hence (p div q) *' q = p by A2,A4,HURWITZ:def 5;
end;
end;
theorem div2:
for F being Field,
p,q being Polynomial of F holds p mod q = 0_.(F) iff q divides p
proof
let F be Field, p,q be Polynomial of F;
A: now assume p mod q = 0_.(F);
then (p div q) *' q
= (p - (p div q) *' q) + (p div q) *' q by POLYNOM3:28
.= p + (-((p div q) *' q) + (p div q) *' q) by POLYNOM3:26
.= p + ((p div q) *' q - (p div q) *' q)
.= p + 0_.(F) by POLYNOM3:29
.= p by POLYNOM3:28;
hence q divides p by T2;
end;
now assume A: q divides p;
thus p mod q = p - p by A,div0
.= 0_.(F) by POLYNOM3:29;
end;
hence thesis by A;
end;
theorem div5:
for F being Field,
p,q being Polynomial of F holds p = (p div q) *' q + (p mod q)
proof
let F be Field, p,q be Polynomial of F;
thus p = p + 0_.(F) by POLYNOM3:28
.= p + ((p div q) *' q - (p div q) *' q) by POLYNOM3:29
.= (p + -((p div q) *' q)) + (p div q) *' q by POLYNOM3:26
.= (p div q) *' q + (p mod q);
end;
theorem div4:
for F being Field,
p,r being Polynomial of F
for q being non zero Polynomial of F
holds (p + r) div q = (p div q) + (r div q) &
(p + r) mod q = (p mod q) + (r mod q)
proof
let F be Field, p,r be Polynomial of F;
let q be non zero Polynomial of F;
H: q <> 0_.(F);
A: p + r
= ((p div q) *' q + (p mod q)) + r by div5
.= ((p div q) *' q + (p mod q)) + ((r div q) *' q + (r mod q)) by div5
.= (p div q) *' q + ((p mod q) + ((r div q) *' q + (r mod q)))
by POLYNOM3:26
.= (p div q) *' q + (((p mod q) + (r mod q)) + ((r div q) *' q))
by POLYNOM3:26
.= ((p div q) *' q + (r div q) *' q) + ((p mod q) + (r mod q))
by POLYNOM3:26
.= ((p div q) + (r div q)) *' q + ((p mod q) + (r mod q))
by POLYNOM3:32;
B: deg((p mod q) + (r mod q)) <= max(deg(p mod q),deg(r mod q))
by HURWITZ:22;
C: deg(p mod q) < deg q by RING_2:29;
deg(r mod q) < deg q by RING_2:29;
then max(deg(p mod q),deg(r mod q)) < max(deg q,deg q) by C,XXREAL_0:27;
then D: deg((p mod q) + (r mod q)) < deg q by B,XXREAL_0:2;
hence (p + r) div q = (p div q) + (r div q) by A,H,HURWITZ:def 5;
thus (p + r) mod q
= ((p div q) + (r div q)) *' q + ((p mod q) + (r mod q)) -
(((p div q) + (r div q)) *' q) by D,A,H,HURWITZ:def 5
.= (((p div q) + (r div q)) *' q - (((p div q) + (r div q)) *' q)) +
((p mod q) + (r mod q)) by POLYNOM3:26
.= 0_.(F) + ((p mod q) + (r mod q)) by POLYNOM3:29
.= (p mod q) + (r mod q) by POLYNOM3:28;
end;
theorem div3a:
for F being Field,
p,r being Polynomial of F
for q being non zero Polynomial of F
holds (p *' r) mod q = ((p mod q) *' (r mod q)) mod q
proof
let F be Field, p,r be Polynomial of F;
let q be non zero Polynomial of F;
H1: (((p div q) *' q) *' ((r div q) *' q) + ((p div q) *' q) *' (r mod q))
= ((((p div q) *' q) *' (r div q))) *' q + ((p div q) *' q) *' (r mod q)
by POLYNOM3:33
.= q *' ((((p div q) *' q) *' (r div q))) + q *' ((p div q) *' (r mod q))
by POLYNOM3:33
.= q *' (((((p div q) *' q) *' (r div q))) + (p div q) *' (r mod q))
by POLYNOM3:31;
H2: (p mod q) *' ((r div q) *' q) = q *' ((p mod q) *' (r div q))
by POLYNOM3:33;
p *' r = ((p div q) *' q + (p mod q)) *' r by div5
.= ((p div q) *' q + (p mod q)) *' ((r div q) *' q + (r mod q)) by div5
.= ((p div q) *' q) *' ((r div q) *' q + (r mod q)) +
(p mod q) *' ((r div q) *' q + (r mod q)) by POLYNOM3:31
.= (((p div q) *' q) *' ((r div q) *' q) +
((p div q) *' q) *' (r mod q)) +
(p mod q) *' ((r div q) *' q + (r mod q)) by POLYNOM3:31
.= (((p div q) *' q) *' ((r div q) *' q) +
((p div q) *' q) *' (r mod q)) +
((p mod q) *' ((r div q) *' q) +
(p mod q) *' (r mod q)) by POLYNOM3:31;
hence (p *' r) mod q
= ((((p div q) *' q) *' ((r div q) *' q) +
((p div q) *' q) *' (r mod q)) mod q) +
(((p mod q) *' ((r div q) *' q) +
(p mod q) *' (r mod q)) mod q) by div4
.= 0_.(F) +
(((p mod q) *' ((r div q) *' q) +
(p mod q) *' (r mod q)) mod q) by div2,H1,T2
.= (((p mod q) *' ((r div q) *' q) +
(p mod q) *' (r mod q)) mod q) by POLYNOM3:28
.= (((p mod q) *' ((r div q) *' q)) mod q) +
(((p mod q) *' (r mod q)) mod q) by div4
.= 0_.(F) +
(((p mod q) *' (r mod q)) mod q) by div2,H2,T2
.= ((p mod q) *' (r mod q)) mod q by POLYNOM3:28;
end;
theorem div3:
for F being Field,
r,q,u being Polynomial of F
for p being non zero Polynomial of F
holds (((r *' q) mod p) *' u) mod p = (r *' q *' u) mod p
proof
let F be Field, r,q,u be Polynomial of F;
let p be non zero Polynomial of F;
A: (((r *' q) mod p) *' u) mod p
= ((r *' q) *' u + (-((r *' q) div p) *' p) *' u) mod p by POLYNOM3:32
.= (((r *' q) *' u) mod p) + (((-((r *' q) div p) *' p) *' u) mod p)
by div4;
(-((r *' q) div p) *' p) *' u
= (p *' (-((r *' q) div p))) *' u by HURWITZ:12
.= p *' ((-((r *' q) div p)) *' u) by POLYNOM3:33;
hence (((r *' q) mod p) *' u) mod p
= ((r *' q) *' u) mod p + 0_.(F) by A,div2,T2
.= (r *' q *' u) mod p by POLYNOM3:28;
end;
theorem
for L being add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr,
p being sequence of L
holds 0.L * p = 0_.(L)
proof
let L be add-associative right_zeroed right_complementable
left-distributive non empty doubleLoopStr,
p be sequence of L;
set t = 0.L * p;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
thus t.x = 0.L * (p.i) by POLYNOM5:def 4
.= (0_.(L)).x by FUNCOP_1:7;
end;
hence thesis by FUNCT_2:12;
end;
theorem poly2a:
for L being left_unital non empty doubleLoopStr,
p being sequence of L
holds 1.L * p = p
proof
let L be left_unital non empty doubleLoopStr,
p be sequence of L;
set t = 1.L * p;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
thus t.x = 1.L * (p.i) by POLYNOM5:def 4 .= p.x;
end;
hence thesis by FUNCT_2:12;
end;
theorem poly2:
for L being add-associative right_zeroed right_complementable right_unital
distributive associative commutative non empty doubleLoopStr,
p,q being sequence of L,
a being Element of L holds a * (p *' q) = p *' (a * q)
proof
let R be add-associative right_zeroed right_complementable right_unital
distributive associative commutative non empty doubleLoopStr,
p,q be sequence of R, a be Element of R;
set t = a * (p *' q);
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
consider F being FinSequence of the carrier of R such that
H1: len F = i+1 & (p*'q).i = Sum F &
for k being Element of NAT st k in dom F
holds F.k = p.(k-'1) * q.(i+1-'k) by POLYNOM3:def 9;
consider G being FinSequence of the carrier of R such that
H2: len G = i+1 & (p*'(a*q)).i = Sum G &
for k being Element of NAT st k in dom G
holds G.k = p.(k-'1) * (a*q).(i+1-'k) by POLYNOM3:def 9;
H3: dom F = Seg(i+1) by H1,FINSEQ_1:def 3 .= dom G by H2,FINSEQ_1:def 3;
now let x be object;
assume H4: x in dom F;
then reconsider j = x as Element of NAT;
H5: F.j = p.(j-'1) * q.(i+1-'j) by H4,H1;
G/.j = G.j by H3,H4,PARTFUN1:def 6
.= p.(j-'1) * (a*q).(i+1-'j) by H2,H4,H3
.= p.(j-'1) * (a * q.(i+1-'j)) by POLYNOM5:def 4
.= (p.(j-'1) * q.(i+1-'j)) * a by GROUP_1:def 3
.= a*(F/.j) by PARTFUN1:def 6,H5,H4;
hence G/.x = a * (F/.x);
end;
then G = a * F by H3,POLYNOM1:def 1;
then Sum G = a * (Sum F) by POLYNOM1:12;
hence t.x = (p *' (a * q)).x by H1,POLYNOM5:def 4,H2;
end;
hence thesis by FUNCT_2:12;
end;
theorem poly3:
for L being associative non empty multMagma,
p being sequence of L,
a,b being Element of L holds (a * b) * p = a * (b * p)
proof
let L be associative non empty multMagma,
p being sequence of L, a,b being Element of L;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
thus ((a * b) * p).x = (a * b) * (p.i) by POLYNOM5:def 4
.= a * (b * (p.i)) by GROUP_1:def 3
.= a * ((b * p).i) by POLYNOM5:def 4
.= (a * (b * p)).x by POLYNOM5:def 4;
end;
hence thesis by FUNCT_2:12;
end;
theorem poly1:
for L being add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr
for p being sequence of L holds (1_.(L)) *' p = p
proof
let R be add-associative right_zeroed right_complementable
left-distributive left_unital non empty doubleLoopStr,
p be sequence of R;
set q = 1_.(R);
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
consider F being FinSequence of the carrier of R such that
H: len F = i+1 & (q*'p).i = Sum F &
for k being Element of NAT st k in dom F
holds F.k = q.(k-'1) * p.(i+1-'k) by POLYNOM3:def 9;
D: now let j be Element of NAT;
assume B: j in dom F & j <> 1;
then j in Seg(len F) by FINSEQ_1:def 3;
then 1 <= j & j <= i+1 by H,FINSEQ_1:1;
then j > 1 by B,XXREAL_0:1;
then q.(j-'1) = 0.R by POLYNOM3:30,NAT_D:36;
hence 0.R = q.(j-'1) * p.(i+1-'j)
.= F.j by B,H
.= F/.j by B,PARTFUN1:def 6;
end;
G: dom F = Seg(i+1) by H,FINSEQ_1:def 3;
E: 1 <= 1 & 1 <= i + 1 by NAT_1:11; then
F: Sum F = F/.1 by D,POLYNOM2:3,G,FINSEQ_1:1;
F.1 = q.(1-'1) * p.(i+1-'1) by H,E,G,FINSEQ_1:1
.= q.0 * p.(i+1-'1) by XREAL_1:232
.= q.0 * p.i by NAT_D:34
.= 1.R * p.i by POLYNOM3:30
.= p.i;
hence (q*'p).x = p.x by E,H,F,PARTFUN1:def 6,G,FINSEQ_1:1;
end;
hence thesis by FUNCT_2:12;
end;
registration
let L be add-associative right_zeroed right_complementable well-unital
distributive non empty doubleLoopStr;
cluster Polynom-Ring L -> well-unital;
coherence
proof
set R = Polynom-Ring L;
now let x be Element of R;
reconsider p = x as Polynomial of L by POLYNOM3:def 10;
set e = 1.R;
A2: 1.R = 1_.L by POLYNOM3:def 10;
hence x*e = p*'1_.L by POLYNOM3:def 10 .= x by POLYNOM3:35;
thus e*x = (1_.L)*'p by A2,POLYNOM3:def 10 .= x by poly1;
end;
hence thesis by VECTSP_1:def 6;
end;
end;
begin :: Constant Polynomials
definition
let R be add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr;
let x be Element of the carrier of Polynom-Ring R;
attr x is constant means :defconst:
deg x <= 0;
end;
registration
let R be non degenerated Ring;
cluster non zero constant for Element of Polynom-Ring R;
existence
proof
reconsider a = 1_.(R) as Element of Polynom-Ring R
by POLYNOM3:def 10;
reconsider p = a as Element of the carrier of Polynom-Ring R;
take a;
thus a is non zero by POLYNOM3:def 10;
thus a is constant by RATFUNC1:def 2;
end;
cluster non zero constant for Element of the carrier of Polynom-Ring R;
existence
proof
reconsider a = 1_.(R) as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
take a;
thus a is non zero;
len 1_.(R) = 1 by POLYNOM4:4;
hence a is constant;
end;
end;
registration
let R be domRing;
cluster non constant for Element of Polynom-Ring R;
existence
proof
set p = rpoly(1,0.R) *' rpoly(1,0.R);
reconsider a = p as Element of Polynom-Ring R by POLYNOM3:def 10;
take a;
deg(rpoly(1,0.R) *' rpoly(1,0.R))
= deg rpoly(1,0.R) + deg rpoly(1,0.R) by HURWITZ:23
.= 1 + deg rpoly(1,0.R) by HURWITZ:27
.= 1 + 1 by HURWITZ:27;
hence a is non constant;
end;
cluster non constant for Element of the carrier of Polynom-Ring R;
existence
proof
set p = rpoly(1,0.R) *' rpoly(1,0.R);
reconsider a = p as Element of Polynom-Ring R by POLYNOM3:def 10;
take a;
deg(rpoly(1,0.R) *' rpoly(1,0.R))
= deg rpoly(1,0.R) + deg rpoly(1,0.R) by HURWITZ:23
.= 1 + deg rpoly(1,0.R) by HURWITZ:27
.= 1 + 1 by HURWITZ:27;
hence a is non constant;
end;
end;
definition
let L be non empty ZeroStr;
let a be Element of L;
func a|L -> sequence of L equals
0_.(L)+*(0,a);
coherence;
end;
registration
let L be non empty ZeroStr;
let a be Element of L;
cluster a|L -> finite-Support;
coherence
proof
take 1;
let i be Nat;
assume i >=1;
hence (a|L).i = (0_.(L)).i by FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
end;
Th28:
for L be non empty ZeroStr, a be Element of L
holds (a|L).0 = a & for n be Nat st n <> 0 holds (a|L).n = 0.L
proof
let L be non empty ZeroStr, a be Element of L;
0 in NAT; then 0 in dom 0_.(L) by FUNCT_2:def 1;
hence (a|L).0 = a by FUNCT_7:31;
let n be Nat;
assume n <> 0;
hence (a|L).n = (0_.(L)).n by FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
T6: for L being non empty ZeroStr holds (0.L)|L = 0_.L
proof
let L be non empty ZeroStr;
set p = (0.L)|L;
A2: now let x be object;
assume x in dom p;
then reconsider i = x as Element of NAT;
per cases;
suppose i = 0;
hence p.x = 0.L by Th28;
end;
suppose i <> 0;
hence p.x = 0.L by Th28;
end;
end;
dom p = NAT by NORMSP_1:12;
hence thesis by A2,FUNCOP_1:11;
end;
registration
let L be non empty ZeroStr;
let a be Element of L;
cluster a|L -> constant;
coherence
proof
per cases;
suppose a = 0.L;
then (a|L) = 0_.L by T6;
then len(a|L) = 0 by POLYNOM4:3;
then deg(a|L) = -1;
hence thesis by RATFUNC1:def 2;
end;
suppose A0: a <> 0.L;
A1: now let i be Nat;
assume that A2: i is_at_least_length_of a|L and
A3: 0+1 > i;
0 >= i by A3,NAT_1:13;
then (a|L).0 = 0.L by A2,ALGSEQ_1:def 2;
hence contradiction by A0,Th28;
end;
for i be Nat st i >= 1 holds (a|L).i = 0.L by Th28;
then len(a|L) = 1 by A1,ALGSEQ_1:def 3,ALGSEQ_1:def 2;
then deg(a|L) = 0;
hence thesis by RATFUNC1:def 2;
end;
end;
end;
registration
let L be non trivial ZeroStr;
let a be non zero Element of L;
cluster a|L -> non zero;
coherence
proof
(a|L).0 = a by Th28;
then (a|L) <> 0_.L by FUNCOP_1:7;
hence thesis by UPROOTS:def 5;
end;
end;
registration
let L be non trivial ZeroStr;
cluster non zero constant for Polynomial of L;
existence
proof
take (the non zero Element of L)|L;
thus thesis;
end;
end;
theorem
for L being non empty ZeroStr holds (0.L)|L = 0_.L by T6;
theorem
for L being non empty multLoopStr_0 holds (1.L)|L = 1_.(L);
registration
let L be non empty ZeroStr;
cluster (0.L)|L -> zero;
coherence by T6;
end;
registration
let L be non degenerated multLoopStr_0;
cluster (1.L)|L -> non zero;
coherence;
end;
theorem LX:
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr,
p being Element of the carrier of Polynom-Ring L
holds p is non zero constant iff deg p = 0
proof
let L be add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr,
p be Element of the carrier of Polynom-Ring L;
A: now assume AS: p is non zero constant;
now assume deg p <> 0;
then len p - 1 + 1 < 0 + 1 by AS,XREAL_1:6;
then len p = 0 by NAT_1:14;
then deg p = -1;
then p = 0_.(L) by HURWITZ:20;
hence contradiction by AS;
end;
hence deg p = 0;
end;
now assume AS: deg p = 0;
then p <> 0_.(L) by HURWITZ:20;
hence p is non zero by UPROOTS:def 5;
thus p is constant by AS;
end;
hence thesis by A;
end;
theorem LX1:
for L being add-associative right_zeroed right_complementable
right-distributive right_unital non empty doubleLoopStr,
a being Element of L holds a|L = a * 1_.(L)
proof
let L be add-associative right_zeroed right_complementable
right-distributive right_unital non empty doubleLoopStr,
a be Element of L;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
per cases;
suppose A: i = 0;
thus (a * 1_.(L)).x = a * (1_.(L)).i by POLYNOM5:def 4
.= a * 1.L by A,POLYNOM3:30
.= a
.= (a|L).x by Th28,A;
end;
suppose A: i > 0;
thus (a * 1_.(L)).x = a * (1_.(L)).i by POLYNOM5:def 4
.= a * 0.L by A,POLYNOM3:30
.= (a|L).x by Th28,A;
end;
end;
hence thesis by FUNCT_2:12;
end;
theorem T4a:
for R being Ring
for a,b being Element of R holds a|R + b|R = (a + b)|R
proof
let R be Ring, a,b be Element of R;
set p = (a|R) + (b|R), q = (a + b)|R;
A: dom p = NAT by FUNCT_2:def 1 .= dom q by FUNCT_2:def 1;
now let x be object;
assume x in dom q;
then reconsider i = x as Element of NAT;
B: p.i = (a|R).i + (b|R).i by NORMSP_1:def 2;
per cases;
suppose S: i = 0;
hence q.x = a + b by Th28
.= (a|R).i + b by S,Th28
.= p.x by B,S,Th28;
end;
suppose S: i <> 0;
hence q.x = 0.R by Th28
.= (a|R).i + 0.R by S,Th28
.= p.x by B,S,Th28;
end;
end;
hence thesis by A,FUNCT_1:2;
end;
theorem T4:
for R being Ring
for a,b being Element of R holds (a|R) *' (b|R) = (a * b)|R
proof
let R be Ring, a,b being Element of R;
set p = a|R, q = b|R;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
consider F being FinSequence of the carrier of R such that
H: len F = i+1 & (p*'q).i = Sum F &
for k being Element of NAT st k in dom F
holds F.k = p.(k-'1) * q.(i+1-'k) by POLYNOM3:def 9;
per cases;
suppose A: i = 0;
then 1 in Seg(len F) by H,FINSEQ_1:1;
then 1 in dom F by FINSEQ_1:def 3;
then F.1 = p.(0+1-'1) * q.(i+1-'1) by H
.= p.0 * q.(i+1-'1) by NAT_D:34
.= p.0 * q.0 by NAT_D:34,A
.= a * q.0 by Th28
.= a * b by Th28;
then F = <*a*b*> by FINSEQ_1:40,A,H;
hence (p*'q).x = a * b by H,RLVECT_1:44 .= (a * b)|R.x by A,Th28;
end;
suppose A: i > 0;
now let j be Element of NAT;
assume B: j in dom F;
then j in Seg(len F) by FINSEQ_1:def 3;
then C: 1 <= j & j <= i+1 by H,FINSEQ_1:1;
p.(j-'1) = 0.R or q.(i+1-'j) = 0.R
proof
assume p.(j-'1) <> 0.R;
then j <= 1 by NAT_D:36,Th28;
then j = 1 by C,XXREAL_0:1;
then i + 1 -'j = i by NAT_D:34;
hence q.(i+1-'j) = 0.R by A,Th28;
end;
hence 0.R = p.(j-'1) * q.(i+1-'j) .= F.j by B,H;
end;
hence (p*'q).x = 0.R by H,POLYNOM3:1 .= (a * b)|R.x by A,Th28;
end;
end;
hence thesis by FUNCT_2:12;
end;
theorem T9:
for R being Ring
for a,b being Element of R holds a|R = b|R iff a = b
proof
let R be Ring, a,b be Element of R;
now assume a|R = b|R;
hence a = (b|R).0 by Th28 .= b by Th28;
end;
hence thesis;
end;
theorem T11:
for R being Ring
for p being Element of the carrier of Polynom-Ring R
holds p is constant iff ex a being Element of R st p = a|R
proof
let L be Ring, p be Element of the carrier of Polynom-Ring L;
reconsider g = p as Polynomial of L;
now assume p is constant;
then AS: (len p) - 1 + 1 <= 0+1 by XREAL_1:6;
per cases by AS,NAT_1:25;
suppose len p = 0;
then p = 0_.(L) by POLYNOM4:5 .= (0.L)|L by T6;
hence ex a being Element of L st p = a|L;
end;
suppose AS: len p = 1;
set q = (p.0)|L;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
per cases;
suppose i = 0;
hence q.x = p.x by Th28;
end;
suppose B: i <> 0;
then i + 1 > 0 + 1 by XREAL_1:6;
then i >= len p by AS,NAT_1:13;
hence p.x = 0.L by ALGSEQ_1:8 .= q.x by B,Th28;
end;
end;
hence ex a being Element of L st p = a|L by FUNCT_2:12;
end;
end;
hence thesis by RATFUNC1:def 2;
end;
theorem T11a:
for R being Ring,
a being Element of R holds deg(a|R) = 0 iff a <> 0.R
proof
let L be Ring, a be Element of L;
now assume Y: a <> 0.L;
now assume deg(a|L) < 0;
then a|L = 0_.(L) by T8b .= (0.L)|L by T6;
hence contradiction by Y,T9;
end;
hence deg(a|L) = 0 by RATFUNC1:def 2;
end;
hence thesis by T8b,T6;
end;
begin :: Monic Polynomials
notation
let L be non empty doubleLoopStr;
let p be Polynomial of L;
synonym p is monic for p is normalized;
end;
registration
let L be non degenerated doubleLoopStr;
cluster 1_.(L) -> monic;
coherence
proof
len(1_.(L)) -' 1 = 1 -' 1 by POLYNOM4:4 .= 0 by XREAL_1:232;
then LC(1_.(L)) = 1.L by POLYNOM3:30;
hence 1_.(L) is monic by RATFUNC1:def 7;
end;
cluster 0_.(L) -> non monic;
coherence
proof
C: 1.L <> 0.L;
LC(0_.(L)) = 0.L by FUNCOP_1:7;
hence 0_.(L) is non monic by C,RATFUNC1:def 7;
end;
end;
registration
let L be non degenerated doubleLoopStr;
cluster monic for Polynomial of L;
existence
proof
1_.(L) is monic;
hence thesis;
end;
cluster non monic for Polynomial of L;
existence
proof
0_.(L) is non monic;
hence thesis;
end;
end;
registration
let L be add-associative right_zeroed right_complementable distributive
non degenerated doubleLoopStr;
cluster monic for Element of the carrier of Polynom-Ring L;
existence
proof
1_.(L) is Element of the carrier of Polynom-Ring L by POLYNOM3:def 10;
hence thesis;
end;
cluster non monic for Element of the carrier of Polynom-Ring L;
existence
proof
0_.(L) is Element of the carrier of Polynom-Ring L by POLYNOM3:def 10;
hence thesis;
end;
end;
registration
let L be well-unital non degenerated doubleLoopStr;
let x be Element of L;
cluster rpoly(1,x) -> monic;
coherence
proof
set p = rpoly(1,x);
1 = deg p by HURWITZ:27 .= len(p) - 1;
then 1 + 1 = len p;
then len(p) -' 1 = 1 by NAT_D:34;
then LC p = 1.L by HURWITZ:25;
hence p is monic by RATFUNC1:def 7;
end;
end;
definition
let L be Field;
let p be Element of the carrier of Polynom-Ring L;
redefine func NormPolynomial p -> Element of the carrier of Polynom-Ring L; :: redefines NormPolynomial (POLYNOM5, definition)
coherence by POLYNOM3:def 10;
end;
registration
let F be Field;
let p be non zero Polynomial of F;
cluster NormPolynomial p -> monic;
coherence;
end;
registration
let L be Field;
let p be non zero Element of the carrier of Polynom-Ring L;
cluster NormPolynomial p -> monic;
coherence;
end;
theorem npl0:
for F being Field holds NormPolynomial(0_.(F)) = 0_.(F)
proof
let F be Field;
set q = 0_.(F); set p = NormPolynomial q;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
p.i = q.i / q.(len q-'1) by POLYNOM5:def 11
.= 0.F * (q.(len q-'1))" by FUNCOP_1:7
.= q.i by FUNCOP_1:7;
hence p.x = q.x;
end;
hence thesis by FUNCT_2:12;
end;
theorem npl:
for F being Field,
p being non zero Element of the carrier of Polynom-Ring F
holds NormPolynomial p = (LC p)" * p
proof
let F be Field,
p be non zero Element of the carrier of Polynom-Ring F;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
thus ((LC p)" * p).x = (LC p)" * (p.i) by POLYNOM5:def 4
.= p.i / p.(len p-'1)
.= (NormPolynomial p).x by POLYNOM5:def 11;
end;
hence thesis by FUNCT_2:12;
end;
theorem
for F being Field,
p being non zero Element of the carrier of Polynom-Ring F
holds p is monic iff NormPolynomial p = p
proof
let F be Field,
p be non zero Element of the carrier of Polynom-Ring F;
hereby assume p is monic;
then LC p = 1.F by RATFUNC1:def 7;
hence NormPolynomial p = (1.F)" * p by npl .= p by poly2a;
end;
thus thesis;
end;
theorem np1:
for F being Field,
p,q being Element of the carrier of Polynom-Ring F
holds q divides p iff NormPolynomial(q) divides p
proof
let F be Field, p,q being Element of the carrier of Polynom-Ring F;
per cases;
suppose q = 0_.(F);
hence thesis by npl0;
end;
suppose AS: q <> 0_.(F);
then AS1: q is non zero by UPROOTS:def 5;
A: now assume q divides p;
then consider r being Polynomial of F such that
A1: p = q *' r by T2;
set a = (LC q)";
reconsider qq = NormPolynomial(q) as Polynomial of F;
q is non zero by AS,UPROOTS:def 5; then
LC q <> 0.F; then
(LC q)" * (LC q) = 1.F by VECTSP_1:def 10; then
a <> 0.F; then
a" * a = 1.F by VECTSP_1:def 10; then
p = (a * a") * p by poly2a
.= (a * (a" * (q *' r))) by A1,poly3
.= (a * (q *' (a" * r))) by poly2
.= (a * q) *' (a" * r) by poly2
.= qq *' (a" * r) by AS1,npl;
hence NormPolynomial(q) divides p by T2;
end;
now assume A0: NormPolynomial(q) divides p;
reconsider qq = NormPolynomial(q) as Polynomial of F;
consider r being Polynomial of F such that
A1: p = qq *' r by A0,T2;
p = ((LC q)" * q) *' r by AS1,A1,npl
.= (LC q)" * (q *' r) by poly2
.= q *' ((LC q)" * r) by poly2;
hence q divides p by T2;
end;
hence thesis by A;
end;
end;
theorem np2:
for F being Field,
p,q being Element of the carrier of Polynom-Ring F
holds q divides p iff q divides NormPolynomial(p)
proof
let F be Field, p,q being Element of the carrier of Polynom-Ring F;
per cases;
suppose p = 0_.(F);
hence thesis by npl0;
end;
suppose AS: p <> 0_.(F);
then AS1: p is non zero by UPROOTS:def 5;
A: now assume q divides p;
then consider r being Polynomial of F such that
A1: p = q *' r by T2;
set a = (LC p)";
NormPolynomial p = a * (q *' r) by AS1,A1,npl
.= q *' (a * r) by poly2;
hence q divides NormPolynomial(p) by T2;
end;
now assume q divides NormPolynomial(p);
then consider r being Polynomial of F such that
A1: NormPolynomial(p) = q *' r by T2;
set a = (LC p)";
p is non zero by AS,UPROOTS:def 5; then
LC p <> 0.F; then
(LC p)" * (LC p) = 1.F by VECTSP_1:def 10; then
a <> 0.F; then
a" * a = 1.F by VECTSP_1:def 10; then
p = (a" * a) * p by poly2a
.= a" * (a * p) by poly3
.= a" * (q *' r) by AS1,A1,npl
.= q *' (a" * r) by poly2;
hence q divides p by T2;
end;
hence thesis by A;
end;
end;
theorem np3:
for F being Field,
p being Element of the carrier of Polynom-Ring F
holds NormPolynomial(p) is_associated_to p
proof
let F be Field, p be Element of the carrier of Polynom-Ring F;
reconsider a = p, b = NormPolynomial(p) as Element of Polynom-Ring F;
A: p *' 1_.(F) = p by POLYNOM3:35;
then B: p divides NormPolynomial(p) by T2,np2;
NormPolynomial(p) divides p by A,np1,T2;
hence thesis by B;
end;
theorem thirr2:
for F being Field,
p being Element of the carrier of Polynom-Ring F
holds NormPolynomial(p) is irreducible iff p is irreducible
proof
let F be Field, p be Element of the carrier of Polynom-Ring F;
now assume B: NormPolynomial p is irreducible;
NormPolynomial p is_associated_to p by np3;
hence p is irreducible by B, RING_2:23;
end;
hence thesis by np3,RING_2:23;
end;
theorem np00:
for R being domRing,
p,q being Element of the carrier of Polynom-Ring R
holds p is_associated_to q implies deg p = deg q
proof
let R be domRing,
p,q be Element of the carrier of Polynom-Ring R;
assume A: p is_associated_to q;
then consider c being Element of Polynom-Ring R such that
K2: q = p * c by GCD_1:def 1;
reconsider r = c as Element of the carrier of Polynom-Ring R;
consider d being Element of Polynom-Ring R such that
K3: p = q * d by A,GCD_1:def 1;
reconsider s = d as Element of the carrier of Polynom-Ring R;
K4: q = p *' r by K2,POLYNOM3:def 10;
K5: p = q *' s by K3,POLYNOM3:def 10;
per cases;
suppose p = 0_.(R);
hence thesis by K4,POLYNOM3:34;
end;
suppose q = 0_.(R);
hence thesis by K5,POLYNOM3:34;
end;
suppose A: p <> 0_.(R) & q <> 0_.(R);
then A1: r <> 0_.(R) & s <> 0_.(R) by K4,K5,POLYNOM3:34;
then A2: deg r is Element of NAT & deg s is Element of NAT by T8b;
A3: deg q = deg p + deg r & deg p = deg q + deg s
by A,A1,K4,K5,HURWITZ:23;
then deg r + deg s = 0;
then deg r = 0 & deg s = 0 by A2;
hence thesis by A3;
end;
end;
theorem np0:
for R being domRing,
p,q being monic Element of the carrier of Polynom-Ring R
holds p is_associated_to q iff p = q
proof
let R be domRing,
p,q be monic Element of the carrier of Polynom-Ring R;
K1: LC p = 1.R & LC q = 1.R by RATFUNC1:def 7;
now assume AS: p is_associated_to q;
then consider c being Element of Polynom-Ring R such that
K2: q = p * c by GCD_1:def 1;
reconsider r = c as Element of the carrier of Polynom-Ring R;
K3: q = p *' r by K2,POLYNOM3:def 10;
r <> 0_.(R) by K3,POLYNOM3:34;
then deg q = deg p + deg r by K3,HURWITZ:23
.= deg q + deg r by AS,np00;
then r is constant;
then consider a being Element of R such that K5: r = a|R by T11;
X: deg p = deg q by AS,np00;
r = a * 1_.(R) by K5,LX1;
then q = a * (p *' 1_.(R)) by K3,poly2 .= a * p by poly1;
then q.(len q-'1) = a * 1.R by X,K1,POLYNOM5:def 4
.= a;
then r = 1_.(R) by K5,K1;
hence p = q by K3,poly1;
end;
hence thesis;
end;
begin :: Canonical Homomorphism from R into R[X]
definition
let R be Ring;
func canHom R -> Function of R, Polynom-Ring R means :defcanhom:
for x being Element of R holds it.x = x|R;
existence
proof
set B = Polynom-Ring R;
defpred P[object,object] means
ex a being Element of R st $1 = a & $2 = a|R;
X: for x being object st x in the carrier of R
ex y being object st y in the carrier of B & P[x,y]
proof
let x be object;
assume x in the carrier of R;
then reconsider a = x as Element of R;
reconsider y = a|R as Element of B by POLYNOM3:def 10;
take y;
thus thesis;
end;
consider g being Function of the carrier of R,the carrier of B
such that
Z: for x being object st x in the carrier of R holds P[x,g.x]
from FUNCT_2:sch 1(X);
now let x be Element of R;
consider a being Element of R such that H: x = a & g.x = a|R by Z;
thus g.x = x|R by H;
end;
then consider f being Function of R,B such that
Y: for x being Element of R holds f.x = x|R;
take f;
thus thesis by Y;
end;
uniqueness
proof
set B = Polynom-Ring R;
let g1,g2 be Function of R,B such that
A1: for a being Element of R holds g1.a = a|R and
A2: for a being Element of R holds g2.a = a|R;
A: dom g1 = the carrier of R by FUNCT_2:def 1
.= dom g2 by FUNCT_2:def 1;
now let x be object;
assume x in dom g1;
then reconsider a = x as Element of R;
thus g1.x = a|R by A1 .= g2.x by A2;
end;
hence thesis by A,FUNCT_1:2;
end;
end;
registration
let R be Ring;
cluster canHom R -> additive multiplicative unity-preserving;
coherence
proof
set f = canHom R;
hereby
let x,y be Element of R;
f.x = x|R & f.y = y|R by defcanhom;
hence f.x + f.y = (x|R) + (y|R) by POLYNOM3:def 10
.= (x + y)|R by T4a
.= f.(x+y) by defcanhom;
end;
hereby
let x,y be Element of R;
f.x = x|R & f.y = y|R by defcanhom;
hence f.x * f.y = (x|R) *' (y|R) by POLYNOM3:def 10
.= (x * y)|R by T4
.= f.(x*y) by defcanhom;
end;
thus f.1_R = (1.R)|R by defcanhom
.= 1_.(R)
.= 1_(Polynom-Ring R) by POLYNOM3:def 10;
end;
end;
registration
let R be Ring;
cluster canHom R -> monomorphism;
coherence
proof
set f = canHom R;
A: f is linear by RINGCAT1:def 1;
now let x1,x2 be object;
assume AS: x1 in the carrier of R & x2 in the carrier of R & f.x1 = f.x2;
then reconsider a = x1, b = x2 as Element of R;
a|R = f.x2 by AS,defcanhom .= b|R by defcanhom;
hence x1 = x2 by T9;
end;
then f is one-to-one by FUNCT_2:19;
hence thesis by A;
end;
end;
registration
let R be Ring;
cluster Polynom-Ring R -> R-homomorphic R-monomorphic;
coherence
proof
A: canHom R is additive multiplicative unity-preserving monomorphism;
hence Polynom-Ring R is R-homomorphic by RING_2:def 4;
thus thesis by A,RING_3:def 3;
end;
end;
theorem
for R being Ring holds Char(Polynom-Ring R) = Char R by RING_3:88;
registration
let R be non degenerated Ring;
cluster Polynom-Ring R -> infinite;
coherence
proof
set PR = Polynom-Ring R;
defpred P[Element of NAT,object] means $2 = rpoly($1,0.R);
A0: for x be Element of NAT
ex y being Element of the carrier of PR st P[x,y]
proof
let x be Element of NAT;
take rpoly(x,0.R);
thus thesis by POLYNOM3:def 10;
end;
consider f being Function of NAT,the carrier of PR such that
A1: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A0);
A2: dom f = NAT by FUNCT_2:def 1;
now let x1,x2 be object;
assume A3: x1 in NAT & x2 in NAT & f.x1 = f.x2;
then reconsider n = x1, m = x2 as Element of NAT;
rpoly(n,0.R) = f.m by A1,A3 .= rpoly(m,0.R) by A1;
then n = deg(rpoly(m,0.R)) by HURWITZ:27 .= m by HURWITZ:27;
hence x1 = x2;
end;
then f is one-to-one by FUNCT_2:19;
then rng f is infinite by A2,CARD_1:59;
hence thesis;
end;
end;
registration
cluster -> infinite for 0-characteristic Ring;
coherence
proof
let R be 0-characteristic Ring; set f = canHom_Int R;
dom f = the carrier of INT.Ring by FUNCT_2:def 1;
then rng f is infinite by CARD_1:59;
hence thesis;
end;
end;
theorem
for R being Ring st Char R = 0 holds R is infinite
proof
let R be Ring; assume Char R = 0;
then R is 0-characteristic by RING_3:def 6;
hence thesis;
end;
registration
let n be non trivial Nat;
cluster Polynom-Ring(Z/n) -> infinite;
coherence;
end;
theorem
for n being non trivial Nat holds Char Polynom-Ring(Z/n) <> 0;
registration
let n be non trivial Nat;
cluster n-characteristic infinite for Ring;
existence
proof
take Polynom-Ring(Z/n);
thus thesis;
end;
end;
begin :: Units and Irreducible Polynomials
lemr: for R being domRing holds Polynom-Ring R is non almost_left_invertible
proof
let R be domRing; set PR = Polynom-Ring R;
reconsider p = rpoly(2,0.R) as Element of the carrier of PR by POLYNOM3:def 10;
A3: p <> 0.PR by POLYNOM3:def 10;
now assume ex q being Element of PR st q*p = 1.PR;
then consider q being Element of PR such that A1: q*p = 1.PR;
A9: q <> 0.PR by A1;
reconsider q as Element of the carrier of PR;
A4: q <> 0_.(R) by A9,POLYNOM3:def 10;
then A5: deg q is Element of NAT by T8b;
q *' p = 1.PR by A1,POLYNOM3:def 10
.= 1_.(R) by POLYNOM3:def 10;
then A2: deg q + deg p = deg(1_.(R)) by A4,HURWITZ:23;
A8: len(1_.(R)) = 1 by POLYNOM4:4;
deg p = 2 by HURWITZ:27;
hence contradiction by A5,A8,A2;
end;
then not p is left_invertible;
hence PR is non almost_left_invertible by A3;
end;
registration
cluster non almost_left_invertible for domRing;
existence
proof
take Polynom-Ring the Field;
thus thesis by lemr;
end;
end;
lemf:
for R being domRing holds
R is Field iff for a being NonUnit of R holds a = 0.R
proof
let R be domRing;
A: now assume R is Field;
then B: R is almost_left_invertible;
let a be NonUnit of R;
now assume a <> 0.R;
then consider b being Element of R such that
C: b * a = 1.R by B,ALGSTR_0:def 27;
a divides 1.R by C;
hence contradiction by GCD_1:def 20;
end;
hence a = 0.R;
end;
now assume B: for a being NonUnit of R holds a = 0.R;
now let a be Element of R;
assume a <> 0.R;
then a is Unit of R by B;
then a divides 1.R by GCD_1:def 20;
then consider b being Element of R such that C: a * b = 1.R;
thus a is left_invertible by C;
end;
then R is almost_left_invertible;
hence R is Field;
end;
hence thesis by A;
end;
registration
let R be non almost_left_invertible domRing;
cluster non zero for NonUnit of R;
existence
proof
consider a being NonUnit of R such that H: a <> 0.R by lemf;
a is non zero by H;
hence thesis;
end;
end;
registration
cluster INT.Ring -> non almost_left_invertible;
coherence
proof
set R = INT.Ring; set a = 1.R + 1.R;
now assume ex y being Element of R st y*a = 1.R;
then consider y being Element of R such that A1: y*a = 1.R;
reconsider i = y as Integer;
consider k being Nat such that
A2: k = 1 * 2" or -k = 1 * 2" by A1,INT_1:def 1;
thus contradiction by A2,NAT_1:14;
end;
then not a is left_invertible;
hence R is non almost_left_invertible;
end;
end;
registration
let R be domRing;
cluster Polynom-Ring R -> non almost_left_invertible;
coherence by lemr;
end;
theorem
for R being domRing holds
R is Field iff for a being NonUnit of R holds a = 0.R by lemf;
theorem Th90:
for R being domRing,
a being Element of R
holds a|R is Unit of Polynom-Ring R iff a is Unit of R
proof
let L be domRing, a be Element of L;
set R = Polynom-Ring L;
H1: 1.R = 1_.(L) by POLYNOM3:def 10;
reconsider p = a|L as Element of Polynom-Ring L
by POLYNOM3:def 10;
A: now assume AS: p is Unit of R;
then (a|L) divides 1_.(L) by H1,GCD_1:def 20;
then consider q being Polynomial of L such that
H3: (a|L) *' q = 1_.(L) by T2;
reconsider qq = q as Element of R by POLYNOM3:def 10;
p <> 0.R by AS; then
H4: a|L <> 0_.(L) by POLYNOM3:def 10;
q <> 0_.(L) by H3,POLYNOM3:34; then
H6: deg(a|L) + deg(q) = deg(1_.(L)) by H3,H4,HURWITZ:23
.= 1 - 1 by POLYNOM4:4;
deg(a|L) is Element of NAT by H4,T8b;
then qq is constant by H6;
then consider b being Element of L such that H5: qq = b|L by T11;
(a*b)|L = (1.L)|L by H3,H5,T4;
then a divides 1.L by T9;
hence a is Unit of L by GCD_1:def 20;
end;
now assume a is Unit of L;
then a divides 1.L by GCD_1:def 20;
then consider b being Element of L such that
H3: a * b = 1.L;
(a|L) *' (b|L) = (1.L)|L by T4,H3 .= 1_.(L);
then (a|L) divides 1_.(L) by T2;
hence p is Unit of R by H1,GCD_1:def 20;
end;
hence thesis by A;
end;
theorem T88:
for F being domRing, p being Element of the carrier of Polynom-Ring F
holds p is Unit of Polynom-Ring F implies deg p = 0
proof
let L be domRing;
let p be Element of the carrier of Polynom-Ring L;
set R = Polynom-Ring L;
H: 1.R = 1_.(L) by POLYNOM3:def 10;
assume AS: p is Unit of R;
then H0: p <> 0.R;
then H1: p <> 0_.(L) by POLYNOM3:def 10;
reconsider degp = deg p as Element of NAT by H0,T8a;
p divides 1_.(L) by AS,H,GCD_1:def 20;
then consider t being Polynomial of L such that
H3: p *' t = 1_.(L) by T2;
reconsider t as Element of the carrier of R by POLYNOM3:def 10;
H5: t <> 0_.(L) by POLYNOM3:34,H3;
then t <> 0.R by POLYNOM3:def 10;
then reconsider degt = deg t as Element of NAT by T8a;
degt + degp = deg(1_.(L)) by H1,H3,H5,HURWITZ:23
.= 1 - 1 by POLYNOM4:4;
hence deg p = 0;
end;
theorem T8:
for F being Field, p being Element of the carrier of Polynom-Ring F
holds p is Unit of Polynom-Ring F iff deg p = 0
proof
let L be Field;
let p be Element of the carrier of Polynom-Ring L;
set R = Polynom-Ring L;
H: 1.R = 1_.(L) by POLYNOM3:def 10;
A: now assume AS: p is Unit of R;
then H0: p <> 0.R;
then H1: p <> 0_.(L) by POLYNOM3:def 10;
reconsider degp = deg p as Element of NAT by H0,T8a;
p divides 1_.(L) by AS,H,GCD_1:def 20;
then consider t being Polynomial of L such that
H3: p *' t = 1_.(L) by T2;
reconsider t as Element of the carrier of R by POLYNOM3:def 10;
H5: t <> 0_.(L) by POLYNOM3:34,H3;
then t <> 0.R by POLYNOM3:def 10;
then reconsider degt = deg t as Element of NAT by T8a;
degt + degp = deg(1_.(L)) by H1,H3,H5,HURWITZ:23
.= 1 - 1 by POLYNOM4:4;
hence deg p = 0;
end;
now assume AS: deg p = 0;
then AS1: p <> 0_.(L) by HURWITZ:20;
p <> 0.R by AS1,POLYNOM3:def 10;
then reconsider degp = deg p as Nat by T8a;
p is constant by AS;
then consider a being Element of L such that X: p = a|L by T11;
H3: a <> 0.L by X,AS,HURWITZ:20,UPROOTS:def 5;
set t = (a")|L;
t *' p = (a" * a) | L by X,T4
.= 1_.(L) by H3,VECTSP_1:def 10;
then p divides 1_.(L) by T2;
hence p is Unit of R by H,GCD_1:def 20;
end;
hence thesis by A;
end;
theorem
for R being domRing,
p being Element of the carrier of Polynom-Ring R
holds p is Unit of Polynom-Ring R implies p is non zero constant
proof
let F be domRing, p be Element of the carrier of Polynom-Ring F;
p is Unit of Polynom-Ring F implies deg p = 0 by T88;
hence thesis by LX;
end;
theorem
for F being Field,
p being Element of the carrier of Polynom-Ring F
holds p is Unit of Polynom-Ring F iff p is non zero constant
proof
let F be Field, p be Element of the carrier of Polynom-Ring F;
p is Unit of Polynom-Ring F iff deg p = 0 by T8;
hence thesis by LX;
end;
registration
let R be domRing;
cluster non constant -> non zero non unital for Element of Polynom-Ring R;
coherence
proof
let a be Element of Polynom-Ring R;
reconsider p = a as Element of the carrier of Polynom-Ring R;
assume AS: a is non constant;
then A: deg p > 0;
now assume a = 0.(Polynom-Ring R);
then p = 0_.(R) by POLYNOM3:def 10;
then len p = 0 by POLYNOM4:3;
hence contradiction by A;
end;
hence a is non zero;
thus a is non unital by AS,T88;
end;
end;
registration
let F be domRing;
cluster non constant -> non zero non unital
for Element of the carrier of Polynom-Ring F;
coherence
proof
let a be Element of the carrier of Polynom-Ring F;
assume AS: a is non constant;
now assume a = 0_.(F);
then len a = 0 by POLYNOM4:3;
hence contradiction by AS;
end;
hence a is non zero by UPROOTS:def 5;
thus a is non unital by AS;
end;
end;
registration
let F be Field;
cluster non zero constant -> unital for Element of Polynom-Ring F;
coherence
proof
let p be Element of Polynom-Ring F;
assume AS: p is non zero constant;
then A: p <> 0_.(F) by POLYNOM3:def 10;
reconsider pp = p as Element of the carrier of Polynom-Ring F;
pp is non zero by A,UPROOTS:def 5; then deg pp = 0 by AS;
hence p is unital by T8;
end;
cluster unital -> non zero constant for Element of Polynom-Ring F;
coherence;
end;
registration
let F be Field;
cluster non zero constant -> unital
for Element of the carrier of Polynom-Ring F;
coherence
proof
let p be Element of the carrier of Polynom-Ring F;
assume p is non zero constant;
then deg p = 0;
hence p is unital by T8;
end;
cluster unital -> non zero constant
for Element of the carrier of Polynom-Ring F;
coherence
proof
let a be Element of the carrier of Polynom-Ring F;
reconsider p = a as Element of Polynom-Ring F;
assume AS: a is unital;
then deg a = 0 by T88;
then a <> 0_.(F) by HURWITZ:20;
hence a is non zero by UPROOTS:def 5;
thus thesis by AS;
end;
end;
theorem T88a:
for R being domRing
for p being Element of the carrier of Polynom-Ring R
holds (ex q being Element of the carrier of Polynom-Ring R
st q divides p & 1 <= deg q & deg q < deg p)
implies p is reducible
proof
let R be domRing, p be Element of the carrier of Polynom-Ring R;
set K = Polynom-Ring R;
reconsider pp = p as Polynomial of R;
assume ex q being Element of the carrier of Polynom-Ring R
st q divides p & 1 <= deg q & deg q < deg p;
then consider q being Element of the carrier of Polynom-Ring R such that
A0: q divides p & 1 <= deg q & deg q < deg p;
A1: not q is Unit of K by T88,A0;
now assume q is_associated_to p;
then consider r being Element of K such that
A2: r is unital & q * r = p by GCD_1:18;
reconsider rr = r as Element of the carrier of K;
A5: p = q *' rr by A2,POLYNOM3:def 10;
then A4: r <> 0_.(R) by HURWITZ:20,A0,POLYNOM3:34;
q <> 0_.(R) by A5,A0,POLYNOM3:34;
then deg p = deg q + deg rr by A4,A5,HURWITZ:23 .= deg q + 0 by A2,T88;
hence contradiction by A0;
end;
hence p is reducible by A0,A1,RING_2:def 9;
end;
theorem T88b:
for F being Field
for p being Element of the carrier of Polynom-Ring F
holds p is reducible iff
(p = 0_.(F) or p is Unit of Polynom-Ring F or
ex q being Element of the carrier of Polynom-Ring F
st q divides p & 1 <= deg q & deg q < deg p)
proof
let R be Field, p be Element of the carrier of Polynom-Ring R;
set K = Polynom-Ring R;
reconsider pp = p as Polynomial of R;
A: now assume p is reducible;
then AS: p = 0.K or p is Unit of K or
ex a being Element of K st a divides p &
not(a is Unit of K) & not(a is_associated_to p) by RING_2:def 9;
thus p = 0_.(R) or p is Unit of Polynom-Ring R or
ex q being Element of the carrier of Polynom-Ring R
st q divides p & 1 <= deg q & deg q < deg p
proof
assume A0: not(p = 0_.(R)) & not(p is Unit of K);
then consider a being Element of K such that
A1: a divides p & not(a is Unit of K) & not(a is_associated_to p)
by AS,POLYNOM3:def 10;
reconsider q = a as Polynomial of R by POLYNOM3:def 10;
q divides pp by A1; then
consider r being Polynomial of R such that
A2: pp = q *' r by T2;
reconsider rr = r as Element of K by POLYNOM3:def 10;
A10: p = a * rr by A2,POLYNOM3:def 10;
A5: q <> 0_.(R) by A0,A2,POLYNOM3:34;
A6: r <> 0_.(R) by A0,A2,POLYNOM3:34;
then A9: deg p = (deg q) + (deg r) by A2,A5,HURWITZ:23;
A11: deg q is Element of NAT & deg r is Element of NAT by A5,A6,T8b;
then A7: deg q <= deg p by A9,NAT_1:11;
A3: now assume deg q = deg p;
then rr is Unit of K by A9,T8;
hence contradiction by A1,A10,GCD_1:18;
end;
thus ex b being Element of the carrier of K
st b divides p & 1 <= deg b & deg b < deg p
proof
reconsider qq = q as Element of the carrier of K;
take qq;
thus qq divides p by A1;
thus 1 <= deg qq by A1,A11,T8,NAT_1:14;
thus deg qq < deg p by A3,A7,XXREAL_0:1;
end;
end;
end;
now assume AS: p = 0_.(R) or p is Unit of Polynom-Ring R or
ex q being Element of the carrier of Polynom-Ring R
st q divides p & 1 <= deg q & deg q < deg p;
per cases by AS;
suppose p = 0_.(R);
then p = 0.K by POLYNOM3:def 10;
hence p is reducible;
end;
suppose p is Unit of Polynom-Ring R;
hence p is reducible;
end;
suppose ex q being Element of the carrier of Polynom-Ring R
st q divides p & 1 <= deg q & deg q < deg p;
hence p is reducible by T88a;
end;
end;
hence thesis by A;
end;
theorem thirr0:
for R being domRing,
p being monic Element of the carrier of Polynom-Ring R
st deg p = 1 holds p is irreducible
proof
let R be domRing, p be monic Element of the carrier of Polynom-Ring R;
set K = Polynom-Ring R;
reconsider x = p as Element of K;
assume AS: deg p = 1;
then len p -' 1 = 1 + 1 -' 1 .= 1 by NAT_D:34;
then LC p = p.1;
then E: p.1 = 1.R by RATFUNC1:def 7;
p <> 0_.(R); then
A: x <> 0.K by POLYNOM3:def 10;
B: not x is Unit of K by AS,T88;
now let a be Element of K;
assume a divides x;
then consider b being Element of K such that H1: a * b = x;
reconsider q = a, r = b as Element of the carrier of K;
q *' r = p by H1,POLYNOM3:def 10;
then H2: q <> 0_.(R) & r <> 0_.(R) by POLYNOM3:34;
then H4: deg q + deg r = deg(q *' r) by HURWITZ:23
.= 1 by AS,H1,POLYNOM3:def 10;
per cases;
suppose deg q = 0;
then q is constant; then consider u being Element of R such that
C1: q = u|R by T11;
q = u * 1_.(R) by LX1,C1;
then q *' r = u * ((1_.(R)) *' r) by poly2 .= u * r by poly1;
then u * (r.1) = (q *'r).1 by POLYNOM5:def 4
.= 1.R by H1,POLYNOM3:def 10,E;
then u divides 1.R;
then u is Unit of R by GCD_1:def 20;
hence a is Unit of K or a is_associated_to x by Th90,C1;
end;
suppose deg q <> 0;
then deg q > 0 by H2,T8b;
then deg q + deg r > 0 + deg r by XREAL_1:6;
then r is constant by H4,NAT_1:14;
then consider u being Element of R such that C1: r = u|R by T11;
C3: r = u * 1_.(R) by LX1,C1;
q *' r = u * ((1_.(R)) *' q) by C3,poly2 .= u * q by poly1;
then u * (q.1) = (q *'r).1 by POLYNOM5:def 4
.= 1.R by H1,POLYNOM3:def 10,E;
then u divides 1.R;
then u is Unit of R by GCD_1:def 20;
then r is Unit of K by Th90,C1;
hence a is Unit of K or a is_associated_to x by H1,GCD_1:18;
end;
end;
hence thesis by A,B,RING_2:def 9;
end;
theorem
ex p being non monic Element of the carrier of Polynom-Ring(INT.Ring)
st deg p = 1 & p is reducible
proof
set R = INT.Ring; set K = Polynom-Ring R;
set a = 1.R + 1.R; set p = (a|R) *' rpoly(1,0.R);
a <> 0.R; then
reconsider a as non zero Element of R by STRUCT_0:def 12;
reconsider q = a|R as Element of the carrier of K by POLYNOM3:def 10;
q is constant by RATFUNC1:def 2; then
reconsider q as non zero constant Element of the carrier of K;
reconsider r = rpoly(1,0.R) as Element of the carrier of K
by POLYNOM3:def 10;
A1: p = (a * 1_.(R)) *' rpoly(1,0.R) by LX1
.= a * ((1_.(R)) *' rpoly(1,0.R)) by poly2
.= a * rpoly(1,0.R) by poly1;
A2: deg p = deg q + deg rpoly(1,0.R) by HURWITZ:23
.= 0 + deg rpoly(1,0.R) by LX
.= 1 by HURWITZ:27;
then p.(len p -' 1) = (a * rpoly(1,0.R)).(2-1) by A1,XREAL_1:233
.= a * (rpoly(1,0.R)).1 by POLYNOM5:def 4
.= a * 1.R by HURWITZ:25
.= a; then
LC p = a; then
reconsider pp = p as non monic Element of the carrier of K
by RATFUNC1:def 7,POLYNOM3:def 10;
take pp;
thus deg pp = 1 by A2;
B0: p = q * r by POLYNOM3:def 10;
B1: q divides pp by B0,GCD_1:def 1;
B4: now assume q is Unit of K;
then a is Unit of R by Th90;
then a divides 1.R by GCD_1:def 20;
then consider c being Element of the carrier of R such that
C1: a * c = 1.R;
thus contradiction by C1,INT_1:9;
end;
now assume q is_associated_to pp;
then consider c being Element of the carrier of K such that
C1: c is unital & q * c = p by GCD_1:18;
C2: (a|R) *' c = p by C1,POLYNOM3:def 10;
deg c = 0 by C1,T88; then
c <> 0_.(R) by HURWITZ:20; then
1 = deg q + deg c by HURWITZ:23,C2,A2 .= 0 + deg c by LX;
hence contradiction by C1,T88;
end;
hence pp is reducible by B1,B4,RING_2:def 9;
end;
theorem thirr:
for F being Field,
p being Element of the carrier of Polynom-Ring F
st deg p = 1 holds p is irreducible
proof
let R be Field, p be Element of the carrier of Polynom-Ring R;
set K = Polynom-Ring R;
reconsider x = p as Element of K;
assume AS: deg p = 1;
then p <> 0_.(R) by HURWITZ:20; then
A: x <> 0.K by POLYNOM3:def 10;
B: not x is Unit of K by AS,T88;
now let a be Element of K;
assume a divides x;
then consider b being Element of K such that H1: a * b = x;
reconsider q = a, r = b as Element of the carrier of K;
q *' r = p by H1,POLYNOM3:def 10;
then H2: q <> 0_.(R) & r <> 0_.(R) by AS,HURWITZ:20,POLYNOM3:34;
then H4: deg q + deg r = deg(q *' r) by HURWITZ:23
.= 1 by AS,H1,POLYNOM3:def 10;
per cases;
suppose C0: deg q = 0;
then q is constant; then consider u being Element of R such that
C1: q = u|R by T11;
u is non zero by C1,C0,T11a;
hence a is Unit of K or a is_associated_to x by Th90,C1;
end;
suppose deg q <> 0;
then deg q > 0 by H2,T8b;
then deg q + deg r > 0 + deg r by XREAL_1:6;
then r is constant by H4,NAT_1:14;
then consider u being Element of R such that C1: r = u|R by T11;
u is non zero by C1,T6,H2;
then r is Unit of K by Th90,C1;
hence a is Unit of K or a is_associated_to x by H1,GCD_1:18;
end;
end;
hence thesis by A,B,RING_2:def 9;
end;
theorem thirr1:
for F being algebraic-closed Field,
p being Element of the carrier of Polynom-Ring F
holds p is irreducible iff deg p = 1
proof
let R be algebraic-closed Field,
p be Element of the carrier of Polynom-Ring R;
set K = Polynom-Ring R;
now assume AS: p is irreducible;
then p is non constant;
then (len p -1) + 1 > 0 + 1 by XREAL_1:6;
then consider x being Element of R such that
A: x is_a_root_of p by POLYNOM5:def 8,POLYNOM5:def 9;
consider q being Polynomial of R such that
B: p = rpoly(1,x) *' q by A,HURWITZ:33;
reconsider y = q, z = rpoly(1,x) as Element of Polynom-Ring R
by POLYNOM3:def 10;
p = z * y by B,POLYNOM3:def 10; then z divides p;
then C: z is Unit of K or z is_associated_to p by AS,RING_2:def 9;
z is non constant by HURWITZ:27;
then consider e being Element of K such that
D: e is unital & z * e = p by C,GCD_1:18;
reconsider u = e as Element of the carrier of K;
F: deg u = 0 by D,T88;
rpoly(1,x) *' u = p by D,POLYNOM3:def 10;
hence deg p = deg(rpoly(1,x)) + deg u by D,HURWITZ:23
.= 1 by F,HURWITZ:27;
end;
hence thesis by thirr;
end;
theorem
for F being Field holds
F is algebraic-closed iff
for p being monic Element of the carrier of Polynom-Ring F
holds p is irreducible iff deg p = 1
proof
let R be Field;
now assume AS: for p being monic Element of the carrier of Polynom-Ring R
holds p is irreducible iff deg p = 1;
now let p be Polynomial of R;
assume A: len p > 1;
then A1: p <> 0_.(R) by POLYNOM4:3;
A4: len p - 1 > 1 - 1 by A,XREAL_1:9;
then deg p is Element of NAT by INT_1:3;
then A3: deg p >= 1 by NAT_1:14,A4;
defpred P[Nat] means
for p being Polynomial of R st deg p = $1 holds p is with_roots;
II: for k being Nat st k >= 1 &
(for n being Nat st n >= 1 & n < k holds P[n]) holds P[k]
proof
let k be Nat;
assume IAS: k >= 1 & for n being Nat st n >= 1 & n < k holds P[n];
per cases by IAS,XXREAL_0:1;
suppose IA1: k = 1;
thus P[k]
proof
now let p be Polynomial of R;
assume deg p = 1;
then consider x,z being Element of R such that
I1: x <> 0.R & p = x * rpoly(1,z) by HURWITZ:28;
eval(p,z) = x * eval(rpoly(1,z),z) by I1,POLYNOM5:30
.= x * (z - z) by HURWITZ:29
.= x *0.R by RLVECT_1:15;
hence p is with_roots by POLYNOM5:def 8,POLYNOM5:def 7;
end;
hence thesis by IA1;
end;
end;
suppose IA1: k > 1;
thus P[k]
proof
now let p be Polynomial of R;
reconsider pp = p as Element of Polynom-Ring R by POLYNOM3:def 10;
set q = NormPolynomial(p);
reconsider qq = q as Element of Polynom-Ring R by POLYNOM3:def 10;
assume K: deg p = k;
then len p <> 0;
then I3: deg q > 1 by K,IA1,POLYNOM5:57;
p <> 0_.(R) by K,HURWITZ:20;
then p is non zero by UPROOTS:def 5;
then I4: qq is reducible by AS,I3;
I5: pp <> 0_.(R) by K,HURWITZ:20;
not p is Unit of Polynom-Ring R by T8,K,IA1; then
consider r being Element of the carrier of Polynom-Ring R such that
I6: r divides p & 1 <= deg r & deg r < deg p by I4,I5,T88b,thirr2;
r <> 0_.(R) by I6,HURWITZ:20; then
deg r is Element of NAT by T8b;
then consider x being Element of R such that
I8: x is_a_root_of r by K,I6,IAS,POLYNOM5:def 8;
reconsider rr=r,ppp=p as Element of Polynom-Ring R by POLYNOM3:def 10;
rr divides ppp by I6; then
consider u being Element of the carrier of Polynom-Ring R such that
I10: ppp = rr * u;
p = r *'u by I10,POLYNOM3:def 10; then
eval(p,x) = eval(r,x) * eval(u,x) by POLYNOM4:24
.= 0.R * eval(u,x) by I8,POLYNOM5:def 7
.= 0.R;
hence p is with_roots by POLYNOM5:def 8,POLYNOM5:def 7;
end;
hence thesis;
end;
end; end;
I: for k being Nat st 1 <= k holds P[k] from NAT_1:sch 9(II);
deg p is Element of NAT by A1,T8b; then
consider n being Nat such that H: n >= 1 & deg p = n by A3;
thus p is with_roots by H,I;
end;
hence R is algebraic-closed by POLYNOM5:def 9;
end;
hence thesis by thirr1;
end;
registration
let R be domRing;
cluster irreducible for Element of Polynom-Ring R;
existence
proof
set K = Polynom-Ring R;
reconsider x = rpoly(1,0.R) as Element of K by POLYNOM3:def 10;
deg rpoly(1,0.R) = 1 by HURWITZ:27;
then x is irreducible by thirr0;
hence thesis;
end;
end;
registration
let R be domRing;
cluster irreducible for Element of the carrier of Polynom-Ring R;
existence
proof
set K = Polynom-Ring R;
reconsider x = rpoly(1,0.R) as Element of the carrier of K
by POLYNOM3:def 10;
deg rpoly(1,0.R) = 1 by HURWITZ:27;
then x is irreducible by thirr0;
hence thesis;
end;
end;
registration
let R be Ring;
cluster reducible for Element of Polynom-Ring R;
existence
proof
take p = 0.(Polynom-Ring R);
thus thesis;
end;
end;
registration
let R be Ring;
cluster reducible for Element of the carrier of Polynom-Ring R;
existence
proof
take p = 0_.(R);
reconsider q = p as Element of Polynom-Ring R by POLYNOM3:def 10;
q = 0.(Polynom-Ring R) by POLYNOM3:def 10;
hence thesis;
end;
end;
registration
let R be domRing;
cluster IRR(Polynom-Ring R) -> non empty;
coherence
proof
now let p be irreducible Element of Polynom-Ring R;
p in {x where x is Element of Polynom-Ring R : x is irreducible};
hence p in IRR(Polynom-Ring R) by RING_2:def 10;
end;
hence thesis;
end;
end;
registration
let F be Field;
cluster constant -> reducible for Element of Polynom-Ring F;
coherence;
end;
registration
let F be Field;
cluster constant -> reducible for Element of the carrier of Polynom-Ring F;
coherence;
end;
registration
let F be Field;
cluster irreducible -> non constant for Element of Polynom-Ring F;
coherence;
end;
registration
let F be Field;
cluster irreducible
-> non constant for Element of the carrier of Polynom-Ring F;
coherence;
end;
begin :: The Field F[X]/<p>
registration
let F be Field,
p be Element of the carrier of Polynom-Ring F;
cluster (Polynom-Ring F)/({p}-Ideal) ->
Abelian add-associative right_zeroed right_complementable
commutative associative well-unital distributive;
coherence;
end;
registration
let F be Field,
p be irreducible Element of the carrier of Polynom-Ring F;
cluster (Polynom-Ring F)/({p}-Ideal) -> non degenerated almost_left_invertible;
coherence by RING_2:26,RING_1:21;
end;
definition
let F be Field,
p be Polynomial of F;
func poly_mult_mod p -> BinOp of Polynom-Ring F means :defpmm:
for r,q being Polynomial of F holds it.(r,q) = (r *' q) mod p;
existence
proof
set B = Polynom-Ring F; set D = the carrier of B;
defpred P[object,object,object] means
ex r,q being Element of D st $1 = r & $2 = q & $3 = (r *' q) mod p;
I: now let x,y be object;
assume x in D & y in D;
then reconsider xx=x,yy=y as Element of D;
reconsider r=xx,q=yy as Polynomial of F;
thus ex z being object st z in D & P[x,y,z]
proof
take s = (r *' q) mod p;
thus s in D by POLYNOM3:def 10;
take xx,yy;
thus thesis;
end;
end;
consider f being Function of [:D,D:],D such that
H: for x,y being object st x in D & y in D holds P[x,y,f.(x,y)]
from BINOP_1:sch 1(I);
take f;
now let r,q be Polynomial of F;
r in D & q in D by POLYNOM3:def 10;
then P[r,q,f.(r,q)] by H;
then consider rr,qq being Element of D such that
K: rr = r & qq = q & f.(rr,qq) = (rr *' qq) mod p;
thus f.(r,q) = (r *' q) mod p by K;
end;
hence thesis;
end;
uniqueness
proof
set B = Polynom-Ring F;
let g1,g2 be BinOp of B such that
A1: for r,q being Polynomial of F holds g1.(r,q) = (r *' q) mod p and
A2: for r,q being Polynomial of F holds g2.(r,q) = (r *' q) mod p;
A: dom g1 = [:the carrier of B,the carrier of B:] by FUNCT_2:def 1
.= dom g2 by FUNCT_2:def 1;
now let x be object;
assume x in dom g1;
then consider r,q being object such that
H: r in the carrier of B & q in the carrier of B &
x = [r,q] by ZFMISC_1:def 2;
reconsider r,q as Polynomial of F by H,POLYNOM3:def 10;
thus g1.x = g1.(r,q) by H
.= (r *' q) mod p by A1
.= g2.(r,q) by A2
.= g2.x by H;
end;
hence thesis by A,FUNCT_1:2;
end;
end;
pr1: for F be Field,
p be Element of the carrier of Polynom-Ring F
holds {q where q is Polynomial of F : deg q < deg p}
is Preserv of (the addF of Polynom-Ring F)
proof
let F be Field,
p be Element of the carrier of Polynom-Ring F;
set C = {q where q is Polynomial of F : deg q < deg p};
now let x be set;
assume x in C;
then ex r being Polynomial of F st x = r & deg r < deg p;
hence x in the carrier of Polynom-Ring F by POLYNOM3:def 10;
end;
then C c= the carrier of Polynom-Ring F;
then reconsider C as Subset of the carrier of Polynom-Ring F;
set A = the addF of Polynom-Ring F;
now let x be set;
assume x in [:C,C:];
then consider a,b being object such that
A2: a in C and
A3: b in C and
A4: x = [a,b] by ZFMISC_1:def 2;
consider u being Polynomial of F such that
A5: a = u & deg u < deg p by A2;
consider v being Polynomial of F such that
A6: b = v & deg v < deg p by A3;
reconsider a,b as Element of Polynom-Ring F by A5,A6,POLYNOM3:def 10;
A7: deg(u+v) <= max(deg(u),deg(v)) by HURWITZ:22;
max(deg(u),deg(v)) < deg p by A5,A6,XXREAL_0:29;
then A8: deg(u+v) < deg p by A7,XXREAL_0:2;
A.x = a + b by A4
.= u + v by A5,A6,POLYNOM3:def 10;
hence A.x in C by A8;
end;
hence thesis by REALSET1:def 1;
end;
pr2: for F be Field,
p be non constant Element of the carrier of Polynom-Ring F
holds {q where q is Polynomial of F : deg q < deg p}
is Preserv of (poly_mult_mod p)
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
set C = {q where q is Polynomial of F : deg q < deg p};
now let x be set;
assume x in C;
then ex r being Polynomial of F st x = r & deg r < deg p;
hence x in the carrier of Polynom-Ring F by POLYNOM3:def 10;
end;
then C c= the carrier of Polynom-Ring F;
then reconsider C as Subset of the carrier of Polynom-Ring F;
set A = poly_mult_mod p;
now let x be set;
assume x in [:C,C:];
then consider a,b being object such that
A2: a in C and
A3: b in C and
A4: x = [a,b] by ZFMISC_1:def 2;
consider u being Polynomial of F such that
A5: a = u & deg u < deg p by A2;
consider v being Polynomial of F such that
A6: b = v & deg v < deg p by A3;
reconsider a,b as Element of Polynom-Ring F by A5,A6,POLYNOM3:def 10;
A8: deg((u *' v) mod p) < deg p by RING_2:29;
A.x = (poly_mult_mod p).(u,v) by A5,A6,A4
.= (u *' v) mod p by defpmm;
hence A.x in C by A8;
end;
hence thesis by REALSET1:def 1;
end;
pr3: for F be Field,
p be non constant Element of the carrier of Polynom-Ring F
holds 1_.(F) in {q where q is Polynomial of F : deg q < deg p}
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
A: deg p > 0 by defconst;
len 1_.(F) = 1 by POLYNOM4:4;
then deg 1_.(F) = 0;
hence thesis by A;
end;
pr4: for F be Field,
p be non constant Element of the carrier of Polynom-Ring F
holds 0_.(F) in {q where q is Polynomial of F : deg q < deg p}
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
deg 0_.(F) = -1 by HURWITZ:20;
hence thesis;
end;
definition
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
func Polynom-Ring(p) -> strict doubleLoopStr means :defprfp:
the carrier of it = {q where q is Polynomial of F : deg q < deg p} &
the addF of it = (the addF of Polynom-Ring F)||(the carrier of it) &
the multF of it = (poly_mult_mod p)||(the carrier of it) &
the OneF of it = 1_.(F) &
the ZeroF of it = 0_.(F);
existence
proof
set B = Polynom-Ring F;
set C = {q where q is Polynomial of F : deg q < deg p};
set A = the addF of B;
set M = poly_mult_mod p;
reconsider C1 = C as Preserv of A by pr1;
reconsider ad = A||C1 as BinOp of C;
reconsider C2 = C as Preserv of M by pr2;
reconsider mu = M||C2 as BinOp of C;
reconsider O = 1_.(F) as Element of C by pr3;
reconsider Z = 0_.(F) as Element of C by pr4;
take doubleLoopStr(#C,ad,mu,O,Z#);
thus thesis;
end;
uniqueness;
end;
registration
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
cluster Polynom-Ring(p) -> non degenerated;
coherence
proof
set P = Polynom-Ring(p);
1.P = 1_.(F) by defprfp;
hence 0.P <> 1.P by defprfp;
end;
end;
registration
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
cluster Polynom-Ring(p) -> Abelian
add-associative right_zeroed right_complementable;
coherence
proof
set P = Polynom-Ring(p);
set C = {q where q is Polynomial of F : deg q < deg p};
H0: C = the carrier of P by defprfp;
H1: 0.P = 0_.(F) by defprfp;
now let x,y be Element of P;
x in the carrier of P;
then x in C by defprfp;
then consider q being Polynomial of F such that A1: x = q & deg q < deg p;
y in the carrier of P;
then y in C by defprfp;
then consider r being Polynomial of F such that A2: y = r & deg r < deg p;
reconsider q,r as Element of Polynom-Ring F by POLYNOM3:def 10;
A3: [x,y] in [:C,C:] & [y,x] in [:C,C:] by H0,ZFMISC_1:def 2;
thus
x + y = ((the addF of Polynom-Ring F)||C).(x,y) by H0,defprfp
.= q + r by A1,A2,A3,FUNCT_1:49
.= (the addF of Polynom-Ring F).(y,x) by A1,A2,ALGSTR_0:def 1
.= ((the addF of Polynom-Ring F)||C).(y,x) by A3,FUNCT_1:49
.= y + x by H0,defprfp;
end;
hence P is Abelian by RLVECT_1:def 2;
now let x,y,z be Element of P;
x in the carrier of P;
then x in C by defprfp;
then consider q being Polynomial of F such that A1: x = q & deg q < deg p;
y in the carrier of P;
then y in C by defprfp;
then consider r being Polynomial of F such that A2: y = r & deg r < deg p;
z in the carrier of P;
then z in C by defprfp;
then consider u being Polynomial of F such that A3: z = u & deg u < deg p;
A3a: [x,y] in [:C,C:] & [y,z] in [:C,C:] by H0,ZFMISC_1:def 2;
A3b: [x+y,z] in [:C,C:] & [x,y+z] in [:C,C:] by H0,ZFMISC_1:def 2;
reconsider q,r,u as Element of Polynom-Ring F by POLYNOM3:def 10;
A4: x + y
= ((the addF of Polynom-Ring F)||C).(x,y) by H0,defprfp
.= q + r by A1,A2,A3a,FUNCT_1:49;
A5: y + z
= ((the addF of Polynom-Ring F)||C).(y,z) by H0,defprfp
.= r + u by A3,A2,A3a,FUNCT_1:49;
A6: (x + y) + z
= ((the addF of Polynom-Ring F)||C).(x+y,z) by H0,defprfp
.= (q + r) + u by A3,A4,A3b,FUNCT_1:49
.= q + (r + u) by RLVECT_1:def 3;
thus x + (y + z)
= ((the addF of Polynom-Ring F)||C).(x,y+z) by H0,defprfp
.= (x + y) + z by A6,A5,A1,A3b,FUNCT_1:49;
end;
hence P is add-associative by RLVECT_1:def 3;
now let x be Element of P;
x in the carrier of P;
then x in C by defprfp;
then consider q being Polynomial of F such that A1: x = q & deg q < deg p;
reconsider q1 = q as Element of Polynom-Ring F by POLYNOM3:def 10;
reconsider r = 0_.(F) as Element of Polynom-Ring F by POLYNOM3:def 10;
A3: [x,0.P] in [:C,C:] by H0,ZFMISC_1:def 2;
thus
x + 0.P
= ((the addF of Polynom-Ring F)||C).(x,0.P) by H0,defprfp
.= (the addF of Polynom-Ring F).(x,0.P) by A3,FUNCT_1:49
.= q1 + r by defprfp,A1
.= q + 0_.(F) by POLYNOM3:def 10
.= x by A1,POLYNOM3:28;
end;
hence P is right_zeroed by RLVECT_1:def 4;
now let x be Element of P;
x in the carrier of P;
then x in C by defprfp;
then consider q being Polynomial of F such that A1: x = q & deg q < deg p;
reconsider q1 = q as Element of Polynom-Ring F by POLYNOM3:def 10;
reconsider r = -q as Element of Polynom-Ring F by POLYNOM3:def 10;
deg(-q) = deg q by POLYNOM4:8;
then -q in C by A1;
then reconsider y = -q as Element of P by defprfp;
A3: [x,y] in [:C,C:] by H0,ZFMISC_1:def 2;
x + y = ((the addF of Polynom-Ring F)||C).(x,y) by H0,defprfp
.= q1 + r by A1,A3,FUNCT_1:49
.= q - q by POLYNOM3:def 10
.= 0_.(F) by POLYNOM3:29;
hence x is right_complementable by H1;
end;
hence P is right_complementable;
end;
end;
registration
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
cluster Polynom-Ring(p) -> associative well-unital distributive;
coherence
proof
set P = Polynom-Ring(p);
set C = {q where q is Polynomial of F : deg q < deg p};
H0: C = the carrier of P by defprfp;
H2: 1.P = 1_.(F) by defprfp;
reconsider p1 = p as Polynomial of F;
now let x,y,z be Element of P;
x in the carrier of P;
then x in C by defprfp;
then consider q being Polynomial of F such that A1: x = q & deg q < deg p;
y in the carrier of P;
then y in C by defprfp;
then consider r being Polynomial of F such that A2: y = r & deg r < deg p;
z in the carrier of P;
then z in C by defprfp;
then consider u being Polynomial of F such that A3: z = u & deg u < deg p;
A3a: [x,y] in [:C,C:] & [y,z] in [:C,C:] by H0,ZFMISC_1:def 2;
A3b: [x*y,z] in [:C,C:] & [x,y*z] in [:C,C:] by H0,ZFMISC_1:def 2;
A4: x * y
= ((poly_mult_mod p)||C).(x,y) by H0,defprfp
.= (poly_mult_mod p).(x,y) by A3a,FUNCT_1:49
.= (q *' r) mod p1 by A1,A2,defpmm;
A5: y * z
= ((poly_mult_mod p)||C).(y,z) by H0,defprfp
.= (poly_mult_mod p).(y,z) by A3a,FUNCT_1:49
.= (r *' u) mod p1 by A3,A2,defpmm;
A6: (x * y) * z
= ((poly_mult_mod p)||C).(x*y,z) by H0,defprfp
.= (poly_mult_mod p).(x*y,z) by A3b,FUNCT_1:49
.= (((q *' r) mod p1) *' u) mod p1 by A3,A4,defpmm
.= ( q *' r *' u) mod p1 by div3;
thus x * (y * z)
= ((poly_mult_mod p)||C).(x,y*z) by H0,defprfp
.= (poly_mult_mod p).(x,y*z) by A3b,FUNCT_1:49
.= (((r *' u) mod p1) *' q) mod p1 by A1,A5,defpmm
.= (r *' u *' q) mod p1 by div3
.= (x * y) * z by A6,POLYNOM3:33;
end;
hence P is associative by GROUP_1:def 3;
now let x being Element of P;
x in the carrier of P;
then x in C by defprfp;
then consider q being Polynomial of F such that A1: x = q & deg q < deg p;
A3a: [x,1.P] in [:C,C:] & [1.P,x] in [:C,C:] by H0,ZFMISC_1:def 2;
thus x * 1.P
= ((poly_mult_mod p)||C).(x,1.P) by H0,defprfp
.= (poly_mult_mod p).(x,1.P) by A3a,FUNCT_1:49
.= (q *' 1_.(F)) mod p1 by H2,A1,defpmm
.= q mod p1 by POLYNOM3:35
.= x by A1,div1;
thus 1.P * x
= ((poly_mult_mod p)||C).(1.P,x) by H0,defprfp
.= (poly_mult_mod p).(1.P,x) by A3a,FUNCT_1:49
.= ((1_.(F)) *' q) mod p1 by H2,A1,defpmm
.= q mod p1 by POLYNOM3:35
.= x by A1,div1;
end;
hence P is well-unital by VECTSP_1:def 6;
now let x,y,z be Element of P;
x in the carrier of P;
then x in C by defprfp;
then consider q being Polynomial of F such that A1: x = q & deg q < deg p;
y in the carrier of P;
then y in C by defprfp;
then consider r being Polynomial of F such that A2: y = r & deg r < deg p;
z in the carrier of P;
then z in C by defprfp;
then consider u being Polynomial of F such that A3: z = u & deg u < deg p;
reconsider q1=q,r1=r,u1=u as Element of Polynom-Ring F by POLYNOM3:def 10;
A3a: [x,y] in [:C,C:] & [x,z] in [:C,C:] &
[y,z] in [:C,C:] by H0,ZFMISC_1:def 2;
A3b: [x*y,x*z] in [:C,C:] & [x,y*z] in [:C,C:] &
[x,y+z] in [:C,C:] by H0,ZFMISC_1:def 2;
A4: y + z
= ((the addF of Polynom-Ring F)||C).(y,z) by H0,defprfp
.= r1 + u1 by A2,A3,A3a,FUNCT_1:49
.= r + u by POLYNOM3:def 10;
A5: x* (y+z)
= ((poly_mult_mod p)||C).(x,y+z) by H0,defprfp
.= (poly_mult_mod p).(x,y+z) by A3b,FUNCT_1:49
.= (q *' (r +u)) mod p1 by A1,A4,defpmm;
A6: x * y
= ((poly_mult_mod p)||C).(x,y) by H0,defprfp
.= (poly_mult_mod p).(x,y) by A3a,FUNCT_1:49
.= (q *' r) mod p1 by A1,A2,defpmm;
A7: x * z
= ((poly_mult_mod p)||C).(x,z) by H0,defprfp
.= (poly_mult_mod p).(x,z) by A3a,FUNCT_1:49
.= (q *' u) mod p1 by A1,A3,defpmm;
reconsider s = (q*'r) mod p1 as Element of Polynom-Ring F by POLYNOM3:def 10;
reconsider t = (q*'u) mod p1 as Element of Polynom-Ring F by POLYNOM3:def 10;
thus x*y+x*z
= ((the addF of Polynom-Ring F)||C).(x*y,x*z) by H0,defprfp
.= s + t by A6,A7,A3b,FUNCT_1:49
.= ((q*'r) mod p1) + ((q*'u) mod p1) by POLYNOM3:def 10
.= (q*'r + q*'u) mod p1 by div4
.= x* (y+z) by A5,POLYNOM3:31;
A3a: [y,x] in [:C,C:] & [z,x] in [:C,C:] &
[y,z] in [:C,C:] by H0,ZFMISC_1:def 2;
A3b: [y*x,z*x] in [:C,C:] & [x,y*z] in [:C,C:] &
[y+z,x] in [:C,C:] by H0,ZFMISC_1:def 2;
A4: y + z
= ((the addF of Polynom-Ring F)||C).(y,z) by H0,defprfp
.= r1 + u1 by A2,A3,A3a,FUNCT_1:49
.= r + u by POLYNOM3:def 10;
A5: (y+z) * x
= ((poly_mult_mod p)||C).(y+z,x) by H0,defprfp
.= (poly_mult_mod p).(y+z,x) by A3b,FUNCT_1:49
.= ((r +u) *' q) mod p1 by A1,A4,defpmm;
A6: y * x
= ((poly_mult_mod p)||C).(y,x) by H0,defprfp
.= (poly_mult_mod p).(y,x) by A3a,FUNCT_1:49
.= (r *' q) mod p1 by A1,A2,defpmm;
A7: z * x
= ((poly_mult_mod p)||C).(z,x) by H0,defprfp
.= (poly_mult_mod p).(z,x) by A3a,FUNCT_1:49
.= (u *' q) mod p1 by A1,A3,defpmm;
reconsider s = (r*'q) mod p1 as Element of Polynom-Ring F by POLYNOM3:def 10;
reconsider t = (u*'q) mod p1 as Element of Polynom-Ring F by POLYNOM3:def 10;
thus y*x+z*x
= ((the addF of Polynom-Ring F)||C).(y*x,z*x) by H0,defprfp
.= s + t by A6,A7,A3b,FUNCT_1:49
.= ((q*'r) mod p1) + ((q*'u) mod p1) by POLYNOM3:def 10
.= (q*'r + q*'u) mod p1 by div4
.= (y+z) * x by A5,POLYNOM3:31;
end;
hence P is distributive by VECTSP_1:def 7;
end;
end;
definition
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
func poly_mod p -> Function of Polynom-Ring F, Polynom-Ring(p) means :dpm:
for q being Polynomial of F holds it.q = q mod p;
existence
proof
set B = Polynom-Ring F; set D = the carrier of B;
defpred P[object,object] means
ex q being Element of D st $1 = q & $2 = q mod p;
now let x be object;
assume x in D;
then reconsider xx=x as Element of D;
reconsider r=xx as Polynomial of F;
thus ex z being object st z in the carrier of Polynom-Ring(p) & P[x,z]
proof
take s = r mod p;
deg s < deg p by RING_2:29;
then s in {q where q is Polynomial of F : deg q < deg p};
hence s in the carrier of Polynom-Ring(p) by defprfp;
take xx;
thus thesis;
end;
end;
then I:
for x being object st x in D ex y being object
st y in the carrier of Polynom-Ring(p) & P[x,y];
consider f being Function of D,Polynom-Ring(p) such that
H: for x being object st x in D holds P[x,f.x]
from FUNCT_2:sch 1(I);
reconsider f as Function of B,Polynom-Ring(p);
take f;
now let q be Polynomial of F;
q in B by POLYNOM3:def 10;
then P[q,f.q] by H;
then consider qq being Element of D such that
K: qq = q & f.qq = qq mod p;
thus f.q = q mod p by K;
end;
hence thesis;
end;
uniqueness
proof
set B = Polynom-Ring F;
let g1,g2 be Function of B,Polynom-Ring(p) such that
A1: for q being Polynomial of F holds g1.q = q mod p and
A2: for q being Polynomial of F holds g2.q = q mod p;
A: dom g1 = the carrier of B by FUNCT_2:def 1
.= dom g2 by FUNCT_2:def 1;
now let x be object;
assume x in dom g1;
then reconsider q = x as Polynomial of F by POLYNOM3:def 10;
thus g1.x = q mod p by A1 .= g2.x by A2;
end;
hence thesis by A,FUNCT_1:2;
end;
end;
registration
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
cluster poly_mod p -> additive multiplicative unity-preserving;
coherence
proof
set f = poly_mod p, K = Polynom-Ring(p);
set C = the carrier of K;
hereby
let x1,y1 be Element of Polynom-Ring F;
reconsider x=x1,y=y1 as Element of the carrier of Polynom-Ring F;
H: f.x = x mod p & f.y = y mod p by dpm;
then reconsider fx = f.x, fy = f.y as Element of Polynom-Ring F
by POLYNOM3:def 10;
A3: [f.x,f.y] in [:C,C:] by ZFMISC_1:def 2;
thus f.x1 + f.y1
= ((the addF of Polynom-Ring F)||(the carrier of K)).(f.x1,f.y1)
by defprfp
.= fx + fy by A3,FUNCT_1:49
.= (x mod p) + (y mod p) by H,POLYNOM3:def 10
.= (x + y) mod p by div4
.= f.(x+y) by dpm
.= f.(x1+y1) by POLYNOM3:def 10;
end;
hereby
let x1,y1 be Element of Polynom-Ring F;
reconsider x=x1,y=y1 as Element of the carrier of Polynom-Ring F;
H: f.x = x mod p & f.y = y mod p by dpm;
then reconsider fx = f.x, fy = f.y as Element of Polynom-Ring F
by POLYNOM3:def 10;
A3: [f.x,f.y] in [:C,C:] by ZFMISC_1:def 2;
thus f.x1 * f.y1
= ((poly_mult_mod p)||(the carrier of K)).(f.x1,f.y1)
by defprfp
.= (poly_mult_mod p).(f.x,f.y) by A3,FUNCT_1:49
.= ((x mod p) *' (y mod p)) mod p by H,defpmm
.= (x *' y) mod p by div3a
.= f.(x*'y) by dpm
.= f.(x1*y1) by POLYNOM3:def 10;
end;
deg p > 0 by defconst;
then H: deg 1_.(F) < deg p by RATFUNC1:def 2;
thus f.(1_(Polynom-Ring F))
= f.(1_.(F)) by POLYNOM3:def 10
.= 1_.(F) mod p by dpm
.= 1_.(F) by H,div1
.= 1_K by defprfp;
end;
end;
registration
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
cluster Polynom-Ring(p) -> (Polynom-Ring F)-homomorphic;
coherence
proof
poly_mod p is linear
proof
thus poly_mod p is additive multiplicative unity-preserving;
end;
hence thesis by RING_2:def 4;
end;
end;
registration
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
cluster poly_mod p -> onto;
coherence
proof
set f = poly_mod p;
now let x be object;
assume x in the carrier of Polynom-Ring(p);
then x in {q where q is Polynomial of F : deg q < deg p} by defprfp;
then consider q being Polynomial of F such that
B: q = x & deg q < deg p;
q mod p = q by B,div1;
then C: f.x = q by B,dpm;
dom f = the carrier of Polynom-Ring F by FUNCT_2:def 1;
then q in dom f by POLYNOM3:def 10;
hence x in rng f by B,C,FUNCT_1:def 3;
end;
then for x be object holds x in rng f iff x in the carrier of
Polynom-Ring(p);
hence thesis by FUNCT_2:def 3,TARSKI:2;
end;
end;
lemminuspoly:
for R be Ring, a be Element of Polynom-Ring R,
b be Polynomial of R st a = b holds -a = -b
proof
let R be Ring, a be Element of Polynom-Ring R, b be Polynomial of R;
assume AS: a = b;
set K = Polynom-Ring R;
reconsider c = -b as Element of Polynom-Ring R by POLYNOM3:def 10;
a + c = b - b by AS,POLYNOM3:def 10
.= 0_.(R) by POLYNOM3:29
.= 0.K by POLYNOM3:def 10
.= a + (-a) by RLVECT_1:5;
hence thesis by RLVECT_1:8;
end;
theorem kerp:
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
holds ker(poly_mod p) = {p}-Ideal
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
set R = Polynom-Ring F, S = Polynom-Ring(p);
set f = poly_mod p;
reconsider p1 = p as Element of R;
A: now let x be object;
assume A0: x in ker f;
then x in {v where v is Element of R : f.v = 0.S} by VECTSP10:def 9;
then consider y being Element of R such that A1: y = x & f.y = 0.S;
reconsider q = x as Element of the carrier of R by A0;
reconsider q1 = x as Element of R by A0;
A2: q - (q div p) *' p = q mod p
.= 0.S by A1,dpm
.= 0_.(F) by defprfp;
reconsider qp = q div p as Element of R by POLYNOM3:def 10;
qp * p1 = (q div p) *' p by POLYNOM3:def 10;
then A3: -(qp * p1) = -((q div p) *' p) by lemminuspoly;
q1 - qp * p1 = q + -((q div p) *' p) by A3,POLYNOM3:def 10
.= 0.R by A2,POLYNOM3:def 10;
then qp * p1 = q1 by RLVECT_1:21;
then q in the set of all p*r where r is Element of R;
hence x in {p}-Ideal by IDEAL_1:64;
end;
now let x be object;
assume x in {p}-Ideal;
then x in the set of all p*r where r is Element of R by IDEAL_1:64;
then consider y being Element of R such that A1: x = p * y;
reconsider q = y as Element of the carrier of R;
p * y = p *' q by POLYNOM3:def 10; then
f.x = (p *' q) mod p by A1,dpm
.= 0_.(F) by T2,div2
.= 0.S by defprfp;
then x in {v where v is Element of R : f.v = 0.S} by A1;
hence x in ker(poly_mod p) by VECTSP10:def 9;
end;
hence thesis by A,TARSKI:2;
end;
theorem ISO:
for F being Field,
p being non constant Element of the carrier of Polynom-Ring F
holds (Polynom-Ring F)/({p}-Ideal), Polynom-Ring(p) are_isomorphic
proof
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
set R = Polynom-Ring F, S = Polynom-Ring(p);
R/ker(poly_mod p), S are_isomorphic by RING_2:16;
hence thesis by kerp;
end;
registration
let F be Field,
p be non constant Element of the carrier of Polynom-Ring F;
cluster Polynom-Ring(p) -> commutative;
coherence
proof
set R = (Polynom-Ring F)/({p}-Ideal), S = Polynom-Ring(p);
ex f being Function of R,S st f is RingIsomorphism by ISO,QUOFIELD:def 23;
then Polynom-Ring(p) is R-isomorphic by RING_3:def 4;
hence S is commutative;
end;
end;
registration
let F be Field,
p be irreducible Element of the carrier of Polynom-Ring F;
cluster Polynom-Ring(p) -> almost_left_invertible;
coherence
proof
set R = (Polynom-Ring F)/({p}-Ideal), S = Polynom-Ring(p);
ex f being Function of R,S st f is RingIsomorphism by ISO,QUOFIELD:def 23;
then Polynom-Ring(p) is R-isomorphic by RING_3:def 4;
hence thesis;
end;
end;
begin :: Polynomial GCDs
definition
let L be non empty multMagma;
let x,y be Element of L;
let z be Element of L;
attr z is x,y-gcd means :defGCD:
z divides x & z divides y &
for r being Element of L st r divides x & r divides y holds r divides z;
end;
registration
let L be gcdDomain;
let x,y be Element of L;
cluster x,y-gcd for Element of L;
existence
proof
consider z being Element of L such that
H: z divides x & z divides y & for zz being Element of L st zz
divides x & zz divides y holds zz divides z by GCD_1:def 11;
take z;
thus thesis by H;
end;
end;
definition
let L be gcdDomain;
let x,y be Element of L;
mode a_gcd of x,y is x,y-gcd Element of L;
end;
theorem gcd1:
for L being gcdDomain
for x,y being Element of L
for u,v being a_gcd of x,y holds u is_associated_to v
proof
let L be gcdDomain;
let p,q be Element of L;
let u,v be a_gcd of p,q;
A: u divides p & u divides q by defGCD;
v divides p & v divides q by defGCD;
hence thesis by A,defGCD;
end;
registration
let L be gcdDomain;
let x,y be Element of L;
cluster x,y-gcd -> y,x-gcd for Element of L;
coherence;
end;
definition
let F be Field;
let p,q be Element of the carrier of Polynom-Ring F;
func p gcd q -> Element of the carrier of Polynom-Ring F means :dpg:
it = 0_.(F) if p = 0_.(F) & q = 0_.(F)
otherwise it is a_gcd of p,q & it is monic;
existence
proof
per cases;
suppose p = 0_.(F) & q = 0_.(F);
hence thesis;
end;
suppose AS: p <> 0_.(F) or q <> 0_.(F);
reconsider g = the a_gcd of p,q as Element of the carrier of Polynom-Ring F;
reconsider p1 = p, q1 = q as Element of Polynom-Ring F;
set r = NormPolynomial g;
reconsider r1 = r as Element of Polynom-Ring F;
A: now assume g is zero;
then g = 0_.(F) by UPROOTS:def 5;
then D1: g = 0.(Polynom-Ring F) by POLYNOM3:def 10;
g divides p1 by defGCD; then
consider u being Element of the carrier of Polynom-Ring F such that
D2: g * u = p1;
g divides q1 by defGCD; then
consider v being Element of the carrier of Polynom-Ring F such that
D4: g * v = q1;
thus contradiction by D1,D4,D2,AS,POLYNOM3:def 10;
end;
g divides p1 by defGCD;
then g divides p;
then F: r divides p by np1;
g divides q1 by defGCD;
then g divides q;
then B: r divides q by np1;
now let z be Element of Polynom-Ring F;
reconsider z1 = z as Element of the carrier of Polynom-Ring F;
assume z divides p & z divides q;
then z divides g by defGCD;
then z1 divides g;
then z1 divides r by np2;
hence z divides r1;
end;
then r1 is p,q-gcd by B,F;
hence thesis by A;
end;
end;
uniqueness
proof
per cases;
suppose p = 0_.(F) & q = 0_.(F);
hence thesis;
end;
suppose p <> 0_.(F) or q <> 0_.(F);
thus thesis by gcd1,np0;
end;
end;
consistency;
end;
definition
let F be Field;
let p,q be Element of the carrier of Polynom-Ring F;
redefine func p gcd q; :: redefines gcd (RING_4, definition)
commutativity
proof
now let p,q be Element of the carrier of Polynom-Ring F;
per cases;
suppose AS: p = 0_.(F) & q = 0_.(F);
thus p gcd q = q gcd p by AS;
end;
suppose AS: p <> 0_.(F) or q <> 0_.(F);
then (p gcd q) is a_gcd of p,q & (p gcd q) is monic by dpg;
hence p gcd q = q gcd p by AS,dpg;
end;
end;
hence thesis;
end;
end;
definition
let F be Field;
let p,q be Element of Polynom-Ring F;
redefine func p gcd q; :: redefines gcd (RING_4, definition)
commutativity
proof
for p,q being Element of Polynom-Ring F holds p gcd q = q gcd p;
hence thesis;
end;
end;
registration
let F be Field;
let p,q be Element of the carrier of Polynom-Ring F;
cluster p gcd q -> p,q-gcd;
coherence
proof
per cases;
suppose A: p = 0_.(F) & q = 0_.(F);
reconsider g = p gcd q as Element of Polynom-Ring F;
g divides p & g divides q by A,dpg;
hence thesis by A,dpg;
end;
suppose A: p <> 0_.(F) or q <> 0_.(F);
set g = p gcd q;
reconsider p1 = p, q1 = q as Element of Polynom-Ring F;
set g1 = p1 gcd q1;
reconsider g1 as Element of Polynom-Ring F;
thus thesis by A,dpg;
end;
end;
end;
registration
let F be Field;
let p,q be Element of Polynom-Ring F;
cluster p gcd q -> p,q-gcd;
coherence;
end;
registration
let F be Field;
let p be Element of the carrier of Polynom-Ring F;
let q be non zero Element of the carrier of Polynom-Ring F;
cluster p gcd q -> non zero monic;
coherence
proof
reconsider p1 = p, q1 = q as Element of Polynom-Ring F;
set g1 = p1 gcd q1;
set g = p gcd q;
reconsider g1 as Element of Polynom-Ring F;
D: now assume g is zero;
then g = 0_.(F) by UPROOTS:def 5;
then D1: g = 0.(Polynom-Ring F) by POLYNOM3:def 10;
D3: q <> 0_.(F);
g1 divides q1 by defGCD; then
consider v being Element of the carrier of Polynom-Ring F such that
D4: g1 * v = q;
thus contradiction by D1,D4,D3,POLYNOM3:def 10;
end;
hence g is non zero;
g <> 0_.(F) by D;
hence thesis by dpg;
end;
end;
registration
let F be Field;
let p be Element of Polynom-Ring F;
let q be non zero Element of Polynom-Ring F;
cluster p gcd q -> non zero monic;
coherence
proof
set g = p gcd q;
reconsider g1 = g as Element of Polynom-Ring F;
q <> 0.(Polynom-Ring F); then
D3: q <> 0_.(F) by POLYNOM3:def 10;
now assume g is zero;
then g = 0_.(F) by UPROOTS:def 5;
then D1: g = 0.(Polynom-Ring F) by POLYNOM3:def 10;
g1 divides q by defGCD; then
consider v being Element of the carrier of Polynom-Ring F such that
D4: g1 * v = q;
thus contradiction by D1,D4;
end;
hence g is non zero;
thus thesis by D3,dpg;
end;
end;
registration
let F be Field;
let p,q be zero Element of the carrier of Polynom-Ring F;
cluster p gcd q -> zero;
coherence
proof
reconsider g = p gcd q as Element of Polynom-Ring F;
p = 0_.(F) & q = 0_.(F) by UPROOTS:def 5;
hence p gcd q is zero by dpg;
end;
end;
registration
let F be Field;
let p,q be zero Element of Polynom-Ring F;
cluster p gcd q -> zero;
coherence
proof
reconsider g = p gcd q as Element of Polynom-Ring F;
p = 0.(Polynom-Ring F) & q = 0.(Polynom-Ring F) by STRUCT_0:def 12;
then p = 0_.(F) & q = 0_.(F) by POLYNOM3:def 10;
hence p gcd q is zero;
end;
end;
theorem
for F being Field,
p,q being Element of the carrier of Polynom-Ring F
holds (p gcd q) divides p & (p gcd q) divides q &
for r being Element of the carrier of Polynom-Ring F
st r divides p & r divides q holds r divides (p gcd q)
proof
let F be Field,
p,q be Element of the carrier of Polynom-Ring F;
set g = p gcd q;
reconsider g1 = p gcd q as Element of Polynom-Ring F;
g1 divides p & g1 divides q by defGCD;
hence g divides p & g divides q;
now let r be Element of the carrier of Polynom-Ring F;
reconsider r1 = r as Element of Polynom-Ring F;
assume r divides p & r divides q;
then r1 divides g1 by defGCD;
hence r divides g;
end;
hence thesis;
end;
theorem
for F being Field,
p,q being Element of Polynom-Ring F
holds (p gcd q) divides p & (p gcd q) divides q &
for r being Element of Polynom-Ring F
st r divides p & r divides q holds r divides (p gcd q) by defGCD;
definition
let F be Field;
let p,q be Polynomial of F;
func p gcd q -> Polynomial of F means :dd:
ex a,b being Element of Polynom-Ring F st a = p & b = q & it = a gcd b;
existence
proof
reconsider a = p, b = q as Element of Polynom-Ring F by POLYNOM3:def 10;
take a gcd b;
thus thesis;
end;
uniqueness;
end;
definition
let F be Field;
let p,q be Polynomial of F;
redefine func p gcd q; :: redefines gcd (RING_4, definition)
commutativity
proof
now let p,q be Polynomial of F;
reconsider a = p, b = q as Element of Polynom-Ring F by POLYNOM3:def 10;
thus p gcd q = a gcd b by dd .= q gcd p by dd;
end;
hence thesis;
end;
end;
registration
let F be Field;
let p be Polynomial of F;
let q be non zero Polynomial of F;
cluster p gcd q -> non zero monic;
coherence
proof
reconsider a = p, b = q as Element of Polynom-Ring F by POLYNOM3:def 10;
A0: p gcd q = a gcd b by dd;
q <> 0_.(F); then
q <> 0.(Polynom-Ring F) by POLYNOM3:def 10; then
reconsider b as non zero Element of Polynom-Ring F by STRUCT_0:def 12;
thus p gcd q is non zero by A0;
thus thesis by A0;
end;
end;
registration
let F be Field;
let p,q be zero Polynomial of F;
cluster p gcd q -> zero;
coherence
proof
p = 0_.(F) & q = 0_.(F) by UPROOTS:def 5; then
p = 0.(Polynom-Ring F) & q = 0.(Polynom-Ring F) by POLYNOM3:def 10; then
reconsider a = p, b = q as zero Element of Polynom-Ring F;
p gcd q = a gcd b by dd;
hence p gcd q is zero;
end;
end;
theorem G1:
for F being Field,
p,q being Polynomial of F
holds (p gcd q) divides p & (p gcd q) divides q &
for r being Polynomial of F
st r divides p & r divides q holds r divides (p gcd q)
proof
let F be Field, p,q being Polynomial of F;
reconsider a = p, b = q as Element of Polynom-Ring F by POLYNOM3:def 10;
set g = a gcd b;
A0: p gcd q = g by dd;
g divides a by defGCD;
then consider c being Element of Polynom-Ring F such that A1: g * c = a;
reconsider r = c as Polynomial of F by POLYNOM3:def 10;
(p gcd q) *' r = p by A0,A1,POLYNOM3:def 10;
hence p gcd q divides p by T2;
g divides b by defGCD;
then consider c being Element of Polynom-Ring F such that A1: g * c = b;
reconsider r = c as Polynomial of F by POLYNOM3:def 10;
(p gcd q) *' r = q by A0,A1,POLYNOM3:def 10;
hence p gcd q divides q by T2;
now let r be Polynomial of F;
assume A1: r divides p & r divides q;
reconsider c = r as Element of Polynom-Ring F by POLYNOM3:def 10;
consider s being Polynomial of F such that A2: r *' s = p by A1,T2;
consider t being Polynomial of F such that A3: r *' t = q by A1,T2;
reconsider x=s, y=t as Element of Polynom-Ring F by POLYNOM3:def 10;
c * x = a & c * y = b by A2,A3,POLYNOM3:def 10;
then c divides a & c divides b;
then c divides a gcd b by defGCD;
hence r divides (p gcd q) by dd;
end;
hence thesis;
end;
theorem
for F being Field
for p being Polynomial of F
for q being non zero Polynomial of F
for s being monic Polynomial of F
holds s = p gcd q iff
(s divides p & s divides q &
for r being Polynomial of F st r divides p & r divides q
holds r divides s)
proof
let F be Field, p be Polynomial of F; let q be non zero Polynomial of F;
let s be monic Polynomial of F;
now assume AS: s divides p & s divides q &
for r being Polynomial of F st r divides p & r divides q
holds r divides s;
reconsider a = p, b = q as Element of Polynom-Ring F by POLYNOM3:def 10;
reconsider g = s as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
B: b <> 0_.(F);
now let d be Element of Polynom-Ring F;
assume C: d divides a & d divides b;
reconsider h = d as Polynomial of F by POLYNOM3:def 10;
h divides p & h divides q by C;
then h divides s by AS;
hence d divides g;
end;
then g is a,b-gcd by AS;
then g = a gcd b by dpg,B;
hence s = p gcd q by dd;
end;
hence thesis by G1;
end;