:: Field Extensions and {K}ronecker's Construction
:: by Christoph Schwarzweller
::
:: Received August 29, 2019
:: Copyright (c) 2019-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, VECTSP_1, ALGSTR_0, TARSKI, XCMPLX_0, VECTSP_2,
STRUCT_0, SUBSET_1, SUPINF_2, BINOP_1, INT_1, ALGSEQ_1, FINSET_1,
MESFUNC1, INT_3, REALSET1, C0SP1, GAUSSINT, NAT_1, WAYBEL20, MOD_4,
POLYNOM1, POLYNOM2, POLYNOM3, POLYNOM8, COMPLFLD, FUNCSDOM, GROEB_2,
EC_PF_1, HURWITZ, FINSEQ_1, RING_4, GROUP_1, FUNCT_2, ARYTM_1, CARD_3,
FUNCT_1, RELAT_1, FUNCOP_1, CARD_1, IDEAL_1, QUOFIELD, FDIFF_1, EQREL_1,
XBOOLE_0, NUMBERS, POLYNOM5, RING_2, RING_3, GROUP_6, FUNCT_4, ZFMISC_1,
XXREAL_0, FUNCT_7, YELLOW_8, ALGNUM_1, MSSUBFAM, RING_5, ORDINAL1,
GROUP_2, RLVECT_1, RLVECT_2, RLVECT_3, RLVECT_5, FIELD_1, FIELD_2,
FIELD_3, FIELD_4, FOMODEL1;
notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, RELAT_1, RELSET_1, REALSET1,
FUNCT_1, FUNCT_2, FINSEQ_1, FUNCOP_1, NUMBERS, ZFMISC_1, FUNCT_7,
EQREL_1, ORDINAL1, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, INT_1, INT_3,
GAUSSINT, VFUNCT_1, IDEAL_1, COMPLFLD, POLYNOM1, ALGSEQ_1, POLYNOM3,
POLYNOM4, POLYNOM5, FINSET_1, RINGCAT1, GROUP_1, GROUP_6, MOD_4,
RLVECT_1, ALGSTR_0, STRUCT_0, HURWITZ, MATRLIN, VECTSP_6, VECTSP_7,
VECTSP_9, VECTSP_2, VECTSP_1, C0SP1, EC_PF_1, RATFUNC1, QUOFIELD, RING_1,
RING_2, RING_3, RING_4, RING_5, ALGNUM_1, FIELD_1, FIELD_2, FIELD_3;
constructors REAL_1, FINSOP_1, BINARITH, VECTSP_2, POLYNOM3, ALGSTR_1,
MCART_1, NUMBERS, RING_1, ZFMISC_1, RELAT_1, XREAL_0, HURWITZ, VALUED_0,
STRUCT_0, C0SP1, GCD_1, COMPLFLD, FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0,
XXREAL_0, SUBSET_1, ORDINAL1, NAT_1, ALGSTR_0, POLYNOM4, XBOOLE_0,
RELSET_1, ARYTM_3, FUNCT_7, NAT_D, FINSEQ_1, VFUNCT_1, CARD_1, FINSET_1,
GAUSSINT, RATFUNC1, GROUP_6, REALSET1, UPROOTS, TSEP_1, ALGSTR_2, INT_3,
RINGCAT1, MEMBERED, IDEAL_1, RING_3, EC_PF_1, ALGSEQ_1, RING_2, VECTSP_9,
EQREL_1, RING_4, FUNCOP_1, GROUP_4, ALGNUM_1, MOD_4, RING_5, VECTSP_6,
FIELD_1, FIELD_2, FIELD_3;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
STRUCT_0, VECTSP_1, ALGSTR_1, VFUNCT_1, POLYNOM4, FUNCT_2, ALGSTR_0,
POLYNOM3, SUBSET_1, RLVECT_1, COMPLFLD, FUNCT_1, FINSET_1, INT_3,
RATFUNC1, GAUSSINT, RELAT_1, MOD_4, RING_2, RING_3, RING_4, RING_5,
REALSET1, FIELD_1, FIELD_2, FIELD_3;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions ALGSTR_0, VECTSP_1, RLVECT_1;
equalities BINOP_1, REALSET1, XCMPLX_0, STRUCT_0, ALGSTR_0, VECTSP_1;
expansions STRUCT_0, GROUP_1, VECTSP_1, RINGCAT1, TARSKI, GROUP_6, FUNCT_1,
FUNCT_2, RING_4;
theorems GROUP_1, VECTSP_2, RLVECT_1, IDEAL_1, GCD_1, C0SP1, SUBSET_1,
FUNCT_2, TARSKI, FUNCT_1, RELAT_1, POLYNOM1, EC_PF_1, POLYNOM4, ZFMISC_1,
GAUSSINT, ALGSEQ_1, RING_2, POLYNOM3, ALGNUM_1, NAT_1, RING_3, XXREAL_0,
XBOOLE_1, FINSEQ_1, NORMSP_1, RING_4, HURWITZ, XREAL_1, XREAL_0, MATRLIN,
POLYNOM5, XBOOLE_0, UPROOTS, RATFUNC1, RINGCAT1, STRUCT_0, RING_1,
RING_5, FIELD_1, FIELD_2, ALGSTR_0, VECTSP_1, VECTSP_6, VECTSP_7,
VECTSP_4, ORDINAL1, FIELD_3, LIOUVIL2;
schemes FUNCT_2;
begin :: Preliminaries
reserve K,F,E for Field,
R,S for Ring;
Th1:
R is Subring of R by LIOUVIL2:18;
theorem
K is Subfield of K
proof
A1: the addF of K = (the addF of K) || the carrier of K;
A2: the multF of K = (the multF of K) || the carrier of K;
the carrier of K c= the carrier of K & 1.K = 1.K & 0.K = 0.K;
hence thesis by A1,A2,EC_PF_1:def 1;
end;
registration
let R be non degenerated Ring;
cluster -> non degenerated for Subring of R;
coherence
proof
let S be Subring of R;
0.R = 0.S & 1.R = 1.S by C0SP1:def 3;
hence thesis;
end;
end;
registration
let R be comRing;
cluster -> commutative for Subring of R;
coherence
proof
let S be Subring of R;
now let a,b be Element of S;
the carrier of S c= the carrier of R by C0SP1:def 3; then
reconsider x = a, y = b as Element of R;
A1: [x,y] in [:the carrier of S, the carrier of S:] by ZFMISC_1:def 2;
A2: [y,x] in [:the carrier of S, the carrier of S:] by ZFMISC_1:def 2;
thus
a * b = ((the multF of R)||the carrier of S).(x,y) by C0SP1:def 3
.= x * y by A1,FUNCT_1:49
.= y * x by GROUP_1:def 12
.= ((the multF of R)||the carrier of S).(b,a) by A2,FUNCT_1:49
.= b * a by C0SP1:def 3;
end;
hence thesis;
end;
end;
registration
let R be domRing;
cluster -> domRing-like for Subring of R;
coherence
proof
let S be Subring of R;
now let a,b be Element of S;
assume
A1: a * b = 0.S;
the carrier of S c= the carrier of R by C0SP1:def 3; then
reconsider x = a, y = b as Element of R;
A2: [x,y] in [:the carrier of S, the carrier of S:] by ZFMISC_1:def 2;
A3: 0.S = 0.R by C0SP1:def 3;
a * b = ((the multF of R)||the carrier of S).(x,y) by C0SP1:def 3
.= x * y by A2,FUNCT_1:49;
hence a = 0.S or b = 0.S by A1,A3,VECTSP_2:def 1;
end;
hence thesis by VECTSP_2:def 1;
end;
end;
theorem Th2:
for S being Subring of R, F being FinSequence of R, G being FinSequence of S
st F = G holds Sum F = Sum G
proof
let S be Subring of R, F be FinSequence of R, G be FinSequence of S;
assume
A1: F = G;
the carrier of S c= the carrier of R by C0SP1:def 3; then
In(Sum G,R) = Sum G by SUBSET_1:def 8;
hence thesis by A1,ALGNUM_1:10;
end;
begin :: Ring and Field Extensions
definition
let R,S be Ring;
attr S is R-extending means :Def1:
R is Subring of S;
end;
registration
let R be Ring;
cluster R-extending for Ring;
existence
proof
take R;
thus thesis by Th1;
end;
end;
registration
let R be comRing;
cluster R-extending for comRing;
existence
proof
take R;
thus thesis by Th1;
end;
end;
registration
let R be domRing;
cluster R-extending for domRing;
existence
proof
take R;
thus thesis by Th1;
end;
end;
registration
let F be Field;
cluster F-extending for Field;
existence
proof
take F;
thus thesis by Th1;
end;
end;
definition
let R be Ring;
mode RingExtension of R is R-extending Ring;
end;
definition
let R be comRing;
mode comRingExtension of R is R-extending comRing;
end;
definition
let R be domRing;
mode domRingExtension of R is R-extending domRing;
end;
definition
let F be Field;
mode FieldExtension of F is F-extending Field;
end;
theorem
R is RingExtension of R
proof
R is Subring of R by Th1;
hence thesis by Def1;
end;
theorem
for R being comRing holds R is comRingExtension of R
proof
let R be comRing;
R is Subring of R by Th1;
hence thesis by Def1;
end;
theorem
for R being domRing holds R is domRingExtension of R
proof
let R be domRing;
R is Subring of R by Th1;
hence thesis by Def1;
end;
theorem Th3:
F is FieldExtension of F
proof
F is Subring of F by Th1;
hence thesis by Def1;
end;
theorem Th4:
E is FieldExtension of F iff F is Subfield of E
proof
A1: now assume E is FieldExtension of F; then
F is Subring of E by Def1;
hence F is Subfield of E by RING_3:45;
end;
now assume F is Subfield of E; then
F is Subring of E by RING_3:43;
hence E is FieldExtension of F by Def1;
end;
hence thesis by A1;
end;
registration
cluster F_Complex -> (F_Real)-extending;
coherence by RING_3:43,RING_3:48;
end;
registration
cluster F_Real -> (F_Rat)-extending;
coherence by RING_3:43,GAUSSINT:14;
end;
registration
cluster F_Rat -> (INT.Ring)-extending;
coherence by RING_3:47;
end;
registration
let R be Ring, S be RingExtension of R;
cluster -> R-extending for RingExtension of S;
coherence
proof
let T be RingExtension of S;
S is Subring of T & R is Subring of S by Def1;
hence thesis by ALGNUM_1:1;
end;
end;
registration
let R be comRing, S be comRingExtension of R;
cluster -> R-extending for comRingExtension of S;
coherence;
end;
registration
let R be domRing, S be domRingExtension of R;
cluster -> R-extending for domRingExtension of S;
coherence;
end;
registration
let F be Field, E be FieldExtension of F;
cluster -> F-extending for FieldExtension of E;
coherence;
end;
registration
let R be non degenerated Ring;
cluster -> non degenerated for RingExtension of R;
coherence
proof
let S be RingExtension of R;
A1: R is Subring of S by Def1;
now assume S is degenerated; then
1.R = 0.S by A1,C0SP1:def 3 .= 0.R by A1,C0SP1:def 3;
hence contradiction;
end;
hence thesis;
end;
end;
begin :: Extensions of Polynomial Rings
theorem Th5:
for S being RingExtension of R, p being Polynomial of R holds
p is Polynomial of S
proof
let S be RingExtension of R, p be Polynomial of R;
A1: R is Subring of S by Def1; then
A2: the carrier of R c= the carrier of S by C0SP1:def 3;
A3: 0.S = 0.R by A1,C0SP1:def 3;
rng p c= the carrier of R by RELAT_1:def 19; then
rng p c= the carrier of S by A2; then
reconsider p1 = p as sequence of (the carrier of S) by FUNCT_2:6;
A4: Support p is finite by POLYNOM1:def 5;
now let o be object;
assume
A5: o in Support p1; then
reconsider n = o as Element of NAT;
A6: 0.R <> p.n by A3,A5,POLYNOM1:def 3;
dom p = NAT by FUNCT_2:def 1;
hence o in Support p by A6,POLYNOM1:def 3;
end; then
Support p1 c= Support p;
hence thesis by A4,POLYNOM1:def 5;
end;
theorem
for R being Subring of S, p being Polynomial of R holds
p is Polynomial of S
proof
let R be Subring of S, p be Polynomial of R;
A2: the carrier of R c= the carrier of S by C0SP1:def 3;
A3: 0.S = 0.R by C0SP1:def 3;
rng p c= the carrier of R by RELAT_1:def 19; then
rng p c= the carrier of S by A2; then
reconsider p1 = p as sequence of (the carrier of S) by FUNCT_2:6;
A4: Support p is finite by POLYNOM1:def 5;
now let o be object;
assume
A5: o in Support p1; then
reconsider n = o as Element of NAT;
A6: 0.R <> p.n by A3,A5,POLYNOM1:def 3;
dom p = NAT by FUNCT_2:def 1;
hence o in Support p by A6,POLYNOM1:def 3;
end; then
Support p1 c= Support p;
hence thesis by A4,POLYNOM1:def 5;
end;
theorem Th6:
for S being RingExtension of R holds
the carrier of Polynom-Ring R c= the carrier of Polynom-Ring S
proof
let S be RingExtension of R;
now let o be object;
assume o in the carrier of Polynom-Ring R; then
o is Polynomial of R by POLYNOM3:def 10; then
o is Polynomial of S by Th5;
hence o in the carrier of Polynom-Ring S by POLYNOM3:def 10;
end;
hence thesis;
end;
theorem Th7:
S is RingExtension of R implies 0.(Polynom-Ring S) = 0.(Polynom-Ring R)
proof
assume S is R-extending Ring; then
A1: R is Subring of S by Def1;
thus
0.(Polynom-Ring R) = 0_.(R) by POLYNOM3:def 10
.= NAT --> 0.R by POLYNOM3:def 7
.= NAT --> 0.S by A1,C0SP1:def 3
.= 0_.(S) by POLYNOM3:def 7
.= 0.(Polynom-Ring S) by POLYNOM3:def 10;
end;
theorem Th8:
S is RingExtension of R implies 0_.(S) = 0_.(R)
proof
assume
A1: S is R-extending Ring;
thus 0_.(S) = 0.(Polynom-Ring S) by POLYNOM3:def 10
.= 0.(Polynom-Ring R) by A1,Th7
.= 0_.(R) by POLYNOM3:def 10;
end;
theorem Th9:
S is RingExtension of R implies 1.(Polynom-Ring S) = 1.(Polynom-Ring R)
proof
assume
A1: S is R-extending Ring; then
A2: R is Subring of S by Def1;
thus 1.(Polynom-Ring R) = 1_.(R) by POLYNOM3:def 10
.= 0_.(R)+*(0,1.R) by POLYNOM3:def 8
.= 0_.(R)+*(0,1.S) by A2,C0SP1:def 3
.= 0_.(S)+*(0,1.S) by A1,Th8
.= 1_.(S) by POLYNOM3:def 8
.= 1.(Polynom-Ring S) by POLYNOM3:def 10;
end;
theorem
for S being RingExtension of R holds 1_.(S) = 1_.(R)
proof
let S be R-extending Ring;
thus
1_.(S) = 1.(Polynom-Ring S) by POLYNOM3:def 10
.= 1.(Polynom-Ring R) by Th9
.= 1_.(R) by POLYNOM3:def 10;
end;
theorem Th10:
for S being RingExtension of R, p,q being Polynomial of R
for p1,q1 being Polynomial of S st p = p1 & q = q1 holds p + q = p1 + q1
proof
let S be RingExtension of R, p,q be Polynomial of R;
let p1,q2 be Polynomial of S;
assume
A1: p = p1 & q = q2;
A2: R is Subring of S by Def1;
now let n be Element of NAT;
p.n = p1.n & q.n = q2.n by A1; then
A3: [p1.n,q2.n] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
thus (p+q).n = p.n + q.n by NORMSP_1:def 2
.= ((the addF of S)||the carrier of R).(p1.n,q2.n) by A1,A2,C0SP1:def 3
.= p1.n + q2.n by A3,FUNCT_1:49
.= (p1+q2).n by NORMSP_1:def 2;
end;
hence thesis;
end;
theorem Th11:
for S being RingExtension of R holds
the addF of Polynom-Ring R
= (the addF of Polynom-Ring S)||the carrier of Polynom-Ring R
proof
let S be RingExtension of R;
set aR = the addF of Polynom-Ring R,
aS = (the addF of Polynom-Ring S)||the carrier of Polynom-Ring R;
set cR = the carrier of Polynom-Ring R,
cS = the carrier of Polynom-Ring S;
A1: cR c= cS by Th6;
A2: dom aS = dom(the addF of Polynom-Ring S) /\ [:cR,cR:] by RELAT_1:61
.= [:cS,cS:] /\ [:cR,cR:] by FUNCT_2:def 1
.= [:cR,cR:] by A1,ZFMISC_1:96,XBOOLE_1:28
.= dom aR by FUNCT_2:def 1;
now let o be object;
assume
A3: o in dom aR; then
consider p,q being object such that
A4: p in the carrier of Polynom-Ring R &
q in the carrier of Polynom-Ring R & o = [p,q] by ZFMISC_1:def 2;
reconsider p,q as Element of cR by A4;
reconsider p1 = p, q1 = q as Element of cS by A1;
reconsider p2 = p, q2 = q as Polynomial of R;
reconsider p3 = p1, q3 = q1 as Polynomial of S;
thus
aR.o = p + q by A4
.= p2 + q2 by POLYNOM3:def 10
.= p3 + q3 by Th10
.= p1 + q1 by POLYNOM3:def 10
.= aS.o by A2,A3,A4,FUNCT_1:47;
end;
hence thesis by A2;
end;
theorem Th12:
for S being RingExtension of R
for p,q being Polynomial of R
for p1,q1 being Polynomial of S st p = p1 & q = q1 holds p *' q = p1 *' q1
proof
let S be RingExtension of R;
let p,q be Polynomial of R; let p1,q2 be Polynomial of S;
assume
A1: p = p1 & q = q2;
A2: R is Subring of S by Def1;
now let n be Element of NAT;
consider r being FinSequence of the carrier of R such that
A3: len r = n+1 & (p*'q).n = Sum r &
for k being Element of NAT st k in dom r
holds r.k = p.(k-'1) * q.(n+1-'k) by POLYNOM3:def 9;
consider r1 being FinSequence of the carrier of S such that
A4: len r1 = n+1 & (p1*'q2).n = Sum r1 &
for k being Element of NAT st k in dom r1
holds r1.k = p1.(k-'1) * q2.(n+1-'k) by POLYNOM3:def 9;
A5: dom r1 = Seg(len r) by A3,A4,FINSEQ_1:def 3
.= dom r by FINSEQ_1:def 3;
now let m be Nat;
assume
A6: m in dom r;
p.(m-'1) = p1.(m-'1) & q.(n+1-'m) = q2.(n+1-'m) by A1; then
A7: [p1.(m-'1),q2.(n+1-'m)] in [:the carrier of R,the carrier of R:]
by ZFMISC_1:def 2;
thus
r.m = p.(m-'1) * q.(n+1-'m) by A6,A3
.= ((the multF of S)||the carrier of R).(p1.(m-'1),q2.(n+1-'m))
by A1,A2,C0SP1:def 3
.= p1.(m-'1) * q2.(n+1-'m) by A7,FUNCT_1:49
.= r1.m by A6,A5,A4;
end; then
r = r1 by A5;
hence (p*'q).n = (p1*'q2).n by A4,A3,A2,Th2;
end;
hence thesis;
end;
theorem Th13:
S is RingExtension of R implies the multF of Polynom-Ring R
= (the multF of Polynom-Ring S)||the carrier of Polynom-Ring R
proof
assume
AS: S is RingExtension of R;
set mR = the multF of Polynom-Ring R,
mS = (the multF of Polynom-Ring S)||the carrier of Polynom-Ring R;
set cR = the carrier of Polynom-Ring R,
cS = the carrier of Polynom-Ring S;
A1: cR c= cS by AS,Th6;
A2: dom mS = dom(the multF of Polynom-Ring S) /\ [:cR,cR:] by RELAT_1:61
.= [:cS,cS:] /\ [:cR,cR:] by FUNCT_2:def 1
.= [:cR,cR:] by A1,ZFMISC_1:96,XBOOLE_1:28
.= dom mR by FUNCT_2:def 1;
now let o be object;
assume
A3: o in dom mR; then
consider p,q being object such that
A4: p in cR & q in cR & o = [p,q] by ZFMISC_1:def 2;
reconsider p,q as Element of cR by A4;
reconsider p1 = p, q1 = q as Element of cS by A1;
reconsider p2 = p, q2 = q as Polynomial of R;
reconsider p3 = p1, q3 = q1 as Polynomial of S;
thus
mR.o = p * q by A4
.= p2 *' q2 by POLYNOM3:def 10
.= p3 *' q3 by AS,Th12
.= p1 * q1 by POLYNOM3:def 10
.= mS.o by A4,A2,A3,FUNCT_1:47;
end;
hence thesis by A2;
end;
registration
let R be Ring;
let S be RingExtension of R;
cluster Polynom-Ring S -> (Polynom-Ring R)-extending;
coherence
proof
set PS = Polynom-Ring S, PR = Polynom-Ring R;
A1: the addF of PR = (the addF of PS)||the carrier of PR by Th11;
A2: the multF of PR = (the multF of PS)||the carrier of PR by Th13;
1.PS = 1.PR & 0.PS = 0.PR by Th7,Th9;
hence thesis by Th6,A1,A2,C0SP1:def 3;
end;
end;
theorem
for R being Ring, S being RingExtension of R
holds Polynom-Ring S is RingExtension of Polynom-Ring R;
theorem
for S being RingExtension of R,
p being Element of the carrier of Polynom-Ring R,
q being Element of the carrier of Polynom-Ring S st p = q
holds deg p = deg q
proof
let S be RingExtension of R;
let p be Element of the carrier of Polynom-Ring R,
q be Element of the carrier of Polynom-Ring S;
assume
A1: p = q;
A2: R is Subring of S by Def1;
per cases;
suppose q is zero; then
len q = 0 by UPROOTS:17; then
A3: deg q = 0 - 1 by HURWITZ:def 2; then
q = 0_.(S) by HURWITZ:20
.= 0.(Polynom-Ring S) by POLYNOM3:def 10
.= 0.(Polynom-Ring R) by Th7
.= 0_.(R) by POLYNOM3:def 10;
hence deg p = deg q by A1,A3,HURWITZ:20;
end;
suppose
A4: q is non zero; then
len q > 0 by UPROOTS:17; then
A5: len q -' 1 = len q - 1 by XREAL_0:def 2; then
reconsider lenq = len q - 1 as Element of NAT;
A6: now let i be Nat;
assume i >= len q; then
q.i = 0.S by ALGSEQ_1:8;
hence p.i = 0.R by A1,A2,C0SP1:def 3;
end;
now let m be Nat;
assume
A7: m is_at_least_length_of p;
now assume len q > m; then
lenq + 1 > m; then
lenq >= m by NAT_1:13; then
p.(len q-'1) = 0.R by A5,A7,ALGSEQ_1:def 2; then
A8: q.(len q-'1) = 0.S by A1,A2,C0SP1:def 3;
0 + 1 < len q + 1 by A4,XREAL_1:8,UPROOTS:17; then
len q >= 1 by NAT_1:13; then
(len q-'1) + 1 = len q by XREAL_1:235;
hence contradiction by A8,ALGSEQ_1:10;
end;
hence len q <= m;
end; then
len p = len q by A6,ALGSEQ_1:def 3,ALGSEQ_1:def 2;
hence deg p = len q - 1 by HURWITZ:def 2 .= deg q by HURWITZ:def 2;
end;
end;
Lm2:
for S being RingExtension of R, a being Element of R, b being Element of S
st a = b holds -a = -b
proof
let S be RingExtension of R;
let a be Element of R, b be Element of S;
assume
A1: a = b;
A2: R is Subring of S by Def1; then
the carrier of R c= the carrier of S by C0SP1:def 3; then
reconsider x = -a as Element of S;
A3: [a,-a] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
A4: (the addF of S)||the carrier of R = the addF of R by A2,C0SP1:def 3;
b + x = a + -a by A1,A4,A3,FUNCT_1:49
.= 0.R by RLVECT_1:5
.= 0.S by A2,C0SP1:def 3;
hence thesis by RLVECT_1:def 10;
end;
theorem
for R being non degenerated Ring, S being RingExtension of R,
a being Element of R, b being Element of S st a = b
holds rpoly(1,a) = rpoly(1,b)
proof
let R be non degenerated Ring, S be RingExtension of R;
let a be Element of R, b be Element of S;
assume
A1: a = b;
A2: R is Subring of S by Def1;
A3: the carrier of Polynom-Ring R c= the carrier of Polynom-Ring S by Th6;
set q = rpoly(1,b);
reconsider p = rpoly(1,a) as Element of the carrier
of Polynom-Ring R by POLYNOM3:def 10;
reconsider p as Element of the carrier of Polynom-Ring S by A3;
reconsider p as Polynomial of S;
len q > 0 by UPROOTS:17; then
A4: len q -' 1 = len q - 1 by XREAL_0:def 2; then
reconsider lenq = len q - 1 as Element of NAT;
A5: 1 = deg q by HURWITZ:27 .= len q - 1 by HURWITZ:def 2; then
A6: len q = 1 + 1;
A7: now let i be Nat;
assume
A8: i >= len q;
reconsider j = i as Element of NAT by ORDINAL1:def 12;
j <> 0 & j <> 1 by A8,A6; then
rpoly(1,a).j = 0.R by HURWITZ:26;
hence p.i = 0.S by A2,C0SP1:def 3;
end;
now let m be Nat;
assume
A9: m is_at_least_length_of p;
reconsider j = lenq as Element of NAT;
now assume len q > m; then
lenq + 1 > m; then
lenq >= m by NAT_1:13; then
A10: p.(len q-'1) = 0.S by A4,A9,ALGSEQ_1:def 2;
rpoly(1,a).1 = 1_R by HURWITZ:25 .= 1.S by A2,C0SP1:def 3;
hence contradiction by A10,A5,XREAL_0:def 2;
end;
hence len q <= m;
end; then
A11: len p = len q by A7,ALGSEQ_1:def 3,ALGSEQ_1:def 2;
now let k be Nat;
assume
A12: k < len q;
len q - 1 = deg q by HURWITZ:def 2 .= 1 by HURWITZ:27; then
k < 1 + 1 by A12; then
A13: k <= 1 by NAT_1:13;
per cases;
suppose
A14: k = 0; then
A15: rpoly(1,a).k = -power(R).(a,0+1) by HURWITZ:25
.= -(power(R).(a,0) * a) by GROUP_1:def 7
.= -(1_R * a) by GROUP_1:def 7
.= -b by A1,Lm2;
q.k = -power(S).(b,0+1) by A14,HURWITZ:25
.= -(power(S).(b,0) * b) by GROUP_1:def 7
.= -(1_S * b) by GROUP_1:def 7
.= -b;
hence p.k = q.k by A15;
end;
suppose k <> 0; then
k + 1 > 0 + 1 by XREAL_1:6; then
A16: k >= 1 by NAT_1:13; then
A17: k = 1 by A13,XXREAL_0:1;
rpoly(1,a).1 = 1_R by HURWITZ:25 .= 1.S by A2,C0SP1:def 3;
hence p.k = 1_S by A16,A13,XXREAL_0:1 .= q.k by
A17,HURWITZ:25;
end;
end;
hence thesis by A11,ALGSEQ_1:12;
end;
begin :: Evaluation of Polynomials in Ring Extensions
theorem
for a be Element of S holds
S is RingExtension of R implies Ext_eval(0_.(R),a) = 0.S by ALGNUM_1:13;
theorem
for R being non degenerated Ring, S being RingExtension of R,
a being Element of S holds Ext_eval(1_.(R),a) = 1.S
proof
let R be non degenerated Ring, S be RingExtension of R;
let a be Element of S;
R is Subring of S by Def1;
hence thesis by ALGNUM_1:14;
end;
theorem
for S being RingExtension of R,a being Element of S,
p,q being Polynomial of R holds
Ext_eval(p+q,a) = Ext_eval(p,a) + Ext_eval(q,a)
proof
let S be RingExtension of R, a be Element of S;
let p,q be Polynomial of R;
R is Subring of S by Def1;
hence thesis by ALGNUM_1:15;
end;
theorem
for R being comRing, S being comRingExtension of R, a being Element of S,
p,q being Polynomial of R holds
Ext_eval(p*'q,a) = Ext_eval(p,a) * Ext_eval(q,a)
proof
let R be comRing, S be comRingExtension of R;
let a be Element of S;
let p,q be Polynomial of R;
R is Subring of S by Def1;
hence thesis by ALGNUM_1:20;
end;
Th14:
for S being RingExtension of R,
p being Element of the carrier of Polynom-Ring R,
a being Element of R, b being Element of S st b = a holds
Ext_eval(p,b) = eval(p,a)
proof
let S be RingExtension of R;
let p be Element of the carrier of Polynom-Ring R;
let a be Element of R, b be Element of S;
assume
A1: b = a;
A2: R is Subring of S by Def1; then
A3: the carrier of R c= the carrier of S by C0SP1:def 3;
Ext_eval(p,In(a,S)) = In(eval(p,a),S) by A2,ALGNUM_1:12
.= eval(p,a) by A3,SUBSET_1:def 8;
hence thesis by A1;
end;
theorem Th15:
for S being RingExtension of R,
p being Element of the carrier of (Polynom-Ring R),
q being Element of the carrier of Polynom-Ring S,
a being Element of S st p = q holds Ext_eval(p,a) = eval(q,a)
proof
let S be RingExtension of R;
let p be Element of the carrier of (Polynom-Ring R),
q be Element of the carrier of Polynom-Ring S;
let a be Element of S;
assume
A1: p = q;
A2: R is Subring of S by Def1;
per cases;
suppose q is zero; then
A3: q = 0_.(S) by UPROOTS:def 5;
p = 0.(Polynom-Ring S) by A1,A3,POLYNOM3:def 10
.= 0.(Polynom-Ring R) by Th7
.= 0_.(R) by POLYNOM3:def 10;
hence
Ext_eval(p,a) = 0.S by ALGNUM_1:13 .= eval(q,a) by A3,POLYNOM4:17;
end;
suppose
A4: q is non zero; then
len q > 0 by UPROOTS:17; then
A5: len q -' 1 = len q - 1 by XREAL_0:def 2; then
reconsider lenq = len q - 1 as Element of NAT;
consider Fp being FinSequence of S such that
A6: Ext_eval(p,a) = Sum Fp & len Fp = len p &
for n being Element of NAT st n in dom Fp holds
Fp.n = In(p.(n-'1),S) * (power S).(a,n-'1) by ALGNUM_1:def 1;
consider Fq being FinSequence of the carrier of S such that
A7: eval(q,a) = Sum Fq & len Fq = len q &
for n being Element of NAT st n in dom Fq holds
Fq.n = q.(n-'1) * (power S).(a,n-'1) by POLYNOM4:def 2;
A8: now let i be Nat;
assume i >= len q; then
q.i = 0.S by ALGSEQ_1:8;
hence p.i = 0.R by A1,A2,C0SP1:def 3;
end;
now let m be Nat;
assume
A9: m is_at_least_length_of p;
now assume len q > m; then
lenq + 1 > m; then
lenq >= m by NAT_1:13; then
p.(len q-'1) = 0.R by A5,A9,ALGSEQ_1:def 2; then
A10: q.(len q-'1) = 0.S by A1,A2,C0SP1:def 3;
0 + 1 < len q + 1 by A4,XREAL_1:8,UPROOTS:17; then
len q >= 1 by NAT_1:13; then
(len q-'1) + 1 = len q by XREAL_1:235;
hence contradiction by A10,ALGSEQ_1:10;
end;
hence len q <= m;
end; then
len p = len q by A8,ALGSEQ_1:def 3,ALGSEQ_1:def 2; then
A11: dom Fq = Seg(len p) by A7,FINSEQ_1:def 3
.= dom Fp by A6,FINSEQ_1:def 3;
for n being Nat st n in dom Fp holds Fq.n = Fp.n
proof
let n be Nat;
assume
A12: n in dom Fp;
hence Fp.n = In(p.(n-'1),S) * (power S).(a,n-'1) by A6
.= q.(n-'1) * (power S).(a,n-'1) by A1
.= Fq.n by A7,A11,A12;
end;
hence thesis by A6,A7,A11,FINSEQ_1:13;
end;
end;
theorem
for S being RingExtension of R,
p being Element of the carrier of (Polynom-Ring R),
q being Element of the carrier of Polynom-Ring S,
a being Element of R, b being Element of S st q = p & b = a
holds eval(q,b) = eval(p,a)
proof
let S be RingExtension of R,
p be Element of the carrier of (Polynom-Ring R),
q be Element of the carrier of Polynom-Ring S,
a being Element of R, b being Element of S;
assume that
A1: p = q and
A2: a = b;
thus eval(p,a) = Ext_eval(p,b) by A2,Th14 .= eval(q,b) by A1,Th15;
end;
definition
let R be Ring, S be RingExtension of R;
let p be Element of the carrier of Polynom-Ring R;
let a be Element of S;
pred a is_a_root_of p,S means
Ext_eval(p,a) = 0.S;
end;
definition
let R be Ring, S be RingExtension of R;
let p be Element of the carrier of Polynom-Ring R;
pred p is_with_roots_in S means
ex a being Element of S st a is_a_root_of p,S;
end;
definition
let R be Ring, S be RingExtension of R;
let p be Element of the carrier of Polynom-Ring R;
func Roots(S,p) -> Subset of S equals
{a where a is Element of S : a is_a_root_of p,S};
coherence
proof
now let o be object;
assume o in {a where a is Element of S : a is_a_root_of p,S}; then
consider a being Element of S such that
A1: o = a & a is_a_root_of p,S;
thus o in the carrier of S by A1;
end;
hence thesis by TARSKI:def 3;
end;
end;
theorem
for S being RingExtension of R,
p being Element of the carrier of Polynom-Ring R
holds Roots p c= Roots(S,p)
proof
let S be RingExtension of R;
let p be Element of the carrier of Polynom-Ring R;
A1: R is Subring of S by Def1; then
A2: the carrier of R c= the carrier of S by C0SP1:def 3;
now let o be object;
assume
A3: o in Roots p; then
reconsider a = o as Element of R;
A4: a is_a_root_of p by A3,POLYNOM5:def 10;
reconsider b = a as Element of S by A2;
Ext_eval(p,b) = eval(p,a) by Th14
.= 0.R by A4,POLYNOM5:def 7
.= 0.S by A1,C0SP1:def 3; then
b is_a_root_of p,S;
hence o in Roots(S,p);
end;
hence thesis;
end;
::: changed Element of the carrier of Polynom-Ring R -> Polynomial R
definition
let R be Ring, S be non degenerated Ring;
let p be Polynomial of R;
pred p splits_in S means
ex a being non zero Element of S, q being Ppoly of S st p = a * q;
end;
::: changed Element of the carrier of Polynom-Ring R -> Polynomial R
theorem
for F being Field, p be Polynomial of F st deg p = 1 holds p splits_in F
proof
let F be Field;
let p be Polynomial of F;
assume deg p = 1; then
consider x,z being Element of F such that
A1: x <> 0.F & p = x * rpoly(1,z) by HURWITZ:28;
reconsider x as non zero Element of F by A1,STRUCT_0:def 12;
reconsider q = rpoly(1,z) as Ppoly of F by RING_5:51;
p = x * q by A1;
hence thesis;
end;
begin :: Degree of Extension
definition
let R be Ring, S be RingExtension of R;
func VecSp(S,R) -> strict ModuleStr over R means
:Def5:
the carrier of it = the carrier of S &
the addF of it = the addF of S &
the ZeroF of it = 0.S &
the lmult of it = (the multF of S)|[:the carrier of R,the carrier of S:];
existence
proof
set C = the carrier of S;
R is Subring of S by Def1; then
the carrier of R c= C by C0SP1:def 3; then
[:the carrier of R,C:] c= [:C,C:] by ZFMISC_1:96; then
reconsider lm = (the multF of S)|[:the carrier of R,C:]
as Function of [:the carrier of R,C:],C by FUNCT_2:32;
take ModuleStr (# C,the addF of S,0.S,lm #);
thus thesis;
end;
uniqueness;
end;
registration
let R be Ring, S be RingExtension of R;
cluster VecSp(S,R) -> non empty;
coherence
proof
0.S in the carrier of S;
hence thesis by Def5;
end;
end;
registration
let R be Ring, S be RingExtension of R;
cluster VecSp(S,R) ->
Abelian add-associative right_zeroed right_complementable;
coherence
proof
set E = S, F = R; set P = VecSp(E,F);
A1: 0.P = 0.E by Def5;
hereby
let x,y be Element of P;
reconsider a = x, b = y as Element of E by Def5;
thus
x+y = a+b by Def5 .= b+a by RLVECT_1:def 2 .= y+x by Def5;
end;
hereby
let x,y,z be Element of P;
reconsider a = x, b = y, c = z as Element of E by Def5;
A2: y+z = b+c by Def5;
x+y = a+b by Def5;
hence x+y+z = a+b+c by Def5
.= a+(b+c) by RLVECT_1:def 3
.= x+(y+z) by A2,Def5;
end;
hereby
let x be Element of P;
reconsider a = x as Element of E by Def5;
thus x+0.P = a+0.E by A1,Def5 .= x;
end;
let x be Element of P;
reconsider a = x as Element of E by Def5;
consider b being Element of E such that
A3: a + b = 0.E by ALGSTR_0:def 11;
reconsider y = b as Element of P by Def5;
take y;
thus x+y = a+b by Def5 .= 0.P by A3,Def5;
end;
end;
Lm3:
for E be RingExtension of R, a,b be Element of E, s be Element of R,
v be Element of VecSp(E,R) st a = s & b = v holds a*b = s*v
proof
let E be RingExtension of R;
let a,b be Element of E;
let s be Element of R, v be Element of VecSp(E,R) such that
A1: a = s & b = v;
the carrier of VecSp(E,R) = the carrier of E by Def5; then
A2: [s,v] in [:the carrier of R,the carrier of E:] by ZFMISC_1:def 2;
thus
s * v
= ((the multF of E)|[:the carrier of R,the carrier of E:]).(s,v) by Def5
.= a*b by A1,A2,FUNCT_1:49;
end;
Lm4:
for E be RingExtension of R, a,b be Element of E, x,y be Element of R
st a = x & b = y holds a+b = x+y
proof
let E be RingExtension of R;
let a,b be Element of E;
let x,y be Element of R such that
A1: a = x & b = y;
A2: R is Subring of E by Def1;
A3: [x,y] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
thus
x+y = ((the addF of E)||(the carrier of R)).(x,y) by A2,C0SP1:def 3
.= a+b by A1,A3,FUNCT_1:49;
end;
Lm5:
for E be RingExtension of R, a,b be Element of E, x,y be Element of R
st a = x & b = y holds a*b = x*y
proof
let E be RingExtension of R;
let a,b be Element of E;
let x,y be Element of R such that
A1: a = x & b = y;
A2: R is Subring of E by Def1;
A3: [x,y] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
thus
x*y = ((the multF of E)||(the carrier of R)).(x,y) by A2,C0SP1:def 3
.= a*b by A1,A3,FUNCT_1:49;
end;
registration
let R be Ring, S be RingExtension of R;
cluster VecSp(S,R) ->
scalar-distributive scalar-associative scalar-unital vector-distributive;
coherence
proof
set E = S, F = R; set P = VecSp(E,F);
A1: F is Subring of E by Def1; then
A2: the carrier of F c= the carrier of E by C0SP1:def 3;
hereby
let x,y be Element of F;
let v be Element of P;
reconsider a = x, b = y, c = v as Element of E by A2,Def5;
A3: (a+b)*c = a*c+b*c by VECTSP_1:def 3;
x*v = a*c & y*v = b*c by Lm3; then
x*v+y*v = a*c + b*c by Def5;
hence (x+y)*v = x*v+y*v by A3,Lm3,Lm4;
end;
hereby
let x,y be Element of F;
let v be Element of P;
reconsider a = x, b = y, c = v as Element of E by A2,Def5;
A4: (a*b)*c = a*(b*c) by GROUP_1:def 3;
A5: (a*b)*c = (x*y)*v by Lm3,Lm5;
b*c = y*v by Lm3;
hence (x*y) * v = x * (y*v) by A4,A5,Lm3;
end;
hereby
let v be Element of P;
reconsider c = v as Element of E by Def5;
A6: 1.F = 1.E by C0SP1:def 3,A1;
(1.E) * c = c;
hence (1.F) * v = v by Lm3,A6;
end;
hereby
let x be Element of F;
let v,w be Element of P;
reconsider a = x, b = v, c = w as Element of E by A2,Def5;
A7: a*(b+c) = a*b+a*c by VECTSP_1:def 2;
b+c = v+w by Def5; then
A8: a*(b+c) = x*(v+w) by Lm3;
a*b = x*v & a*c = x*w by Lm3;
hence x*(v+w) = x*v+x*w by A7,A8,Def5;
end;
end;
end;
theorem
for S being RingExtension of R holds VecSp(S,R) is VectSp of R;
definition
let F be Field, E be FieldExtension of F;
func deg(E,F) -> Integer equals
:Def6:
dim VecSp(E,F) if VecSp(E,F) is finite-dimensional
otherwise -1;
coherence;
consistency;
end;
registration
let F be Field, E be FieldExtension of F;
cluster deg(E,F) -> dim-like;
coherence
proof
now assume
A1: not deg(E,F) = -1;
dim VecSp(E,F) is Nat;
hence deg(E,F) is natural by Def6,A1;
end;
hence thesis;
end;
end;
definition
let F be Field, E be FieldExtension of F;
attr E is F-finite means
:Def7:
VecSp(E,F) is finite-dimensional;
end;
registration
let F be Field;
cluster F-finite for FieldExtension of F;
existence
proof
reconsider E = F as FieldExtension of F by Th3;
take E;
set V = VecSp(E,F);
A1: the carrier of V = the carrier of E by Def5;
reconsider e = 1.E as Vector of V by Def5;
for x be object st x in {1.E} holds x in the carrier of V by A1; then
reconsider A = {e} as Subset of V by TARSKI:def 3;
0.V = 0.E by Def5; then
A2: A is linearly-independent by VECTSP_7:3;
A3: the carrier of Lin(A) =
the set of all Sum(l) where l is Linear_Combination of A by VECTSP_7:def 2;
A4: now let o be object;
assume o in the carrier of V; then
reconsider v = o as Element of the carrier of V;
reconsider a = v as Element of E by Def5;
defpred P[object,object] means
($1 = e & $2 = a) or ($1 <> e & $2 = 0.E);
A6: for x being object st x in the carrier of V
ex y being object st y in the carrier of E & P[x,y]
proof
let o be object;
assume o in the carrier of V;
per cases;
suppose
A7: o = e;
take a;
thus thesis by A7;
end;
suppose
A8: o <> e;
take 0.E;
thus thesis by A8;
end;
end;
consider f being Function of the carrier of V, the carrier of E
such that
A9: for x being object st x in the carrier of V holds P[x,f.x]
from FUNCT_2:sch 1(A6);
dom f = the carrier of V & rng f c= the carrier of E
by RELAT_1:def 19,FUNCT_2:def 1; then
reconsider f as Element of Funcs(the carrier of V, the carrier of E)
by FUNCT_2:def 2;
ex T being finite Subset of V st
for v being Element of V st not v in T holds f.v = 0.E
proof
e in the carrier of V; then
for x be object holds x in {e} implies x in the carrier of V
by TARSKI:def 1; then
reconsider T = {e} as finite Subset of V by TARSKI:def 3;
take T;
now let u be Element of V;
assume not u in T; then
u <> e by TARSKI:def 1;
hence f.u = 0.E by A9;
end;
hence thesis;
end; then
reconsider l = f as Linear_Combination of V by VECTSP_6:def 1;
now let o be object;
assume o in Carrier l; then
o in {v where v is Element of V: l.v <> 0.E} by VECTSP_6:def 2; then
consider u being Element of V such that
A10: o = u & l.u <> 0.E;
u = e by A10,A9;
hence o in A by A10,TARSKI:def 1;
end; then
Carrier l c= A; then
reconsider l as Linear_Combination of A by VECTSP_6:def 4;
Sum l = l.e * e by VECTSP_6:17
.= ((the multF of E)|[:the carrier of F,the carrier of E:]).(l.e,e)
by Def5
.= a * 1.E by A9
.= v;
hence o in the set of all Sum(l) where l is Linear_Combination of A;
end;
now let o be object;
assume o in the set of all Sum(l) where l is Linear_Combination of A;
then
consider l being Linear_Combination of A such that
A11: o = Sum l;
thus o in the carrier of V by A11;
end; then
the carrier of V = the set of all Sum(l) where
l is Linear_Combination of A by A4,TARSKI:2; then
A is Basis of V by A3,A2,VECTSP_4:31,VECTSP_7:def 3;
hence thesis by MATRLIN:def 1;
end;
end;
registration
let F be Field;
let E be F-finite FieldExtension of F;
cluster deg(E,F) -> natural;
coherence
proof
dim VecSp(E,F) is Nat;
hence deg(E,F) is natural by Def7,Def6;
end;
end;
begin :: Kronecker's Theorem
registration
let F be Field, p be non constant Element of the carrier of Polynom-Ring F;
cluster the carrier of (Polynom-Ring p) -> F-polynomial-membered;
coherence
proof
A1: the carrier of (Polynom-Ring p) =
{q where q is Polynomial of F : deg q < deg p} by RING_4:def 8;
now let o be object;
assume o in the carrier of (Polynom-Ring p); then
consider q being Polynomial of F such that
A2: q = o & deg q < deg p by A1;
thus
o is Polynomial of F by A2;
end;
hence thesis;
end;
cluster Polynom-Ring p -> F-polynomial-membered;
coherence;
end;
definition
let F be Field, p be irreducible Element of the carrier of Polynom-Ring F;
func KroneckerIso p ->
Function of the carrier of Polynom-Ring p,the carrier of KroneckerField(F,p)
means
:Def8:
for q being Element of the carrier of Polynom-Ring p
holds it.q = Class(EqRel(Polynom-Ring F,{p}-Ideal),q);
existence
proof
deffunc F(object) = Class(EqRel(Polynom-Ring F,{p}-Ideal),$1);
A1: the carrier of Polynom-Ring p =
{q where q is Polynomial of F : deg q < deg p} by RING_4:def 8;
A2: now let x be object;
assume
A3: x in the carrier of Polynom-Ring p;
for a being Element of Polynom-Ring p
holds a in the carrier of Polynom-Ring F
proof
let a be Element of Polynom-Ring p;
a in {q where q is Polynomial of F : deg q < deg p} by A1; then
ex r being Polynomial of F st r = a & deg r < deg p;
hence thesis by POLYNOM3:def 10;
end; then
reconsider a = x as Element of Polynom-Ring F by A3;
Class(EqRel(Polynom-Ring F,{p}-Ideal),a) is
Element of (Polynom-Ring F)/({p}-Ideal) by RING_1:12; then
Class(EqRel(Polynom-Ring F,{p}-Ideal),a) in
the carrier of (Polynom-Ring F)/({p}-Ideal);
hence F(x) in the carrier of KroneckerField(F,p) by FIELD_1:def 3;
end;
consider g being Function of the carrier of Polynom-Ring p,
the carrier of KroneckerField(F,p) such that
A4: for x being object st x in the carrier of Polynom-Ring p holds
g.x = F(x) from FUNCT_2:sch 2(A2);
take g;
thus
thesis by A4;
end;
uniqueness
proof
set R = Polynom-Ring p;
let F1,F2 be Function of the carrier of Polynom-Ring p,
the carrier of KroneckerField(F,p) such that
A5: for q being Element of R
holds F1.q = Class(EqRel(Polynom-Ring F,{p}-Ideal),q) and
A6: for q being Element of R
holds F2.q = Class(EqRel(Polynom-Ring F,{p}-Ideal),q);
now let q be Element of R;
thus
F1.q = Class(EqRel(Polynom-Ring F,{p}-Ideal),q) by A5 .= F2.q by A6;
end;
hence thesis;
end;
end;
Lm6:
for L be Ring, a be Element of Polynom-Ring L, p be Polynomial of L
st a = p holds - a = -p
proof
let L be Ring, 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
.= p - p by POLYNOM3:def 6
.= 0_.(L) by POLYNOM3:29
.= 0.(Polynom-Ring(L)) by POLYNOM3:def 10; then
a = - x by RLVECT_1:6;
hence - a = -p;
end;
Lm7:
for L be Ring, a,b be Element of Polynom-Ring L, p,q be Polynomial of L
st a = p & b = q holds a -b = p - q
proof
let L be Ring, a,b be Element of Polynom-Ring L, p,q be Polynomial of L;
assume
A1: a = p & b = q; then
-b = -q by Lm6;
hence a - b = p + (-q) by A1,POLYNOM3:def 10
.= p - q by POLYNOM3:def 6;
end;
Lm8:
for F be Field, p be irreducible Element of the carrier of Polynom-Ring F,
a be Element of Polynom-Ring p holds
a in the carrier of Polynom-Ring F
proof
let F be Field,
p be irreducible Element of the carrier of Polynom-Ring F,
a be Element of Polynom-Ring p;
the carrier of Polynom-Ring p
= {q where q is Polynomial of F : deg q < deg p} by RING_4:def 8; then
a in {q where q is Polynomial of F : deg q < deg p}; then
ex r being Polynomial of F st r = a & deg r < deg p;
hence a in the carrier of Polynom-Ring F by POLYNOM3:def 10;
end;
Lm9:
for F be Field,
p be irreducible Element of the carrier of Polynom-Ring F,
a be Element of the carrier of Polynom-Ring F,
q be Element of Polynom-Ring p st a = q
holds - a = -q
proof
let F be Field,
p be irreducible Element of the carrier of Polynom-Ring F,
a be Element of the carrier of Polynom-Ring F,
q be Element of Polynom-Ring p;
reconsider x = -q as Element of Polynom-Ring F by Lm8;
A1: the addF of Polynom-Ring p
= (the addF of Polynom-Ring F)||(the carrier of Polynom-Ring p)
by RING_4:def 8;
A2: the ZeroF of Polynom-Ring p = 0_.(F) by RING_4:def 8;
assume
A3: a = q;
[a,x] in [:the carrier of Polynom-Ring p,
the carrier of Polynom-Ring p:] by A3,ZFMISC_1:def 2; then
a + x = q + -q by A3,A1,FUNCT_1:49
.= 0.(Polynom-Ring p) by RLVECT_1:5
.= 0.(Polynom-Ring(F)) by A2,POLYNOM3:def 10; then
a = - x by RLVECT_1:6;
hence - a = -q;
end;
Lm10:
for F be Field, p be irreducible Element of the carrier of Polynom-Ring F,
a,b be Element of the carrier of Polynom-Ring F,
q,r be Element of Polynom-Ring p st a = q & b = r holds a - b = q - r
proof
let F be Field, p be irreducible Element of the carrier of Polynom-Ring F,
a,b be Element of the carrier of Polynom-Ring F,
q,r be Element of Polynom-Ring p;
assume
A1: a = q & b = r; then
-b = -r by Lm9; then
A2: [a,-b] in [:the carrier of Polynom-Ring p,
the carrier of Polynom-Ring p:] by A1,ZFMISC_1:def 2;
A3: the addF of Polynom-Ring p
= (the addF of Polynom-Ring F)||(the carrier of Polynom-Ring p)
by RING_4:def 8;
a - b = (the addF of Polynom-Ring p).(a,-b) by A2,A3,FUNCT_1:49
.= q - r by A1,Lm9;
hence thesis;
end;
registration
let F be Field, p be irreducible Element of the carrier of Polynom-Ring F;
cluster KroneckerIso p ->
additive multiplicative unity-preserving one-to-one onto;
coherence
proof
set R = Polynom-Ring p, f = KroneckerIso p;
now let a,b be Element of R;
reconsider r = a, q = b as Element of Polynom-Ring F by Lm8;
reconsider fa = f.a, fb = f.b as Element of (Polynom-Ring F)/({p}-Ideal)
by FIELD_1:def 3;
A1: fa = Class(EqRel(Polynom-Ring F,{p}-Ideal),a) by Def8;
A2: fb = Class(EqRel(Polynom-Ring F,{p}-Ideal),b) by Def8;
A3: [a,b] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
A4: a + b = ((the addF of Polynom-Ring F)||(the carrier of R)).(a,b)
by RING_4:def 8
.= r + q by A3,FUNCT_1:49;
thus f.a + f.b = fa + fb by FIELD_1:def 3
.= Class(EqRel(Polynom-Ring F,{p}-Ideal),a+b) by A4,A1,A2,RING_1:13
.= f.(a+b) by Def8;
end;
hence f is additive;
now let a,b be Element of R;
reconsider r = a, q = b as Element of the carrier of Polynom-Ring F
by Lm8;
reconsider fa = f.a, fb = f.b as Element of (Polynom-Ring F)/({p}-Ideal)
by FIELD_1:def 3;
A5: fa = Class(EqRel(Polynom-Ring F,{p}-Ideal),a) by Def8;
A6: fb = Class(EqRel(Polynom-Ring F,{p}-Ideal),b) by Def8;
A7: [a,b] in [:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
A8: a * b = (poly_mult_mod p)||(the carrier of R).(a,b) by RING_4:def 8
.= (poly_mult_mod p).(r,q) by A7,FUNCT_1:49
.= (r *' q) mod p by RING_4:def 7;
reconsider c = (r *' q) mod p as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
reconsider d = (r *' q) div p as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
A9: (r *' q) - ((r *' q) mod p)
= ((r *' q) div p) *' p + ((r *' q) mod p)-((r *' q) mod p) by RING_4:4
.= (((r *' q) div p) *' p + ((r *' q) mod p)) + -((r *' q) mod p)
by POLYNOM3:def 6
.= ((r *' q) div p) *' p + (((r *' q) mod p) + -((r *' q) mod p))
by POLYNOM3:26
.= ((r *' q) div p) *' p + (((r *' q) mod p) - ((r *' q) mod p))
by POLYNOM3:def 6
.= ((r *' q) div p) *' p + 0_.(F) by POLYNOM3:29
.= ((r *' q) div p) *' p;
r * q = r *' q by POLYNOM3:def 10; then
A10: r * q - c = ((r *' q) div p) *' p by A9,Lm7
.= p * d by POLYNOM3:def 10;
{p}-Ideal = the set of all p * r where r is Element of Polynom-Ring F
by IDEAL_1:64; then
A11: r*q - c in {p}-Ideal by A10;
thus
f.a * f.b = fa * fb by FIELD_1:def 3
.= Class(EqRel(Polynom-Ring F,{p}-Ideal),r*q) by A5,A6,RING_1:14
.= Class(EqRel(Polynom-Ring F,{p}-Ideal),a*b) by A11,A8,RING_1:6
.= f.(a*b) by Def8;
end;
hence f is multiplicative;
f.1_R = Class(EqRel(Polynom-Ring F,{p}-Ideal),1.R) by Def8
.= Class(EqRel(Polynom-Ring F,{p}-Ideal),1_.(F)) by RING_4:def 8
.= Class(EqRel(Polynom-Ring F,{p}-Ideal),1.(Polynom-Ring F))
by POLYNOM3:def 10
.= 1.((Polynom-Ring F)/({p}-Ideal)) by RING_1:def 6
.= 1_KroneckerField(F,p) by FIELD_1:def 3;
hence f is unity-preserving;
now let x1,x2 be object;
assume
A12: x1 in dom f & x2 in dom f & f.x1 = f.x2; then
reconsider a = x1, b = x2 as Element of the carrier of Polynom-Ring p;
reconsider q = a, r = b as Element of the carrier of Polynom-Ring F by Lm8;
Class(EqRel(Polynom-Ring F,{p}-Ideal),q) = f.b by A12,Def8
.= Class(EqRel(Polynom-Ring F,{p}-Ideal),r) by Def8; then
q - r in {p}-Ideal by RING_1:6; then
q - r in the set of all p*s where s is Element of Polynom-Ring F
by IDEAL_1:64; then
consider u being Element of the carrier of Polynom-Ring F such that
A13: q - r = p * u;
reconsider s = p *'u as Polynomial of F;
A14: q - r = a - b by Lm10;
now assume
A15: u <> 0_.(F); then
reconsider degu = deg u as Element of NAT by FIELD_1:1;
degu >= 0; then
A16: deg p + deg u >= deg p + 0 by XREAL_1:6;
now assume p *' u in {q where q is Polynomial of F : deg q < deg p};
then
consider s being Polynomial of F such that
A17: s = p *' u & deg s < deg p;
thus
contradiction by A17,A16,A15,HURWITZ:23;
end; then
not p *' u in the carrier of Polynom-Ring p by RING_4:def 8; then
not q - r in the carrier of Polynom-Ring p by A13,POLYNOM3:def 10;
hence contradiction by A14;
end; then
q - r = p *' (0_.(F)) by A13,POLYNOM3:def 10
.= 0.(Polynom-Ring F) by POLYNOM3:def 10;
hence x1 = x2 by RLVECT_1:21;
end;
hence f is one-to-one;
A18: now let x be object;
assume
A19: x in rng f;
rng f c= the carrier of KroneckerField(F,p) by RELAT_1:def 19;
hence x in the carrier of KroneckerField(F,p) by A19;
end;
now let x be object;
assume x in the carrier of KroneckerField(F,p); then
x in the carrier of (Polynom-Ring F)/({p}-Ideal) by FIELD_1:def 3; then
consider q being Element of the carrier of Polynom-Ring F such that
A20: x = Class(EqRel(Polynom-Ring F,{p}-Ideal),q) by RING_1:11;
reconsider d = q div p as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
p <> 0_.(F); then
consider t being Polynomial of F such that
A21: q = (q div p) *' p + t & deg t < deg p by HURWITZ:def 5;
reconsider r = t as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
q - (q div p) *' p
= ((q div p) *' p + t) + -((q div p) *' p) by A21,POLYNOM3:def 6
.= t + ((q div p) *' p + -((q div p) *' p)) by POLYNOM3:26
.= t + ((q div p) *' p - ((q div p) *' p)) by POLYNOM3:def 6
.= t + 0_.(F) by POLYNOM3:29
.= t; then
A22: r = q mod p by HURWITZ:def 6;
r in {q where q is Polynomial of F : deg q < deg p} by A21; then
A23: r in the carrier of Polynom-Ring p by RING_4:def 8; then
A24: r in dom f by FUNCT_2:def 1;
q = (q div p) *' p + (q mod p) by RING_4:4; then
A25: q - r = ((q div p) *' p + (q mod p)) - (q mod p) by A22,Lm7
.= ((q div p) *' p + (q mod p)) + -(q mod p) by POLYNOM3:def 6
.= (q div p) *' p + ((q mod p) + -(q mod p)) by POLYNOM3:26
.= (q div p) *' p + ((q mod p) - (q mod p)) by POLYNOM3:def 6
.= (q div p) *' p + 0_.(F) by POLYNOM3:29
.= p * d by POLYNOM3:def 10;
{p}-Ideal = the set of all p * r where r is Element of Polynom-Ring F
by IDEAL_1:64; then
A26: q - r in {p}-Ideal by A25;
f.r = Class(EqRel(Polynom-Ring F,{p}-Ideal),r) by A23,Def8
.= Class(EqRel(Polynom-Ring F,{p}-Ideal),q) by A26,RING_1:6;
hence x in rng f by A20,A24,FUNCT_1:3;
end;
hence f is onto by A18,TARSKI:2;
end;
end;
registration
let F be Field, p be irreducible Element of the carrier of Polynom-Ring F;
cluster KroneckerField(F,p) -> (Polynom-Ring p)-homomorphic
(Polynom-Ring p)-monomorphic
(Polynom-Ring p)-isomorphic;
coherence
proof
A1: KroneckerIso p is linear one-to-one;
hence KroneckerField(F,p) is (Polynom-Ring p)-homomorphic by RING_2:def 4;
thus
KroneckerField(F,p) is (Polynom-Ring p)-monomorphic by A1,RING_3:def 3;
thus
KroneckerField(F,p) is (Polynom-Ring p)-isomorphic by A1,RING_3:def 4;
end;
cluster Polynom-Ring p -> (KroneckerField(F,p))-homomorphic
(KroneckerField(F,p))-monomorphic
(KroneckerField(F,p))-isomorphic;
coherence
proof
reconsider g = (KroneckerIso p)" as Isomorphism of
KroneckerField(F,p),Polynom-Ring p by RING_3:73;
g is Homomorphism of KroneckerField(F,p),Polynom-Ring p;
hence Polynom-Ring p is (KroneckerField(F,p))-homomorphic by RING_2:def 4;
g is monomorphism;
hence Polynom-Ring p is (KroneckerField(F,p))-monomorphic by RING_3:def 3;
g is Isomorphism of KroneckerField(F,p),Polynom-Ring p;
hence Polynom-Ring p is (KroneckerField(F,p))-isomorphic by RING_3:def 4;
end;
cluster Polynom-Ring p -> F-homomorphic F-monomorphic;
coherence;
end;
Lm11:
for F being polynomial_disjoint Field
for p being irreducible Element of the carrier of Polynom-Ring F
ex E being FieldExtension of F st p is_with_roots_in E
proof
let F be polynomial_disjoint Field;
let p be irreducible Element of the carrier of Polynom-Ring F;
A1: now assume not F,Polynom-Ring p are_disjoint; then
A2: ([#]F) /\ ([#]Polynom-Ring p) <> {} by FIELD_2:def 1;
let a be Element of
(the carrier of F)/\(the carrier of Polynom-Ring p);
A3: a in the carrier of F & a in the carrier of Polynom-Ring p
by A2,XBOOLE_0:def 4;
the carrier of Polynom-Ring p =
{q where q is Polynomial of F : deg q < deg p} by RING_4:def 8; then
consider q being Polynomial of F such that
A4: a = q & deg q < deg p by A3;
a in the carrier of Polynom-Ring F by A4,POLYNOM3:def 10; then
a in ([#]F) /\ ([#]Polynom-Ring F) by A3,XBOOLE_0:def 4;
hence contradiction by FIELD_3:def 3;
end;
reconsider KroneckerIsop = (KroneckerIso p)" as
Isomorphism of KroneckerField(F,p),Polynom-Ring p by RING_3:73;
set h = KroneckerIsop * (emb p);
reconsider h as Function of F,Polynom-Ring p by FUNCT_2:13;
h is linear one-to-one by RINGCAT1:1; then
reconsider h as Monomorphism of F,Polynom-Ring p;
reconsider E = embField h as Field by A1,FIELD_2:12;
emb_iso h is onto by A1,FIELD_2:15; then
reconsider embisoh = (emb_iso h)" as Function of Polynom-Ring p,E
by FUNCT_2:25;
A5: emb_iso h is linear one-to-one onto
by A1,FIELD_2:13,FIELD_2:14, FIELD_2:15; then
reconsider P = (Polynom-Ring p) as E-isomorphic Field by RING_3:def 4;
reconsider embisoh as Isomorphism of P,E by A5,RING_3:73;
set iso = embisoh * KroneckerIsop, u = KrRoot p;
reconsider iso as Function of KroneckerField(F,p),E by FUNCT_2:13;
A6: iso is RingHomomorphism by RINGCAT1:1; then
reconsider E as KroneckerField(F,p)-homomorphic Field by RING_2:def 4;
reconsider iso as Homomorphism of KroneckerField(F,p),E by A6;
u is_a_root_of emb(p,p) by FIELD_1:42; then
A7: eval((PolyHom iso).(emb(p,p)),iso.u) = 0.E by FIELD_1:33,POLYNOM5:def 7;
F is Subfield of E by FIELD_2:17; then
reconsider E as FieldExtension of F by Th4;
take E;
reconsider a = iso.u as Element of E;
(PolyHom iso).(emb(p,p)) = p
proof
set g = (PolyHom iso).(emb(p,p));
A8: KroneckerField(F,p) = (Polynom-Ring F)/({p}-Ideal) by FIELD_1:def 3;
A9: for a being Element of F holds h.a = a|F
proof
let a be Element of F;
dom(emb p) = the carrier of F by FUNCT_2:def 1; then
A10: h.a = KroneckerIsop.((emb p).a) by FUNCT_1:13
.= KroneckerIsop.Class(EqRel(Polynom-Ring F,{p}-Ideal),a|F)
by FIELD_1:39;
A11: the carrier of Polynom-Ring p =
{q where q is Polynomial of F : deg q < deg p} by RING_4:def 8;
deg(a|F) <= 0 & deg p > 0 by RATFUNC1:def 2,RING_4:def 4; then
a|F in the carrier of Polynom-Ring p by A11; then
reconsider b1 = a|F as Element of Polynom-Ring p;
A12: dom(KroneckerIso p) = the carrier of Polynom-Ring p by FUNCT_2:def 1;
(KroneckerIso p).b1
= Class(EqRel(Polynom-Ring F,{p}-Ideal),b1) by Def8;
hence thesis by A12,A10,FUNCT_1:32;
end;
A13: for a being Element of F holds iso.((emb p).a) = a
proof
let a be Element of F;
rng KroneckerIso p = the carrier of KroneckerField(F,p)
by FUNCT_2:def 3; then
A14: dom KroneckerIsop = the carrier of KroneckerField(F,p) by FUNCT_1:33;
reconsider b = a|F as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
A15: the carrier of Polynom-Ring p =
{q where q is Polynomial of F : deg q < deg p} by RING_4:def 8;
deg(a|F) <= 0 & deg p > 0 by RATFUNC1:def 2,RING_4:def 4; then
a|F in the carrier of Polynom-Ring p by A15; then
reconsider b1 = a|F as Element of Polynom-Ring p;
reconsider v = Class(EqRel(Polynom-Ring F,{p}-Ideal),b)
as Element of KroneckerField(F,p) by A8,RING_1:12;
A16: (KroneckerIso p).b1
= Class(EqRel(Polynom-Ring F,{p}-Ideal),b1) by Def8;
A17: dom(KroneckerIso p) = the carrier of Polynom-Ring p by FUNCT_2:def 1;
the carrier of (embField h) = carr h by FIELD_2:def 7
.= (([#]Polynom-Ring p) \ (rng h)) \/ ([#]F)
by FIELD_2:def 2; then
reconsider a1 = a as Element of embField h by XBOOLE_0:def 3;
a in F; then
A18: (emb_iso h).a1 = h.a by FIELD_2:def 8 .= a|F by A9;
A19: dom(emb_iso h) = the carrier of embField h by FUNCT_2:def 1;
thus iso.((emb p).a) = iso.v by FIELD_1:39
.= embisoh.(KroneckerIsop.v) by A14,FUNCT_1:13
.= embisoh.b by A16,A17,FUNCT_1:32
.= a by A18,A19,FUNCT_1:32;
end;
now let x be object;
assume x in NAT; then
reconsider i = x as Element of NAT;
g.i = iso.(emb(p,p).i) by FIELD_1:def 2
.= iso.(Class(EqRel(Polynom-Ring F,{p}-Ideal),(p.i)|F)) by FIELD_1:40
.= iso.((emb p).(p.i)) by FIELD_1:39;
hence g.x = p.x by A13;
end;
hence thesis;
end; then
a is_a_root_of p,E by A7,Th15;
hence thesis;
end;
theorem :: Kronecker
for F being polynomial_disjoint Field
for f being non constant Element of the carrier of Polynom-Ring F
ex E being FieldExtension of F st f is_with_roots_in E
proof
let F be polynomial_disjoint Field;
let f be non constant Element of the carrier of Polynom-Ring F;
consider p being Element of the carrier of Polynom-Ring F such that
A1: p is_a_irreducible_factor_of f by FIELD_1:3;
reconsider p as irreducible Element of the carrier of Polynom-Ring F
by A1,FIELD_1:def 1;
consider q being Element of the carrier of Polynom-Ring F such that
A2: p * q = f by A1,FIELD_1:def 1,GCD_1:def 1;
consider E being FieldExtension of F such that
A3: p is_with_roots_in E by Lm11;
take E;
consider a being Element of E such that
A4: a is_a_root_of p,E by A3;
reconsider p1 = p, q1 = q as Polynomial of F;
A5: F is Subring of E by Def1;
Ext_eval(f,a) = Ext_eval(p1*'q1,a) by A2,POLYNOM3:def 10
.= Ext_eval(p1,a) * Ext_eval(q1,a) by A5,ALGNUM_1:20
.= 0.E by A4; then
a is_a_root_of f,E;
hence thesis;
end;