:: Ring and Field Adjunctions, Algebraic Elements and Minimal Polynomials
:: by Christoph Schwarzweller
::
:: Received October 25, 2020
:: Copyright (c) 2020-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, ALGSEQ_1, VECTSP_2,
STRUCT_0, SUBSET_1, SUPINF_2, BINOP_1, NAT_1, MESFUNC1, REALSET1, C0SP1,
FUNCT_4, FUNCT_2, POLYNOM1, POLYNOM2, POLYNOM3, FUNCSDOM, RLVECT_5,
PARTFUN1, EC_PF_1, HURWITZ, RLVECT_1, RLVECT_2, FINSEQ_1, CARD_FIL,
FUNCT_1, RELAT_1, LATTICES, CARD_1, IDEAL_1, GCD_1, GROUP_6, XBOOLE_0,
FINSET_1, NUMBERS, MSSUBFAM, POLYNOM5, GROUP_1, ZFMISC_1, FUNCT_7,
POLYNOM4, AFINSQ_1, GROUP_4, INT_1, VECTSP10, CAT_1, FDIFF_1, YELLOW_8,
RATFUNC1, RING_2, RING_3, ALGNUM_1, ARYTM_1, RLVECT_3, FIELD_4, NEWTON,
WELLORD1, XXREAL_0, CARD_3, FUNCOP_1, XCMPLX_0, FOMODEL1, FIELD_1,
RLSUB_1, FIELD_6;
notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, RELAT_1, ORDINAL1, REALSET1,
PARTFUN1, FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1, ZFMISC_1, NUMBERS,
FINSET_1, CARD_1, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, FUNCT_4, FUNCT_7,
IDEAL_1, STRUCT_0, GCD_1, VFUNCT_1, POLYNOM1, POLYNOM3, POLYNOM4,
POLYNOM5, GROUP_1, GROUP_6, VECTSP10, VECTSP_4, VECTSP_6, VECTSP_7,
BINOM, ALGSTR_0, RLVECT_1, VECTSP_2, VECTSP_9, MATRLIN, HURWITZ,
VECTSP_1, ALGSEQ_1, C0SP1, EC_PF_1, RATFUNC1, RING_1, RING_2, RING_3,
RING_4, ALGNUM_1, FIELD_1, FIELD_4, FIELD_5;
constructors FUNCT_4, POLYNOM4, FUNCT_7, NAT_D, VFUNCT_1, RATFUNC1, GCD_1,
REALSET1, BINOM, RINGCAT1, ALGSEQ_1, VECTSP_9, POLYDIFF, ALGNUM_1,
VECTSP_6, FIELD_4, FIELD_5;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, STRUCT_0, VECTSP_1, ALGSTR_1, EC_PF_1,
POLYNOM4, FUNCT_2, ALGSTR_0, POLYNOM3, SUBSET_1, MOD_4, RLVECT_1,
FINSET_1, FUNCT_1, VFUNCT_1, CARD_1, C0SP1, RATFUNC1, RELAT_1, RINGCAT1,
RING_1, RING_2, RING_3, RING_4, RING_5, POLYDIFF, REALSET1, POLYNOM5,
FIELD_4, FIELD_5;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions STRUCT_0, ALGSTR_0, RLVECT_1;
equalities BINOP_1, REALSET1, XCMPLX_0, STRUCT_0, ALGSTR_0, POLYNOM3,
VECTSP_1, ALGNUM_1;
expansions STRUCT_0, GROUP_1, VECTSP_1, IDEAL_1, GCD_1, TARSKI, GROUP_6,
QUOFIELD, FUNCT_1, FUNCT_2, ALGNUM_1;
theorems GROUP_1, VECTSP_1, VECTSP_2, RLVECT_1, IDEAL_1, FUNCT_2, GCD_1,
C0SP1, SUBSET_1, TARSKI, CARD_1, BHSP_1, UPROOTS, FUNCT_1, RELAT_1,
EC_PF_1, POLYNOM4, RING_3, GAUSSINT, NORMSP_1, REALSET1, ORDINAL1,
VECTSP_6, VECTSP10, RATFUNC1, POLYNOM5, RING_4, RING_5, CARD_2, HURWITZ,
XREAL_1, INT_1, BINOM, XBOOLE_0, FUNCT_7, NAT_2, POLYNOM2, RING_2,
FUNCOP_1, POLYNOM3, ALGNUM_1, NAT_1, FINSEQ_1, FINSEQ_3, ZFMISC_1,
XXREAL_0, XBOOLE_1, MATRLIN, XREAL_0, ALGSEQ_1, PARTFUN1, VECTSP_4,
RING_1, POLYDIFF, POLYNOM1, FIELD_4, FUNCT_4, VECTSP_7, VECTSP_9,
FIELD_1, FIELD_5, LIOUVIL2;
schemes NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, INT_1;
begin :: Preliminaries
theorem degen:
for R being Ring holds R is degenerated iff the carrier of R = {0.R}
proof
let L be Ring;
now assume AS: L is degenerated;
B: {0.L} c= the carrier of L;
now let o be object;
assume o in the carrier of L; then
reconsider a = o as Element of L;
a = a * 1.L .= 0.L by AS;
hence o in {0.L} by TARSKI:def 1;
end;
hence the carrier of L = {0.L} by B,TARSKI:2;
end;
hence thesis;
end;
registration
let F be Field;
cluster {0.F}-Ideal -> maximal;
coherence
proof
set I = {0.F}-Ideal;
I = {0.F} by IDEAL_1:47;
then not(1.F in I) by TARSKI:def 1;
then A: I is proper by IDEAL_1:19;
for J being Ideal of F st I c= J holds J = I or J is non proper
proof
let J be Ideal of F;
per cases by IDEAL_1:22;
suppose J = {0.F};
hence thesis by IDEAL_1:47;
end;
suppose J = the carrier of F;
then J = [#] F;
hence thesis;
end;
end;
hence thesis by A,RING_1:def 3,RING_1:def 4;
end;
end;
registration
let R be non degenerated non almost_left_invertible comRing;
cluster {0.R}-Ideal -> non maximal;
coherence
proof
set I = {0.R}-Ideal;
consider J being Ideal of R such that
H: J <> {0.R} & J <> the carrier of R by IDEAL_1:22;
A: I c= J
proof
now let o be object;
assume o in I;
then o in {0.R} by IDEAL_1:47;
then o = 0.R by TARSKI:def 1;
hence o in J by IDEAL_1:2;
end;
hence thesis;
end;
B: J is proper by H,SUBSET_1:def 6;
J <> I by H,IDEAL_1:47;
hence thesis by A,B,RING_1:def 3;
end;
end;
definition
let R be Ring;
attr R is field-containing means :deffc:
ex F being Field st F is Subring of R;
end;
registration
cluster field-containing for Ring;
existence
proof
ex R being Ring st R is field-containing
proof
set F = the Field;
take F;
F is Subfield of F by FIELD_4:1;
then F is Subring of F by FIELD_5:12;
hence thesis;
end;
hence thesis;
end;
end;
definition
let R be field-containing Ring;
mode Subfield of R -> Field means :defsubfr:
it is Subring of R;
existence by deffc;
end;
theorem thLC:
for R being non degenerated Ring
for p being non zero Polynomial of R holds p.(deg p) = LC p
proof
let R be non degenerated Ring, p be non zero Polynomial of R;
deg p = len p - 1 by HURWITZ:def 2;
hence p.(deg p) = p.(len p -'1) by XREAL_0:def 2
.= LC p by RATFUNC1:def 6;
end;
registration
let R be non degenerated Ring;
let p be non zero Polynomial of R;
cluster LM p -> non zero;
coherence
proof
len LM p = len p by POLYNOM4:15; then
LM p <> 0_.(R) by POLYNOM4:5,POLYNOM4:3;
hence thesis by UPROOTS:def 5;
end;
end;
theorem thdegLM:
for R being Ring, p being Polynomial of R holds deg(LM p) = deg p
proof
let R be Ring, p be Polynomial of R;
thus deg(LM p) = len(LM p) - 1 by HURWITZ:def 2
.= len(p) - 1 by POLYNOM4:15
.= deg p by HURWITZ:def 2;
end;
theorem thdegLC:
for R being Ring, p being Polynomial of R holds LC (LM p) = LC p
proof
let R be Ring, p be Polynomial of R;
thus LC(LM p) = (LM p).(len(LM p)-'1) by RATFUNC1:def 6
.= (LM p).(len(p)-'1) by POLYNOM4:15
.= p.(len(p)-'1) by POLYNOM4:def 1
.= LC p by RATFUNC1:def 6;
end;
theorem thdLM:
for R being non degenerated Ring
for p being non zero Polynomial of R holds deg(p - LM p) < deg p
proof
let R be non degenerated Ring, p be non zero Polynomial of R;
per cases;
suppose p - LM p = 0_.(R);
hence thesis by HURWITZ:20;
end;
suppose p - LM p <> 0_.(R);
then reconsider q = p-LM p as non zero Polynomial of R by UPROOTS:def 5;
A: now assume deg q = deg p; then
LC q = q.(deg p) by thLC
.= p.(deg p) - (LM p).(deg p) by POLYNOM3:27
.= p.(deg p) - (LM p).(deg(LM p)) by thdegLM
.= p.(deg p) - LC(LM p) by thLC
.= p.(deg p) - LC p by thdegLC
.= LC p - LC p by thLC
.= 0.R by RLVECT_1:15;
hence contradiction;
end;
now assume B0: deg q > deg p; then
deg q >= deg p + 1 by INT_1:7; then
B1: deg q >= (len p - 1) + 1 by HURWITZ:def 2;
p <> 0_.(R); then
len p <> 0 by POLYNOM4:5; then
len p + 1 > 0 + 1 by XREAL_1:6; then
D: len p >= 1 by NAT_1:13;
deg q <> len p - 1 by B0,HURWITZ:def 2; then
deg q <> len p -' 1 by D,XREAL_0:def 2; then
B2: (LM p).(deg q) = 0.R by POLYNOM4:def 1;
LC q = q.(deg q) by thLC
.= p.(deg q) - (LM p).(deg q) by POLYNOM3:27
.= 0.R - 0.R by ALGSEQ_1:8,B1,B2;
hence contradiction;
end;
hence thesis by A,XXREAL_0:1;
end;
end;
theorem thE1:
for R being Ring
for p being Polynomial of R
for i being Nat holds (<%0.R,1.R%> *' p).(i+1) = p.i
proof
let R be Ring, p be Polynomial of R; let i be Nat;
set q = <%0.R,1.R%>;
consider r being FinSequence of the carrier of R such that
A: len r = (i+1)+1 & (<%0.R,1.R%> *' p).(i+1) = Sum r &
for k being Element of NAT st k in dom r
holds r.k = q.(k-'1) * p.((i+1)+1-'k) by POLYNOM3:def 9;
B: dom r = Seg(i+2) by A,FINSEQ_1:def 3;
C: Seg 2 c= dom r by B,FINSEQ_1:5,NAT_1:11;
D: 2 in dom r by C,FINSEQ_1:3;
H2: 2 - 2 <= (i + 2) - 2 by NAT_1:11,XREAL_1:9;
H3: 0 <= 2 - 1;
E: r/.2 = r.2 by D,PARTFUN1:def 6
.= q.(2-'1) * p.((i+1)+1-'2) by D,A
.= q.1 * p.((i+1)+1-'2) by H3,XREAL_0:def 2
.= q.1 * p.i by H2,XREAL_0:def 2
.= 1.R * p.i by POLYNOM5:38;
F: now let k be Element of NAT;
assume F: k in dom r & k <> 2; then
per cases by XXREAL_0:1;
suppose k < 2; then
k + 1 <= 2 by INT_1:7; then
F4: k + 1 - 1 <= 2 - 1 by XREAL_1:9;
F5: 1 <= k by F,B,FINSEQ_1:1; then
F3: k = 1 by F4,XXREAL_0:1;
F2: k -' 1 = k - 1 by F5,XREAL_0:def 2;
thus r/.k = r.k by F,PARTFUN1:def 6
.= q.(k-'1) * p.((i+1)+1-'k) by A,F
.= 0.R * p.((i+1)+1-'k) by F3,F2,POLYNOM5:38
.= 0.R;
end;
suppose F4: k > 2; then
2 + 1 <= k by INT_1:7; then
F3: 2 + 1 - 1 <= k - 1 by XREAL_1:9;
F2: k - 1 = k -' 1 by F4,XREAL_0:def 2;
thus r/.k = r.k by F,PARTFUN1:def 6
.= q.(k-'1) * p.((i+1)+1-'k) by A,F
.= 0.R * p.((i+1)+1-'k) by F2,F3,POLYNOM5:38
.= 0.R;
end;
end;
thus (<%0.R,1.R%> *' p).(i+1) = p.i by E,A,D,F,POLYNOM2:3;
end;
theorem thE2:
for R being Ring
for p being Polynomial of R holds (<%0.R,1.R%> *' p).0 = 0.R
proof
let R be Ring, p be Polynomial of R;
set q = <%0.R,1.R%>;
consider r being FinSequence of the carrier of R such that
A: len r = 0+1 & (<%0.R,1.R%> *' p).0 = Sum r & for k being Element of NAT
st k in dom r holds r.k = q.(k-'1) * p.(0+1-'k) by POLYNOM3:def 9;
dom r = { 1 } by FINSEQ_1:2,A,FINSEQ_1:def 3; then
1 in dom r by TARSKI:def 1; then
C: r.1 = q.(1-'1) * p.(0+1-'1) by A
.= q.0 * p.(1-'1) by NAT_2:8
.= q.0 * p.0 by NAT_2:8
.= 0.R * p.0 by POLYNOM5:38;
r = <*r.1*> by A,FINSEQ_1:40;
hence thesis by A,C,RLVECT_1:44;
end;
theorem
for R being domRing
for p being non zero Polynomial of R holds deg(<%0.R,1.R%> *' p) = deg(p) + 1
proof
let R be domRing, p be non zero Polynomial of R;
B: len <%0.R,1.R%> = 2 by POLYNOM5:40; then
A: <%0.R,1.R%> <> 0_.(R) by POLYNOM4:3;
C: deg <%0.R,1.R%> = 2 - 1 by B,HURWITZ:def 2;
thus deg(<%0.R,1.R%> *' p) = deg(p) + 1 by C,A,HURWITZ:23;
end;
help1:
for R being domRing, n being Element of NAT holds (<%0.R,1.R%>`^n).n = 1.R
proof
let R be domRing, n be Element of NAT;
<%0.R,1.R%>`^n = anpoly(1.R,n) by FIELD_1:12;
hence thesis by POLYDIFF:24;
end;
help2:
for R being domRing, n,i being Element of NAT
st i <> n holds (<%0.R,1.R%>`^n).i = 0.R
proof
let R be domRing, n,i be Element of NAT;
assume AS: i <> n;
<%0.R,1.R%>`^n = anpoly(1.R,n) by FIELD_1:12;
hence (<%0.R,1.R%>`^n).i = 0.R by AS,POLYDIFF:25;
end;
help3a:
for R being domRing for n being Element of NAT st n <> 0
for a being Element of R holds eval(<%0.R,1.R%>`^n,a) = a|^n
proof
let R be domRing; let n be Element of NAT; assume A: n <> 0;
let a be Element of R;
<%0.R,1.R%>`^n = anpoly(1.R,n) by FIELD_1:12;
hence eval(<%0.R,1.R%>`^n,a) = 1.R * a|^n by A,FIELD_1:6 .= a|^n;
end;
theorem
for R being comRing,
p being Polynomial of R
for a being Element of R holds eval(<%0.R,1.R%> *' p,a) = a * eval(p,a)
proof
let R be comRing, p be Polynomial of R; let a be Element of R;
per cases;
suppose R is degenerated; then
A: the carrier of R = {0.R} by degen;
hence eval(<%0.R,1.R%> *' p,a) = 0.R by TARSKI:def 1
.= a * eval(p,a) by A,TARSKI:def 1;
end;
suppose R is non degenerated;
hence eval(<%0.R,1.R%> *' p,a)
= eval(<%0.R,1.R%>,a) * eval(p,a) by POLYNOM4:24
.= (0.R + 1.R * a) * eval(p,a) by POLYNOM5:44
.= a * eval(p,a);
end;
end;
theorem FIELD427:
for R being Ring,
S being RingExtension of R
for 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 R be Ring, 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 FIELD_4:def 1; 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 lemma7:
for F being Field,
p being Element of the carrier of Polynom-Ring F
for E being FieldExtension of F,
K being E-extending FieldExtension of F
for a being Element of E, b being Element of K st a = b
holds Ext_eval(p,a) = Ext_eval(p,b)
proof
let F be Field,
p be Element of the carrier of Polynom-Ring F;
let E be FieldExtension of F,
U be E-extending FieldExtension of F;
let a be Element of E, b be Element of U;
assume AS2: a = b;
H1: E is Subring of U by FIELD_4:def 1; then
H2: the carrier of E c= the carrier of U by C0SP1:def 3;
F is Subring of E by FIELD_4:def 1; then
H4: the carrier of F c= the carrier of E by C0SP1:def 3;
consider Fp being FinSequence of E such that
A: 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),E) * (power E).(a,n-'1) by ALGNUM_1:def 1;
consider Fq being FinSequence of U such that
B: Ext_eval(p,b) = Sum Fq & len Fq = len p &
for n being Element of NAT st n in dom Fq holds
Fq.n = In(p.(n-'1),U) * (power U).(b,n-'1) by ALGNUM_1:def 1;
C: now let n be Element of NAT;
thus (power U).(b,n-'1) = (power U).(In(b,U),n-'1)
.= In((power E).(a,n-'1),U) by AS2,H1,ALGNUM_1:7
.= (power E).(a,n-'1) by H2,SUBSET_1:def 8;
end;
D: dom Fp = Seg(len Fq) by A,B,FINSEQ_1:def 3 .= dom Fq by FINSEQ_1:def 3;
E: now let n be Element of NAT;
p.(n-'1) in U by H2,H4;
hence In(p.(n-'1),U) = p.(n-'1) by SUBSET_1:def 8
.= In(p.(n-'1),E) by H4,SUBSET_1:def 8;
end;
H: for n being Element of NAT holds [In(p.(n-'1),E),(power E).(a,n-'1)]
in [:the carrier of E,the carrier of E:] by ZFMISC_1:def 2;
now let n be Nat;
assume F: n in dom Fq;
G: n is Element of NAT by ORDINAL1:def 12;
thus Fq.n = In(p.(n-'1),U) * (power U).(b,n-'1) by B,F
.= (the multF of U).(In(p.(n-'1),U),(power E).(a,n-'1)) by C,G
.= (the multF of U).(In(p.(n-'1),E),(power E).(a,n-'1)) by E,G
.= ((the multF of U)||(the carrier of E)).
(In(p.(n-'1),E),(power E).(a,n-'1)) by G,H,FUNCT_1:49
.= In(p.(n-'1),E) * (power E).(a,n-'1) by H1,C0SP1:def 3
.= Fp.n by A,D,F;
end;
then Fp = Fq by D;
hence thesis by H1,A,B,FIELD_4:2;
end;
registration
let L be non empty ZeroStr,
a,b be Element of L;
let f be (the carrier of L)-valued Function;
let x,y be object;
cluster f +* (x,y) --> (a,b) -> (the carrier of L)-valued;
coherence
proof
set g = f +* (x,y) --> (a,b);
I: dom((x,y) --> (a,b)) = {x,y} by FUNCT_2:def 1; then
H: dom g = dom f \/ {x,y} by FUNCT_4:def 1;
now let o be object;
assume o in rng g; then
consider z being object such that
A: z in dom g & g.z = o by FUNCT_1:def 3;
per cases;
suppose B: z in {x,y}; then
per cases by TARSKI:def 2;
suppose z = x; then
G: g.z = ((x,y) --> (a,b)).x by B,I,FUNCT_4:13;
per cases;
suppose x <> y; then
g.z = a by G,FUNCT_4:63;
hence o in the carrier of L by A;
end;
suppose x = y; then
g.z = b by G,FUNCT_4:63;
hence o in the carrier of L by A;
end;
end;
suppose z = y; then
g.z = ((x,y) --> (a,b)).y by B,I,FUNCT_4:13
.= b by FUNCT_4:63;
hence o in the carrier of L by A;
end;
end;
suppose D: not z in {x,y}; then
not z in dom((x,y) --> (a,b)); then
C: g.z = f.z by FUNCT_4:11;
z in dom f by D,A,H,XBOOLE_0:def 3; then
f.z in rng f by FUNCT_1:def 3;
hence o in the carrier of L by A,C;
end;
end;
then rng g c= the carrier of L;
hence thesis by RELAT_1:def 19;
end;
end;
registration
let L be non empty ZeroStr,
a,b be Element of L;
let f be finite-Support sequence of L;
let x,y be object;
cluster f +* (x,y) --> (a,b) -> finite-Support for sequence of L;
coherence
proof
let g be sequence of L such that A1: g = f +* (x,y) --> (a,b);
H0: dom((x,y) --> (a,b)) = {x,y} by FUNCT_4:62; then
H1: dom g = dom f \/ {x,y} by A1,FUNCT_4:def 1;
A2: Support f is finite by POLYNOM1:def 5;
now let o be object;
assume o in Support g; then
B0: o in dom g & g.o <> 0.L by POLYNOM1:def 3;
per cases;
suppose B1: not o in {x,y}; then
B2: g.o = f.o by A1,H0,FUNCT_4:11;
o in dom f by B0,B1,H1,XBOOLE_0:def 3; then
o in Support f by B2,B0,POLYNOM1:def 3;
hence o in Support f \/ {x,y} by XBOOLE_0:def 3;
end;
suppose o in {x,y};
hence o in Support f \/ {x,y} by XBOOLE_0:def 3;
end;
end; then
Support g c= Support f \/ {x,y};
hence thesis by A2,POLYNOM1:def 5;
end;
end;
begin :: On Subrings and Subfields
theorem RE:
for R1,R2 being strict Ring
st R1 is Subring of R2 & R2 is Subring of R1 holds R1 = R2
proof
let K1,K2 be strict Ring;
assume A1: K1 is Subring of K2 & K2 is Subring of K1;
A2: the carrier of K1 c= the carrier of K2 &
the carrier of K2 c= the carrier of K1 by A1,C0SP1:def 3; then
A3: the carrier of K1 = the carrier of K2 by XBOOLE_0:def 10;
A4: the addF of K2 = (the addF of K2) || the carrier of K1 by A3
.= the addF of K1 by A1,C0SP1:def 3;
A5: the multF of K2 = (the multF of K2)||the carrier of K1 by A3
.= the multF of K1 by A1,C0SP1:def 3;
1.K1 = 1.K2 & 0.K1 = 0.K2 by A1,C0SP1:def 3;
hence thesis by A4,A5,A2,XBOOLE_0:def 10;
end;
theorem Th6:
for S being Ring,
R1,R2 being Subring of S
holds R1 is Subring of R2 iff the carrier of R1 c= the carrier of R2
proof
let K be Ring, SK1,SK2 be Subring of K;
set C1 = the carrier of SK1;
set C2 = the carrier of SK2;
set ADD = the addF of K;
set MULT = the multF of K;
thus SK1 is Subring of SK2 implies C1 c= C2 by C0SP1:def 3;
assume A1: C1 c= C2;
then A2: [:C1,C1:] c= [:C2,C2:] by ZFMISC_1:96;
the addF of SK2 = ADD || C2 by C0SP1:def 3;
then A3: (the addF of SK2) || C1 = ADD || C1 by A2,FUNCT_1:51
.= the addF of SK1 by C0SP1:def 3;
the multF of SK2 = MULT || C2 by C0SP1:def 3;
then A4: (the multF of SK2) || C1 = MULT || C1 by A2,FUNCT_1:51
.= the multF of SK1 by C0SP1:def 3;
1.SK1 = 1.K & 0.SK1 = 0.K by C0SP1:def 3;
then 1.SK1 = 1.SK2 & 0.SK1 = 0.SK2 by C0SP1:def 3;
hence thesis by A1,A3,A4,C0SP1:def 3;
end;
theorem RE1:
for S being Ring,
R1,R2 being strict Subring of S
holds R1 = R2 iff the carrier of R1 = the carrier of R2
proof
let K be Ring;
let SK1, SK2 be strict Subring of K;
thus SK1 = SK2 implies
the carrier of SK1 = the carrier of SK2;
assume A1: the carrier of SK1 = the carrier of SK2;
then A2: SK2 is strict Subring of SK1 by Th6;
SK1 is strict Subring of SK2 by A1,Th6;
hence thesis by A2,RE;
end;
theorem Th17:
for S being Ring,
R being Subring of S
for x,y being Element of S,
x1,y1 being Element of R st x = x1 & y = y1 holds x + y = x1 + y1
proof
let R be Ring, S be Subring of R;
let x,y be Element of R, x1,y1 be Element of S;
set C1 = the carrier of S;
the addF of S = (the addF of R) || C1 by C0SP1:def 3;
hence thesis by FUNCT_1:49,ZFMISC_1:87;
end;
theorem Th18:
for S being Ring,
R being Subring of S
for x,y being Element of S,
x1,y1 being Element of R st x = x1 & y = y1 holds x * y = x1 * y1
proof
let R be Ring, S being Subring of R;
let x,y be Element of R, x1,y1 be Element of S;
set C1 = the carrier of S;
the multF of S = (the multF of R) || C1 by C0SP1:def 3;
hence thesis by FUNCT_1:49,ZFMISC_1:87;
end;
theorem Th19:
for S being Ring,
R being Subring of S
for x being Element of S, x1 being Element of R st x = x1 holds -x = -x1
proof
let R be Ring, S being Subring of R;
let x be Element of R, x1 be Element of S;
set C = the carrier of R, C1 = the carrier of S, a = -x1;
assume A1: x = x1;
C1 c= C by C0SP1:def 3;
then reconsider g = a as Element of R;
x + g = x1 + a by A1,Th17 .= 0.S by VECTSP_1:19 .= 0.R by C0SP1:def 3;
hence thesis by VECTSP_1:16;
end;
theorem Th19f:
for E being Field,
F being Subfield of E
for x being non zero Element of E,
x1 being Element of F st x = x1 holds x" = x1"
proof
let R be Field, S being Subfield of R;
let x be non zero Element of R, x1 be Element of S;
set C = the carrier of R, C1 = the carrier of S, a = x1";
assume A1: x = x1;
A2: x <> 0.R; then
A3: x1 <> 0.S by A1,EC_PF_1:def 1;
C1 c= C by EC_PF_1:def 1;
then reconsider g = a as Element of R;
R is FieldExtension of S by FIELD_4:7; then
S is Subring of R by FIELD_4:def 1; then
g * x = a * x1 by A1,Th18 .= 1.S by A3,VECTSP_1:def 10 .= 1.R by EC_PF_1:def 1;
hence thesis by A2,VECTSP_1:def 10;
end;
theorem pr5:
for S being Ring,
R being Subring of S
for x being Element of S, x1 being Element of R
for n being Element of NAT st x = x1 holds x|^n = x1|^n
proof
let S be Ring, R be Subring of S;
let x be Element of S, x1 be Element of R; let n be Element of NAT;
assume AS: x = x1;
defpred P[Nat] means
for x be Element of S, x1 be Element of R st x=x1 holds x|^($1) = x1|^($1);
now let x be Element of S, x1 be Element of R;
assume x = x1;
thus x|^0 = 1_S by BINOM:8 .= 1_R by C0SP1:def 3 .= x1|^0 by BINOM:8;
end; then
IA: P[0];
A: the multF of R = (the multF of S)||the carrier of R by C0SP1:def 3;
IS: now let k be Nat;
assume IV: P[k];
now let x be Element of S, x1 be Element of R;
assume AS: x = x1; then
C: x|^k = x1|^k by IV;
B: [x1|^k,x1] in
[:the carrier of R,the carrier of R:] by ZFMISC_1:def 2;
thus x|^(k+1) = x|^k *x|^1 by BINOM:10
.= x|^k * x by BINOM:8
.= x1|^k * x1 by AS,A,B,C,FUNCT_1:49
.= x1|^k * x1|^1 by BINOM:8
.= x1|^(k+1) by BINOM:10;
end;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
hence thesis by AS;
end;
theorem pr20:
for S being Ring,
R being Subring of S
for x1,x2 being Element of S, y1,y2 being Element of R
st x1 = y1 & x2 = y2 holds <%x1,x2%> = <%y1,y2%>
proof
let S be Ring, R be Subring of S;
let x1,x2 be Element of S, y1,y2 be Element of R;
assume AS: x1 = y1 & x2 = y2;
set p = <%x1,x2%>, q = <%y1,y2%>;
now let n be Element of NAT;
per cases;
suppose A: n is trivial;
per cases by A,NAT_2:def 1;
suppose B: n = 0;
hence p.n = y1 by AS,POLYNOM5:38 .= q.n by B,POLYNOM5:38;
end;
suppose B: n = 1;
hence p.n = y2 by AS,POLYNOM5:38 .= q.n by B,POLYNOM5:38;
end;
end;
suppose A: n is non trivial;
hence p.n = 0.S by NAT_2:29,POLYNOM5:38
.= 0.R by C0SP1:def 3
.= q.n by A,NAT_2:29,POLYNOM5:38;
end;
end;
hence thesis;
end;
theorem helpp:
for R being comRing,
S being comRingExtension of R
for x1,x2 being Element of S, y1,y2 being Element of R
for n being Element of NAT
st x1 = y1 & x2 = y2 holds <%x1,x2%>`^n = <%y1,y2%>`^n
proof
let R be comRing, S be comRingExtension of R;
let x1,x2 be Element of S, y1,y2 be Element of R;
let n be Element of NAT;
assume A: x1 = y1 & x2 = y2;
defpred P[Nat] means <%x1,x2%>`^($1) = <%y1,y2%>`^($1);
<%x1,x2%>`^0 = 1_.(S) by POLYNOM5:15
.= 1_.(R) by FIELD_4:14
.= <%y1,y2%>`^0 by POLYNOM5:15; then
IA: P[0];
reconsider qS = <%x1,x2%> as Element of the carrier of Polynom-Ring S
by POLYNOM3:def 10;
reconsider qR = <%y1,y2%> as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
R is Subring of S by FIELD_4:def 1; then
E: <%x1,x2%> = <%y1,y2%> by A,pr20;
IS: now let k be Nat;
assume IV: P[k];
B: <%x1,x2%>`^(k+1)
= (power Polynom-Ring S).(<%x1,x2%>,k+1) by POLYNOM5:def 3
.= (power Polynom-Ring S).(qS,k) * qS by GROUP_1:def 7;
C: <%y1,y2%>`^(k+1)
= (power Polynom-Ring R).(<%y1,y2%>,k+1) by POLYNOM5:def 3
.= (power Polynom-Ring R).(qR,k) * qR by GROUP_1:def 7;
D: (power Polynom-Ring R).(qR,k)
= <%x1,x2%>`^k by IV,POLYNOM5:def 3
.= (power Polynom-Ring S).(qS,k) by POLYNOM5:def 3;
reconsider u = (power Polynom-Ring R).(qR,k) as Polynomial of R
by POLYNOM3:def 10;
reconsider v = (power Polynom-Ring S).(qS,k) as Polynomial of S
by POLYNOM3:def 10;
(power Polynom-Ring R).(qR,k) * qR
= u *' <%y1,y2%> by POLYNOM3:def 10
.= v *' <%x1,x2%> by D,E,FIELD_4:17
.= (power Polynom-Ring S).(qS,k) * qS by POLYNOM3:def 10;
hence P[k+1] by B,C;
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
hence thesis;
end;
theorem help3:
for R being domRing,
S being domRingExtension of R
for n being non zero Element of NAT
for a being Element of S holds Ext_eval(<%0.R,1.R%>`^n,a) = a|^n
proof
let R be domRing, S be domRingExtension of R;
let n be non zero Element of NAT; let a be Element of S;
reconsider q = <%0.S,1.S%>`^n as Element of the carrier of Polynom-Ring S
by POLYNOM3:def 10;
reconsider p = <%0.R,1.R%>`^n as Element of the carrier of Polynom-Ring R
by POLYNOM3:def 10;
R is Subring of S by FIELD_4:def 1; then
0.R = 0.S & 1.R = 1.S by C0SP1:def 3; then
<%0.R,1.R%>`^n = <%0.S,1.S%>`^n by helpp; then
Ext_eval(p,a) = eval(q,a) by FIELD_4:26 .= a|^n by help3a;
hence thesis;
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;
A: a|L = 0_.(L) +* (0,a) by RING_4:def 5;
0 in dom 0_.(L);
hence (a|L).0 = a by A,FUNCT_7:31;
let n be Nat;
assume n <> 0;
hence (a|L).n = (0_.(L)).n by A,FUNCT_7:32
.= 0.L by ORDINAL1:def 12,FUNCOP_1:7;
end;
theorem constpol:
for R being Ring,
S being RingExtension of R
for a being Element of R, b being Element of S st a = b holds a|R = b|S
proof
let F be Ring, E be RingExtension of F;
let a be Element of F, b be Element of E;
assume AS: a = b;
set ap = a|F, bp = b|E;
X: F is Subring of E by FIELD_4:def 1;
now let n be Element of NAT;
per cases;
suppose A: n = 0;
hence ap.n = b by AS,Th28 .= bp.n by A,Th28;
end;
suppose A: n <> 0;
hence ap.n = 0.F by Th28 .= 0.E by X,C0SP1:def 3
.= bp.n by A,Th28;
end;
end;
hence thesis;
end;
theorem pr0:
for F being Field,
E being FieldExtension of F
for p being Element of the carrier of Polynom-Ring F
for q being Element of the carrier of Polynom-Ring E st p = q
holds NormPolynomial p = NormPolynomial q
proof
let F be Field, E be FieldExtension of F;
let p be Element of the carrier of Polynom-Ring F;
let q be Element of the carrier of Polynom-Ring E;
assume AS: p = q;
set np = NormPolynomial p, nq = NormPolynomial q;
B1: F is Subfield of E by FIELD_4:7;
B: F is Subring of E by FIELD_4:def 1;
per cases;
suppose q is zero;
then B: q = 0_.(E) by UPROOTS:def 5;
then A: nq = 0_.(E) by RING_4:22 .= 0_.(F) by FIELD_4:12;
p = 0_.(F) by AS,B,FIELD_4:12;
hence thesis by A,RING_4:22;
end;
suppose q is non zero; then
LC q is non zero; then
A1: q.(len q-'1) is non zero by RATFUNC1:def 6;
len p - 1 = deg p by HURWITZ:def 2
.= deg q by AS,FIELD_4:20
.= len q - 1 by HURWITZ:def 2; then
A: (p.(len p-'1))" = (q.(len q-'1))" by AS,A1,B1,Th19f;
now let n be Element of NAT;
thus np.n = p.n / p.(len p-'1) by POLYNOM5:def 11
.= q.n / q.(len q-'1) by B,A,AS,Th18
.= nq.n by POLYNOM5:def 11;
end;
hence thesis;
end;
end;
theorem pr1:
for F being Field,
E being FieldExtension of F
for p being Element of the carrier of Polynom-Ring F
for a being Element of E
holds Ext_eval(p,a) = 0.E iff Ext_eval(NormPolynomial p,a) = 0.E
proof
let F be Field, E be FieldExtension of F;
let p be Element of the carrier of Polynom-Ring F;
let a be Element of E;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E
by FIELD_4:10;
then reconsider q = p as Element of the carrier of Polynom-Ring E;
reconsider qa = q as Polynomial of E;
reconsider ra = rpoly(1,a) as Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
A: now assume Ext_eval(p,a) = 0.E; then
eval(qa,a) = 0.E by FIELD_4:26; then
ra divides NormPolynomial qa by RING_4:26,RING_5:11; then
eval(NormPolynomial q,a) = 0.E by RING_5:11;
hence Ext_eval(NormPolynomial p,a) = 0.E by pr0,FIELD_4:26;
end;
now assume Ext_eval(NormPolynomial p,a) = 0.E;
then eval(NormPolynomial q,a) = 0.E by pr0,FIELD_4:26;
then ra divides NormPolynomial qa by RING_5:11;
then eval(qa,a) = 0.E by RING_5:11,RING_4:26;
hence Ext_eval(p,a) = 0.E by FIELD_4:26;
end;
hence thesis by A;
end;
theorem exevalminus:
for R being Ring,
S being RingExtension of R
for a being Element of S,
p being Polynomial of R holds Ext_eval(-p,a) = - Ext_eval(p,a)
proof
let R be Ring, S be RingExtension of R;
let a be Element of S, p be Polynomial of R;
consider G being FinSequence of S such that
A: Ext_eval(p,a) = Sum G & len G = len p &
for n being Element of NAT st n in dom G
holds G.n = In(p.(n-'1),S) * (power S).(a,n-'1) by ALGNUM_1:def 1;
consider H being FinSequence of S such that
B: Ext_eval(-p,a) = Sum H & len H = len -p &
for n being Element of NAT st n in dom H
holds H.n = In((-p).(n-'1),S) * (power S).(a,n-'1) by ALGNUM_1:def 1;
K: R is Subring of S by FIELD_4:def 1; then
H: the carrier of R c= the carrier of S by C0SP1:def 3;
C: len G = len H by A,B,POLYNOM4:8;
now let n be Nat, b be Element of S;
assume D1: n in dom H & b = G.n;
D2: dom H = Seg(len G) by C,FINSEQ_1:def 3 .= dom G by FINSEQ_1:def 3;
reconsider pn1 = p.(n-'1), mpn1 = -p.(n-'1) as Element of S by H;
thus H.n = In((-p).(n-'1),S) * (power S).(a,n-'1) by B,D1
.= In(-(p.(n-'1)),S) * (power S).(a,n-'1) by BHSP_1:44
.= mpn1 * (power S).(a,n-'1)
.= (- pn1) * (power S).(a,n-'1) by K,Th19
.= -(In(p.(n-'1),S) * (power S).(a,n-'1)) by VECTSP_1:9
.= - b by D1,D2,A;
end;
hence thesis by A,B,POLYNOM4:8,RLVECT_1:40;
end;
theorem exevalminus2:
for R being Ring,
S being RingExtension of R
for 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 Ring, S be RingExtension of R;
let a be Element of S, p,q be Polynomial of R;
R is Subring of S by FIELD_4:def 1;
hence Ext_eval(p-q,a) = Ext_eval(p,a) + Ext_eval(-q,a) by ALGNUM_1:15
.= Ext_eval(p,a) - Ext_eval(q,a) by exevalminus;
end;
theorem exevalconst:
for R being Ring,
S being RingExtension of R
for a being Element of S,
p being constant Polynomial of R holds Ext_eval(p,a) = LC p
proof
let R be Ring, S be RingExtension of R;
let a be Element of S, p be constant Polynomial of R;
A: R is Subring of S by FIELD_4:def 1;
per cases;
suppose A0: p = 0_.(R);
hence Ext_eval(p,a) = 0.S by ALGNUM_1:13
.= p.(len p-'1) by A0,A,C0SP1:def 3
.= LC p by RATFUNC1:def 6;
end;
suppose A0: p <> 0_.(R);
the carrier of R c= the carrier of S by A,C0SP1:def 3; then
reconsider p0 = p.0 as Element of S;
consider F being FinSequence of S such that
A1: Ext_eval(p,a) = Sum F and
A2: len F = len p and
A3: for n be Element of NAT st n in dom F holds
F.n = In(p.(n-'1),S)*(power S).(a,n-'1) by ALGNUM_1:def 1;
reconsider degp = deg p as Element of NAT by A0,FIELD_1:1;
A7: degp = 0 by RATFUNC1:def 2;
A6: deg p = len p - 1 by HURWITZ:def 2; then
A4: F.1 = In(p.(1-'1),S) * (power S).(a,1-'1) by A7,A2,A3,FINSEQ_3:25
.= In(p.0,S) * (power S).(a,1-'1) by XREAL_1:232
.= p0 * (power S).(a,0) by XREAL_1:232
.= p0 * 1_S by GROUP_1:def 7
.= p0;
Sum F = Sum <*p0*> by A6,A7,A2,FINSEQ_1:40,A4
.= p.(1-1) by RLVECT_1:44
.= p.(1-'1) by XREAL_0:def 2
.= LC p by A6,A7,RATFUNC1:def 6;
hence thesis by A1;
end;
end;
theorem exevalLM:
for R being non degenerated Ring,
S being RingExtension of R
for a,b being Element of S,
p being non zero Polynomial of R st b = LC p holds
Ext_eval(Leading-Monomial p,a) = b * a|^(deg p)
proof
let R be non degenerated Ring, S be RingExtension of R;
let a,b be Element of S, p be non zero Polynomial of R;
assume AS: b = LC p;
H0: R is Subring of S by FIELD_4:def 1;
H2: p.(len p-'1) = LC p by RATFUNC1:def 6;
deg p = len p - 1 by HURWITZ:def 2; then
H3: len p -' 1 = deg p by XREAL_0:def 2;
thus Ext_eval(Leading-Monomial p,a)
= In(p.(len p-'1),S) * (power S).(a,len p-'1) by H0,ALGNUM_1:17
.= b * a|^(deg p) by AS,H2,H3,BINOM:def 2;
end;
begin :: Ring and Field Adjunctions
definition
let R be Ring,
S be RingExtension of R;
let T be Subset of S;
func carrierRA(T) -> non empty Subset of S equals
{x where x is Element of S :
for U being Subring of S
st R is Subring of U & T is Subset of U holds x in U};
coherence
proof
set M = {x where x is Element of S :
for U being Subring of S
st R is Subring of U & T is Subset of U holds x in U};
now let U be Subring of S;
assume R is Subring of U & T is Subset of U;
1.U = 1.S by C0SP1:def 3;
hence 1.S in U;
end;
then A: 1.S in M;
now let o be object;
assume o in M;
then consider x being Element of S such that
H: o = x & for U being Subring of S st R is Subring of U & T is Subset of U
holds x in U;
thus o in the carrier of S by H;
end;
hence thesis by TARSKI:def 3,A;
end;
end;
definition
let R be Ring,
S be RingExtension of R;
let T be Subset of S;
func RingAdjunction(R,T) -> strict doubleLoopStr means :dRA:
the carrier of it = carrierRA(T) &
the addF of it = (the addF of S)||carrierRA(T) &
the multF of it = (the multF of S)||carrierRA(T) &
the OneF of it = 1.S &
the ZeroF of it = 0.S;
existence
proof
set C = carrierRA T;
set f = the addF of S;
C is Preserv of f
proof
now let x be set;
assume x in [:C,C:];
then consider x1,x2 being object such that
A1: x1 in C and
A2: x2 in C and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider y1 being Element of S such that
A4: x1 = y1 and
A5: for U being Subring of S st R is Subring of U & T is Subset of U
holds y1 in U by A1;
consider y2 being Element of S such that
A6: x2 = y2 and
A7: for U being Subring of S st R is Subring of U & T is Subset of U
holds y2 in U by A2;
now let U be Subring of S;
assume R is Subring of U & T is Subset of U;
then y1 in U & y2 in U by A5,A7;
then reconsider a1 = y1, a2 = y2 as Element of U;
the addF of U = f || the carrier of U by C0SP1:def 3;
then (the addF of U).(a1,a2) = f.(a1,a2) by RING_3:1;
hence f.(y1,y2) in U;
end;
hence f.x in C by A3,A4,A6;
end;
hence thesis by REALSET1:def 1;
end;
then reconsider C as Preserv of the addF of S;
set f = the multF of S;
C is Preserv of f
proof
now let x be set;
assume x in [:C,C:];
then consider x1,x2 being object such that
A1: x1 in C and
A2: x2 in C and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider y1 being Element of S such that
A4: x1 = y1 and
A5: for U being Subring of S st R is Subring of U & T is Subset of U
holds y1 in U by A1;
consider y2 being Element of S such that
A6: x2 = y2 and
A7: for U being Subring of S st R is Subring of U & T is Subset of U
holds y2 in U by A2;
now let U be Subring of S;
assume R is Subring of U & T is Subset of U;
then y1 in U & y2 in U by A5,A7;
then reconsider a1 = y1, a2 = y2 as Element of U;
the multF of U = f || the carrier of U by C0SP1:def 3;
then (the multF of U).(a1,a2) = f.(a1,a2) by RING_3:1;
hence f.(y1,y2) in U;
end;
hence f.x in C by A3,A4,A6;
end;
hence thesis by REALSET1:def 1;
end;
then reconsider D = C as Preserv of the multF of S;
reconsider m = (the multF of S)||D as BinOp of C;
set o = 1.S, z = 0.S;
ex x being Element of S st x = o &
for U being Subring of S st R is Subring of U & T is Subset of U
holds x in U
proof
take o;
now let U be Subring of S;
assume T is Subset of U;
1.U = 1.S by C0SP1:def 3;
hence o in U;
end;
hence thesis;
end;
then o in C;
then reconsider o as Element of C;
ex x being Element of S st x = z &
for U being Subring of S st R is Subring of U & T is Subset of U
holds x in U
proof
take z;
now let U be Subring of S;
assume R is Subring of U & T is Subset of U;
0.U = 0.S by C0SP1:def 3;
hence z in U;
end;
hence thesis;
end;
then z in C;
then reconsider z as Element of C;
take doubleLoopStr (# C,(the addF of S)||C,m,o,z #);
thus thesis;
end;
uniqueness;
end;
notation
let R be Ring,
S be RingExtension of R;
let T be Subset of S;
synonym RAdj(R,T) for RingAdjunction(R,T);
end;
registration
let R be Ring,
S be RingExtension of R;
let T be Subset of S;
cluster RAdj(R,T) -> non empty;
coherence
proof
the carrier of RAdj(R,T) = carrierRA(T) by dRA;
hence thesis;
end;
end;
registration
let R be non degenerated Ring,
S be RingExtension of R;
let T be Subset of S;
cluster RAdj(R,T) -> non degenerated;
coherence
proof
set RA = RAdj(R,T);
0.RA = 0.S & 1.RA = 1.S by dRA;
hence 0.RA <> 1.RA;
end;
end;
Lm10:
for R be Ring, S be RingExtension of R, T be Subset of S
for x being Element of RAdj(R,T) holds x is Element of S
proof
let R be Ring, S be RingExtension of R,
T be Subset of S; let x be Element of RAdj(R,T);
A1: the carrier of RAdj(R,T) = carrierRA(T) by dRA;
x in the carrier of RAdj(R,T);
hence thesis by A1;
end;
Lm11:
for R be Ring, S be RingExtension of R, T be Subset of S
for a,b being Element of S
for x,y being Element of RAdj(R,T) st a = x & b = y holds
a+b = x+y
proof
let R be Ring, S be RingExtension of R, T be Subset of S;
let a,b be Element of S; let x,y be Element of RAdj(R,T) such that
A1: a = x & b = y;
the carrier of RAdj(R,T) = carrierRA(T) by dRA;
hence a+b = (the addF of S)||(carrierRA(T)).(x,y) by A1,RING_3:1
.= x+y by dRA;
end;
Lm12:
for R be Ring, S be RingExtension of R, T be Subset of S
for a,b being Element of S
for x,y being Element of RAdj(R,T) st a = x & b = y holds
a*b = x*y
proof
let R be Ring, S be RingExtension of R, T be Subset of S;
let a,b be Element of S;
let x,y be Element of RAdj(R,T) such that
A1: a = x & b = y;
the carrier of RAdj(R,T) = carrierRA(T) by dRA;
hence a*b = (the multF of S)||(carrierRA(T)).(x,y) by A1,RING_3:1
.= x*y by dRA;
end;
registration
let R be Ring,
S be RingExtension of R;
let T be Subset of S;
cluster RAdj(R,T) -> Abelian add-associative right_zeroed right_complementable;
coherence
proof
set P = RAdj(R,T);
A1: 0.P = 0.S by dRA;
A2: the carrier of RAdj(R,T) = carrierRA(T) by dRA;
hereby
let x,y be Element of P;
reconsider a = x, b = y as Element of S by Lm10;
thus x+y = a+b by Lm11
.= y+x by Lm11;
end;
hereby
let x,y,z be Element of P;
reconsider a = x, b = y, c = z as Element of S by Lm10;
A3: y+z = b+c by Lm11;
x+y = a+b by Lm11;
hence x+y+z = a+b+c by Lm11
.= a+(b+c) by RLVECT_1:def 3
.= x+(y+z) by A3,Lm11;
end;
hereby
let x be Element of P;
reconsider a = x as Element of S by Lm10;
thus x+0.P = a+0.S by A1,Lm11
.= x;
end;
let x be Element of P;
reconsider a = x as Element of S by Lm10;
x in carrierRA(T) by A2;
then consider x1 being Element of S such that
A4: x = x1 and
A5: for U being Subring of S st R is Subring of U & T is Subset of U
holds x1 in U;
now let U be Subring of S;
assume R is Subring of U & T is Subset of U;
then x1 in U by A5;
then reconsider t = x1 as Element of U;
-t = -x1 by Th19;
hence -x1 in U;
end;
then -x1 in carrierRA(T);
then reconsider y = -x1 as Element of P by dRA;
take y;
thus x+y = a+-x1 by Lm11
.= 0.P by A1,A4,RLVECT_1:5;
end;
end;
registration
let R be comRing,
S be comRingExtension of R;
let T be Subset of S;
cluster RAdj(R,T) -> commutative;
coherence
proof
now let x,y be Element of RAdj(R,T);
reconsider a = x, b = y as Element of S by Lm10;
thus x*y = a*b by Lm12 .= b * a by GROUP_1:def 12 .= y*x by Lm12;
end;
hence thesis;
end;
end;
registration
let R be Ring,
S be RingExtension of R;
let T be Subset of S;
cluster RAdj(R,T) -> associative well-unital distributive;
coherence
proof
set P = RAdj(R,T);
A1: 1.P = 1.S by dRA;
now let x,y,z be Element of P;
reconsider a = x, b = y, c = z as Element of S by Lm10;
A3: y*z = b*c by Lm12;
x*y = a*b by Lm12;
hence (x*y)*z = (a*b)*c by Lm12
.= a*(b*c) by GROUP_1:def 3
.= x*(y*z) by A3,Lm12;
end;
hence P is associative;
now let x be Element of P;
reconsider a = x as Element of S by Lm10;
thus x * 1.P = a * 1.S by A1,Lm12
.= x;
thus 1.P * x = 1.S * a by A1,Lm12
.= x;
end;
hence P is well-unital;
now let x,y,z be Element of P;
reconsider a = x, b = y, c = z as Element of S by Lm10;
A4: a*b = x*y & a*c = x*z by Lm12;
A6: b*a = y*x & c*a = z*x by Lm12;
A5: y+z = b+c by Lm11;
hence x*(y+z) = a*(b+c) by Lm12
.= a*b+a*c by VECTSP_1:def 7
.= x*y+x*z by A4,Lm11;
thus (y+z)*x = (b+c)*a by A5,Lm12
.= b*a+c*a by VECTSP_1:def 7
.= y*x+z*x by A6,Lm11;
end;
hence thesis;
end;
end;
theorem RAt:
for R being Ring,
S being RingExtension of R
for T being Subset of S holds T is Subset of RAdj(R,T)
proof
let R be Ring, S be RingExtension of R; let T be Subset of S;
set P = RAdj(R,T);
now let o be object;
assume A: o in T;
then reconsider a = o as Element of S;
for U be Subring of S st R is Subring of U & T is Subset of U
holds o in U by A;
then a in carrierRA(T);
hence o in the carrier of P by dRA;
end;
hence thesis by TARSKI:def 3;
end;
theorem RAsub:
for R being Ring,
S being RingExtension of R
for T being Subset of S holds R is Subring of RAdj(R,T)
proof
let R be Ring, S be RingExtension of R; let T be Subset of S;
set P = RAdj(R,T);
X: R is Subring of S by FIELD_4:def 1;
A: 1.P = 1.S by dRA .= 1.R by X,C0SP1:def 3;
B: 0.P = 0.S by dRA .= 0.R by X,C0SP1:def 3;
C: the carrier of R c= the carrier of P
proof
now let o be object;
assume C1: o in the carrier of R;
the carrier of R c= the carrier of S by X,C0SP1:def 3;
then reconsider a = o as Element of S by C1;
now let U be Subring of S;
assume R is Subring of U & T is Subset of U;
then the carrier of R c= the carrier of U by C0SP1:def 3;
hence o in U by C1;
end;
then a in carrierRA(T);
hence o in the carrier of P by dRA;
end;
hence thesis;
end;
then Y: [:the carrier of R,the carrier of R:] c=
[:the carrier of P,the carrier of P:] by ZFMISC_1:96;
D: (the addF of P)||the carrier of R
= ((the addF of S)||carrierRA(T))||the carrier of R by dRA
.= ((the addF of S)||the carrier of P)||the carrier of R by dRA
.= (the addF of S)||the carrier of R by Y,FUNCT_1:51
.= the addF of R by X,C0SP1:def 3;
(the multF of P)||the carrier of R
= ((the multF of S)||carrierRA(T))||the carrier of R by dRA
.= ((the multF of S)||the carrier of P)||the carrier of R by dRA
.= (the multF of S)||the carrier of R by Y,FUNCT_1:51
.= the multF of R by X,C0SP1:def 3;
hence thesis by A,B,C,D,C0SP1:def 3;
end;
theorem RAsub2:
for R being Ring,
S being RingExtension of R,
T being Subset of S
for U being Subring of S st R is Subring of U & T is Subset of U
holds RAdj(R,T) is Subring of U
proof
let R be Ring, S be RingExtension of R; let T be Subset of S;
let U be Subring of S;
assume AS: R is Subring of U & T is Subset of U;
set P = RAdj(R,T);
A: 1.P = 1.S by dRA .= 1.U by C0SP1:def 3;
B: 0.P = 0.S by dRA .= 0.U by C0SP1:def 3;
C: the carrier of P c= the carrier of U
proof
now let o be object;
assume o in the carrier of P;
then o in carrierRA(T) by dRA;
then consider x being Element of S such that
C2: x = o & for U being Subring of S
st R is Subring of U & T is Subset of U holds x in U;
x in U by C2,AS;
hence o in the carrier of U by C2;
end;
hence thesis;
end;
then Y: [:the carrier of P,the carrier of P:] c=
[:the carrier of U,the carrier of U:] by ZFMISC_1:96;
D: (the addF of U)||the carrier of P
= ((the addF of S)||the carrier of U)||the carrier of P by C0SP1:def 3
.= (the addF of S)||the carrier of P by Y,FUNCT_1:51
.= (the addF of S)||carrierRA(T) by dRA
.= the addF of P by dRA;
(the multF of U)||the carrier of P
= ((the multF of S)||the carrier of U)||the carrier of P by C0SP1:def 3
.= (the multF of S)||the carrier of P by Y,FUNCT_1:51
.= (the multF of S)||carrierRA(T) by dRA
.= the multF of P by dRA;
hence thesis by A,B,C,D,C0SP1:def 3;
end;
theorem
for R being strict Ring,
S being RingExtension of R,
T being Subset of S holds RAdj(R,T) = R iff T is Subset of R
proof
let R be strict Ring, S be RingExtension of R; let T be Subset of S;
set P = RAdj(R,T);
X: R is Subring of R & R is Subring of S by FIELD_4:def 1,LIOUVIL2:18;
Z: now let o be object;
assume C1: o in the carrier of R;
the carrier of R c= the carrier of S by X,C0SP1:def 3;
then reconsider a = o as Element of S by C1;
now let U be Subring of S;
assume R is Subring of U & T is Subset of U;
then the carrier of R c= the carrier of U by C0SP1:def 3;
hence o in U by C1;
end;
then a in carrierRA(T);
hence o in the carrier of P by dRA;
end;
now assume B0: T is Subset of R;
B5: now let o be object;
assume o in the carrier of P;
then o in carrierRA(T) by dRA;
then consider x being Element of S such that
B1: x = o & for U being Subring of S
st R is Subring of U & T is Subset of U holds x in U;
x in R by X,B0,B1;
hence o in the carrier of R by B1;
end;
then B1: the carrier of R = the carrier of P by Z,TARSKI:2;
B2: 1.P = 1.S by dRA .= 1.R by X,C0SP1:def 3;
B3: 0.P = 0.S by dRA .= 0.R by X,C0SP1:def 3;
B4: the addF of P = (the addF of S)||carrierRA(T) by dRA
.= (the addF of S)||the carrier of R by B1,dRA
.= the addF of R by X,C0SP1:def 3;
the multF of P = (the multF of S)||carrierRA(T) by dRA
.= (the multF of S)||the carrier of R by B1,dRA
.= the multF of R by X,C0SP1:def 3;
hence RAdj(R,T) = R by Z,TARSKI:2,B5,B2,B3,B4;
end;
hence thesis by RAt;
end;
definition
let R be Ring,
S be RingExtension of R;
let T be Subset of S;
redefine func RAdj(R,T) -> strict Subring of S; :: redefines RAdj (FIELD_6, synonym) → RingAdjunction (FIELD_6, definition)
coherence
proof
R is Subring of S & S is Subring of S by LIOUVIL2:18,FIELD_4:def 1;
hence thesis by RAsub2;
end;
end;
registration
let R be Ring,
S be RingExtension of R;
let T be Subset of S;
cluster RAdj(R,T) -> R-extending;
coherence
proof
R is Subring of RAdj(R,T) by RAsub;
hence thesis by FIELD_4:def 1;
end;
end;
registration
let F be Field,
R be RingExtension of F;
let T be Subset of R;
cluster RAdj(F,T) -> field-containing;
coherence
proof
ex E being Field st E is Subring of RAdj(F,T)
proof
take F;
thus thesis by RAsub;
end;
hence thesis;
end;
end;
theorem
for F being Field,
R being RingExtension of F
for T being Subset of R holds F is Subfield of RAdj(F,T)
proof
let F be Field, R be RingExtension of F, T be Subset of R;
F is Subring of RAdj(F,T) by RAsub;
hence thesis by defsubfr;
end;
definition
let F be Field,
E be FieldExtension of F;
let T be Subset of E;
func carrierFA(T) -> non empty Subset of E equals
{x where x is Element of E :
for U being Subfield of E
st F is Subfield of U & T is Subset of U holds x in U};
coherence
proof
set M = {x where x is Element of E :
for U being Subfield of E
st F is Subfield of U & T is Subset of U holds x in U};
now let U be Subfield of E;
assume F is Subfield of U & T is Subset of U;
1.U = 1.E by EC_PF_1:def 1;
hence 1.E in U;
end;
then A: 1.E in M;
now let o be object;
assume o in M;
then consider x being Element of E such that
H: o = x & for U being Subfield of E st F is Subfield of U & T is Subset of U
holds x in U;
thus o in the carrier of E by H;
end;
hence thesis by TARSKI:def 3,A;
end;
end;
definition
let F be Field,
E be FieldExtension of F;
let T be Subset of E;
func FieldAdjunction(F,T) -> strict doubleLoopStr means :dFA:
the carrier of it = carrierFA(T) &
the addF of it = (the addF of E)||carrierFA(T) &
the multF of it = (the multF of E)||carrierFA(T) &
the OneF of it = 1.E &
the ZeroF of it = 0.E;
existence
proof
set C = carrierFA(T);
set f = the addF of E;
C is Preserv of f
proof
now let x be set;
assume x in [:C,C:];
then consider x1,x2 being object such that
A1: x1 in C and
A2: x2 in C and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider y1 being Element of E such that
A4: x1 = y1 and
A5: for U being Subfield of E st F is Subfield of U & T is Subset of U
holds y1 in U by A1;
consider y2 being Element of E such that
A6: x2 = y2 and
A7: for U being Subfield of E st F is Subfield of U & T is Subset of U
holds y2 in U by A2;
now let U be Subfield of E;
assume F is Subfield of U & T is Subset of U;
then y1 in U & y2 in U by A5,A7;
then reconsider a1 = y1, a2 = y2 as Element of U;
the addF of U = f || the carrier of U by EC_PF_1:def 1;
then (the addF of U).(a1,a2) = f.(a1,a2) by RING_3:1;
hence f.(y1,y2) in U;
end;
hence f.x in C by A3,A4,A6;
end;
hence thesis by REALSET1:def 1;
end;
then reconsider C as Preserv of the addF of E;
set f = the multF of E;
C is Preserv of f
proof
now let x be set;
assume x in [:C,C:];
then consider x1,x2 being object such that
A1: x1 in C and
A2: x2 in C and
A3: x = [x1,x2] by ZFMISC_1:def 2;
consider y1 being Element of E such that
A4: x1 = y1 and
A5: for U being Subfield of E st F is Subfield of U & T is Subset of U
holds y1 in U by A1;
consider y2 being Element of E such that
A6: x2 = y2 and
A7: for U being Subfield of E st F is Subfield of U & T is Subset of U
holds y2 in U by A2;
now let U be Subfield of E;
assume F is Subfield of U & T is Subset of U;
then y1 in U & y2 in U by A5,A7;
then reconsider a1 = y1, a2 = y2 as Element of U;
the multF of U = f || the carrier of U by EC_PF_1:def 1;
then (the multF of U).(a1,a2) = f.(a1,a2) by RING_3:1;
hence f.(y1,y2) in U;
end;
hence f.x in C by A3,A4,A6;
end;
hence thesis by REALSET1:def 1;
end;
then reconsider D = C as Preserv of the multF of E;
reconsider m = (the multF of E)||D as BinOp of C;
set o = 1.E, z = 0.E;
ex x being Element of E st x = o &
for U being Subfield of E st F is Subfield of U & T is Subset of U
holds x in U
proof
take o;
now let U be Subfield of E;
assume T is Subset of U;
1.U = 1.E by EC_PF_1:def 1;
hence o in U;
end;
hence thesis;
end;
then o in C;
then reconsider o as Element of C;
ex x being Element of E st x = z &
for U being Subfield of E st F is Subfield of U & T is Subset of U
holds x in U
proof
take z;
now let U be Subfield of E;
assume F is Subfield of U & T is Subset of U;
0.U = 0.E by EC_PF_1:def 1;
hence z in U;
end;
hence thesis;
end;
then z in C;
then reconsider z as Element of C;
take doubleLoopStr (# C,(the addF of E)||C,m,o,z #);
thus thesis;
end;
uniqueness;
end;
notation
let F be Field,
E be FieldExtension of F;
let T be Subset of E;
synonym FAdj(F,T) for FieldAdjunction(F,T);
end;
registration
let F be Field,
E be FieldExtension of F;
let T be Subset of E;
cluster FAdj(F,T) -> non degenerated;
coherence
proof
set FA = FAdj(F,T);
0.FA = 0.E & 1.FA = 1.E by dFA;
hence 0.FA <> 1.FA;
end;
end;
Lm10f:
for R be Field, S be FieldExtension of R, T be Subset of S
for x being Element of FAdj(R,T) holds x is Element of S
proof
let R be Field, S be FieldExtension of R,
T be Subset of S; let x be Element of FAdj(R,T);
A1: the carrier of FAdj(R,T) = carrierFA(T) by dFA;
x in the carrier of FAdj(R,T);
hence thesis by A1;
end;
Lm11f:
for R be Field, S be FieldExtension of R, T be Subset of S
for a,b being Element of S
for x,y being Element of FAdj(R,T) st a = x & b = y holds
a+b = x+y
proof
let R be Field, S be FieldExtension of R, T be Subset of S;
let a,b be Element of S;
let x,y be Element of FAdj(R,T) such that
A1: a = x & b = y;
the carrier of FAdj(R,T) = carrierFA(T) by dFA;
hence a+b = (the addF of S)||(carrierFA(T)).(x,y) by A1,RING_3:1
.= x+y by dFA;
end;
Lm12f:
for R be Field, S be FieldExtension of R, T be Subset of S
for a,b being Element of S
for x,y being Element of FAdj(R,T) st a = x & b = y holds
a*b = x*y
proof
let R be Field, S be FieldExtension of R, T be Subset of S;
let a,b be Element of S;
let x,y be Element of FAdj(R,T) such that
A1: a = x & b = y;
the carrier of FAdj(R,T) = carrierFA(T) by dFA;
hence a*b = (the multF of S)||(carrierFA(T)).(x,y) by A1,RING_3:1
.= x*y by dFA;
end;
registration
let F be Field,
E be FieldExtension of F;
let T be Subset of E;
cluster FAdj(F,T) -> Abelian add-associative right_zeroed right_complementable;
coherence
proof
set P = FAdj(F,T);
A1: 0.P = 0.E by dFA;
A2: the carrier of FAdj(F,T) = carrierFA(T) by dFA;
hereby
let x,y be Element of P;
reconsider a = x, b = y as Element of E by Lm10f;
thus x+y = a+b by Lm11f
.= y+x by Lm11f;
end;
hereby
let x,y,z be Element of P;
reconsider a = x, b = y, c = z as Element of E by Lm10f;
A3: y+z = b+c by Lm11f;
x+y = a+b by Lm11f;
hence x+y+z = a+b+c by Lm11f
.= a+(b+c) by RLVECT_1:def 3
.= x+(y+z) by A3,Lm11f;
end;
hereby
let x be Element of P;
reconsider a = x as Element of E by Lm10f;
thus x+0.P = a+0.E by A1,Lm11f
.= x;
end;
let x be Element of P;
reconsider a = x as Element of E by Lm10f;
x in carrierFA(T) by A2;
then consider x1 being Element of E such that
A4: x = x1 and
A5: for U being Subfield of E st F is Subfield of U & T is Subset of U
holds x1 in U;
now let U be Subfield of E;
assume F is Subfield of U & T is Subset of U;
then x1 in U by A5;
then reconsider t = x1 as Element of U;
-t = -x1 by GAUSSINT:19;
hence -x1 in U;
end;
then -x1 in carrierFA(T);
then reconsider y = -x1 as Element of P by dFA;
take y;
thus x+y = a+-x1 by Lm11f
.= 0.P by A1,A4,RLVECT_1:5;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let T be Subset of E;
cluster FieldAdjunction(F,T) -> commutative associative well-unital
distributive almost_left_invertible;
coherence
proof
set P = FAdj(F,T);
A1: 1.P = 1.E by dFA;
A2: 0.P = 0.E by dFA;
now let x,y be Element of P;
reconsider a = x, b = y as Element of E by Lm10f;
thus x*y = a*b by Lm12f .= b*a by GROUP_1:def 12 .= y*x by Lm12f;
end;
hence P is commutative;
now let x,y,z be Element of P;
reconsider a = x, b = y, c = z as Element of E by Lm10f;
A3: y*z = b*c by Lm12f;
x*y = a*b by Lm12f;
hence (x*y)*z = (a*b)*c by Lm12f
.= a*(b*c) by GROUP_1:def 3
.= x*(y*z) by A3,Lm12f;
end;
hence P is associative;
now let x be Element of P;
reconsider a = x as Element of E by Lm10f;
thus x * 1.P = a * 1.E by A1,Lm12f
.= x;
thus 1.P * x = 1.E * a by A1,Lm12f
.= x;
end;
hence P is well-unital;
now let x,y,z be Element of P;
reconsider a = x, b = y, c = z as Element of E by Lm10f;
A4: a*b = x*y & a*c = x*z by Lm12f;
A6: b*a = y*x & c*a = z*x by Lm12f;
A5: y+z = b+c by Lm11f;
hence x*(y+z) = a*(b+c) by Lm12f
.= a*b+a*c by VECTSP_1:def 7
.= x*y+x*z by A4,Lm11f;
thus (y+z)*x = (b+c)*a by A5,Lm12f
.= b*a+c*a by VECTSP_1:def 7
.= y*x+z*x by A6,Lm11f;
end;
hence P is distributive;
now let x be Element of P such that
A5: x <> 0.P;
reconsider a = x as Element of E by Lm10f;
the carrier of P = carrierFA(T) by dFA;
then x in carrierFA(T);
then consider x1 being Element of E such that
A6: x = x1 and
A7: for U being Subfield of E st F is Subfield of U & T is Subset of U
holds x1 in U;
now
let U be Subfield of E;
assume F is Subfield of U & T is Subset of U;
then x1 in U by A7;
then reconsider t = x1 as Element of U;
t" = x1" by A5,A6,A2,GAUSSINT:21;
hence x1" in U;
end;
then x1" in carrierFA(T);
then reconsider y = x1" as Element of P by dFA;
take y;
thus y*x = x1"*a by Lm12f
.= 1.P by A1,A2,A5,A6,VECTSP_1:def 10;
end;
hence thesis;
end;
end;
theorem FAt:
for F being Field,
E being FieldExtension of F
for T being Subset of E holds T is Subset of FAdj(F,T)
proof
let R be Field, S be FieldExtension of R; let T be Subset of S;
set P = FAdj(R,T);
now let o be object;
assume A: o in T;
then reconsider a = o as Element of S;
for U be Subfield of S st R is Subfield of U & T is Subset of U
holds o in U by A;
then a in carrierFA(T);
hence o in the carrier of P by dFA;
end;
hence thesis by TARSKI:def 3;
end;
theorem FAsub:
for F being Field,
E being FieldExtension of F
for T being Subset of E holds F is Subfield of FAdj(F,T)
proof
let R be Field, S be FieldExtension of R; let T be Subset of S;
set P = FAdj(R,T);
X: R is Subring of S by FIELD_4:def 1;
A: 1.P = 1.S by dFA .= 1.R by X,C0SP1:def 3;
B: 0.P = 0.S by dFA .= 0.R by X,C0SP1:def 3;
C: the carrier of R c= the carrier of P
proof
now let o be object;
assume C1: o in the carrier of R;
the carrier of R c= the carrier of S by X,C0SP1:def 3;
then reconsider a = o as Element of S by C1;
now let U be Subfield of S;
assume R is Subfield of U & T is Subset of U;
then the carrier of R c= the carrier of U by EC_PF_1:def 1;
hence o in U by C1;
end;
then a in carrierFA(T);
hence o in the carrier of P by dFA;
end;
hence thesis;
end;
then Y: [:the carrier of R,the carrier of R:] c=
[:the carrier of P,the carrier of P:] by ZFMISC_1:96;
D: (the addF of P)||the carrier of R
= ((the addF of S)||carrierFA(T))||the carrier of R by dFA
.= ((the addF of S)||the carrier of P)||the carrier of R by dFA
.= (the addF of S)||the carrier of R by Y,FUNCT_1:51
.= the addF of R by X,C0SP1:def 3;
(the multF of P)||the carrier of R
= ((the multF of S)||carrierFA(T))||the carrier of R by dFA
.= ((the multF of S)||the carrier of P)||the carrier of R by dFA
.= (the multF of S)||the carrier of R by Y,FUNCT_1:51
.= the multF of R by X,C0SP1:def 3;
hence thesis by A,B,C,D,EC_PF_1:def 1;
end;
theorem FAsub2:
for F being Field,
E being FieldExtension of F,
T being Subset of E
for U being Subfield of E st F is Subfield of U & T is Subset of U
holds FAdj(F,T) is Subfield of U
proof
let R be Field, S be FieldExtension of R; let T be Subset of S;
let U be Subfield of S;
assume AS: R is Subfield of U & T is Subset of U;
set P = FAdj(R,T);
A: 1.P = 1.S by dFA .= 1.U by EC_PF_1:def 1;
B: 0.P = 0.S by dFA .= 0.U by EC_PF_1:def 1;
C: the carrier of P c= the carrier of U
proof
now let o be object;
assume o in the carrier of P;
then o in carrierFA(T) by dFA;
then consider x being Element of S such that
C2: x = o & for U being Subfield of S
st R is Subfield of U & T is Subset of U holds x in U;
x in U by C2,AS;
hence o in the carrier of U by C2;
end;
hence thesis;
end;
then Y: [:the carrier of P,the carrier of P:] c=
[:the carrier of U,the carrier of U:] by ZFMISC_1:96;
D: (the addF of U)||the carrier of P
= ((the addF of S)||the carrier of U)||the carrier of P by EC_PF_1:def 1
.= (the addF of S)||the carrier of P by Y,FUNCT_1:51
.= (the addF of S)||carrierFA(T) by dFA
.= the addF of P by dFA;
(the multF of U)||the carrier of P
= ((the multF of S)||the carrier of U)||the carrier of P by EC_PF_1:def 1
.= (the multF of S)||the carrier of P by Y,FUNCT_1:51
.= (the multF of S)||carrierFA(T) by dFA
.= the multF of P by dFA;
hence thesis by A,B,C,D,EC_PF_1:def 1;
end;
theorem
for F being strict Field,
E being FieldExtension of F,
T being Subset of E holds FAdj(F,T) = F iff T is Subset of F
proof
let R be strict Field, S be FieldExtension of R; let T be Subset of S;
set P = FAdj(R,T);
X: R is Subring of R & R is Subring of S by FIELD_4:def 1,LIOUVIL2:18;
X1: R is Subfield of R & R is Subfield of S by FIELD_4:7,FIELD_4:1;
Z: now let o be object;
assume C1: o in the carrier of R;
the carrier of R c= the carrier of S by X,C0SP1:def 3;
then reconsider a = o as Element of S by C1;
now let U be Subfield of S;
assume R is Subfield of U & T is Subset of U;
then the carrier of R c= the carrier of U by EC_PF_1:def 1;
hence o in U by C1;
end;
then a in carrierFA(T);
hence o in the carrier of P by dFA;
end;
now assume B0: T is Subset of R;
B5: now let o be object;
assume o in the carrier of P;
then o in carrierFA(T) by dFA;
then consider x being Element of S such that
B1: x = o & for U being Subfield of S
st R is Subfield of U & T is Subset of U holds x in U;
x in R by X1,B0,B1;
hence o in the carrier of R by B1;
end;
then B1: the carrier of R = the carrier of P by Z,TARSKI:2;
B2: 1.P = 1.S by dFA .= 1.R by X,C0SP1:def 3;
B3: 0.P = 0.S by dFA .= 0.R by X,C0SP1:def 3;
B4: the addF of P = (the addF of S)||carrierFA(T) by dFA
.= (the addF of S)||the carrier of R by B1,dFA
.= the addF of R by X,C0SP1:def 3;
the multF of P = (the multF of S)||carrierFA(T) by dFA
.= (the multF of S)||the carrier of R by B1,dFA
.= the multF of R by X,C0SP1:def 3;
hence FAdj(R,T) = R by Z,TARSKI:2,B5,B2,B3,B4;
end;
hence thesis by FAt;
end;
definition
let F be Field,
E be FieldExtension of F;
let T be Subset of E;
redefine func FAdj(F,T) -> strict Subfield of E; :: redefines FAdj (FIELD_6, synonym) → FieldAdjunction (FIELD_6, definition)
coherence
proof
A: F is Subfield of E by FIELD_4:7;
E is Subfield of E by FIELD_4:1;
hence thesis by A,FAsub2;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let T be Subset of E;
cluster FAdj(F,T) -> F-extending;
coherence
proof
F is Subfield of FAdj(F,T) by FAsub;
then F is Subring of FAdj(F,T) by RING_3:43;
hence thesis by FIELD_4:def 1;
end;
end;
theorem RF:
for F being Field,
E being FieldExtension of F,
T being Subset of E holds RAdj(F,T) is Subring of FAdj(F,T)
proof
let F be Field, E be FieldExtension of F; let T be Subset of E;
set Pf = FAdj(F,T), Pr = RAdj(F,T);
A: 1.Pr = 1.E by dRA .= 1.Pf by dFA;
B: 0.Pr = 0.E by dRA .= 0.Pf by dFA;
now let o be object;
assume o in the carrier of Pr;
then o in carrierRA(T) by dRA;
then consider x being Element of E such that
B1: x = o & for U being Subring of E
st F is Subring of U & T is Subset of U holds x in U;
now let U be Subfield of E;
assume F is Subfield of U & T is Subset of U;
then F is Subring of U &
U is Subring of E & T is Subset of U by RING_3:43;
hence x in U by B1;
end;
then x in carrierFA(T);
hence o in the carrier of Pf by B1,dFA;
end;
then C: the carrier of Pr c= the carrier of Pf;
then Y: [:the carrier of Pr,the carrier of Pr:] c=
[:the carrier of Pf,the carrier of Pf:] by ZFMISC_1:96;
D: (the addF of Pf)||the carrier of Pr
= ((the addF of E)||carrierFA(T))||the carrier of Pr by dFA
.= ((the addF of E)||the carrier of Pf)||the carrier of Pr by dFA
.= (the addF of E)||the carrier of Pr by Y,FUNCT_1:51
.= (the addF of E)||carrierRA(T) by dRA
.= the addF of Pr by dRA;
(the multF of Pf)||the carrier of Pr
= ((the multF of E)||carrierFA(T))||the carrier of Pr by dFA
.= ((the multF of E)||the carrier of Pf)||the carrier of Pr by dFA
.= (the multF of E)||the carrier of Pr by Y,FUNCT_1:51
.= (the multF of E)||carrierRA(T) by dRA
.= the multF of Pr by dRA;
hence thesis by A,B,C,D,C0SP1:def 3;
end;
theorem RF2:
for F being Field,
E being FieldExtension of F,
T being Subset of E holds RAdj(F,T) = FAdj(F,T) iff RAdj(F,T) is Field
proof
let F be Field, E be FieldExtension of F; let T be Subset of E;
set Pf = FAdj(F,T), Pr = RAdj(F,T);
now assume Pr is Field;
then reconsider Prf = Pr as Field;
F is Subring of Prf by RAsub; then
A: F is Subfield of Prf by FIELD_5:13;
B: Prf is Subfield of E by FIELD_5:13;
T is Subset of Prf by RAt; then
Pf is Subfield of Prf by A,B,FAsub2; then
C: Pf is Subring of Prf by FIELD_5:12;
Pr is Subring of Pf by RF;
hence Pf = Pr by C,RE;
end;
hence thesis;
end;
lcsub1:
for F being Field,
E being FieldExtension of F
for a being Element of E
for n being Element of NAT holds a|^n in the carrier of FAdj(F,{a})
proof
let F be Field, E be FieldExtension of F;
let a be Element of E; let n be Element of NAT;
defpred P[Nat] means a|^($1) in the carrier of FAdj(F,{a});
set K = FAdj(F,{a});
H: {a} is Subset of K by FAt;
a in {a} by TARSKI:def 1; then
reconsider a1 = a as Element of K by H;
a|^0 = 1_E by BINOM:8 .= 1.K by dFA; then
IA: P[0];
IS: now let k be Nat;
assume P[k];
then reconsider ak = a|^k as Element of K;
carrierFA({a}) = the carrier of K by dFA; then
I: [ak,a1] in [:carrierFA({a}),carrierFA({a}):] by ZFMISC_1:def 2;
a|^(k+1) = a|^k * a|^1 by BINOM:10
.= (the multF of E).(ak,a1) by BINOM:8
.= ((the multF of E)||carrierFA({a})).(ak,a1) by I,FUNCT_1:49
.= ak * a1 by dFA;
hence P[k+1];
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
hence thesis;
end;
begin :: Algebraic Elements
registration
let R be non degenerated comRing,
S be comRingExtension of R;
let a be Element of S;
cluster hom_Ext_eval(a,R) -> additive multiplicative unity-preserving;
coherence
proof
set F = R, E = S; X: F is Subring of E by FIELD_4:def 1;
set g = hom_Ext_eval(a,F);
now let x,y be Element of Polynom-Ring F;
reconsider p = x, q = y as Polynomial of F by POLYNOM3:def 10;
thus g.(x+y) = g.(p+q) by POLYNOM3:def 10
.= Ext_eval(p+q,a) by ALGNUM_1:def 11
.= Ext_eval(p,a) + Ext_eval(q,a) by X,ALGNUM_1:15
.= g.x + Ext_eval(q,a) by ALGNUM_1:def 11
.= g.x + g.y by ALGNUM_1:def 11;
end;
hence g is additive;
now let x,y be Element of Polynom-Ring F;
reconsider p = x, q = y as Polynomial of F by POLYNOM3:def 10;
thus g.(x*y) = g.(p*'q) by POLYNOM3:def 10
.= Ext_eval(p*'q,a) by ALGNUM_1:def 11
.= Ext_eval(p,a) * Ext_eval(q,a) by X,ALGNUM_1:20
.= g.x * Ext_eval(q,a) by ALGNUM_1:def 11
.= g.x * g.y by ALGNUM_1:def 11;
end;
hence g is multiplicative;
g.(1_(Polynom-Ring F))
= g.(1_.(F)) by POLYNOM3:37
.= Ext_eval(1_.F,a) by ALGNUM_1:def 11
.= 1_E by X,ALGNUM_1:14;
hence g is unity-preserving;
end;
end;
registration
let R be non degenerated comRing;
cluster -> (Polynom-Ring R)-homomorphic for comRingExtension of R;
coherence
proof
let S be comRingExtension of R;
set a = the Element of S;
hom_Ext_eval(a,R) is additive multiplicative unity-preserving;
hence thesis by RING_2:def 4;
end;
end;
registration
let F be Field;
cluster (Polynom-Ring F)-homomorphic for FieldExtension of F;
existence
proof
set E = the FieldExtension of F;
set a = the Element of E;
take E;
thus thesis;
end;
end;
definition
let F be Field,
E be FieldExtension of F;
let a be Element of E;
attr a is F-algebraic means
ker(hom_Ext_eval(a,F)) <> {0.(Polynom-Ring F)};
end;
notation
let F be Field,
E be FieldExtension of F;
let a be Element of E;
antonym a is F-transcendental for a is F-algebraic;
end;
theorem alg0:
for R being Ring,
S being RingExtension of R
for a being Element of S holds Ann_Poly(a,R) = ker(hom_Ext_eval(a,R))
proof
let F be Ring, E being RingExtension of F;
let a be Element of E;
set g = hom_Ext_eval(a,F);
A: now let o be object;
assume o in Ann_Poly(a,F);
then consider p being Polynomial of F such that
A1: o = p & Ext_eval(p,a) = 0.E;
A2: g.p = 0.E by A1,ALGNUM_1:def 11;
reconsider b = p as Element of Polynom-Ring F by POLYNOM3:def 10;
b in {x where x is Element of Polynom-Ring F : g.x = 0.E} by A2;
hence o in ker(hom_Ext_eval(a,F)) by A1,VECTSP10:def 9;
end;
now let o be object;
assume o in ker(hom_Ext_eval(a,F)); then
o in {x where x is Element of Polynom-Ring F : g.x = 0.E} by VECTSP10:def 9;
then consider b being Element of Polynom-Ring F such that
A1: o = b & g.b = 0.E;
reconsider p = b as Polynomial of F by POLYNOM3:def 10;
Ext_eval(p,a) = 0.E by A1,ALGNUM_1:def 11;
hence o in Ann_Poly(a,F) by A1;
end;
hence thesis by A,TARSKI:2;
end;
theorem alg1:
for F being Field,
E being FieldExtension of F
for a being Element of E holds a is F-algebraic iff a is_integral_over F
proof
let F be Field, E being FieldExtension of F; let a be Element of E;
set g = hom_Ext_eval(a,F);
A: now assume a is_integral_over F;
then consider p being Polynomial of F such that
A1: LC p = 1.F & Ext_eval(p,a) = 0.E;
(0_.(F)).(len(0_.(F))-'1) = 0.F; then
p <> 0_.(F) by A1,RATFUNC1:def 6; then
A3: p <> 0.(Polynom-Ring F) by POLYNOM3:def 10;
reconsider b = p as Element of Polynom-Ring F by POLYNOM3:def 10;
g.p = 0.E by A1,ALGNUM_1:def 11;
then b in {x where x is Element of Polynom-Ring F : g.x = 0.E};
then b in ker g by VECTSP10:def 9;
hence a is F-algebraic by A3,TARSKI:def 1;
end;
now assume A0: a is F-algebraic;
now assume AS: not ex p being Element of the carrier of Polynom-Ring F
st p in ker g & p <> 0.(Polynom-Ring F);
for x being object holds x in ker g iff x = 0.(Polynom-Ring F)
proof
let x be object;
now assume A2: x = 0.(Polynom-Ring F);
then g.x = 0.E by RING_2:6;
then x in {v where v is Element of Polynom-Ring F : g.v=0.E} by A2;
hence x in ker g by VECTSP10:def 9;
end;
hence thesis by AS;
end;
hence contradiction by A0,TARSKI:def 1;
end;
then consider p being Element of the carrier of Polynom-Ring F such that
A1: p in ker g & p <> 0.(Polynom-Ring F);
p <> 0_.(F) by A1,POLYNOM3:def 10; then
reconsider p as non zero Element of the carrier of Polynom-Ring F
by UPROOTS:def 5;
set q = NormPolynomial p;
A2: LC q = 1.F by RATFUNC1:def 7;
ker g = {v where v is Element of Polynom-Ring F : g.v = 0.E}
by VECTSP10:def 9;
then consider v being Element of the carrier of Polynom-Ring F such that
A3: v = p & g.v = 0.E by A1;
Ext_eval(p,a) = 0.E by A3,ALGNUM_1:def 11; then
Ext_eval(q,a) = 0.E by pr1;
hence a is_integral_over F by A2;
end;
hence thesis by A;
end;
theorem alg00:
for F being Field,
E being FieldExtension of F
for a being Element of E
holds a is F-algebraic iff
ex p being non zero Polynomial of F st Ext_eval(p,a) = 0.E
proof
let F be Field, E being FieldExtension of F; let a be Element of E;
set g = hom_Ext_eval(a,F);
A: now assume a is F-algebraic;
then a is_integral_over F by alg1;
then consider p being Polynomial of F such that
A1: LC p = 1.F & Ext_eval(p,a) = 0.E;
LC(0_.(F)) = (0_.(F)).(len (0_.(F))-'1) by RATFUNC1:def 6
.= 0.F;
then p is non zero by A1,UPROOTS:def 5;
hence ex p being non zero Polynomial of F st Ext_eval(p,a) = 0.E by A1;
end;
now assume ex p being non zero Polynomial of F st Ext_eval(p,a) = 0.E;
then consider p being non zero Polynomial of F such that
A1: Ext_eval(p,a) = 0.E;
A2: g.p = 0.E by A1,ALGNUM_1:def 11;
reconsider b = p as Element of Polynom-Ring F by POLYNOM3:def 10;
p <> 0_.(F);
then b is non zero by POLYNOM3:def 10; then
reconsider b as non zero Element of Polynom-Ring F;
b in {x where x is Element of Polynom-Ring F : g.x = 0.E} by A2;
then b in ker g by VECTSP10:def 9;
hence a is F-algebraic by TARSKI:def 1;
end;
hence thesis by A;
end;
registration
let F be Field,
E be FieldExtension of F;
cluster F-algebraic for Element of E;
existence
proof
set a = 1.F;
F is Subring of E by FIELD_4:def 1;
then In(a,E) is_integral_over F by ALGNUM_1:23;
hence thesis by alg1;
end;
end;
lemphi1:
for F being Field,
E being FieldExtension of F
for a being Element of E
holds rng hom_Ext_eval(a,F)
= the set of all Ext_eval(p,a) where p is Polynomial of F
proof
let F be Field, E be FieldExtension of F; let a be Element of E;
set g = hom_Ext_eval(a,F);
A: now let x be object;
assume x in rng g; then
consider p being object such that A1: p in dom g & x = g.p
by FUNCT_1:def 3;
reconsider p as Element of the carrier of Polynom-Ring F by A1;
reconsider p as Polynomial of F;
x = Ext_eval(p,a) by A1,ALGNUM_1:def 11;
hence x in the set of all Ext_eval(p,a) where p is Polynomial of F;
end;
now let x be object;
assume x in the set of all Ext_eval(p,a) where p is Polynomial of F;
then consider p being Polynomial of F such that A2: x = Ext_eval(p,a);
A3: g.p = x by A2,ALGNUM_1:def 11;
A4: dom g = the carrier of Polynom-Ring F by FUNCT_2:def 1;
p is Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
hence x in rng g by A3,A4,FUNCT_1:3;
end;
hence thesis by A,TARSKI:2;
end;
lemphi2:
for F being Field,
E being FieldExtension of F
for a being Element of E
holds rng hom_Ext_eval(a,F) c= the carrier of RAdj(F,{a})
proof
let F be Field, E be FieldExtension of F; let a be Element of E;
set g = hom_Ext_eval(a,F);
X: F is Subring of E by FIELD_4:def 1; then
Z: the carrier of F c= the carrier of E by C0SP1:def 3;
F is Subring of RAdj(F,{a}) by RAsub; then
Y: the carrier of F c= the carrier of RAdj(F,{a}) by C0SP1:def 3;
I1: for n being Nat holds (power E).(a,n) in the carrier of RAdj(F,{a})
proof
let n be Nat;
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
H: {a} is Subset of RAdj(F,{a}) by RAt;
a in {a} by TARSKI:def 1; then
reconsider a1 = a as Element of RAdj(F,{a}) by H;
a1|^n1 = a|^n1 by pr5 .= (power E).(a,n) by BINOM:def 2;
hence thesis;
end;
defpred P[Nat] means
for p being Element of the carrier of Polynom-Ring F
st deg p = $1 holds Ext_eval(p,a) in the carrier of RAdj(F,{a});
IA: for p being Element of the carrier of Polynom-Ring F
holds Ext_eval(Leading-Monomial p,a) in the carrier of RAdj(F,{a})
proof
let p being Element of the carrier of Polynom-Ring F;
reconsider x2 = (power E).(a,len p-'1) as Element of RAdj(F,{a}) by I1;
In(p.(len p-'1),E) = p.(len p-'1) by Z,SUBSET_1:def 8; then
reconsider x1 = In(p.(len p-'1),E) as Element of RAdj(F,{a}) by Y;
the carrier of RAdj(F,{a}) = carrierRA({a}) by dRA; then
L: [x1,x2] in [:carrierRA({a}),carrierRA({a}):] by ZFMISC_1:def 2;
Ext_eval(Leading-Monomial(p),a)
= In(p.(len p-'1),E) * (power E).(a,len p-'1) by X,ALGNUM_1:17
.= ((the multF of E)||carrierRA({a})).(x1,x2) by FUNCT_1:49,L
.= x1 * x2 by dRA;
hence thesis;
end;
IS: now let k be Nat;
assume IV: for n being Nat st n < k holds P[n];
now let p be Element of the carrier of Polynom-Ring F;
assume K0: deg p = k;
per cases;
suppose p = 0_.(F);
then Ext_eval(p,a) = 0.E by ALGNUM_1:13
.= 0.(RAdj(F,{a})) by dRA;
hence Ext_eval(p,a) in the carrier of RAdj(F,{a});
end;
suppose p <> 0_.(F);
then consider q being Polynomial of F such that
K1: len q < len p & p = q + Leading-Monomial(p) &
for n be Element of NAT st n < len p-1 holds q.n = p.n
by POLYNOM4:16,POLYNOM4:5;
reconsider q as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
per cases;
suppose q = 0_.(F);
hence Ext_eval(p,a) in the carrier of RAdj(F,{a}) by K1,IA;
end;
suppose q <> 0_.(F);
then reconsider degq = deg q as Nat by FIELD_1:1;
deg p = len p - 1 by HURWITZ:def 2; then
H: len q < k + 1 by K0,K1;
deg q = len q - 1 by HURWITZ:def 2; then
len q = deg q + 1; then
degq < k by XREAL_1:6,H;
then reconsider x1 = Ext_eval(q,a) as Element of RAdj(F,{a}) by IV;
reconsider x2 = Ext_eval(Leading-Monomial p,a) as
Element of RAdj(F,{a}) by IA;
the carrier of RAdj(F,{a}) = carrierRA({a}) by dRA; then
L: [x1,x2] in [:carrierRA({a}),carrierRA({a}):] by ZFMISC_1:def 2;
Ext_eval(p,a)
= Ext_eval(q,a) + Ext_eval(Leading-Monomial p,a) by K1,ALGNUM_1:15,X
.= ((the addF of E)||carrierRA({a})).(x1,x2) by FUNCT_1:49,L
.= x1 + x2 by dRA;
hence Ext_eval(p,a) in the carrier of RAdj(F,{a});
end;
end;
end;
hence P[k];
end;
I: for k being Nat holds P[k] from NAT_1:sch 4(IS);
now let x be object;
assume x in rng g; then
consider p being object such that A1: p in dom g & x = g.p
by FUNCT_1:def 3;
reconsider p as Element of the carrier of Polynom-Ring F by A1;
per cases;
suppose p = 0_.(F);
then x = Ext_eval(0_.(F),a) by A1,ALGNUM_1:def 11
.= 0.E by ALGNUM_1:13
.= 0.(RAdj(F,{a})) by dRA;
hence x in the carrier of RAdj(F,{a});
end;
suppose p <> 0_.(F);
then reconsider degp = deg p as Nat by FIELD_1:1;
P[degp] by I; then
Ext_eval(p,a) in the carrier of RAdj(F,{a});
hence x in the carrier of RAdj(F,{a}) by A1,ALGNUM_1:def 11;
end;
end;
hence thesis;
end;
lemphi3:
for F being Field,
E being (Polynom-Ring F)-homomorphic FieldExtension of F
for a being Element of E
holds F is Subring of Image hom_Ext_eval(a,F)
proof
let F be Field, E be (Polynom-Ring F)-homomorphic FieldExtension of F;
let a be Element of E;
set R = Image(hom_Ext_eval(a,F)), f = hom_Ext_eval(a,F);
X: F is Subring of E by FIELD_4:def 1; then
Y: the carrier of F c= the carrier of E by C0SP1:def 3;
Z: now let x be object;
assume x in the carrier of F;
then reconsider b = x as Element of F;
reconsider c = b as Element of E by Y;
reconsider p = b|F as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
reconsider q = c|E as Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
Ext_eval(p,a) = eval(q,a) by constpol,FIELD_4:26 .= b by RING_5:8;
then b in the set of all Ext_eval(p,a) where p is Polynomial of F;
hence x in rng hom_Ext_eval(a,F) by lemphi1;
end; then
ZZ: the carrier of F c= rng f;
now let x be object;
assume x in the carrier of F;
then x in rng hom_Ext_eval(a,F) by Z;
hence x in the carrier of R by RING_2:def 6;
end;
then A: the carrier of F c= the carrier of R;
set adF = the addF of F, adR = the addF of R;
H1c: dom(the addF of E) = [:the carrier of E, the carrier of E:]
by FUNCT_2:def 1;
adR = (the addF of E)||(rng f) by RING_2:def 6
.= (the addF of E)|[:rng f,rng f:]; then
H1b: dom adR = [:the carrier of E, the carrier of E:] /\ [:rng f,rng f:]
by H1c,RELAT_1:61;
H1: dom(adR||the carrier of F)
= dom(adR) /\ [:the carrier of F, the carrier of F:] by RELAT_1:61
.= [:the carrier of E, the carrier of E:] /\
([:rng f,rng f:] /\ [:the carrier of F, the carrier of F:])
by H1b,XBOOLE_1:16
.= [:the carrier of E, the carrier of E:] /\
[:the carrier of F, the carrier of F:] by ZZ,ZFMISC_1:96,XBOOLE_1:28
.= [:the carrier of F, the carrier of F:] by Y,ZFMISC_1:96,XBOOLE_1:28
.= dom adF by FUNCT_2:def 1;
now let o be object;
assume AS: o in dom adF;
then consider a,b being object such that
B1: a in the carrier of F &
b in the carrier of F & o = [a,b] by ZFMISC_1:def 2;
reconsider a,b as Element of F by B1;
a in rng f & b in rng f by Z; then
B3: o in [:rng f, rng f:] by B1,ZFMISC_1:def 2;
B5: the addF of F = (the addF of E)||(the carrier of F) by C0SP1:def 3, X;
thus adF.o = (the addF of E).o by AS,B5,FUNCT_1:49
.= ((the addF of E)||(rng f)).o by B3,FUNCT_1:49
.= adR.o by RING_2:def 6
.= (adR|[:the carrier of F, the carrier of F:]).o
by AS,H1,FUNCT_1:47;
end;
then B: the addF of F = (the addF of R)||the carrier of F by H1;
set muF = the multF of F, muR = the multF of R;
H1c: dom(the multF of E) = [:the carrier of E, the carrier of E:]
by FUNCT_2:def 1;
muR = (the multF of E)||(rng f) by RING_2:def 6
.= (the multF of E)|[:rng f,rng f:]; then
H1b: dom muR = [:the carrier of E, the carrier of E:] /\ [:rng f,rng f:]
by H1c,RELAT_1:61;
H1: dom(muR||the carrier of F)
= dom(muR) /\ [:the carrier of F, the carrier of F:] by RELAT_1:61
.= [:the carrier of E, the carrier of E:] /\
([:rng f,rng f:] /\ [:the carrier of F, the carrier of F:])
by H1b,XBOOLE_1:16
.= [:the carrier of E, the carrier of E:] /\
[:the carrier of F, the carrier of F:] by ZZ,ZFMISC_1:96,XBOOLE_1:28
.= [:the carrier of F, the carrier of F:] by Y,ZFMISC_1:96,XBOOLE_1:28
.= dom muF by FUNCT_2:def 1;
now let o be object;
assume AS: o in dom muF;
then consider a,b being object such that
B1: a in the carrier of F &
b in the carrier of F & o = [a,b] by ZFMISC_1:def 2;
reconsider a,b as Element of F by B1;
a in rng f & b in rng f by Z; then
B3: o in [:rng f, rng f:] by B1,ZFMISC_1:def 2;
B5: the multF of F=(the multF of E)||(the carrier of F) by C0SP1:def 3,X;
thus muF.o = (the multF of E).o by AS,B5,FUNCT_1:49
.= ((the multF of E)||(rng f)).o by B3,FUNCT_1:49
.= muR.o by RING_2:def 6
.= (muR|[:the carrier of F, the carrier of F:]).o
by AS,H1,FUNCT_1:47;
end;
then C: the multF of F = (the multF of R)||the carrier of F by H1;
D: 0.F = 0.E by X,C0SP1:def 3 .= 0.R by RING_2:def 6;
1.F = 1.E by X,C0SP1:def 3 .= 1.R by RING_2:def 6;
hence thesis by A,B,C,D,C0SP1:def 3;
end;
theorem lemphi4:
for F being Field,
E being (Polynom-Ring F)-homomorphic FieldExtension of F
for a being Element of E holds RAdj(F,{a}) = Image hom_Ext_eval(a,F)
proof
let F be Field, E be (Polynom-Ring F)-homomorphic FieldExtension of F;
let a be Element of E;
A0: F is Subring of E by FIELD_4:def 1;
set R = Image(hom_Ext_eval(a,F)), S = RAdj(F,{a}), f = hom_Ext_eval(a,F);
now let o be object;
assume o in {a}; then
A1: o = a by TARSKI:def 1;
reconsider p = <%0.F,1.F%> as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E
by FIELD_4:10;
then reconsider q = p as Element of the carrier of Polynom-Ring E;
A2: dom f = the carrier of Polynom-Ring F by FUNCT_2:def 1;
0.E = 0.F & 1.E = 1.F by A0,C0SP1:def 3;
then A3: q = <%0.E,1.E%> by A0,pr20;
f.p = Ext_eval(p,a) by ALGNUM_1:def 11
.= eval(q,a) by FIELD_4:26
.= 0.E + 1.E * a by A3,POLYNOM5:44
.= a;
then a in rng f by A2,FUNCT_1:def 3;
hence o in the carrier of R by A1,RING_2:def 6;
end; then
A: {a} is Subset of the carrier of R by TARSKI:def 3;
F is Subring of R by lemphi3; then
S is Subring of R by A,RAsub2; then
the carrier of RAdj(F,{a}) c= the carrier of Image f by C0SP1:def 3; then
V: the carrier of RAdj(F,{a}) c= rng hom_Ext_eval(a,F) by RING_2:def 6;
rng hom_Ext_eval(a,F) c= the carrier of RAdj(F,{a}) by lemphi2;
then the carrier of RAdj(F,{a}) = rng f by V,TARSKI:2
.= the carrier of Image f by RING_2:def 6;
hence thesis by RE1;
end;
theorem lemphi5:
for F being Field,
E being (Polynom-Ring F)-homomorphic FieldExtension of F
for a being Element of E
holds the carrier of RAdj(F,{a})
= the set of all Ext_eval(p,a) where p is Polynomial of F
proof
let F be Field, E be (Polynom-Ring F)-homomorphic FieldExtension of F;
let a be Element of E;
thus the carrier of RAdj(F,{a})
= the carrier of Image hom_Ext_eval(a,F) by lemphi4
.= rng hom_Ext_eval(a,F) by RING_2:def 6
.= the set of all Ext_eval(p,a) where p is Polynomial of F by lemphi1;
end;
begin :: On Linear Combinations and Polynomials
lemlin:
for F being Field, E being F-finite FieldExtension of F
for A being finite Subset of VecSp(E,F) st card A > dim VecSp(E,F)
holds A is linearly-dependent
proof
let F be Field, E be F-finite FieldExtension of F;
let A be finite Subset of VecSp(E,F);
assume H: card A > dim VecSp(E,F);
Y: VecSp(E,F) is finite-dimensional by FIELD_4:def 8;
now assume A is linearly-independent;
then consider I being Basis of VecSp(E,F) such that
X: A c= I by VECTSP_7:19;
Z: card I = dim VecSp(E,F) by Y,VECTSP_9:def 1;
then reconsider I as finite set;
reconsider A as finite set;
thus contradiction by H,Z,X,CARD_1:11,FIELD_5:3;
end;
hence thesis;
end;
Lm12a:
for F be Ring, E be RingExtension of F
for a,b be Element of E
for s be Element of F
for v be Element of VecSp(E,F) st a = s & b = v holds a*b = s*v
proof
let F be Ring, E be RingExtension of F;
let a,b be Element of E;
let s be Element of F, v be Element of VecSp(E,F) such that
A1: a = s & b = v;
the carrier of VecSp(E,F) = the carrier of E by FIELD_4:def 6;
then A2: [s,v] in [:the carrier of F,the carrier of E:] by ZFMISC_1:def 2;
thus s * v
= ((the multF of E)|[:the carrier of F,the carrier of E:]).(s,v)
by FIELD_4:def 6
.= a*b by A1,A2,FUNCT_1:49;
end;
Lm12b:
for F be Ring, E be RingExtension of F
for a,b be Element of E
for x,y be Element of F st a = x & b = y holds a*b = x*y
proof
let F be Ring, E be RingExtension of F;
let a,b be Element of E;
let x,y be Element of F such that
A1: a = x & b = y;
A2: F is Subring of E by FIELD_4:def 1;
A3: [x,y] in [:the carrier of F,the carrier of F:] by ZFMISC_1:def 2;
thus x*y = ((the multF of E)||(the carrier of F)).(x,y)
by A2,C0SP1:def 3
.= a*b by A1,A3,FUNCT_1:49;
end;
theorem lcsub:
for F being Field
for V being VectSp of F, W being Subspace of V
for l1 being Linear_Combination of W
ex l2 being Linear_Combination of V
st Carrier l2 = Carrier l1 &
for v being Element of V st v in Carrier l2 holds l2.v = l1.v
proof
let F be Field; let V be VectSp of F, W be Subspace of V;
let l1 be Linear_Combination of W;
H: the carrier of W c= the carrier of V by VECTSP_4:def 2;
consider f being Function such that
L1: l1 = f & dom f = the carrier of W & rng f c= the carrier of F
by FUNCT_2:def 2;
reconsider f as Function of W,F by L1;
defpred P[Element of V,Element of F] means
($1 in Carrier l1 & $2 = f.($1)) or (not $1 in Carrier l1 & $2 = 0.F);
A: for x being Element of the carrier of V
ex y being Element of the carrier of F st P[x,y]
proof
let v be Element of the carrier of V;
per cases;
suppose A1: v in Carrier l1;
then reconsider v1 = v as Element of W;
reconsider y = f.v1 as Element of F;
take y;
thus thesis by A1;
end;
suppose A1: not v in Carrier l1;
take 0.F;
thus thesis by A1;
end;
end;
consider g being Function of V,F such that
B: for x being Element of V holds P[x,g.x] from FUNCT_2:sch 3(A);
dom g = the carrier of V & rng g c= the carrier of F by FUNCT_2:def 1; then
C: g is Element of Funcs(the carrier of V, the carrier of F) by FUNCT_2:def 2;
for o being object st o in Carrier l1 holds o in the carrier of V by H;
then reconsider C = Carrier l1 as finite Subset of V by TARSKI:def 3;
for v being Element of V st not v in C holds g.v = 0.F by B;
then reconsider l2 = g as Linear_Combination of V by C,VECTSP_6:def 1;
take l2;
G: now let o be object;
assume o in Carrier l2; then
consider v being Element of V such that
G1: o = v & l2.v <> 0.F by VECTSP_6:1;
thus o in Carrier l1 by B,G1;
end;
now let o be object;
assume G0: o in Carrier l1; then
consider v being Element of W such that
G1: o = v & l1.v <> 0.F by VECTSP_6:1;
reconsider v1 = v as Element of V by H;
v1 in Carrier l1 & g.v1 = f.v1 by B,G1,G0;
hence o in Carrier l2 by L1,G1,VECTSP_6:2;
end;
hence Carrier l2 = Carrier l1 by G,TARSKI:2;
hence thesis by B,L1;
end;
theorem lembasx2:
for F being Field,
E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for l being Linear_Combination of VecSp(E,F)
ex p being Polynomial of F
st deg p <= n &
for i being Element of NAT st i <= n holds p.i = l.(a|^i)
proof
let F be Field, E be FieldExtension of F; let a be Element of E;
let n be Element of NAT; let l be Linear_Combination of VecSp(E,F);
set V = VecSp(E,F);
defpred P[object,object] means
(ex i being Nat st i <= n & $1 = i & $2 = l.(a|^i)) or
(ex i being Nat st i > n & $1 = i & $2 = 0.F);
A: for x being Element of NAT
ex y being Element of the carrier of F st P[x,y]
proof
let x be Element of NAT;
reconsider v = a|^x as Element of V by FIELD_4:def 6;
per cases;
suppose A1: ex i being Nat st i <= n & x = i;
reconsider y = l.v as Element of F;
take y;
thus thesis by A1;
end;
suppose A1: ex i being Nat st i > n & x = i;
take 0.F;
thus thesis by A1;
end;
end;
consider p being Function of NAT,the carrier of F such that
B: for x being Element of NAT holds P[x,p.x] from FUNCT_2:sch 3(A);
C1: for i being Nat holds i <= n implies p.i = l.(a|^i)
proof
let i be Nat;
assume C3: i <= n;
i is Element of NAT by ORDINAL1:def 12; then
P[i,p.i] by B;
hence l.(a|^i) = p.i by C3;
end;
C2: for i being Nat holds i >= n + 1 implies p.i = 0.F
proof
let i be Nat;
assume C3: i >= n + 1;
i is Element of NAT by ORDINAL1:def 12; then
P[i,p.i] by B;
hence 0.F = p.i by C3,NAT_1:13;
end; then
reconsider p as Polynomial of F by ALGSEQ_1:def 1;
take p;
n + 1 is_at_least_length_of p by C2,ALGSEQ_1:def 2; then
len p <= n + 1 by ALGSEQ_1:def 3; then
len p - 1 <= n + 1 - 1 by XREAL_1:9;
hence deg p <= n by HURWITZ:def 2;
thus thesis by C1;
end;
theorem lembasx1a:
for F being Field,
E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for l being Linear_Combination of VecSp(E,F),
p being non zero Polynomial of F
st l.(a|^(deg p)) = LC p & Carrier l = {a|^(deg p)}
holds Sum l = Ext_eval(LM p,a)
proof
let F be Field, E be FieldExtension of F;
let a be Element of E; let n be Element of NAT;
let l be Linear_Combination of VecSp(E,F); let p be non zero Polynomial of F;
F is Subring of E by FIELD_4:def 1; then
H2: the carrier of F c= the carrier of E by C0SP1:def 3;
H3: {a} is Subset of FAdj(F,{a}) by FAt;
a in {a} by TARSKI:def 1; then
reconsider a1 = a as Element of FAdj(F,{a}) by H3;
assume A: l.(a|^(deg p)) = LC p & Carrier l = {a|^(deg p)};
reconsider LCp = LC p as Element of E by H2;
reconsider adegp = a|^(deg p) as Element of E;
reconsider v = a|^(deg p) as Element of VecSp(E,F) by FIELD_4:def 6;
thus Sum l = l.v * v by A,VECTSP_6:20
.= LCp * adegp by A,Lm12a
.= Ext_eval(LM p,a) by exevalLM;
end;
theorem lembasx1:
for F being Field,
E being FieldExtension of F
for a being Element of E
for n being Element of NAT
for M being Subset of VecSp(E,F)
st M = {a|^i where i is Element of NAT : i <= n} &
for i,j being Element of NAT st i < j & j <= n holds a|^i <> a|^j
for l being Linear_Combination of M
for p being Polynomial of F
st deg p <= n &
for i being Element of NAT st i <= n holds p.i = l.(a|^i)
holds Ext_eval(p,a) = Sum l
proof
let F be Field, E be FieldExtension of F; let a be Element of E;
let n be Element of NAT; let M be Subset of VecSp(E,F);
assume AS1: M = {a|^i where i is Element of NAT : i <= n} &
for i,j being Element of NAT st i < j & j <= n holds a|^i <> a|^j;
let l be Linear_Combination of M; let p be Polynomial of F;
assume AS2: deg p <= n &
for i being Element of NAT st i <= n holds p.i = l.(a|^i);
set V = VecSp(E,F);
defpred P[Nat] means
for l being Linear_Combination of M st card Carrier(l) = $1
for p being Polynomial of F
st deg p <= n &
for i being Element of NAT st i <=n holds p.i = l.(a|^i)
holds Sum l = Ext_eval(p,a);
IA: P[0]
proof
let l be Linear_Combination of M;
assume card Carrier(l) = 0; then
Carrier l = {}; then
A2: l = ZeroLC(V) by VECTSP_6:def 3;
let p be Polynomial of F; assume
A4: deg p <= n &
for i being Element of NAT st i <= n holds p.i = l.(a|^i);
now let i be Element of NAT;
per cases;
suppose i > n;
then A5: i > deg p by A4,XXREAL_0:2;
deg p = len p - 1 by HURWITZ:def 2;
then i + 1 > len p - 1 + 1 by A5,XREAL_1:6;
hence p.i = (0_.(F)).i by NAT_1:13,ALGSEQ_1:8;
end;
suppose A5: i <= n; then
a|^i in M by AS1; then
reconsider v = a|^i as Element of V;
thus p.i = l.v by A4,A5 .= (0_.(F)).i by A2,VECTSP_6:3;
end;
end;
then p = 0_.(F);
hence Ext_eval(p,a) = 0.E by ALGNUM_1:13
.= 0.V by FIELD_4:def 6
.= Sum l by A2,VECTSP_6:15;
end;
IS: now let k be Nat;
assume B0: P[k];
now let l be Linear_Combination of M;
assume B1: card Carrier(l) = k+1;
let pp be Polynomial of F;
assume B2: deg pp <= n &
for i being Element of NAT st i <= n holds pp.i=l.(a|^i);
now assume C0: pp = 0_.(F);
now let o be object;
assume C1: o in Carrier l;
Carrier l c= M by VECTSP_6:def 4;
then o in M by C1;
then consider i being Element of NAT such that
C2: o = a|^i & i <= n by AS1;
l.(a|^i) = pp.i by B2,C2 .= 0.F by C0;
hence contradiction by C1,C2,VECTSP_6:2;
end;
then Carrier l = {} by XBOOLE_0:def 1;
hence contradiction by B1;
end;
then reconsider p = pp as non zero Polynomial of F by UPROOTS:def 5;
defpred Q[object,object] means
($1 = a|^(deg p) & $2 = LC p) or ($1 <> a|^(deg p) & $2 = 0.F);
A: for x being object st x in the carrier of V
ex y being object st y in the carrier of F & Q[x,y]
proof
let x be object;
assume x in the carrier of V;
per cases;
suppose x = a|^(deg p);
hence ex y being object st y in the carrier of F & Q[x,y];
end;
suppose x <> a|^(deg p);
hence ex y being object st y in the carrier of F & Q[x,y];
end;
end;
consider lp being Function of the carrier of V,the carrier of F such that
L: for x being object st x in the carrier of V holds Q[x,lp.x]
from FUNCT_2:sch 1(A);
reconsider lp as Element of Funcs(the carrier of V, the carrier of F)
by FUNCT_2:8;
U: M is finite
proof
deffunc F(Nat) = a|^($1);
defpred P[Nat] means $1 <= n;
D: {F(i) where i is Nat: i<=n & P[i]} is finite from FINSEQ_1:sch 6;
E: now let o be object;
assume o in {F(i) where i is Nat: i<=n & P[i]};
then consider i being Nat such that
E1: o = a|^i & i <= n & i <= n;
i is Element of NAT by ORDINAL1:def 12;
hence o in M by E1,AS1;
end;
now let o be object;
assume o in M; then
consider i being Element of NAT such that
E1: o = a|^i & i <= n by AS1;
thus o in {F(i) where i is Nat: i<=n & P[i]} by E1;
end;
hence thesis by D,E,TARSKI:2;
end;
for v being Element of V st not v in M holds lp.v = 0.F
proof
let v being Element of V;
assume not v in M;
then v <> a|^(deg p) by B2,AS1;
hence lp.v = 0.F by L;
end;
then reconsider lp as Linear_Combination of V by U,VECTSP_6:def 1;
now let o be object;
assume o in Carrier lp;
then consider v being Element of V such that
A1: o = v & lp.v <> 0.F by VECTSP_6:1;
v = a|^(deg p) & lp.v = LC p by L,A1;
hence o in M by A1,B2,AS1;
end;
then Carrier(lp) c= M;
then reconsider lp as Linear_Combination of M by VECTSP_6:def 4;
X1: {a} is Subset of FAdj(F,{a}) by FAt;
a in {a} by TARSKI:def 1; then
reconsider a1 = a as Element of the carrier of FAdj(F,{a}) by X1;
X: a|^(deg p) is Element of V by FIELD_4:def 6;
C0: Carrier lp = {a|^(deg p)}
proof
C2: now let o be object;
assume o in {a|^(deg p)}; then
C3: o = a|^(deg p) by TARSKI:def 1; then
lp.o <> 0.F by X,L;
hence o in Carrier lp by X,C3,VECTSP_6:2;
end;
now let o be object;
assume C3: o in Carrier lp;
Carrier lp = {v where v is Element of V: lp.v <> 0.F}
by VECTSP_6:def 2;
then consider v being Element of V such that
C4: o = v & lp.v <> 0.F by C3;
o = a|^(deg p) by C4,L;
hence o in {a|^(deg p)} by TARSKI:def 1;
end;
hence thesis by C2,TARSKI:2;
end;
lp.(a|^(deg p)) = LC p by X,L; then
C: Ext_eval(LM p,a) = Sum lp by C0,lembasx1a;
set q = p - (LM p);
reconsider lk = l - lp as Linear_Combination of M by VECTSP_6:42;
C2: l = lk + lp
proof
thus lk + lp = (l + -lp) + lp by VECTSP_6:def 11
.= l + (-lp + lp) by VECTSP_6:26
.= l + (lp + -lp) by VECTSP_6:25
.= l + (lp - lp) by VECTSP_6:def 11
.= l + ZeroLC(V) by VECTSP_6:43
.= l by VECTSP_6:27;
end;
C3: Carrier lk = Carrier(l) \ Carrier(lp)
proof
C4: now let o be object;
assume o in Carrier lk;
then consider v being Element of V such that
C5: o = v & lk.v <> 0.F by VECTSP_6:1;
C6: now assume C7: v = a|^(deg p); then
C9: l.v = p.(deg p) by B2 .= LC p by thLC;
lk.v = l.v - lp.v by VECTSP_6:40
.= LC p - LC p by L,C7,C9;
hence contradiction by C5,RLVECT_1:15;
end; then
C7: not v in Carrier(lp) by C0,TARSKI:def 1;
lk.v = l.v - lp.v by VECTSP_6:40
.= l.v - 0.F by C6,L; then
v in Carrier l by C5,VECTSP_6:2;
hence o in Carrier(l) \ Carrier(lp) by C7,C5,XBOOLE_0:def 5;
end;
now let o be object;
assume o in Carrier(l) \ Carrier(lp); then
C5: o in Carrier(l) & not o in Carrier(lp) by XBOOLE_0:def 5; then
consider v being Element of V such that
C6: o = v & l.v <> 0.F by VECTSP_6:1;
C7: o <> a|^(deg p) by C0,C5,TARSKI:def 1;
lk.v = l.v - lp.v by VECTSP_6:40
.= l.v - 0.F by C6,C7,L;
hence o in Carrier lk by C6,VECTSP_6:1;
end;
hence thesis by C4,TARSKI:2;
end;
now let o be object;
assume C5: o in Carrier lp; then
C4: o = a|^(deg p) by C0,TARSKI:def 1;
reconsider v = o as Element of V by C5;
lp.v = LC p by L,C4 .= pp.(deg p) by thLC .= l.v by C4,B2; then
l.v <> 0.F by C5,VECTSP_6:2;
hence o in Carrier l by VECTSP_6:2;
end; then
Carrier lp c= Carrier l; then
A: card(Carrier(l) \ Carrier(lp))
= card(Carrier l) - card(Carrier lp) by CARD_2:44
.= (k + 1) - 1 by B1,C0,CARD_2:42;
B: deg q < n by thdLM,B2,XXREAL_0:2;
for i being Element of NAT st i <= n holds q.i = lk.(a|^i)
proof
let i be Element of NAT;
assume B1: i <= n;
reconsider v = a|^i as Element of V by FIELD_4:def 6;
per cases;
suppose B3: i = deg p;
hence q.i = p.(deg p) - (LM p).(deg p) by POLYNOM3:27
.= p.(deg p) - (LM p).(deg (LM p)) by thdegLM
.= l.v - (LM p).(deg (LM p)) by B3,B2
.= l.v - LC(LM p) by thLC
.= l.v - LC p by thdegLC
.= l.v - lp.v by B3,L
.= lk.(a|^i) by VECTSP_6:40;
end;
suppose D2: i <> deg p;
D3: a|^i <> a|^(deg p)
proof
per cases by D2,XXREAL_0:1;
suppose i < deg p;
hence thesis by B2,AS1;
end;
suppose i > deg p;
hence thesis by B1,AS1;
end;
end;
p <> 0_.(F);
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 D5: len p -' 1 = len p - 1 by XREAL_0:def 2;
D4: i <> len p -' 1 by D5,D2,HURWITZ:def 2;
thus q.i = p.i - (LM p).i by POLYNOM3:27
.= p.i - 0.F by D4,POLYNOM4:def 1
.= l.v - 0.F by B2,B1
.= l.v - lp.v by D3,L
.= lk.(a|^i) by VECTSP_6:40;
end;
end;
then D: Ext_eval(q,a) = Sum lk by A,C3,B,B0;
thus Sum l
= Sum(lk) + Sum(lp) by C2,VECTSP_6:44
.= (the addF of E).(Sum(lk),Sum(lp)) by FIELD_4:def 6
.= (Ext_eval(p,a) - Ext_eval(LM p,a)) + Ext_eval(LM p,a)
by C,D,exevalminus2
.= Ext_eval(p,a) + (-Ext_eval(LM p,a) + Ext_eval(LM p,a))
by RLVECT_1:def 3
.= Ext_eval(p,a) + 0.E by RLVECT_1:5
.= Ext_eval(pp,a);
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that H: card Carrier(l) = n;
thus thesis by AS2,I,H;
end;
begin :: Minimal Polynomials
notation
let F be Field,
E be FieldExtension of F;
let a be F-algebraic Element of E;
synonym MinPoly(a,F) for minimal_polynom(a,F);
end;
lemminirred:
for F being Field,
E being FieldExtension of F,
a being F-algebraic Element of E holds MinPoly(a,F) is irreducible
proof
let F be Field, E be FieldExtension of F, a be F-algebraic Element of E;
set m = MinPoly(a,F);
X: F is Subring of E by FIELD_4:def 1;
a is_integral_over F by alg1; then
Z: m <> 0_.F & {m}-Ideal = Ann_Poly(a,F) & m = NormPolynomial(m)
by X,ALGNUM_1:def 9; then
m in {p where p is Polynomial of F: Ext_eval(p,a) = 0.E} by IDEAL_1:66;
then consider m1 being Polynomial of F such that
Z1: m1 = m & Ext_eval(m1,a) = 0.E;
reconsider m2 = m as Element of Polynom-Ring F;
reconsider m1 as non zero Element of the carrier of Polynom-Ring F
by Z1,Z,UPROOTS:def 5;
A2: m <> 0.(Polynom-Ring F) by Z,POLYNOM3:def 10;
A3: now assume m2 is Unit of Polynom-Ring F;
then A4: {m}-Ideal = [#](Polynom-Ring F) by RING_2:20;
ker(hom_Ext_eval(a,F)) is proper;
hence contradiction by A4,Z,alg0;
end;
now let x be Element of Polynom-Ring F;
assume B: x divides m;
consider y being Element of Polynom-Ring F such that
A4: x * y = m2 by B;
reconsider x1 = x, y1 = y as Polynomial of F by POLYNOM3:def 10;
m1 = x1 *' y1 by Z1,A4,POLYNOM3:def 10; then
A5: Ext_eval(m1,a) = Ext_eval(x1,a) * Ext_eval(y1,a) by ALGNUM_1:20,X;
per cases by A5,Z1,VECTSP_2:def 1;
suppose Ext_eval(x1,a) = 0.E;
then x1 in {m}-Ideal by Z;
then x1 in the set of all m*r where r is Element of Polynom-Ring F
by IDEAL_1:64;
then consider r being Element of Polynom-Ring F such that
A6: x = m2 * r;
m2 divides x by A6;
hence (x is Unit of (Polynom-Ring F) or x is_associated_to m) by B;
end;
suppose Ext_eval(y1,a) = 0.E;
then y1 in {m}-Ideal by Z;
then y1 in the set of all m*r where r is Element of Polynom-Ring F
by IDEAL_1:64;
then consider r being Element of Polynom-Ring F such that
A6: y1 = m * r;
reconsider r1 = r as Polynomial of F by POLYNOM3:def 10;
A8: x * r = x1 *' r1 by POLYNOM3:def 10;
1.(Polynom-Ring F) * m = x * (r * m) by A6,A4,GROUP_1:def 12
.= (x * r) * m by GROUP_1:def 3;
then (1_.(F)) *' m1 = (x1 *' r1) *' m1 by Z1,A8,POLYNOM3:def 10;
then 1_.(F) = x1 *' r1 by RATFUNC1:7
.= x * r by POLYNOM3:def 10;
then 1.(Polynom-Ring F) = x* r by POLYNOM3:def 10;
then x divides 1.(Polynom-Ring F);
hence (x is Unit of (Polynom-Ring F) or x is_associated_to m)
by GCD_1:def 20;
end;
end;
hence thesis by A2,A3,RING_2:def 9;
end;
registration
let F be Field,
E be FieldExtension of F;
let a be F-algebraic Element of E;
cluster MinPoly(a,F) -> monic irreducible;
coherence
proof
X: F is Subring of E by FIELD_4:def 1;
a is_integral_over F by alg1; then
Z: MinPoly(a,F) <> 0_.F & MinPoly(a,F) = NormPolynomial MinPoly(a,F)
by X,ALGNUM_1:def 9;
then MinPoly(a,F) is non zero by UPROOTS:def 5;
hence MinPoly(a,F) is monic by Z;
thus thesis by lemminirred;
end;
end;
theorem mpol1:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E,
p being Element of the carrier of Polynom-Ring F
holds p = MinPoly(a,F) iff
(p is monic & p is irreducible & ker(hom_Ext_eval(a,F)) = {p}-Ideal)
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E,
p be Element of the carrier of Polynom-Ring F;
set m = MinPoly(a,F);
X: F is Subring of E by FIELD_4:def 1;
Y: a is_integral_over F by alg1; then
Z: m <> 0_.F & {m}-Ideal = Ann_Poly(a,F) & m = NormPolynomial(m)
by X,ALGNUM_1:def 9;
now assume A0: p is monic & p is irreducible &
ker(hom_Ext_eval(a,F)) = {p}-Ideal;
then A1: p <> 0_.F;
A2: {p}-Ideal = Ann_Poly(a,F) by A0,alg0;
p = NormPolynomial(p) by A0,RING_4:24;
hence p = m by X,Y,A1,A2,ALGNUM_1:def 9;
end;
hence thesis by Z,alg0;
end;
theorem mpol2:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E,
p being Element of the carrier of Polynom-Ring F
holds p = MinPoly(a,F) iff
(p is monic & Ext_eval(p,a) = 0.E &
for q being non zero Polynomial of F
st Ext_eval(q,a) = 0.E holds deg p <= deg q)
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E,
p be Element of the carrier of Polynom-Ring F;
set m = MinPoly(a,F), g = hom_Ext_eval(a,F);
X: F is Subring of E by FIELD_4:def 1;
a is_integral_over F by alg1; then
Z: m <> 0_.F & {m}-Ideal = Ann_Poly(a,F) & m = NormPolynomial(m)
by X,ALGNUM_1:def 9; then
m in {p where p is Polynomial of F: Ext_eval(p,a) = 0.E} by IDEAL_1:66;
then consider m1 being Polynomial of F such that
Z1: m1 = m & Ext_eval(m1,a) = 0.E;
A: now assume A1: p = MinPoly(a,F);
hence p is monic;
thus Ext_eval(p,a) = 0.E by Z1,A1;
thus for q being non zero Polynomial of F
st Ext_eval(q,a) = 0.E holds deg p <= deg q
proof
let q be non zero Polynomial of F;
assume Ext_eval(q,a) = 0.E;
then q in {m}-Ideal by Z;
then q in the set of all m*r where r is Element of Polynom-Ring F
by IDEAL_1:64; then
consider r being Element of the carrier of Polynom-Ring F such that
A2: q = m * r;
reconsider r1 = r as Polynomial of F;
A3: m1 *' r1 = m * r by Z1,POLYNOM3:def 10;
A5: r1 <> 0_.(F) by A2,A3;
then A6: deg q = deg(p) + deg(r1) by A1,A3,A2,Z1,HURWITZ:23;
deg r1 is Nat by A5,FIELD_1:1;
hence deg p <= deg q by A6,INT_1:6;
end;
end;
now assume A: p is monic & Ext_eval(p,a) = 0.E &
for q being non zero Polynomial of F
st Ext_eval(q,a) = 0.E holds deg p <= deg q;
then A1: p <> 0_.(F);
reconsider p1 = p as Element of Polynom-Ring F;
A2: now assume p1 is Unit of Polynom-Ring F;
then p1 divides 1.(Polynom-Ring F) by GCD_1:def 20;
then consider u1 being Element of Polynom-Ring F such that
A3: p1 * u1 = 1.(Polynom-Ring F);
reconsider u = u1 as Element of the carrier of Polynom-Ring F;
p *' u = 1.(Polynom-Ring F) by A3,POLYNOM3:def 10
.= 1_.(F) by POLYNOM3:def 10;
then Ext_eval(1_.(F),a)
= Ext_eval(p,a) * Ext_eval(u,a) by X,ALGNUM_1:20
.= 0.E by A;
then Ext_eval(1_.(F),a) <> 1.E;
hence contradiction by X,ALGNUM_1:14;
end;
B: now assume p is reducible;
then consider q being Element of the carrier of Polynom-Ring F such that
A4: q divides p & 1 <= deg q & deg q < deg p by A1,A2,RING_4:41;
reconsider q1 = q as Polynomial of F;
consider u1 being Polynomial of F such that
A3: q1 *' u1 = p1 by A4,RING_4:1;
A6: q1 <> 0_.(F) by A3,A;
A7: u1 <> 0_.(F) by A3,A;
then Y: deg q1 is Nat & deg u1 is Element of NAT by A6,FIELD_1:1;
A11: deg p = deg(q1) + deg(u1) by A3,A7,A6,HURWITZ:23; then
A10: deg u1 <= deg p by Y,INT_1:6;
A19: 0.E = Ext_eval(q1,a) * Ext_eval(u1,a) by X,A3,A,ALGNUM_1:20;
per cases by A19,VECTSP_2:def 1;
suppose A9: Ext_eval(q1,a) = 0.E;
q1 is non zero by A3,A;
hence contradiction by A4,A9,A;
end;
suppose A9: Ext_eval(u1,a) = 0.E;
u1 is non zero by A3,A;
then deg p <= deg u1 by A9,A;
then deg u1 = deg p by A10,XXREAL_0:1;
hence contradiction by A4,A11;
end;
end;
ker g is principal by IDEAL_1:def 28; then
consider u being Element of Polynom-Ring F such that
C1: ker g = {u}-Ideal;
hom_Ext_eval(a,F).p = 0.E by A,ALGNUM_1:def 11; then
p in {v where v is Element of Polynom-Ring F : g.v = 0.E}; then
C2: p in {u}-Ideal by C1,VECTSP10:def 9;
p in the set of all u*r where r is Element of Polynom-Ring F
by C2,IDEAL_1:64; then
consider v being Element of Polynom-Ring F such that
C3: p = u * v;
reconsider u1 = u, v1 = v, p1 = p as Polynomial of F by POLYNOM3:def 10;
C3a: p = u1 *' v1 by C3,POLYNOM3:def 10; then
C3b: u1 <> 0_.(F) & v1 <> 0_.(F) by A;
C3c: u1 is non zero by C3a,A;
C4: deg p = deg u1 + deg v1 by C3a,C3b,HURWITZ:23;
u in ker g by C1,IDEAL_1:66; then
u in {v where v is Element of Polynom-Ring F : g.v = 0.E}
by VECTSP10:def 9; then
consider w be Element of Polynom-Ring F such that
C5: u = w & g.w = 0.E;
Ext_eval(u1,a) = 0.E by C5,ALGNUM_1:def 11; then
C10: deg p + deg v1 <= deg p by A,C3c,C4,XREAL_1:6;
reconsider degv = deg v1 as Element of NAT by C3b,FIELD_1:1;
(deg p + deg v1) - deg p <= deg p - deg p by C10,XREAL_1:9; then
consider b being Element of F such that
C6: v1 = b|F by RING_4:20,RING_4:def 4;
reconsider v2 = ((b")|F) as Element of Polynom-Ring F by POLYNOM3:def 10;
C7: b <> 0.F by A,C3a,C6;
(u1 *' v1) *' ((b")|F)
= u1 *' (v1 *' ((b")|F)) by POLYNOM3:33
.= u1 *' ((b"*b)|F) by C6,RING_4:18
.= u1 *' ((1.F)|F) by C7,VECTSP_1:def 10
.= u1 *' (1_.(F)) by RING_4:14; then
u1 = p1 *' ((b")|F) by C3,POLYNOM3:def 10 .= p * v2 by POLYNOM3:def 10; then
u in the set of all p*r where r is Element of Polynom-Ring F; then
u in {p}-Ideal by IDEAL_1:64; then
C: ker g c= {p}-Ideal by C1,IDEAL_1:67;
{p}-Ideal c= ker g by C1,C2,IDEAL_1:67;
hence p = MinPoly(a,F) by A,B,mpol1,C,TARSKI:2;
end;
hence thesis by A;
end;
theorem mpol3:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E,
p being Element of the carrier of Polynom-Ring F
holds p = MinPoly(a,F) iff
(p is monic & p is irreducible & Ext_eval(p,a) = 0.E)
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E,
p be Element of the carrier of Polynom-Ring F;
set m = MinPoly(a,F), g = hom_Ext_eval(a,F);
X: F is Subring of E by FIELD_4:def 1;
a is_integral_over F by alg1; then
m <> 0_.F & {m}-Ideal = Ann_Poly(a,F) & m = NormPolynomial(m)
by X,ALGNUM_1:def 9; then
m in {p where p is Polynomial of F: Ext_eval(p,a) = 0.E} by IDEAL_1:66;
then consider m1 being Polynomial of F such that
Z1: m1 = m & Ext_eval(m1,a) = 0.E;
now assume A: p is monic & p is irreducible & Ext_eval(p,a) = 0.E;
reconsider p1 = p as Element of Polynom-Ring F;
ker g is principal by IDEAL_1:def 28; then
consider u being Element of Polynom-Ring F such that
C1: ker g = {u}-Ideal;
hom_Ext_eval(a,F).p = 0.E by A,ALGNUM_1:def 11; then
p in {v where v is Element of Polynom-Ring F : g.v = 0.E}; then
C2: p in {u}-Ideal by C1,VECTSP10:def 9;
p in the set of all u*r where r is Element of Polynom-Ring F
by C2,IDEAL_1:64; then
consider v being Element of Polynom-Ring F such that
C3: p = u * v;
reconsider u1 = u as Polynomial of F by POLYNOM3:def 10;
A2: now assume u is Unit of Polynom-Ring F;
then {u}-Ideal = [#](Polynom-Ring F) by RING_2:20;
hence contradiction by C1;
end;
u divides p by C3; then
u is_associated_to p by A2,A,RING_2:def 9;
then {p}-Ideal = ker g by C1,RING_2:21;
hence p = MinPoly(a,F) by A,mpol1;
end;
hence thesis by Z1;
end;
theorem mpol4:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E,
p being Element of the carrier of Polynom-Ring F
holds Ext_eval(p,a) = 0.E iff MinPoly(a,F) divides p
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E,
p be Element of the carrier of Polynom-Ring F;
set ma = MinPoly(a,F), g = hom_Ext_eval(a,F);
X: F is Subring of E by FIELD_4:def 1;
reconsider p1 = p, ma1 = ma as Element of Polynom-Ring F;
A: now assume Ext_eval(p,a) = 0.E; then
g.p = 0.E by ALGNUM_1:def 11; then
p in {v where v is Element of Polynom-Ring F : g.v = 0.E}; then
p in ker g by VECTSP10:def 9; then
p in {ma}-Ideal by mpol1;
hence ma divides p by RING_4:def 3,RING_2:18;
end;
now assume ma divides p;
then consider u being Polynomial of F such that H: ma *' u = p by RING_4:1;
0.E = Ext_eval(ma,a) by mpol2;
hence 0.E = Ext_eval(ma,a) * Ext_eval(u,a)
.= Ext_eval(p,a) by X,H,ALGNUM_1:20;
end;
hence thesis by A;
end;
theorem
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
holds MinPoly(a,F) = rpoly(1,a) iff a in the carrier of F
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E;
set ma = MinPoly(a,F), g = hom_Ext_eval(a,F);
X: F is Subring of E by FIELD_4:def 1;
A: now assume a in the carrier of F;
then reconsider a1 = a as Element of F;
reconsider p = rpoly(1,a1) as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
A3: rpoly(1,a) = rpoly(1,a1) by FIELD_4:21;
deg p = 1 by HURWITZ:27; then
A2: p is irreducible by RING_4:42;
Ext_eval(p,a) = eval(p,a1) by FIELD427
.= a1 - a1 by HURWITZ:29
.= 0.F by RLVECT_1:15
.= 0.E by X,C0SP1:def 3;
hence ma = rpoly(1,a) by A3,A2,mpol3;
end;
now assume ma = rpoly(1,a);
then reconsider p = rpoly(1,a) as Element of the carrier of Polynom-Ring F;
-p.0 = -rpoly(1,a).0 by X,Th19
.= --(power(E).(a,1+0)) by HURWITZ:25
.= --(power(E).(a,0) * a) by GROUP_1:def 7
.= --(1_E * a) by GROUP_1:def 7
.= a;
hence a in the carrier of F;
end;
hence thesis by A;
end;
theorem mpol5:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for i,j being Element of NAT st i < j & j < deg MinPoly(a,F) holds a|^i <> a|^j
proof
let F be Field, E be FieldExtension of F; let a be F-algebraic Element of E;
let i,j be Element of NAT;
assume AS: i < j & j < deg MinPoly(a,F);
set ma = MinPoly(a,F);
reconsider n = deg ma as Element of NAT;
j >= 0 + 1 by AS,INT_1:7; then
X: ma is non linear by AS,FIELD_5:def 1;
j - i <= j by XREAL_1:43; then
j - i < n by AS,XXREAL_0:2; then
Y3: n - n < n - (j - i) by XREAL_1:15; then
0 + 1 <= i + n - j by INT_1:7; then
Y7: 0 + 1 - 1 <= i + n - j - 1 by XREAL_1:9;
i - j < 0 by AS,XREAL_1:49; then
Y4: n + (i - j) < n + 0 by XREAL_1:8;
reconsider k = i + n - j as Element of NAT by Y3,INT_1:3;
Y8: (n + (i - j)) - 1 < n - 1 by Y4,XREAL_1:9;
Y9: now assume i + n - j >= n; then
i + n - j - n >= n - n by XREAL_1:9; then
i - j + j >= 0 + j by XREAL_1:6;
hence contradiction by AS;
end;
reconsider h = n - j as Element of NAT by AS,INT_1:5;
set p = 0_.(F) +* (k,n) --> (1.F,-1.F);
now let x be object;
assume x in {k,n}; then
per cases by TARSKI:def 2;
suppose x = k; hence x in NAT; end;
suppose x = n; hence x in NAT; end;
end; then
A: {k,n} c= NAT;
B: dom((k,n) --> (1.F,-1.F)) = {k,n} & dom(0_.(F)) = NAT
by FUNCT_2:def 1; then
dom p = NAT \/ {k,n} by FUNCT_4:def 1 .= NAT by A,XBOOLE_1:12; then
dom p = NAT & rng p c= the carrier of F; then
reconsider p as sequence of F by FUNCT_2:2;
reconsider p as Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
k in dom((k,n) --> (1.F,-1.F)) by TARSKI:def 2,B; then
p.k = ((k,n) --> (1.F,-1.F)).k by FUNCT_4:13 .= 1.F by Y4,FUNCT_4:63; then
p <> 0_.(F); then
reconsider p as non zero Element of the carrier of Polynom-Ring F
by UPROOTS:def 5;
reconsider p1 = p, ma1 = ma as non zero Polynomial of F;
reconsider q1 = p1 + ma1 as Polynomial of F;
now assume K: p1 + ma1 = 0_.(F);
K1: -p1 = -p1 + 0_.(F)
.= (p1 - p1) + ma1 by K,POLYNOM3:26
.= 0_.(F) + ma1 by POLYNOM3:29;
set q = 0_.(F) +* (n+i-j-1,n-1) --> (-1.F,1.F);
now let x be object;
assume x in {n+i-j-1,n-1}; then
per cases by TARSKI:def 2;
suppose x = n+i-j-1; hence x in NAT by Y7,INT_1:3; end;
suppose x = n-1; hence x in NAT by AS,INT_1:3; end;
end; then
Z2: {n+i-j-1,n-1} c= NAT;
Z3: dom((n+i-j-1,n-1) --> (-1.F,1.F)) = {n+i-j-1,n-1} & dom(0_.(F)) = NAT
by FUNCT_2:def 1; then
dom q = NAT \/ {n+i-j-1,n-1} by FUNCT_4:def 1 .= NAT by Z2,XBOOLE_1:12; then
dom q = NAT & rng q c= the carrier of F; then
reconsider q as sequence of F by FUNCT_2:2;
reconsider q as Polynomial of F;
K: <%0.F,1.F%> *' q = -p1
proof
now let u be Element of NAT;
per cases;
suppose K2: u = 0; then
K3: not u in dom((k,n) --> (1.F,-1.F)) by AS,Y3;
K4: 0.F = (0_.(F)).u
.= p1.u by K3,FUNCT_4:11;
thus (<%0.F,1.F%> *' q).u
= -(p1.u) by K4,K2,thE2
.= (-p1).u by BHSP_1:44;
end;
suppose u <> 0;
then consider u1 being Nat such that K2: u = u1 + 1 by NAT_1:6;
K5: (<%0.F,1.F%> *' q).u = q.u1 by K2,thE1;
per cases;
suppose K6: u = k;
k in dom((k,n) --> (1.F,-1.F)) by TARSKI:def 2,B; then
K7: p.k = ((k,n) --> (1.F,-1.F)).k by FUNCT_4:13
.= 1.F by Y4,FUNCT_4:63;
K8: u1 in dom((n+i-j-1,n-1)-->(-1.F,1.F)) by K2,K6,Z3,TARSKI:def 2;
(n+i-j-1,n-1) --> (-1.F,1.F).u1 = -1.F by K2,K6,Y8,FUNCT_4:63;
hence (<%0.F,1.F%> *' q).u
= -1.F by K8,K5,FUNCT_4:13
.= (-p1).u by K6,K7,BHSP_1:44;
end;
suppose K6: u = n;
n in dom((k,n) --> (1.F,-1.F)) by TARSKI:def 2,B; then
K7: p.n = ((k,n) --> (1.F,-1.F)).n by FUNCT_4:13
.= -1.F by FUNCT_4:63;
K8: u1 in dom((n+i-j-1,n-1)-->(-1.F,1.F)) by K2,K6,Z3,TARSKI:def 2;
(n+i-j-1,n-1) --> (-1.F,1.F).u1 = 1.F by K2,K6,FUNCT_4:63;
hence (<%0.F,1.F%> *' q).u
= -(p1.u) by K6,K7,K8,K5,FUNCT_4:13
.= (-p1).u by BHSP_1:44;
end;
suppose K6: u <> k & u <> n;
then not u in dom((k,n) --> (1.F,-1.F)) by TARSKI:def 2; then
K7: p.u = (0_.(F)).u by FUNCT_4:11 .= 0.F;
u1 <> n+i-j-1 & u1 <> n - 1 by K2,K6; then
not u1 in dom((n+i-j-1,n-1) --> (-1.F,1.F)) by TARSKI:def 2;
then q.u1 = (0_.(F)).u1 by FUNCT_4:11
.= 0.F by ORDINAL1:def 12,FUNCOP_1:7;
hence (<%0.F,1.F%> *' q).u
= -(p1.u) by K7,K2,thE1
.= (-p1).u by BHSP_1:44;
end;
end;
end;
hence thesis;
end;
eval(<%0.F,1.F%>,0.F) = 0.F + 0.F by POLYNOM5:47;
then <%0.F,1.F%> is with_roots by POLYNOM5:def 7,POLYNOM5:def 8;
hence contradiction by K,K1,X;
end;
then reconsider q1 as non zero Polynomial of F by UPROOTS:def 5;
reconsider q = q1 as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
X: F is Subring of E by FIELD_4:def 1;
now assume A0: a|^i = a|^j;
A1: a|^k = a|^(i+h) .= a|^i * a|^h by BINOM:10
.= a|^(j+h) by A0,BINOM:10 .= a|^n;
A: deg q < deg ma
proof
D: now assume B0: deg q1 = deg ma1;
B2: deg ma1 + 1 = (len ma1 - 1) + 1 &
deg q1 + 1 = (len q1 - 1) + 1 by HURWITZ:def 2;
B3: len ma1 -' 1 = n by B2,XREAL_0:def 2;
n in dom((k,n) --> (1.F,-1.F)) by TARSKI:def 2,B; then
p.n = ((k,n) --> (1.F,-1.F)).n by FUNCT_4:13
.= -1.F by FUNCT_4:63;
then q1.n = -1.F + ma1.n by NORMSP_1:def 2
.= -1.F + LC ma1 by B3,RATFUNC1:def 6
.= -1.F + 1.F by RATFUNC1:def 7;
hence contradiction by B2,B0,ALGSEQ_1:10,RLVECT_1:5;
end;
now assume G: deg p1 > n;
B3: deg p1 + 1 = (len p1 - 1) + 1 by HURWITZ:def 2;
not deg p1 in dom((k,n) --> (1.F,-1.F)) by G,Y9,TARSKI:def 2; then
p1.(deg p1) = (0_.(F)).(deg p1) by FUNCT_4:11 .= 0.F;
hence contradiction by B3,ALGSEQ_1:10;
end;
then max(deg p1, deg ma1) = deg ma1 by XXREAL_0:def 10;
then deg q <= deg ma1 by HURWITZ:22;
hence thesis by D,XXREAL_0:1;
end;
reconsider pE = anpoly(1.E,k) + anpoly(-1.E,n) as
Element of the carrier of (Polynom-Ring E) by POLYNOM3:def 10;
p = anpoly(1.E,k) + anpoly(-1.E,n)
proof
set g = anpoly(1.E,k) + anpoly(-1.E,n);
now let u be Element of NAT;
per cases;
suppose H: u = k;
k in dom((k,n) --> (1.F,-1.F)) by TARSKI:def 2,B; then
H1: p.k = ((k,n) --> (1.F,-1.F)).k by FUNCT_4:13
.= 1.F by Y4,FUNCT_4:63;
thus g.u = anpoly(1.E,k).u + anpoly(-1.E,n).u by NORMSP_1:def 2
.= anpoly(1.E,k).u + 0.E by Y4,H,POLYDIFF:25
.= 1.E + 0.E by H,POLYDIFF:24
.= p.u by H1,H,X,C0SP1:def 3;
end;
suppose H: u = n;
n in dom((k,n) --> (1.F,-1.F)) by TARSKI:def 2,B; then
H1: p.n = ((k,n) --> (1.F,-1.F)).n by FUNCT_4:13
.= -1.F by FUNCT_4:63;
H2: 1.E = 1.F by X,C0SP1:def 3;
thus g.u = anpoly(1.E,k).u + anpoly(-1.E,n).u by NORMSP_1:def 2
.= 0.E + anpoly(-1.E,n).u by Y4,H,POLYDIFF:25
.= 0.E + -1.E by H,POLYDIFF:24
.= p.u by H2,H1,H,X,Th19;
end;
suppose H: u <> k & u <> n;
then not u in dom((k,n) --> (1.F,-1.F)) by TARSKI:def 2; then
H1: p.u = (0_.(F)).u by FUNCT_4:11 .= 0.F;
thus g.u = anpoly(1.E,k).u + anpoly(-1.E,n).u by NORMSP_1:def 2
.= 0.E + anpoly(-1.E,n).u by H,POLYDIFF:25
.= 0.E + 0.E by H,POLYDIFF:25
.= p.u by H1,X,C0SP1:def 3;
end;
end;
hence thesis;
end; then
B: Ext_eval(p,a)
= eval(pE,a) by FIELD_4:26
.= eval(anpoly(1.E,k),a) + eval(anpoly(-1.E,n),a) by POLYNOM4:19
.= 1.E * a|^k + eval(anpoly(-1.E,n),a) by Y3,FIELD_1:6
.= 1.E * a|^k + (-1.E) * a|^k by A1,AS,FIELD_1:6
.= (1.E + (-1.E)) * a|^k by VECTSP_1:def 3
.= 0.E * a|^k by RLVECT_1:5;
Ext_eval(q,a) = Ext_eval(p,a) + Ext_eval(ma,a) by X,ALGNUM_1:15
.= 0.E + 0.E by B,mpol3;
hence contradiction by mpol4,A,RING_5:13;
end;
hence thesis;
end;
theorem ch1:
for F being Field,
E being (Polynom-Ring F)-homomorphic FieldExtension of F,
a being Element of E holds a is F-algebraic iff FAdj(F,{a}) = RAdj(F,{a})
proof
let F be Field, E be (Polynom-Ring F)-homomorphic FieldExtension of F,
a be Element of E;
set f = hom_Ext_eval(a,F);
A: now assume a is F-algebraic;
then reconsider b = a as F-algebraic Element of E;
(Polynom-Ring F)/({MinPoly(b,F)}-Ideal) is Field;
then A1: (Polynom-Ring F)/(ker f) is Field by mpol1;
(Polynom-Ring F)/(ker f), Image f are_isomorphic by RING_2:15; then
reconsider K = Image f as ((Polynom-Ring F)/(ker f))-isomorphic Ring
by RING_3:def 4;
K is Field by A1; then
RAdj(F,{a}) is Field by lemphi4;
hence FAdj(F,{a}) = RAdj(F,{a}) by RF2;
end;
now assume FAdj(F,{a}) = RAdj(F,{a});
then B1: Image f is Field by lemphi4;
(Image f),(Polynom-Ring F)/(ker f) are_isomorphic by RING_2:15; then
reconsider K = (Polynom-Ring F)/(ker f) as (Image f)-isomorphic Ring
by RING_3:def 4;
B2: K is Field by B1;
{0.(Polynom-Ring F)}-Ideal = {0.(Polynom-Ring F)} by IDEAL_1:47;
hence a is F-algebraic by B2,RING_1:21;
end;
hence thesis by A;
end;
theorem
for F being Field,
E being (Polynom-Ring F)-homomorphic FieldExtension of F
for a being non zero Element of E holds a is F-algebraic iff a" in RAdj(F,{a})
proof
let F be Field, E be (Polynom-Ring F)-homomorphic FieldExtension of F;
let a be non zero Element of E;
X: F is Subring of E by FIELD_4:def 1;
A: now assume a is F-algebraic;
then A1: FAdj(F,{a}) = RAdj(F,{a}) by ch1;
A2: {a} is Subset of FAdj(F,{a}) by FAt;
a in {a} by TARSKI:def 1; then
reconsider b=a as Element of the carrier of FAdj(F,{a}) by A2;
b" in the carrier of FAdj(F,{a});
hence a" in RAdj(F,{a}) by A1,Th19f;
end;
now assume a" in RAdj(F,{a}); then
a" in the set of all Ext_eval(p,a) where p is Polynomial of F by lemphi5;
then consider p being Polynomial of F such that
A1: a" = Ext_eval(p,a);
set r = (-1.F)|F;
set q = rpoly(1,0.F) *' p + r;
-0.F = 0.F; then
-1.F <> 0.F; then
B0: deg r = 0 by RING_4:21;
B5: deg rpoly(1,0.F) = 1 by HURWITZ:27;
q is non zero
proof
per cases;
suppose p = 0_.(F);
hence thesis by B0,HURWITZ:20;
end;
suppose B3: p <> 0_.(F);
then reconsider degp = deg p as Element of NAT by FIELD_1:1;
B4: deg(rpoly(1,0.F) *' p)
= deg rpoly(1,0.F) + degp by B3,HURWITZ:23;
deg q = max(deg rpoly(1,0.F)+deg p,0) by B0,B4,B5,HURWITZ:21
.= deg rpoly(1,0.F) + degp by XXREAL_0:def 10;
then q <> 0_.(F) by HURWITZ:20;
hence thesis by UPROOTS:def 5;
end;
end;
then reconsider q as non zero Polynomial of F;
1.E = 1.F by X,C0SP1:def 3; then
A2: -1.E = (-1.F) * 1.F by X,Th19
.= (-1.F)*LC(1_.(F)) by RATFUNC1:def 7
.= LC((-1.F)*1_.(F)) by RATFUNC1:18
.= LC((-1.F)|F) by RING_4:16;
A3: 0.E = 0.F by X,C0SP1:def 3;
reconsider rpE = rpoly(1,0.E) as
Element of the carrier of Polynom-Ring E by POLYNOM3:def 10;
reconsider rpF = rpoly(1,0.F) as
Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
A5: a <> 0.E;
Ext_eval(q,a) = Ext_eval(rpoly(1,0.F) *' p,a) + Ext_eval(r,a)
by X,ALGNUM_1:15
.= Ext_eval(rpoly(1,0.F),a) * a" + Ext_eval(r,a)
by X,A1,ALGNUM_1:20
.= Ext_eval(rpF,a) * a" + -1.E by A2,exevalconst
.= eval(rpE,a) * a" + - 1.E by A3,FIELD_4:21,FIELD_4:26
.= (a - 0.E) * a" + - 1.E by HURWITZ:29
.= a" * a + - 1.E by GROUP_1:def 12
.= 1.E + - 1.E by A5,VECTSP_1:def 10
.= 0.E by RLVECT_1:5;
hence a is F-algebraic by alg00;
end;
hence thesis by A;
end;
theorem
for F being Field,
E being FieldExtension of F
for a being Element of E
holds a is F-transcendental iff RAdj(F,{a}),Polynom-Ring F are_isomorphic
proof
let F be Field, E being FieldExtension of F; let a be Element of E;
reconsider E1 = E as (Polynom-Ring F)-homomorphic Field;
reconsider g = hom_Ext_eval(a,F) as Homomorphism of (Polynom-Ring F),E1;
H: (Polynom-Ring F)/(ker g), Image g are_isomorphic by RING_2:15;
A: now assume a is F-transcendental;
then (Polynom-Ring F)/(ker g), (Polynom-Ring F) are_isomorphic by RING_2:17;
then (Polynom-Ring F), (Image g) are_isomorphic by H,RING_3:44;
hence (Polynom-Ring F), RAdj(F,{a}) are_isomorphic by lemphi4;
end;
now assume RAdj(F,{a}),Polynom-Ring F are_isomorphic;
then Polynom-Ring F is (RAdj(F,{a}))-isomorphic by RING_3:def 4;
then RAdj(F,{a}) <> FAdj(F,{a});
hence a is F-transcendental by ch1;
end;
hence thesis by A;
end;
theorem
for F being Field,
E being (Polynom-Ring F)-homomorphic FieldExtension of F
for a being F-algebraic Element of E
holds (Polynom-Ring F)/({MinPoly(a,F)}-Ideal), FAdj(F,{a}) are_isomorphic
proof
let F be Field, E be (Polynom-Ring F)-homomorphic FieldExtension of F;
let a be F-algebraic Element of E;
set f = hom_Ext_eval(a,F);
(Polynom-Ring F)/(ker f), Image f are_isomorphic by RING_2:15;
then (Polynom-Ring F)/({MinPoly(a,F)}-Ideal), Image f are_isomorphic by mpol1;
then (Polynom-Ring F)/({MinPoly(a,F)}-Ideal), RAdj(F,{a}) are_isomorphic
by lemphi4;
hence thesis by ch1;
end;
begin :: The Basis of Vector Space F(a)
definition
let F be Field,
E be FieldExtension of F;
let a be F-algebraic Element of E;
func Base a -> non empty Subset of VecSp(FAdj(F,{a}),F) equals
{ a|^n where n is Element of NAT : n < deg MinPoly(a,F) };
coherence
proof
set M = {a|^n where n is Element of NAT : n < deg MinPoly(a,F)};
X: FAdj(F,{a}) is Subring of E by FIELD_5:12;
deg MinPoly(a,F) > 0 by RING_4:def 4; then
A: a|^0 in M;
now let o be object;
assume o in M;
then consider n being Element of NAT such that
H: o = a|^n & n < deg MinPoly(a,F);
I: the carrier of VecSp(FAdj(F,{a}),F) = the carrier of FAdj(F,{a})
by FIELD_4:def 6;
reconsider U = {a} as Subset of E;
K: {a} is Subset of the carrier of FAdj(F,{a}) by FAt;
a in {a} by TARSKI:def 1;
then reconsider a1 = a as Element of FAdj(F,{a}) by K;
a1|^n in the carrier of FAdj(F,{a});
hence o in the carrier of VecSp(FAdj(F,{a}),F) by I,H,X,pr5;
end;
hence thesis by A,TARSKI:def 3;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let a be F-algebraic Element of E;
cluster Base a -> finite;
coherence
proof
reconsider n = deg MinPoly(a,F) as Element of NAT;
deffunc F(Nat) = a|^($1);
defpred P[Nat] means $1 < n;
D: {F(i) where i is Nat: i<=n & P[i]} is finite from FINSEQ_1:sch 6;
E: now let o be object;
assume o in {F(i) where i is Nat: i<=n & P[i]};
then consider i being Nat such that
E1: o = a|^i & i <= n & i < n;
i is Element of NAT by ORDINAL1:def 12;
hence o in Base a by E1;
end;
now let o be object;
assume o in Base a;
then consider i being Element of NAT such that E1: o = a|^i & i < n;
thus o in {F(i) where i is Nat: i<=n & P[i]} by E1;
end;
hence thesis by D,E,TARSKI:2;
end;
end;
lembas1b:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for p being Polynomial of F st deg p < deg MinPoly(a,F)
holds Ext_eval(Leading-Monomial p,a) in Lin(Base a)
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E; let p be Polynomial of F;
assume AS: deg p < deg MinPoly(a,F);
set LMp = Leading-Monomial p, V = VecSp(FAdj(F,{a}),F),
ma = MinPoly(a,F), K = FAdj(F,{a});
H0a: F is Subring of K by FIELD_4:def 1;
per cases;
suppose J: p = 0_.(F);
then I: LMp = p by POLYNOM4:13;
H: Ext_eval(p,a) = 0.E by J,ALGNUM_1:13
.= 0.(FAdj(F,{a})) by dFA
.= 0.V by FIELD_4:def 6
.= Sum(ZeroLC(V)) by VECTSP_6:15;
ZeroLC(V) is Linear_Combination of Base a by VECTSP_6:5;
hence thesis by I,H,VECTSP_7:7;
end;
suppose J: p <> 0_.(F);
then reconsider n = deg p as Element of NAT by FIELD_1:1;
J1: p is non zero by J,UPROOTS:def 5;
defpred P[object,object] means
($1 = a|^n & $2 = LC p) or ($1 <> a|^n & $2 = 0.F);
A: for x being object st x in the carrier of V
ex y being object st y in the carrier of F & P[x,y]
proof
let x be object;
assume x in the carrier of V;
per cases;
suppose x = a|^n;
hence ex y being object st y in the carrier of F & P[x,y];
end;
suppose x <> a|^n;
hence ex y being object st y in the carrier of F & P[x,y];
end;
end;
consider l being Function of the carrier of V,the carrier of F such that
L: for x being object st x in the carrier of V holds P[x,l.x]
from FUNCT_2:sch 1(A);
reconsider l as Element of Funcs(the carrier of V, the carrier of F)
by FUNCT_2:8;
for v being Element of V st not v in Base a holds l.v = 0.F
proof
let v being Element of V;
assume not v in Base a;
then v <> a|^n by AS;
hence l.v = 0.F by L;
end;
then reconsider l as Linear_Combination of V by VECTSP_6:def 1;
now let o be object;
assume o in Carrier l;
then consider v being Element of V such that
A1: o = v & l.v <> 0.F by VECTSP_6:1;
v = a|^n & l.v = LC p by L,A1;
hence o in Base a by A1,AS;
end;
then Carrier(l) c= Base a;
then reconsider l as Linear_Combination of Base a by VECTSP_6:def 4;
J5: {a} is Subset of K by FAt;
a in {a} by TARSKI:def 1; then
reconsider ak = a as Element of K by J5;
J4: K is Subring of E by FIELD_5:12;
ak|^n is Element of K; then
A8: a|^n is Element of K by J4,pr5; then
reconsider v = a|^n as Element of V by FIELD_4:def 6;
the carrier of F c= the carrier of K &
the carrier of K c= the carrier of E by H0a,C0SP1:def 3,EC_PF_1:def 1;
then reconsider p0 = LC p as Element of E;
reconsider a0 = a|^n as Element of E;
A3: [l.v,v]in[:the carrier of F,the carrier of K:] by A8,ZFMISC_1:def 2;
the carrier of F c= the carrier of K by H0a,C0SP1:def 3; then
LC p in the carrier of K; then
A4: [p0,a0]in[:the carrier of K,the carrier of K:] by A8,ZFMISC_1:def 2;
A9: Carrier l = {v}
proof
Y: now let o be object;
assume o in Carrier l;
then consider w being Element of V such that
A9b: o = w & l.w <> 0.F by VECTSP_6:1;
o = v by A9b,L;
hence o in {v} by TARSKI:def 1;
end;
now let o be object;
assume o in {v}; then
A9c: o = v by TARSKI:def 1;
p is non zero by J,UPROOTS:def 5; then
l.v <> 0.F by L;
hence o in Carrier l by A9c,VECTSP_6:1;
end;
hence thesis by TARSKI:2,Y;
end;
A5: (the multF of K) = (the multF of E)||(the carrier of K)
by EC_PF_1:def 1;
Sum l = l.v * v by A9,VECTSP_6:20
.= ((the multF of K)|[:the carrier of F,the carrier of K:]).(l.v,v)
by FIELD_4:def 6
.= (the multF of K).(l.v,v) by A3,FUNCT_1:49
.= (the multF of K).(p0,a0) by L
.= p0 * a|^n by A4,A5,FUNCT_1:49
.= Ext_eval(LMp,a) by J1,exevalLM;
hence Ext_eval(LMp,a) in Lin(Base a) by VECTSP_7:7;
end;
end;
lembas1a:
for F being Field,
E being (Polynom-Ring F)-homomorphic FieldExtension of F
for a being F-algebraic Element of E
for p being Polynomial of F st deg p < deg MinPoly(a,F)
holds Ext_eval(p,a) in Lin(Base a)
proof
let F be Field, E be (Polynom-Ring F)-homomorphic FieldExtension of F;
let a be F-algebraic Element of E; let p be Polynomial of F;
assume ASdeg: deg p < deg MinPoly(a,F);
H0: F is Subring of E by FIELD_4:def 1;
set V = VecSp(FAdj(F,{a}),F), ma = MinPoly(a,F), K = FAdj(F,{a});
deg ma >= 0 + 1 by INT_1:7,RING_4:def 4; then
reconsider degma = deg MinPoly(a,F) - 1 as Element of NAT by INT_1:3;
H0a: F is Subring of K by FIELD_4:def 1;
per cases;
suppose p = 0_.(F);
then H: Ext_eval(p,a) = 0.E by ALGNUM_1:13
.= 0.(FAdj(F,{a})) by dFA
.= 0.V by FIELD_4:def 6
.= Sum(ZeroLC(V)) by VECTSP_6:15;
ZeroLC(V) is Linear_Combination of Base a by VECTSP_6:5;
hence thesis by H,VECTSP_7:7;
end;
suppose X: p <> 0_.(F);
defpred Q[Nat] means
for p being Polynomial of F
st deg p = $1 holds Ext_eval(p,a) in Lin(Base a);
IA: Q[0]
proof
now let p be Polynomial of F;
assume AS1: deg p = 0;
then AS: p is constant by RATFUNC1:def 2;
defpred P[object,object] means
($1 = a|^0 & $2 = p.0) or ($1 <> a|^0 & $2 = 0.F);
A: for x being object st x in the carrier of V
ex y being object st y in the carrier of F & P[x,y]
proof
let x be object;
assume x in the carrier of V;
per cases;
suppose x = a|^0;
hence ex y being object st y in the carrier of F & P[x,y];
end;
suppose x <> a|^0;
hence ex y being object st y in the carrier of F & P[x,y];
end;
end;
consider l being Function of the carrier of V,the carrier of F such that
L: for x being object st x in the carrier of V holds P[x,l.x]
from FUNCT_2:sch 1(A);
reconsider l as Element of Funcs(the carrier of V, the carrier of F)
by FUNCT_2:8;
A2: not(deg MinPoly(a,F) <= 0) by RING_4:def 4;
for v being Element of V st not v in Base a holds l.v = 0.F
proof
let v being Element of V;
assume not v in Base a;
then v <> a|^0 by A2;
hence l.v = 0.F by L;
end;
then reconsider l as Linear_Combination of V by VECTSP_6:def 1;
now let o be object;
assume o in Carrier l;
then consider v being Element of V such that
A1: o = v & l.v <> 0.F by VECTSP_6:1;
v = a|^0 & l.v = p.0 by L,A1;
hence o in Base a by A1,A2;
end;
then Carrier(l) c= Base a;
then reconsider l as Linear_Combination of Base a by VECTSP_6:def 4;
A6: a|^0 = 1_E by BINOM:8 .= 1.F by H0,C0SP1:def 3; then
A8: a|^0 = 1.K by H0a,C0SP1:def 3;
then reconsider v = a|^0 as Element of V by FIELD_4:def 6;
the carrier of F c= the carrier of K by H0a,C0SP1:def 3; then
reconsider p0 = p.0 as Element of K;
reconsider a0 = a|^0 as Element of K by A8;
A3: [l.v,v]in[:the carrier of F,the carrier of K:] by A8,ZFMISC_1:def 2;
0 = len p - 1 by AS1,HURWITZ:def 2; then
A5: LC p = p.(1 -'1) by RATFUNC1:def 6
.= p.(1-1) by XREAL_0:def 2;
A7: [p.0,1.F]in[:the carrier of F,the carrier of F:] by ZFMISC_1:def 2;
A9: Carrier l = {v}
proof
Y: now let o be object;
assume o in Carrier l;
then consider w being Element of V such that
A9b: o = w & l.w <> 0.F by VECTSP_6:1;
o = v by A9b,L;
hence o in {v} by TARSKI:def 1;
end;
now let o be object;
assume o in {v};
then A9c: o = v by TARSKI:def 1;
p <> 0_.(F) by AS1,HURWITZ:20; then
p is non zero by UPROOTS:def 5; then
l.v <> 0.F by L,A5;
hence o in Carrier l by A9c,VECTSP_6:1;
end;
hence thesis by TARSKI:2,Y;
end;
Sum l = l.v * v by A9,VECTSP_6:20
.= ((the multF of K)|[:the carrier of F,the carrier of K:]).(l.v,v)
by FIELD_4:def 6
.= (the multF of K).(l.v,v) by A3,FUNCT_1:49
.= (the multF of K).(p.0,1.F) by L,A6
.= ((the multF of K)||(the carrier of F)).(p.0,1.F) by A7,FUNCT_1:49
.= p.0 * 1.F by H0a,C0SP1:def 3
.= Ext_eval(p,a) by A5,AS,exevalconst;
hence Ext_eval(p,a) in Lin(Base a) by VECTSP_7:7;
end;
hence Q[0];
end;
IS: for k being Element of NAT st 0 <= k & k < degma holds
(for j being Element of NAT st 0 <= j & j <= k holds Q[j])
implies Q[k+1]
proof let k be Element of NAT;
assume IV0: 0 <= k & k < degma;
assume IV1: for j being Element of NAT st 0 <= j & j <= k holds Q[j];
now let p be Polynomial of F;
assume IS0: deg p = k+1;
IS: deg p = len p - 1 by HURWITZ:def 2;
then len p <> 0 by IS0;
then consider r being Polynomial of F such that
IS1: len r < len p & p = r+Leading-Monomial(p) &
for n being Element of NAT st n < len p-1 holds r.n = p.n
by POLYNOM4:16;
len r - 1 < len p - 1 by IS1,XREAL_1:9; then
IS3: deg r < deg p by IS,HURWITZ:def 2;
IS4: k + 1 < degma + 1 by IV0,XREAL_1:8;
per cases;
suppose r = 0_.(F);
hence Ext_eval(p,a) in Lin Base a by IS1,IS4,IS0,lembas1b;
end;
suppose r <> 0_.(F);
then reconsider degr = deg r as Element of NAT by FIELD_1:1;
degr <= k by IS3,IS0,NAT_1:13;
then consider lr being Linear_Combination of Base a such that
IS5: Ext_eval(r,a) = Sum(lr) by IV1,VECTSP_7:7;
set LMp = Leading-Monomial(p);
Ext_eval(LMp,a) in Lin(Base a) by IS4,IS0,lembas1b;
then consider l being Linear_Combination of Base a such that
IS6: Ext_eval(LMp,a) = Sum(l) by VECTSP_7:7;
reconsider ls = l + lr as Linear_Combination of Base a by VECTSP_6:24;
Ext_eval(LMp,a) in
the set of all Ext_eval(p,a) where p is Polynomial of F;
then Ext_eval(LMp,a) in RAdj(F,{a}) by lemphi5; then
IS8: Ext_eval(LMp,a) in FAdj(F,{a}) by ch1;
Ext_eval(r,a) in
the set of all Ext_eval(p,a) where p is Polynomial of F;
then Ext_eval(r,a) in RAdj(F,{a}) by lemphi5; then
Ext_eval(r,a) in FAdj(F,{a}) by ch1; then
IS7: [Sum l,Sum lr] in [:the carrier of K,the carrier of K:]
by IS5,IS6,IS8,ZFMISC_1:def 2;
Sum ls = Sum l + Sum lr by VECTSP_6:44
.= (the addF of K).(Sum l,Sum lr) by FIELD_4:def 6
.= ((the addF of E)||(the carrier of K)).(Sum l,Sum lr)
by EC_PF_1:def 1
.= Ext_eval(LMp,a) + Ext_eval(r,a) by IS5,IS6,IS7,FUNCT_1:49
.= Ext_eval(p,a) by IS1,H0,ALGNUM_1:15;
hence Ext_eval(p,a) in Lin Base a by VECTSP_7:7;
end;
end;
hence Q[k+1];
end;
I: for j being Element of NAT st 0 <= j & j <= degma holds Q[j]
from INT_1:sch 8(IA,IS);
reconsider degp = deg p as Element of NAT by FIELD_1:1,X;
degp + 1 <= deg ma by ASdeg,INT_1:7;
then degp + 1 - 1 <= deg ma - 1 by XREAL_1:9;
hence thesis by I;
end;
end;
theorem lembas1:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for p being Polynomial of F holds Ext_eval(p,a) in Lin(Base a)
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E; let p be Polynomial of F;
set ma = MinPoly(a,F), r = p mod ma;
B: F is Subring of E by FIELD_4:def 1;
C: p = (p div ma) *' ma + r by RING_4:4;
D: deg r < deg ma by FIELD_5:16;
Ext_eval(p,a)
= Ext_eval((p div ma) *' ma,a) + Ext_eval(r,a) by C,B,ALGNUM_1:15
.= (Ext_eval(p div ma,a) * Ext_eval(ma,a)) + Ext_eval(r,a) by B,ALGNUM_1:20
.= (Ext_eval(p div ma,a) * 0.E) + Ext_eval(r,a) by mpol2
.= Ext_eval(r,a);
hence thesis by D,lembas1a;
end;
theorem lembas2a:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for l being Linear_Combination of Base a
ex p being Polynomial of F
st deg p < deg MinPoly(a,F) &
for i being Element of NAT st i < deg MinPoly(a,F) holds p.i = l.(a|^i)
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E; let l be Linear_Combination of Base a;
not(deg MinPoly(a,F) <= 0) by RING_4:def 4; then
reconsider n = deg MinPoly(a,F) - 1 as Element of NAT by INT_1:3;
E is FAdj(F,{a})-extending by FIELD_4:7; then
B: VecSp(FAdj(F,{a}),F) is Subspace of VecSp(E,F) by FIELD_5:14;
consider l2 being Linear_Combination of VecSp(E,F) such that
K: Carrier l2 = Carrier l &
for v being Element of VecSp(E,F) st v in Carrier l2 holds l2.v = l.v
by B,lcsub;
consider p being Polynomial of F such that
A: deg p <= n &
for i being Element of NAT st i <= n holds p.i = l2.(a|^i) by lembasx2;
take p;
deg p + 0 < (deg MinPoly(a,F) - 1) + 1 by A,XREAL_1:8;
hence deg p < deg MinPoly(a,F);
now let i be Element of NAT;
assume i < deg MinPoly(a,F);
then i < n + 1;
then B: i <= n by NAT_1:13;
the carrier of VecSp(FAdj(F,{a}),F) = the carrier of FAdj(F,{a})
by FIELD_4:def 6; then
V1: a|^i is Element of VecSp(FAdj(F,{a}),F) by lcsub1;
V2: a|^i is Element of VecSp(E,F) by FIELD_4:def 6;
thus p.i = l.(a|^i)
proof
per cases;
suppose a|^i in Carrier l2;
then l2.(a|^i) = l.(a|^i) by K;
hence thesis by A,B;
end;
suppose C: not a|^i in Carrier l2;
then l2.(a|^i) = 0.F by V2,VECTSP_6:2 .= l.(a|^i) by V1,C,K,VECTSP_6:2;
hence thesis by A,B;
end;
end;
end;
hence thesis;
end;
theorem lembas2bb:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for l being Linear_Combination of Base a,
p being non zero Polynomial of F
st l.(a|^(deg p)) = LC p & Carrier l = {a|^(deg p)}
holds Sum l = Ext_eval(LM p,a)
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E;
let l be Linear_Combination of Base a, p be non zero Polynomial of F;
F is Subring of E by FIELD_4:def 1; then
H2: the carrier of F c= the carrier of E by C0SP1:def 3;
H3: {a} is Subset of FAdj(F,{a}) by FAt;
a in {a} by TARSKI:def 1; then
reconsider a1 = a as Element of FAdj(F,{a}) by H3;
H7: FAdj(F,{a}) is Subring of E by FIELD_5:12;
assume A: l.(a|^(deg p)) = LC p & Carrier l = {a|^(deg p)};
reconsider LCpE = LC p as Element of E by H2;
F is Subfield of FAdj(F,{a}) by FAsub; then
the carrier of F c= the carrier of FAdj(F,{a}) by EC_PF_1:def 1; then
reconsider LCp = LC p as Element of FAdj(F,{a});
reconsider degp = deg p as Nat;
H8: a|^(degp) = a1|^(degp) by H7,pr5; then
reconsider adegp = a|^(deg p) as Element of FAdj(F,{a});
reconsider v = a|^(deg p) as Element of VecSp(FAdj(F,{a}),F)
by H8,FIELD_4:def 6;
B: E is FieldExtension of FAdj(F,{a}) by FIELD_4:7;
Sum l = l.v * v by A,VECTSP_6:20
.= LCp * adegp by A,Lm12a
.= LCpE * (a|^(deg p)) by B,Lm12b
.= Ext_eval(LM p,a) by exevalLM;
hence thesis;
end;
theorem lembas2b:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for l being Linear_Combination of Base a
for p being Polynomial of F
st deg p < deg MinPoly(a,F) &
for i being Element of NAT st i < deg MinPoly(a,F) holds p.i = l.(a|^i)
holds Sum l = Ext_eval(p,a)
proof
let F be Field, E be FieldExtension of F; let a be F-algebraic Element of E;
let l be Linear_Combination of Base a; let p be Polynomial of F;
set V = VecSp(FAdj(F,{a}),F);
assume AS: deg p < deg MinPoly(a,F) &
for i being Element of NAT st i < deg MinPoly(a,F) holds p.i = l.(a|^i);
defpred P[Nat] means
for l being Linear_Combination of Base a st card Carrier(l) = $1
for p being Polynomial of F
st deg p < deg MinPoly(a,F) &
for i being Element of NAT st i < deg MinPoly(a,F) holds p.i = l.(a|^i)
holds Sum l = Ext_eval(p,a);
IA: P[0]
proof
let l be Linear_Combination of Base a;
assume card Carrier(l) = 0; then
Carrier l = {}; then
A2: l = ZeroLC(V) by VECTSP_6:def 3;
let p be Polynomial of F; assume
A4: deg p < deg MinPoly(a,F) &
for i being Element of NAT st i < deg MinPoly(a,F) holds p.i = l.(a|^i);
now let i be Element of NAT;
per cases;
suppose i >= deg MinPoly(a,F);
then A5: i > deg p by A4,XXREAL_0:2;
deg p = len p - 1 by HURWITZ:def 2;
then i + 1 > len p - 1 + 1 by A5,XREAL_1:6;
hence p.i = (0_.(F)).i by NAT_1:13,ALGSEQ_1:8;
end;
suppose A5: i < deg MinPoly(a,F); then
a|^i in Base a; then
reconsider v = a|^i as Element of V;
thus p.i = l.v by A4,A5 .= (0_.(F)).i by A2,VECTSP_6:3;
end;
end;
then p = 0_.(F);
hence Ext_eval(p,a) = 0.E by ALGNUM_1:13
.= 0.(FAdj(F,{a})) by dFA
.= 0.V by FIELD_4:def 6
.= Sum l by A2,VECTSP_6:15;
end;
IS: now let k be Nat;
assume B0: P[k];
now let l be Linear_Combination of Base a;
assume B1: card Carrier(l) = k+1;
let pp be Polynomial of F;
assume B2: deg pp < deg MinPoly(a,F) &
for i being Element of NAT st i < deg MinPoly(a,F) holds pp.i=l.(a|^i);
now assume C0: pp = 0_.(F);
now let o be object;
assume C1: o in Carrier l;
Carrier l c= Base a by VECTSP_6:def 4;
then o in Base a by C1;
then consider n being Element of NAT such that
C2: o = a|^n & n < deg MinPoly(a,F);
l.(a|^n) = pp.n by B2,C2 .= 0.F by C0;
hence contradiction by C1,C2,VECTSP_6:2;
end;
then Carrier l = {} by XBOOLE_0:def 1;
hence contradiction by B1;
end;
then reconsider p = pp as non zero Polynomial of F by UPROOTS:def 5;
defpred Q[object,object] means
($1 = a|^(deg p) & $2 = LC p) or ($1 <> a|^(deg p) & $2 = 0.F);
A: for x being object st x in the carrier of V
ex y being object st y in the carrier of F & Q[x,y]
proof
let x be object;
assume x in the carrier of V;
per cases;
suppose x = a|^(deg p);
hence ex y being object st y in the carrier of F & Q[x,y];
end;
suppose x <> a|^(deg p);
hence ex y being object st y in the carrier of F & Q[x,y];
end;
end;
consider lp being Function of the carrier of V,the carrier of F such that
L: for x being object st x in the carrier of V holds Q[x,lp.x]
from FUNCT_2:sch 1(A);
reconsider lp as Element of Funcs(the carrier of V, the carrier of F)
by FUNCT_2:8;
for v being Element of V st not v in Base a holds lp.v = 0.F
proof
let v being Element of V;
assume not v in Base a;
then v <> a|^(deg p) by B2;
hence lp.v = 0.F by L;
end;
then reconsider lp as Linear_Combination of V by VECTSP_6:def 1;
now let o be object;
assume o in Carrier lp;
then consider v being Element of V such that
A1: o = v & lp.v <> 0.F by VECTSP_6:1;
v = a|^(deg p) & lp.v = LC p by L,A1;
hence o in Base a by A1,B2;
end;
then Carrier(lp) c= Base a;
then reconsider lp as Linear_Combination of Base a by VECTSP_6:def 4;
X1: {a} is Subset of FAdj(F,{a}) by FAt;
a in {a} by TARSKI:def 1; then
reconsider a1 = a as Element of the carrier of FAdj(F,{a}) by X1;
FAdj(F,{a}) is Subring of E by FIELD_5:12; then
a|^(deg p) = a1|^(deg p) by pr5; then
X: a|^(deg p) is Element of V by FIELD_4:def 6;
C0: Carrier lp = {a|^(deg p)}
proof
C2: now let o be object;
assume o in {a|^(deg p)}; then
C3: o = a|^(deg p) by TARSKI:def 1; then
lp.o <> 0.F by X,L;
hence o in Carrier lp by X,C3,VECTSP_6:2;
end;
now let o be object;
assume C3: o in Carrier lp;
Carrier lp = {v where v is Element of V: lp.v <> 0.F}
by VECTSP_6:def 2;
then consider v being Element of V such that
C4: o = v & lp.v <> 0.F by C3;
o = a|^(deg p) by C4,L;
hence o in {a|^(deg p)} by TARSKI:def 1;
end;
hence thesis by C2,TARSKI:2;
end;
lp.(a|^(deg p)) = LC p by X,L; then
C: Ext_eval(LM p,a) = Sum lp by C0,lembas2bb;
set q = p - (LM p);
reconsider lk = l - lp as Linear_Combination of Base a by VECTSP_6:42;
C2: l = lk + lp
proof
thus lk + lp = (l + -lp) + lp by VECTSP_6:def 11
.= l + (-lp + lp) by VECTSP_6:26
.= l + (lp + -lp) by VECTSP_6:25
.= l + (lp - lp) by VECTSP_6:def 11
.= l + ZeroLC(V) by VECTSP_6:43
.= l by VECTSP_6:27;
end;
C3: Carrier lk = Carrier(l) \ Carrier(lp)
proof
C4: now let o be object;
assume o in Carrier lk;
then consider v being Element of V such that
C5: o = v & lk.v <> 0.F by VECTSP_6:1;
C6: now assume C7: v = a|^(deg p); then
C9: l.v = p.(deg p) by B2 .= LC p by thLC;
lk.v = l.v - lp.v by VECTSP_6:40
.= LC p - LC p by L,C7,C9;
hence contradiction by C5,RLVECT_1:15;
end; then
C7: not v in Carrier(lp) by C0,TARSKI:def 1;
lk.v = l.v - lp.v by VECTSP_6:40
.= l.v - 0.F by C6,L; then
v in Carrier l by C5,VECTSP_6:2;
hence o in Carrier(l) \ Carrier(lp) by C7,C5,XBOOLE_0:def 5;
end;
now let o be object;
assume o in Carrier(l) \ Carrier(lp); then
C5: o in Carrier(l) & not o in Carrier(lp) by XBOOLE_0:def 5; then
consider v being Element of V such that
C6: o = v & l.v <> 0.F by VECTSP_6:1;
C7: o <> a|^(deg p) by C0,C5,TARSKI:def 1;
lk.v = l.v - lp.v by VECTSP_6:40
.= l.v - 0.F by C6,C7,L;
hence o in Carrier lk by C6,VECTSP_6:1;
end;
hence thesis by C4,TARSKI:2;
end;
now let o be object;
assume C5: o in Carrier lp; then
C4: o = a|^(deg p) by C0,TARSKI:def 1;
reconsider v = o as Element of V by C5;
lp.v = LC p by L,C4 .= pp.(deg p) by thLC .= l.v by C4,B2; then
l.v <> 0.F by C5,VECTSP_6:2;
hence o in Carrier l by VECTSP_6:2;
end; then
Carrier lp c= Carrier l; then
A: card(Carrier(l) \ Carrier(lp))
= card(Carrier l) - card(Carrier lp) by CARD_2:44
.= (k + 1) - 1 by B1,C0,CARD_2:42;
B: deg q < deg MinPoly(a,F) by thdLM,B2,XXREAL_0:2;
for i being Element of NAT st i < deg MinPoly(a,F) holds q.i=lk.(a|^i)
proof
let i be Element of NAT;
assume B1: i < deg MinPoly(a,F);
FAdj(F,{a}) is Subring of E by FIELD_5:12; then
a|^i = a1|^i by pr5; then
reconsider v = a|^i as Element of V by FIELD_4:def 6;
per cases;
suppose B3: i = deg p;
hence q.i = p.(deg p) - (LM p).(deg p) by POLYNOM3:27
.= p.(deg p) - (LM p).(deg (LM p)) by thdegLM
.= l.v - (LM p).(deg (LM p)) by B3,B2
.= l.v - LC(LM p) by thLC
.= l.v - LC p by thdegLC
.= l.v - lp.v by B3,L
.= lk.(a|^i) by VECTSP_6:40;
end;
suppose D2: i <> deg p;
D3: a|^i <> a|^(deg p)
proof
per cases by D2,XXREAL_0:1;
suppose i < deg p;
hence thesis by B2,mpol5;
end;
suppose i > deg p;
hence thesis by B1,mpol5;
end;
end;
p <> 0_.(F);
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 D5: len p -' 1 = len p - 1 by XREAL_0:def 2;
D4: i <> len p -' 1 by D5,D2,HURWITZ:def 2;
thus q.i = p.i - (LM p).i by POLYNOM3:27
.= p.i - 0.F by D4,POLYNOM4:def 1
.= l.v - 0.F by B2,B1
.= l.v - lp.v by D3,L
.= lk.(a|^i) by VECTSP_6:40;
end;
end;
then D: Ext_eval(q,a) = Sum lk by A,C3,B,B0;
Sum(lk) in the carrier of V & Sum(lp) in the carrier of V; then
Sum(lk) in the carrier of FAdj(F,{a}) &
Sum(lp) in the carrier of FAdj(F,{a}) by FIELD_4:def 6; then
Sum(lk) in carrierFA({a}) & Sum(lp) in carrierFA({a}) by dFA; then
E: [Sum(lk),Sum(lp)] in
[:carrierFA({a}),carrierFA({a}):] by ZFMISC_1:def 2;
thus Sum l
= Sum(lk) + Sum(lp) by C2,VECTSP_6:44
.= (the addF of FAdj(F,{a})).(Sum(lk),Sum(lp)) by FIELD_4:def 6
.= ((the addF of E)||carrierFA({a})).(Sum(lk),Sum(lp)) by dFA
.= (the addF of E).(Sum(lk),Sum(lp)) by E,FUNCT_1:49
.= (Ext_eval(p,a) - Ext_eval(LM p,a)) + Ext_eval(LM p,a)
by C,D,exevalminus2
.= Ext_eval(p,a) + (-Ext_eval(LM p,a) + Ext_eval(LM p,a))
by RLVECT_1:def 3
.= Ext_eval(p,a) + 0.E by RLVECT_1:5
.= Ext_eval(pp,a);
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that H: card Carrier(l) = n;
thus thesis by AS,I,H;
end;
theorem lembas2:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for l being Linear_Combination of Base a
holds Sum(l) = 0.F implies l = ZeroLC VecSp(FAdj(F,{a}),F)
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E; let l be Linear_Combination of Base a;
assume AS: Sum(l) = 0.F;
set V = VecSp(FAdj(F,{a}),F), ma = MinPoly(a,F);
H: F is Subring of E by FIELD_4:def 1;
consider p being Polynomial of F such that
A2: deg p < deg MinPoly(a,F) &
for i being Element of NAT st i < deg ma holds p.i = l.(a|^i) by lembas2a;
now assume A3: Carrier l <> {};
set x = the Element of Carrier l;
consider v being Element of V such that
A5: x = v & l.v <> 0.F by A3,VECTSP_6:1;
Carrier l c= Base a by VECTSP_6:def 4; then
v in Base a by A3,A5; then
consider i being Element of NAT such that A6: v=a|^i & i < deg MinPoly(a,F);
p.i <> 0.F by A2,A6,A5; then
p <> 0_.(F);
then reconsider p as non zero Polynomial of F by UPROOTS:def 5;
reconsider pp = p as non zero Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
Ext_eval(pp,a) = 0.F by A2,AS,lembas2b .= 0.E by H,C0SP1:def 3;
hence contradiction by mpol4,A2,RING_5:13;
end;
hence thesis by VECTSP_6:def 3;
end;
theorem lembas:
for F being Field,
E being (Polynom-Ring F)-homomorphic FieldExtension of F
for a being F-algebraic Element of E holds
Base a is Basis of VecSp(FAdj(F,{a}),F)
proof
let F be Field, E be (Polynom-Ring F)-homomorphic FieldExtension of F;
let a be F-algebraic Element of E;
set V = VecSp(FAdj(F,{a}),F), ma = MinPoly(a,F);
H0: F is Subring of E by FIELD_4:def 1;
A: now let l be Linear_Combination of Base a;
assume A1: Sum(l) = 0.V;
0.V = 0.(FAdj(F,{a})) by FIELD_4:def 6
.= 0.E by dFA .= 0.F by H0,C0SP1:def 3;
then l = ZeroLC V by A1,lembas2;
hence Carrier(l) = {} by VECTSP_6:def 3;
end;
E: now let o be object;
assume o in the carrier of the ModuleStr of V; then
o in the carrier of FAdj(F,{a}) by FIELD_4:def 6; then
o in the carrier of RAdj(F,{a}) by ch1; then
o in the set of all Ext_eval(p,a) where p is Polynomial of F by lemphi5;
then consider p being Polynomial of F such that A1: o = Ext_eval(p,a);
o in Lin(Base a) by A1,lembas1;
hence o in the carrier of Lin Base a;
end;
now let o be object;
assume G: o in the carrier of Lin Base a;
the carrier of Lin Base a c= the carrier of V by VECTSP_4:def 2;
hence o in the carrier of V by G;
end;
then Lin Base a = the ModuleStr of V by VECTSP_4:31,E,TARSKI:2;
hence thesis by A,VECTSP_7:def 3,VECTSP_7:def 1;
end;
theorem lembascard:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E holds card(Base a) = deg MinPoly(a,F)
proof
let F be Field, E be FieldExtension of F;
let a be F-algebraic Element of E;
set ma = MinPoly(a,F), m = deg MinPoly(a,F);
defpred P[object,object] means
ex x being Element of Seg m,
y being Element of NAT st $1 = x & y = x-1 & $2 = a|^y;
B1: for x,y1,y2 being object st x in Seg m & P[x,y1] & P[x,y2] holds y1 = y2;
B2: now let x be object;
assume B3: x in Seg m;
then reconsider n = x as Element of Seg m;
1 <= n by B3,FINSEQ_1:1; then
reconsider z = n - 1 as Element of NAT by INT_1:3;
thus ex y being object st P[x,y]
proof
take a|^z;
thus thesis;
end;
end;
consider f being Function such that
C: dom f = Seg m &
for x being object st x in Seg m holds P[x,f.x] from FUNCT_1:sch 2(B1,B2);
A1: now let o be object;
assume o in Base a;
then consider n being Element of NAT such that
A2: o = a|^n & n < m;
A3: 0 + 1 <= n + 1 & n + 1 <= m by A2,INT_1:7; then
reconsider x = n + 1 as Element of Seg m by FINSEQ_1:1;
A4: x in Seg m by FINSEQ_1:1,A3;
P[x,f.x] by C,FINSEQ_1:1,A3;
hence o in rng f by A4,C,A2,FUNCT_1:def 3;
end;
now let o be object;
assume o in rng f;
then consider u being object such that
A2: u in dom f & o = f.u by FUNCT_1:def 3;
P[u,f.u] by C,A2; then
consider x being Element of Seg m, y being Element of NAT such that
A3: u = x & y = x-1 & f.x = a|^y;
not(deg ma <= 0) by RING_4:def 4; then
m in Seg m by FINSEQ_1:3; then
1 <= x & x <= m by FINSEQ_1:1; then
y < m - 1 + 1 by A3,XREAL_1:9,NAT_1:13;
hence o in Base a by A2,A3;
end;
then A: rng f = Base a by A1,TARSKI:2;
now assume not f is one-to-one;
then consider x1,x2 being object such that
A1: x1 in dom f & x2 in dom f & f.x1 = f.x2 & x1 <> x2;
consider n1 being Element of Seg m,
y1 being Element of NAT such that
A2: x1 = n1 & y1 = n1-1 & f.x1 = a|^y1 by A1,C;
consider n2 being Element of Seg m,
y2 being Element of NAT such that
A3: x2 = n2 & y2 = n2-1 & f.x2 = a|^y2 by A1,C;
n1 <= m & n2 <= m by C,A1,FINSEQ_1:1; then
y1 + 1 - 1 <= m - 1 & y2 + 1 - 1 <= m - 1 by A3,A2,XREAL_1:9; then
A4: y1 < m - 1 + 1 & y2 < m - 1 + 1 by NAT_1:13;
A5: y1 <> y2 by A1,A2,A3;
per cases by A5,XXREAL_0:1;
suppose y1 < y2;
hence contradiction by A1,A2,A3,A4,mpol5;
end;
suppose y1 > y2;
hence contradiction by A1,A2,A3,A4,mpol5;
end;
end;
then card Base a = card(Seg m) by A,C,CARD_1:70 .= m by FINSEQ_1:57;
hence thesis;
end;
theorem
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
holds deg(FAdj(F,{a}),F) = deg MinPoly(a,F)
proof
let F be Field, E be FieldExtension of F; let a be F-algebraic Element of E;
set B = Base a, m = deg MinPoly(a,F);
B: card B = m by lembascard;
C: B is Basis of VecSp(FAdj(F,{a}),F) by lembas; then
A: VecSp(FAdj(F,{a}),F) is finite-dimensional by MATRLIN:def 1;
then dim VecSp(FAdj(F,{a}),F) = deg MinPoly(a,F) by C,B,VECTSP_9:def 1;
hence thesis by A,FIELD_4:def 7;
end;
registration
let F be Field,
E be FieldExtension of F;
let a be F-algebraic Element of E;
cluster FAdj(F,{a}) -> F-finite;
coherence
proof
Base a is Basis of VecSp(FAdj(F,{a}),F) by lembas;
then VecSp(FAdj(F,{a}),F) is finite-dimensional by MATRLIN:def 1;
hence FAdj(F,{a}) is F-finite by FIELD_4:def 8;
end;
end;
theorem
for F being Field,
E being FieldExtension of F
for a being Element of E
holds a is F-algebraic iff FAdj(F,{a}) is F-finite
proof
let F be Field, E be FieldExtension of F; let a be Element of E;
now assume AS: FAdj(F,{a}) is F-finite;
then reconsider n = deg(FAdj(F,{a}),F) as Element of NAT by ORDINAL1:def 12;
H: n = dim VecSp(FAdj(F,{a}),F) by FIELD_4:def 7;
per cases;
suppose ex i,j being Element of NAT st i < j & j <= n & a|^i = a|^j;
then consider i,j being Element of NAT such that
U: i < j & j <= n & a|^i = a|^j;
set p1 = <%0.F,1.F%>`^j, p2 = <%0.F,1.F%>`^i;
set p = p1 - p2;
now assume p = 0_.(F);
then 0.F = p.j
.= p1.j - p2.j by POLYNOM3:27
.= 1.F - p2.j by help1
.= 1.F - 0.F by U,help2;
hence contradiction;
end;
then reconsider p as non zero Polynomial of F by UPROOTS:def 5;
per cases;
suppose T: i = 0; then
W: a|^i = 1_E by BINOM:8;
Ext_eval(p,a) = Ext_eval(p1,a) - Ext_eval(p2,a) by exevalminus2
.= Ext_eval(p1,a) - Ext_eval(1_.(F),a) by T,POLYNOM5:15
.= Ext_eval(p1,a) - 1.E by FIELD_4:23
.= a|^j - 1.E by U,help3
.= 0.E by W,U,RLVECT_1:15;
hence a is F-algebraic by alg00;
end;
suppose T: i is non zero;
Ext_eval(p,a) = Ext_eval(p1,a) - Ext_eval(p2,a) by exevalminus2
.= a|^j - Ext_eval(p2,a) by U,help3
.= a|^j - a|^i by T,help3
.= 0.E by U,RLVECT_1:15;
hence a is F-algebraic by alg00;
end;
end;
suppose U: not ex i,j being Element of NAT st i < j & j <= n & a|^i = a|^j;
set M = {a|^i where i is Element of NAT : i <= n},
V = VecSp(FAdj(F,{a}),F);
X: {a} is Subset of FAdj(F,{a}) by FAt;
a in {a} by TARSKI:def 1; then
reconsider a1 = a as Element of FAdj(F,{a}) by X;
I: M c= the carrier of VecSp(FAdj(F,{a}),F)
proof
now let o be object;
assume o in M;
then consider i being Element of NAT such that
H: o = a|^i & i <= n;
I: the carrier of VecSp(FAdj(F,{a}),F) = the carrier of FAdj(F,{a})
by FIELD_4:def 6;
FAdj(F,{a}) is Subring of E by FIELD_5:12; then
a|^i = a1|^i by pr5;
hence o in the carrier of VecSp(FAdj(F,{a}),F) by H,I;
end;
hence thesis;
end;
M is finite
proof
deffunc F(Nat) = a|^($1);
defpred P[Nat] means $1 <= n;
D: {F(i) where i is Nat: i<=n & P[i]} is finite from FINSEQ_1:sch 6;
E: now let o be object;
assume o in {F(i) where i is Nat: i<=n & P[i]};
then consider i being Nat such that
E1: o = a|^i & i <= n & i <= n;
i is Element of NAT by ORDINAL1:def 12;
hence o in M by E1;
end;
now let o be object;
assume o in M; then
consider i being Element of NAT such that E1: o = a|^i & i <= n;
thus o in {F(i) where i is Nat: i<=n & P[i]} by E1;
end;
hence thesis by D,E,TARSKI:2;
end; then
reconsider M as finite Subset of VecSp(FAdj(F,{a}),F) by I;
card M = n + 1
proof
set m = n + 1;
defpred P[object,object] means
ex x being Element of Seg m,
y being Element of NAT st $1 = x & y = x-1 & $2 = a|^y;
B1: for x,y1,y2 being object st x in Seg m & P[x,y1] & P[x,y2]
holds y1 = y2;
B2: now let x be object;
assume B3: x in Seg m;
then reconsider i = x as Element of Seg m;
1 <= i by B3,FINSEQ_1:1; then
reconsider z = i - 1 as Element of NAT by INT_1:3;
thus ex y being object st P[x,y]
proof
take a|^z;
thus thesis;
end;
end;
consider f being Function such that
C: dom f = Seg m &
for x being object st x in Seg m holds P[x,f.x]
from FUNCT_1:sch 2(B1,B2);
A1: now let o be object;
assume o in M;
then consider i being Element of NAT such that
A2: o = a|^i & i <= n;
A3: 0 + 1 <= i + 1 & i + 1 <= n+1 by A2,XREAL_1:6; then
reconsider x = i + 1 as Element of Seg m by FINSEQ_1:1;
A4: x in Seg m by FINSEQ_1:1,A3;
P[x,f.x] by C,FINSEQ_1:1,A3;
hence o in rng f by A4,C,A2,FUNCT_1:def 3;
end;
now let o be object;
assume o in rng f;
then consider u being object such that
A2: u in dom f & o = f.u by FUNCT_1:def 3;
P[u,f.u] by C,A2; then
consider x being Element of Seg m, y being Element of NAT such that
A3: u = x & y = x-1 & f.x = a|^y;
m in Seg m by FINSEQ_1:3; then
1 <= x & x <= m by FINSEQ_1:1; then
y < m - 1 + 1 by A3,XREAL_1:9,NAT_1:13; then
y <= n by NAT_1:13;
hence o in M by A2,A3;
end;
then A: rng f = M by A1,TARSKI:2;
now assume not f is one-to-one;
then consider x1,x2 being object such that
A1: x1 in dom f & x2 in dom f & f.x1 = f.x2 & x1 <> x2;
consider n1 being Element of Seg m,
y1 being Element of NAT such that
A2: x1 = n1 & y1 = n1-1 & f.x1 = a|^y1 by A1,C;
consider n2 being Element of Seg m,
y2 being Element of NAT such that
A3: x2 = n2 & y2 = n2-1 & f.x2 = a|^y2 by A1,C;
n1 <= m & n2 <= m by C,A1,FINSEQ_1:1; then
A4: y1 < m - 1 + 1 & y2 < m - 1 + 1 by A3,A2,XREAL_1:9,NAT_1:13;
A5: y1 <> y2 by A1,A2,A3;
A6: y1 <= n & y2 <= n by A4,NAT_1:13;
per cases by A5,XXREAL_0:1;
suppose y1 < y2;
hence contradiction by U,A1,A2,A3,A6;
end;
suppose y1 > y2;
hence contradiction by U,A1,A2,A3,A6;
end;
end;
then card M = card(Seg m) by A,C,CARD_1:70 .= m by FINSEQ_1:57;
hence thesis;
end;
then card M > n by NAT_1:13;
then M is linearly-dependent by H,AS,lemlin;
then consider l being Linear_Combination of M such that
D1: Sum(l) = 0.V & Carrier(l) <> {} by VECTSP_7:def 1;
set z = the Element of Carrier(l);
consider v being Element of V such that
D2: z = v & l.v <> 0.F by D1,VECTSP_6:1;
H1: M = {a1|^i where i is Element of NAT : i <= n}
proof
V: FAdj(F,{a}) is Subring of E by FIELD_5:12;
A: now let o be object;
assume o in M; then
consider i being Element of NAT such that B: o = a|^i & i <= n;
a|^i = a1|^i by V,pr5;
hence o in {a1|^i where i is Element of NAT : i <= n} by B;
end;
now let o be object;
assume o in {a1|^i where i is Element of NAT : i <= n}; then
consider i being Element of NAT such that B: o = a1|^i & i <= n;
a|^i = a1|^i by V,pr5;
hence o in M by B;
end;
hence thesis by A,TARSKI:2;
end;
H2: for i,j being Element of NAT st i < j & j <= n holds a1|^i <> a1|^j
proof
let i,j be Element of NAT;
assume W: i < j & j <= n;
V: FAdj(F,{a}) is Subring of E by FIELD_5:12;
assume a1|^i = a1|^j;
then a|^i = a1|^j by V,pr5 .= a|^j by V,pr5;
hence thesis by W,U;
end;
I: E is FAdj(F,{a})-extending by FIELD_4:7;
Carrier(l) c= M by VECTSP_6:def 4; then
z in M by D1; then
consider i being Element of NAT such that D3: z = a|^i & i <= n;
FAdj(F,{a}) is Subring of E by FIELD_5:12; then
D3a: a|^i = a1|^i by pr5;
consider pM being Polynomial of F such that
D4a: deg pM <= n &
for i being Element of NAT st i <= n holds pM.i = l.(a1|^i)
by lembasx2;
pM.i <> 0.F by D3a,D3,D2,D4a;
then pM <> 0_.(F); then
reconsider pM as non zero Polynomial of F by UPROOTS:def 5;
reconsider pMC = pM as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
Ext_eval(pMC,a) = Ext_eval(pMC,a1) by I,lemma7
.= 0.V by H1,H2,D1,D4a,lembasx1
.= 0.FAdj(F,{a}) by FIELD_4:def 6
.= 0.E by dFA;
hence a is F-algebraic by alg00;
end;
end;
hence thesis;
end;