:: Normal Extensions
:: by Christoph Schwarzweller
::
:: Received June 30, 2023
:: Copyright (c) 2023-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, STRUCT_0, SUBSET_1,
SUPINF_2, GROUP_6, NAT_1, MESFUNC1, C0SP1, FUNCT_2, UPROOTS, ORDERS_1,
POLYNOM1, POLYNOM2, POLYNOM3, FUNCSDOM, HURWITZ, FINSEQ_1, QUOFIELD,
CARD_3, FDIFF_1, FUNCT_1, RELAT_1, CARD_1, XBOOLE_0, NUMBERS, PRE_POLY,
POLYNOM5, GROUP_1, ZFMISC_1, MOD_4, GLIB_000, REALSET1, PARTFUN1,
ORDINAL1, YELLOW_8, RING_2, RING_3, MSSUBFAM, RLVECT_1, ALGNUM_1,
ARYTM_1, FOMODEL1, FINSET_1, RFINSEQ, LATTICES, XXREAL_0, GAUSSINT,
NEWTON, VECTSP_2, EC_PF_1, FUNCOP_1, XCMPLX_0, FIELD_6, FIELD_8, FUNCT_4,
RING_5, FIELD_1, FIELD_4, FUNCT_7, BINOP_1, FIELD_9, FIELD_10, FIELD_12,
CATALG_1, ORDINAL4, FIELD_13;
notations TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, RELAT_1, RELSET_1, FUNCT_1,
ORDINAL1, FUNCT_2, ZFMISC_1, PARTFUN1, STRUCT_0, CARD_1, NUMBERS,
ENUMSET1, BINOP_1, REALSET1, XCMPLX_0, XXREAL_0, NAT_1, NAT_D, FUNCOP_1,
ORDERS_1, FUNCT_4, FUNCT_7, FINSET_1, PRE_POLY, FINSEQ_1, RFINSEQ,
ALGSEQ_1, POLYNOM1, POLYNOM2, POLYNOM3, POLYNOM4, POLYNOM5, POLYNOM7,
UPROOTS, GROUP_1, GROUP_4, GROUP_6, RECDEF_1, MOD_4, BINOM, ALGSTR_0,
QUOFIELD, RLVECT_1, VECTSP_2, HURWITZ, VECTSP_1, C0SP1, EC_PF_1,
RATFUNC1, GAUSSINT, RING_2, RING_3, RING_4, RING_5, ALGNUM_1, FIELD_1,
FIELD_4, FIELD_5, FIELD_6, FIELD_7, FIELD_8, FIELD_9, FIELD_11, FIELD_12,
FIELD_10;
constructors FINSOP_1, POLYNOM4, FUNCT_7, NAT_D, RATFUNC1, REALSET1, BINOM,
RINGCAT1, ALGSEQ_1, GROUP_4, ALGNUM_1, RING_5, FIELD_8, FIELD_9,
FIELD_11, FIELD_12, ORDERS_1, POLYNOM2, RFINSEQ, RECDEF_1, FIELD_10;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XCMPLX_0, XXREAL_0,
XREAL_0, NAT_1, INT_1, MEMBERED, STRUCT_0, VECTSP_1, FINSEQ_1, ALGSTR_1,
GCD_1, POLYNOM4, VALUED_0, FUNCT_2, ALGSTR_0, POLYNOM3, SUBSET_1,
RLVECT_1, PRE_POLY, FUNCT_1, CARD_1, RINGCAT1, FINSET_1, RATFUNC1,
POLYNOM2, GAUSSINT, RELAT_1, MOD_4, POLYNOM7, RING_2, RING_4, RING_5,
REALSET1, POLYNOM1, POLYNOM5, FIELD_7, FIELD_8, FIELD_12, FIELD_9,
FIELD_4, FIELD_5, FIELD_6, FIELD_10;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
equalities BINOP_1, REALSET1, XCMPLX_0, STRUCT_0, ALGSTR_0, POLYNOM3, FIELD_6,
FUNCOP_1;
expansions STRUCT_0, GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1, TARSKI, GROUP_6,
FUNCT_1, RING_2, FUNCT_2;
theorems C0SP1, SUBSET_1, PARTFUN1, FUNCT_2, TARSKI, FUNCT_1, RELAT_1,
EC_PF_1, POLYNOM4, RING_3, RATFUNC1, UPROOTS, RING_4, RING_5, HURWITZ,
POLYNOM1, XREAL_1, INT_1, BINOM, XBOOLE_0, FUNCT_7, FIELD_4, RING_2,
FUNCOP_1, CARD_1, POLYNOM3, ALGNUM_1, NAT_1, ZFMISC_1, PRE_POLY,
XBOOLE_1, FINSEQ_1, RLVECT_1, REALSET1, STRUCT_0, ORDINAL1, FIELD_1,
ALGSTR_0, FUNCT_4, FIELD_6, POLYNOM2, POLYNOM5, POLYNOM7, PARTFUN2,
ENUMSET1, FIELD_7, FIELD_8, FIELD_9, LIOUVIL2, CARD_2, FIELD_11,
FIELD_12, FINSEQ_5, FIELD_10, FIELD_5, GROUP_1, GROUP_4, GROUP_6, INT_2,
VECTSP_1, VECTSP_2, PBOOLE;
schemes NAT_1, FUNCT_2;
begin :: Preliminaries
definition
let Y be non empty set;
let y1,y2,y3 be Element of Y;
redefine func {y1,y2,y3} -> Subset of Y; :: redefines { (ENUMSET1, definition)
coherence
proof
now let x be object;
assume x in {y1,y2,y3}; then
per cases by ENUMSET1:def 1;
suppose x = y1;
hence x in Y;
end;
suppose x = y2;
hence x in Y;
end;
suppose x = y3;
hence x in Y;
end;
end;
hence thesis by TARSKI:def 3;
end;
end;
T8: for L being non empty ZeroStr, p being Polynomial of L
holds deg p is Element of NAT iff p <> 0_.(L)
proof
let L be non empty ZeroStr;let p be Polynomial of L;
H: deg p = len p - 1 by HURWITZ:def 2;
now assume p <> 0_.(L);
then len p <> 0 by POLYNOM4:5;
then len p + 1 > 0 + 1 by XREAL_1:6;
then len p >= 1 by NAT_1:13;
hence deg p is Element of NAT by H,INT_1:3;
end;
hence thesis by HURWITZ:20;
end;
registration
let R be domRing;
let p,q be constant Polynomial of R;
cluster p *' q -> constant;
coherence
proof
per cases;
suppose p = 0_.R or q = 0_.R;
hence thesis;
end;
suppose A: p <> 0_.R & q <> 0_.R; then
deg p >= 0 & deg q >= 0 by T8; then
B: deg p = 0 & deg q = 0 by RATFUNC1:def 2;
deg(p *' q) = deg p + deg q by A,HURWITZ:23;
hence thesis by B,RATFUNC1:def 2;
end;
end;
end;
registration
let R be Ring;
cluster -> R-homomorphic R-monomorphic for RingExtension of R;
coherence
proof
let T be RingExtension of R; set S = R;
H: S is Subring of T by FIELD_4:def 1;
then rng(id S) c= the carrier of T by C0SP1:def 3;
then reconsider h = id S as
Function of the carrier of S,the carrier of T by FUNCT_2:6;
A:h is additive multiplicative unity-preserving
proof
now let a,b be Element of S;
I: [a,b] in [:the carrier of S,the carrier of S:];
thus h.(a+b)
= ((the addF of T)||(the carrier of S)).(a,b) by H,C0SP1:def 3
.= h.a + h.b by I,FUNCT_1:49;
end;
hence h is additive;
now let a,b be Element of S;
I: [a,b] in [:the carrier of S,the carrier of S:];
thus h.(a*b)
= ((the multF of T)||(the carrier of S)).(a,b) by H,C0SP1:def 3
.= h.a * h.b by I,FUNCT_1:49;
end;
hence h is multiplicative;
thus thesis by H,C0SP1:def 3;
end;
hence T is S-homomorphic;
thus thesis by A,RING_3:def 3;
end;
end;
registration
let F be Field;
let p be non constant Element of the carrier of Polynom-Ring F;
let E be SplittingField of p;
cluster Roots(E,p) -> non empty;
coherence
proof
reconsider p1 = p as Polynomial of F;
p splits_in E by FIELD_8:def 1; then
consider a being non zero Element of E, q being Ppoly of E such that
A: p = a * q by FIELD_4:def 5;
(a*q) is Element of the carrier of Polynom-Ring E by POLYNOM3:def 10; then
Roots(E,p) = Roots(a*q) by A,FIELD_7:13;
hence thesis;
end;
end;
registration
let R be Ring,
S be RingExtension of R,
T be RingExtension of S;
cluster R-fixing for Homomorphism of S,T;
existence
proof
H: S is Subring of T by FIELD_4:def 1;
then rng(id S) c= the carrier of T by C0SP1:def 3;
then reconsider h = id S as
Function of the carrier of S,the carrier of T by FUNCT_2:6;
h is additive multiplicative unity-preserving
proof
now let a,b be Element of S;
I: [a,b] in [:the carrier of S,the carrier of S:];
thus h.(a+b)
= ((the addF of T)||(the carrier of S)).(a,b) by H,C0SP1:def 3
.= h.a + h.b by I,FUNCT_1:49;
end;
hence h is additive;
now let a,b be Element of S;
I: [a,b] in [:the carrier of S,the carrier of S:];
thus h.(a*b)
= ((the multF of T)||(the carrier of S)).(a,b) by H,C0SP1:def 3
.= h.a * h.b by I,FUNCT_1:49;
end;
hence h is multiplicative;
thus thesis by H,C0SP1:def 3;
end;
then reconsider h as Homomorphism of S,T;
now let a be Element of R;
R is Subring of S by FIELD_4:def 1;
then the carrier of R c= the carrier of S by C0SP1:def 3;
hence h.a = a by FUNCT_1:18;
end;
then h is R-fixing by FIELD_8:def 2;
hence thesis;
end;
cluster R-fixing for Monomorphism of S,T;
existence
proof
H: S is Subring of T by FIELD_4:def 1;
then rng(id S) c= the carrier of T by C0SP1:def 3;
then reconsider h = id S as
Function of the carrier of S,the carrier of T by FUNCT_2:6;
h is additive multiplicative unity-preserving
proof
now let a,b be Element of S;
I: [a,b] in [:the carrier of S,the carrier of S:];
thus h.(a+b)
= ((the addF of T)||(the carrier of S)).(a,b) by H,C0SP1:def 3
.= h.a + h.b by I,FUNCT_1:49;
end;
hence h is additive;
now let a,b be Element of S;
I: [a,b] in [:the carrier of S,the carrier of S:];
thus h.(a*b)
= ((the multF of T)||(the carrier of S)).(a,b) by H,C0SP1:def 3
.= h.a * h.b by I,FUNCT_1:49;
end;
hence h is multiplicative;
thus thesis by H,C0SP1:def 3;
end;
then reconsider h = id S as Monomorphism of S,T;
now let a be Element of R;
R is Subring of S by FIELD_4:def 1;
then the carrier of R c= the carrier of S by C0SP1:def 3;
hence h.a = a by FUNCT_1:18;
end;
then h is R-fixing by FIELD_8:def 2;
hence thesis;
end;
end;
theorem Eprod:
for R being Ring,
S being Subring of R
for F being non empty FinSequence of the carrier of R,
G being non empty FinSequence of the carrier of S
st F = G holds Product F = Product G
proof
let R be Ring, S be Subring of R;
let F be non empty FinSequence of the carrier of R,
G be non empty FinSequence of the carrier of S;
assume AS: F = G;
defpred P[Nat] means
for F being non empty FinSequence of the carrier of R,
G being non empty FinSequence of the carrier of S
st len F = $1 & F = G holds Product F = Product G;
A: P[0];
B: now let k be Nat;
assume B0: P[k];
now let F be non empty FinSequence of the carrier of R,
G be non empty FinSequence of the carrier of S;
assume B1: len F = k + 1 & F = G;
consider F1 being FinSequence, x being object such that
B2: F = F1^<*x*> by FINSEQ_1:46;
H: rng F c= the carrier of R by FINSEQ_1:def 4;
rng F1 c= rng F by B2,FINSEQ_1:29; then
reconsider F1 as FinSequence of the carrier of R
by XBOOLE_1:1,H,FINSEQ_1:def 4;
len <*x*> = 1 by FINSEQ_1:40; then
C4: dom F = Seg(len F1 + 1) by B2,FINSEQ_1:def 7;
B4: len F = len F1 + len<*x*> by B2,FINSEQ_1:22
.= len F1 + 1 by FINSEQ_1:39;
B12: 1 <= len F1 + 1 by NAT_1:11;
dom <*x*> = Seg 1 by FINSEQ_1:38; then
B11: 1 in dom <*x*> by FINSEQ_1:3;
D20: x = <*x*>.1
.= F.(len F1 + 1) by B11,B2,FINSEQ_1:def 7; then
B13: x in rng F by B12,C4,FINSEQ_1:1,FUNCT_1:3;
rng F c= the carrier of R by FINSEQ_1:def 4; then
reconsider x as Element of the carrier of R by B13;
consider G1 being FinSequence, y being object such that
D2: G = G1^<*y*> by FINSEQ_1:46;
H: rng G c= the carrier of S by FINSEQ_1:def 4;
rng G1 c= rng G by D2,FINSEQ_1:29; then
reconsider G1 as FinSequence of the carrier of S
by XBOOLE_1:1,H,FINSEQ_1:def 4;
len <*y*> = 1 by FINSEQ_1:40; then
C4: dom G = Seg(len G1 + 1) by D2,FINSEQ_1:def 7;
D4: len G = len G1 + len<*y*> by D2,FINSEQ_1:22
.= len G1 + 1 by FINSEQ_1:39;
B12: 1 <= len G1 + 1 by NAT_1:11;
dom <*y*> = Seg 1 by FINSEQ_1:38; then
B11: 1 in dom <*y*> by FINSEQ_1:3;
D21: y = <*y*>.1
.= G.(len G1 + 1) by B11,D2,FINSEQ_1:def 7; then
B13: y in rng G by B12,C4,FINSEQ_1:1,FUNCT_1:3;
rng G c= the carrier of S by FINSEQ_1:def 4; then
reconsider y as Element of the carrier of S by B13;
B14: G1 = F1
proof
now let k be Nat;
assume 1 <= k & k <= len G1; then
k in Seg(len F1) & k in Seg(len G1) by B1,B4,D4,FINSEQ_1:1; then
K: k in dom F1 & k in dom G1 by FINSEQ_1:def 3;
hence G1.k = F.k by B1,D2,FINSEQ_1:def 7
.= F1.k by K,B2,FINSEQ_1:def 7;
end;
hence thesis by B1,B4,D4,FINSEQ_1:14;
end;
per cases;
suppose F1 is non empty; then
E: Product G1 = Product F1 by B0,B1,B4,B14;
thus Product F
= (Product F1) * x by B2,GROUP_4:6
.= (Product G1) * y by E,B1,B14,D20,D21,FIELD_6:16
.= Product G by D2,GROUP_4:6;
end;
suppose F1 is empty; then
F = <*x*> & G = <*y*> by B14,B2,D2,FINSEQ_1:34; then
Product F = x & Product G = y by GROUP_4:9;
hence Product F = Product G by B1,B14,D20,D21;
end;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(A,B);
consider n being Nat such that H: n = len F;
thus thesis by I,H,AS;
end;
theorem lemNor1dega:
for F being Field
for G being non empty FinSequence of the carrier of Polynom-Ring F
holds Product G = 0_.(F) iff ex i being Element of dom G st G.i = 0_.(F)
proof
let F be Field, G be non empty FinSequence of the carrier of Polynom-Ring F;
A: now assume ex i being Element of dom G st G.i = 0_.(F); then
consider i being Element of dom G such that B: G.i = 0_.(F);
reconsider p = Product(<*G.i*>) as Polynomial of F by POLYNOM3:def 10;
dom G = Seg(len G) by FINSEQ_1:def 3; then
1 <= i & i <= len G by FINSEQ_1:1; then
G = (G|(i-'1)) ^ <*G.i*> ^ (G/^i) by FINSEQ_5:84; then
D: Product G
= Product(G|(i-'1)^<*G.i*>) * Product((G/^i)) by GROUP_4:5
.= (Product(G|(i-'1)) * Product(<*G.i*>)) * Product(G/^i) by GROUP_4:5
.= (Product(<*G.i*>) * Product(G|(i-'1))) * Product(G/^i)
by GROUP_1:def 12
.= Product(<*G.i*>) *(Product(G|(i-'1)) * Product(G/^i))
by GROUP_1:def 3;
reconsider r1 = Product(G|(i-'1)),
r2 = Product(G/^i) as Polynomial of F by POLYNOM3:def 10;
F: p = 0_.(F) by B,GROUP_4:9;
r1 *' r2 = Product(G|(i-'1)) * Product(G/^i) by POLYNOM3:def 10;
hence Product G = (0_.F) *' (r1 *' r2) by F,D,POLYNOM3:def 10
.= 0_.F;
end;
defpred P[Nat] means
for G being non empty FinSequence of the carrier of Polynom-Ring F
st len G = $1 & for i being Element of dom G holds G.i <> 0_.(F)
holds Product G <> 0_.(F);
C: P[1]
proof
now let G be non empty FinSequence of the carrier of Polynom-Ring F;
assume C1: len G = 1 & for i being Element of dom G holds G.i <> 0_.(F);
then C2: G = <*G.1*> by FINSEQ_1:40;
then C3: dom G = Seg 1 by FINSEQ_1:38;
then C4: 1 in dom G by FINSEQ_1:3;
G = <*G/.1*> by C2,C3,PARTFUN1:def 6,FINSEQ_1:3;
then Product G = G/.1 by GROUP_4:9 .= G.1 by C3,PARTFUN1:def 6,FINSEQ_1:3;
hence Product G <> 0_.(F) by C1,C4;
end;
hence thesis;
end;
D: now let k be Nat;
assume 1 <= k;
assume D2: P[k];
now let G be non empty FinSequence of the carrier of Polynom-Ring F;
assume D3: len G = k + 1 &
for i being Element of dom G holds G.i <> 0_.(F);
consider G1 being FinSequence, y being object such that
B2: G = G1^<*y*> by FINSEQ_1:46;
H: rng G c= the carrier of Polynom-Ring F by FINSEQ_1:def 4;
rng G1 c= rng G by B2,FINSEQ_1:29; then
reconsider G1 as FinSequence of the carrier of Polynom-Ring F
by XBOOLE_1:1,H,FINSEQ_1:def 4;
len <*y*> = 1 by FINSEQ_1:40; then
C4: dom G = Seg(len G1 + 1) by B2,FINSEQ_1:def 7;
B12: 1 <= len G1 + 1 by NAT_1:11; then
B21: len G1 + 1 in dom G by C4,FINSEQ_1:1;
dom <*y*> = Seg 1 by FINSEQ_1:38; then
B11: 1 in dom <*y*> by FINSEQ_1:3;
B20: y = <*y*>.1
.= G.(len G1 + 1) by B11,B2,FINSEQ_1:def 7; then
B13: y in rng G by B12,C4,FINSEQ_1:1,FUNCT_1:3;
rng G c= the carrier of Polynom-Ring F by FINSEQ_1:def 4; then
reconsider y as Element of the carrier of Polynom-Ring F by B13;
B3: Product G = (Product G1) * y by B2,GROUP_4:6;
B4: len G = len G1 + len<*y*> by B2,FINSEQ_1:22
.= len G1 + 1 by FINSEQ_1:39;
now assume Product G = 0_.(F); then
Product G = 0.(Polynom-Ring F) by POLYNOM3:def 10; then
per cases by B3,VECTSP_2:def 1;
suppose y = 0.(Polynom-Ring F);
then y = 0_.(F) by POLYNOM3:def 10;
hence contradiction by D3,B20,B21;
end;
suppose D6: Product G1 = 0.(Polynom-Ring F);
D7: Product(<*>(the carrier of Polynom-Ring F)) = 1_(Polynom-Ring F)
by GROUP_4:8; then
D9: G1 is non empty by D6; then
D8: dom G1 <> {};
Product G1 = 0_.(F) by D6,POLYNOM3:def 10; then
consider i being Element of dom G1 such that
D4: G1.i = 0_.(F) by D3,D2,B4,D7;
dom G1 c= dom G by B2,FINSEQ_1:26; then
D5: i in dom G & i in dom G1 by D8;
G1.i = G.i by D9,B2,FINSEQ_1:def 7;
hence contradiction by D3,D4,D5;
end;
end;
hence Product G <> 0_.(F);
end;
hence P[k+1];
end;
I: for k being Nat st k >= 1 holds P[k] from NAT_1:sch 8(C,D);
now assume B: Product G = 0_.(F);
consider n being Nat such that H: n = len G;
n >= 1 by H,NAT_1:14;
hence ex i being Element of dom G st G.i = 0_.(F) by B,I,H;
end;
hence thesis by A;
end;
theorem lemNor1deg:
for F being Field
for G being non empty FinSequence of the carrier of Polynom-Ring F
st for i being Element of dom G holds G.i <> 0_.(F)
for q being Polynomial of F st q = Product G
for i being Element of dom G,
p being Polynomial of F st p = G.i holds deg p <= deg q
proof
let F be Field;
let G be non empty FinSequence of the carrier of Polynom-Ring F;
assume AS: for i being Element of dom G holds G.i <> 0_.(F);
let q be Polynomial of F;
assume A: q = Product G;
let i be Element of dom G, p be Polynomial of F;
assume B: p = G.i;
dom G = Seg(len G) by FINSEQ_1:def 3; then
1 <= i & i <= len G by FINSEQ_1:1; then
G = (G|(i-'1)) ^ <*G.i*> ^ (G/^i) by FINSEQ_5:84; then
D: Product G
= Product(G|(i-'1)^<*G.i*>) * Product((G/^i)) by GROUP_4:5
.= (Product(G|(i-'1)) * Product(<*G.i*>)) * Product(G/^i) by GROUP_4:5
.= (Product(<*G.i*>) * Product(G|(i-'1))) * Product(G/^i) by GROUP_1:def 12
.= Product(<*G.i*>) *(Product(G|(i-'1)) * Product(G/^i)) by GROUP_1:def 3;
reconsider r1 = Product(G|(i-'1)),
r2 = Product(G/^i) as Polynomial of F by POLYNOM3:def 10;
I: G.i = G/.i by PARTFUN1:def 6; then
E: Product(<*G/.i*>) = p by B,GROUP_4:9;
Z: r1 *' r2 = Product(G|(i-'1)) * Product(G/^i) by POLYNOM3:def 10; then
F: q = p *' (r1 *' r2) by A,D,E,I,POLYNOM3:def 10;
G1: r1 *' r2 = Product(G|(i-'1) ^ (G/^i)) by Z,GROUP_4:5;
per cases;
suppose G|(i-'1) ^ (G/^i) = {};
then G|(i-'1) ^ (G/^i) = <*>(the carrier of Polynom-Ring F);
then Product(G|(i-'1) ^ (G/^i))
= 1_(Polynom-Ring F) by GROUP_4:8
.= 1_.F by POLYNOM3:def 10;
hence thesis by F,G1;
end;
suppose S: G|(i-'1) ^ (G/^i) <> {};
G: r1 *' r2 <> 0_.F
proof
now let j be Element of dom(G|(i-'1) ^ (G/^i));
per cases by S,FINSEQ_1:25;
suppose T: j in dom(G|(i-'1));
G3: G|(i-'1) = G|Seg(i-'1) by FINSEQ_1:def 16;
G2: dom(G|(i-'1)) c= dom G by FINSEQ_5:18;
(G|(i-'1) ^ (G/^i)).j = (G|(i-'1)).j by T,FINSEQ_1:def 7
.= G.j by T,G3,FUNCT_1:47;
hence (G|(i-'1) ^ (G/^i)).j <> 0_.(F) by T,G2,AS;
end;
suppose ex n being Nat st n in dom(G/^i) & j = len (G|(i-'1)) + n;
then consider n being Nat such that
G2: n in dom(G/^i) & j = len (G|(i-'1)) + n;
G3: i + n in dom G by G2,FINSEQ_5:26;
(G|(i-'1) ^ (G/^i)).j = (G/^i).n by G2,FINSEQ_1:def 7
.= G.(i+n) by G2,FINSEQ_5:27;
hence (G|(i-'1) ^ (G/^i)).j <> 0_.(F) by G3,AS;
end;
end;
hence thesis by S,G1,lemNor1dega;
end; then
H: deg(r1*'r2) is Nat by T8;
p <> 0_.F by B,AS; then
deg q = deg p + deg(r1*'r2) by F,G,HURWITZ:23;
hence deg p <= deg q by H,INT_1:6;
end;
end;
theorem lemNor1b:
for F being Field,
E being FieldExtension of F
for G being non empty FinSequence of the carrier of Polynom-Ring F
for q being Polynomial of F st q = Product G
for a being Element of E
st ex i being Element of dom G,
p being Polynomial of F st p = G.i & Ext_eval(p,a) = 0.E
holds Ext_eval(q,a) = 0.E
proof
let F be Field, E be FieldExtension of F;
let G be non empty FinSequence of the carrier of Polynom-Ring F;
let q be Polynomial of F;
assume A: q = Product G;
let a be Element of E;
assume ex i being Element of dom G,
p being Polynomial of F st p = G.i & Ext_eval(p,a) = 0.E; then
consider i being Element of dom G, p being Polynomial of F such that
B: p = G.i & Ext_eval(p,a) = 0.E;
H: F is Subring of E by FIELD_4:def 1;
dom G = Seg(len G) by FINSEQ_1:def 3; then
1 <= i & i <= len G by FINSEQ_1:1; then
G = (G|(i-'1)) ^ <*G.i*> ^ (G/^i) by FINSEQ_5:84; then
D: Product G
= Product(G|(i-'1)^<*G.i*>) * Product((G/^i)) by GROUP_4:5
.= (Product(G|(i-'1)) * Product(<*G.i*>)) * Product(G/^i) by GROUP_4:5
.= (Product(<*G.i*>) * Product(G|(i-'1))) * Product(G/^i) by GROUP_1:def 12
.= Product(<*G.i*>) *(Product(G|(i-'1)) * Product(G/^i)) by GROUP_1:def 3;
reconsider r1 = Product(G|(i-'1)),
r2 = Product(G/^i) as Polynomial of F by POLYNOM3:def 10;
I: G.i = G/.i by PARTFUN1:def 6; then
E: Product(<*G/.i*>) = p by B,GROUP_4:9;
r1 *' r2 = Product(G|(i-'1)) * Product(G/^i) by POLYNOM3:def 10; then
q = p *'(r1 *' r2) by A,D,E,I,POLYNOM3:def 10;
hence Ext_eval(q,a)
= 0.E * Ext_eval(r1*'r2,a) by B,H,ALGNUM_1:20
.= 0.E;
end;
theorem lemNor1ah:
for F being Field
for G being non empty FinSequence of the carrier of Polynom-Ring F
for q being non constant Polynomial of F st q = Product G
holds q splits_in F iff
for i being Element of dom G, p being Polynomial of F
st p = G.i holds p is constant or p splits_in F
proof
let F be Field;
let G be non empty FinSequence of the carrier of Polynom-Ring F;
let q be non constant Polynomial of F;
assume AS: q = Product G;
A: now assume A1: q splits_in F;
now let i be Element of dom G, p being Polynomial of F;
assume H2: p = G.i;
H5: G.i = G/.i by PARTFUN1:def 6; then
H4: p = Product <*G/.i*> by H2,GROUP_4:9;
reconsider r1 = Product(G|(i-'1)),
r2 = Product(G/^i) as Polynomial of F by POLYNOM3:def 10;
dom G = Seg(len G) by FINSEQ_1:def 3; then
1 <= i & i <= len G by FINSEQ_1:1; then
G = (G|(i-'1)) ^ <*G.i*> ^ (G/^i) by FINSEQ_5:84; then
H9: Product G
= Product(G|(i-'1)^<*G.i*>) * Product((G/^i)) by GROUP_4:5
.= (Product(G|(i-'1)) * Product(<*G.i*>)) * Product((G/^i))
by GROUP_4:5;
Product(G|(i-'1)) * Product(<*G.i*>) = r1 *' p by H4,H5,POLYNOM3:def 10;
then q = (p *' r1) *' r2 by AS,H9,POLYNOM3:def 10
.= p *' (r1 *' r2) by POLYNOM3:33; then
(r1 *' r2) is non zero & p *' (r1 *' r2) splits_in F by A1;
hence p is constant or p splits_in F by FIELD_8:11;
end;
hence for i being Element of dom G, p being Polynomial of F
st p = G.i holds p is constant or p splits_in F;
end;
now assume C: for i being Element of dom G, p being Polynomial of F
st p = G.i holds p is constant or p splits_in F;
defpred P[Nat] means
for G being FinSequence of the carrier of Polynom-Ring F
st len G = $1
for q being non constant Polynomial of F
st q = Product G &
for i being Element of dom G, p being Polynomial of F
st p = G.i holds p is constant or p splits_in F
holds q splits_in F;
A: P[0]
proof
now let G be FinSequence of the carrier of Polynom-Ring F;
assume A0: len G = 0;
let q be non constant Polynomial of F;
assume A1: q = Product G &
for i being Element of dom G, p being Polynomial of F
st p = G.i holds p is constant or p splits_in F;
G = <*>(the carrier of Polynom-Ring F) by A0;
then Product G = 1_(Polynom-Ring F) by GROUP_4:8
.= 1_.F by POLYNOM3:def 10;
hence q splits_in F by A1;
end;
hence thesis;
end;
B: now let k be Nat;
assume IV: P[k];
now let G be FinSequence of the carrier of Polynom-Ring F;
assume B0: len G = k+1;
let q be non constant Polynomial of F;
assume B1: q = Product G &
for i being Element of dom G, p being Polynomial of F
st p = G.i holds p is constant or p splits_in F;
G <> {} by B0;
then consider G1 being FinSequence, y being object such that
B2: G = G1^<*y*> by FINSEQ_1:46;
H: rng G c= the carrier of Polynom-Ring F by FINSEQ_1:def 4;
rng G1 c= rng G by B2,FINSEQ_1:29; then
reconsider G1 as FinSequence of the carrier of Polynom-Ring F
by XBOOLE_1:1,H,FINSEQ_1:def 4;
reconsider r = Product G1 as Polynomial of F by POLYNOM3:def 10;
len <*y*> = 1 by FINSEQ_1:40; then
C4: dom G = Seg(len G1 + 1) by B2,FINSEQ_1:def 7;
B12: 1 <= len G1 + 1 by NAT_1:11;
dom <*y*> = Seg 1 by FINSEQ_1:38; then
B11: 1 in dom <*y*> by FINSEQ_1:3;
y = <*y*>.1
.= G.(len G1 + 1) by B11,B2,FINSEQ_1:def 7; then
B13: y in rng G by B12,C4,FINSEQ_1:1,FUNCT_1:3;
rng G c= the carrier of Polynom-Ring F by FINSEQ_1:def 4; then
reconsider y as Element of the carrier of Polynom-Ring F by B13;
set G2 = <*y*>;
reconsider p = Product G2 as Polynomial of F by POLYNOM3:def 10;
reconsider p1 = p, r1 = r as Element of the carrier of Polynom-Ring F;
B3: q = (Product G1) * y by B1,B2,GROUP_4:6
.= r1 * p1 by GROUP_4:9
.= r *' p by POLYNOM3:def 10;
B4: len G = len G1 + len<*y*> by B2,FINSEQ_1:22
.= len G1 + 1 by FINSEQ_1:39;
per cases;
suppose dom G1 = {}; then
V4: G1 = {}; then
V2: G = <*y*> by B2,FINSEQ_1:34;
V1: y = <*y*>.1
.= G.(len G1 + 1) by B11,B2,FINSEQ_1:def 7;
dom G = Seg 1 by V2,FINSEQ_1:38; then
len G1 + 1 in dom G by V4,FINSEQ_1:1;
hence q splits_in F by B1,V1,V2,GROUP_4:9;
end;
suppose V: dom G1 <> {};
B6: now let i be Element of dom G1, p being Polynomial of F;
assume p = G1.i;
then B7: p = G.i by V,B2,FINSEQ_1:def 7;
dom G1 c= dom G by B2,FINSEQ_1:26; then
i in dom G by V;
hence p is constant or p splits_in F by B1,B7;
end;
B10: now let i be Element of dom G2, p being Polynomial of F;
assume p = G2.i;
then C2: p = G.(len G1 + i) by B2,FINSEQ_1:def 7;
dom G2 = {1} by FINSEQ_1:38,FINSEQ_1:2; then
C3: i = 1 by TARSKI:def 1;
len G2 = 1 by FINSEQ_1:40; then
C4: dom G = Seg(len G1 + 1) by B2,FINSEQ_1:def 7;
1 <= len G1 + 1 by NAT_1:11; then
len G1 + i in dom G by C4,C3,FINSEQ_1:1;
hence p is constant or p splits_in F by B1,C2;
end;dom G2 = Seg 1 by FINSEQ_1:38; then
B11: 1 in dom G2 by FINSEQ_1:3;
G2.1 = y .= p by GROUP_4:9; then
per cases by B10,B11;
suppose C: p is constant;
then deg p <= 0 by RATFUNC1:def 2;
then consider b being Element of F such that
B9: p1 = b|F by RING_4:20,RING_4:def 4;
b <> 0.F by B3,B9; then
reconsider b as non zero Element of F by STRUCT_0:def 12;
per cases;
suppose r is non constant; then
consider a being non zero Element of F, u being Ppoly of F such that
B8: r = a * u by B0,B4,B6,IV,FIELD_4:def 5;
q = (b * 1_.(F)) *' (a * u) by B3,B8,B9,RING_4:16
.= b * ((a * u) *' 1_.(F)) by RING_4:10
.= (b * a) * u by RING_4:11;
hence q splits_in F by FIELD_4:def 5;
end;
suppose r is constant;
hence q splits_in F by C,B3;
end;
end;
suppose C1: p splits_in F;
per cases;
suppose r is non constant;
then r splits_in F by B4,B6,B0,IV;
hence q splits_in F by B3,C1,FIELD_8:12;
end;
suppose r is constant;
then deg r <= 0 by RATFUNC1:def 2;
then consider b being Element of F such that
C2: r1 = b|F by RING_4:20,RING_4:def 4;
b <> 0.F by B3,C2; then
reconsider b as non zero Element of F by STRUCT_0:def 12;
consider a being non zero Element of F, u being Ppoly of F such that
C3: p = a * u by C1,FIELD_4:def 5;
q = (a * u) *' (b * 1_.(F)) by B3,C3,C2,RING_4:16
.= b * ((a * u) *' 1_.(F)) by RING_4:10
.= (b * a) * u by RING_4:11;
hence q splits_in F by FIELD_4:def 5;
end;
end;
end;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(A,B);
consider n being Nat such that H: len G = n;
thus q splits_in F by C,I,H,AS;
end;
hence thesis by A;
end;
theorem lemNor1a:
for F being Field,
E being FieldExtension of F
for G being non empty FinSequence of the carrier of Polynom-Ring F
for q being non constant Polynomial of F st q = Product G
holds q splits_in E iff
for i being Element of dom G, p being Polynomial of F
st p = G.i holds p is constant or p splits_in E
proof
let F be Field, E be FieldExtension of F;
let G be non empty FinSequence of the carrier of Polynom-Ring F;
let q be non constant Polynomial of F;
assume AS: q = Product G;
J: the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E &
q in the carrier of Polynom-Ring F by FIELD_4:10,POLYNOM3:def 10; then
reconsider q1 = q as Polynomial of E by POLYNOM3:def 10;
H: q is Element of the carrier of Polynom-Ring F &
q1 is Element of the carrier of Polynom-Ring E by POLYNOM3:def 10;
deg q > 0 by RATFUNC1:def 2; then
deg q1 > 0 by H,FIELD_4:20; then
reconsider q1 as non constant Polynomial of E by RATFUNC1:def 2;
rng G c= the carrier of Polynom-Ring F by FINSEQ_1:def 4; then
rng G c= the carrier of Polynom-Ring E by J; then
reconsider G1 = G as non empty
FinSequence of the carrier of Polynom-Ring E by FINSEQ_1:def 4;
Polynom-Ring F is Subring of Polynom-Ring E by FIELD_4:def 1; then
B: Product G1 = Product G by Eprod;
A: now assume q splits_in E; then
consider a being non zero Element of E, q2 being Ppoly of E such that
A3: q = a * q2 by FIELD_4:def 5;
A1: q1 splits_in E by A3,FIELD_4:def 5;
now let i be Element of dom G, p be Polynomial of F;
assume A2: p = G.i;
reconsider p1 = p as Polynomial of E by FIELD_4:8;
H: p is Element of the carrier of Polynom-Ring F &
p1 is Element of the carrier of Polynom-Ring E by POLYNOM3:def 10;
per cases by B,A1,A2,AS,lemNor1ah;
suppose p1 is constant; then
deg p1 <= 0 by RATFUNC1:def 2; then
deg p <= 0 by H,FIELD_4:20;
hence p is constant or p splits_in E by RATFUNC1:def 2;
end;
suppose p1 splits_in E; then
consider b being non zero Element of E, p2 being Ppoly of E such that
A4: p1 = b * p2 by FIELD_4:def 5;
thus p is constant or p splits_in E by A4,FIELD_4:def 5;
end;
end;
hence for i being Element of dom G, p being Polynomial of F
st p = G.i holds p is constant or p splits_in E;
end;
now assume A1: for i being Element of dom G, p being Polynomial of F
st p = G.i holds p is constant or p splits_in E;
now let i be Element of dom G1, p be Polynomial of E;
assume A2: p = G1.i; then
p = G/.i by PARTFUN1:def 6; then
p is Element of the carrier of Polynom-Ring F; then
reconsider p1 = p as Polynomial of F;
H: p1 is Element of the carrier of Polynom-Ring F &
p is Element of the carrier of Polynom-Ring E by POLYNOM3:def 10;
per cases by A1,A2;
suppose p1 is constant; then
deg p1 <= 0 by RATFUNC1:def 2; then
deg p <= 0 by H,FIELD_4:20;
hence p is constant or p splits_in E by RATFUNC1:def 2;
end;
suppose p1 splits_in E; then
consider b being non zero Element of E, p2 being Ppoly of E such that
A4: p1 = b * p2 by FIELD_4:def 5;
thus p is constant or p splits_in E by A4,FIELD_4:def 5;
end;
end;
then q1 splits_in E by B,AS,lemNor1ah; then
consider a being non zero Element of E, q2 being Ppoly of E such that
A3: q1 = a * q2 by FIELD_4:def 5;
thus q splits_in E by A3,FIELD_4:def 5;
end;
hence thesis by A;
end;
theorem F811:
for F being Field,
E being FieldExtension of F
for p being non constant Polynomial of F
for q being non zero Polynomial of F
st p *' q splits_in E holds p splits_in E
proof
let F be Field, E be FieldExtension of F;
let p be non constant Polynomial of F;
let q be non zero Polynomial of F;
assume p *' q splits_in E; then
consider b being non zero Element of E, s being Ppoly of E such that
A: p *' q = b * s by FIELD_4:def 5;
B: F is Subring of E by FIELD_4:def 1; then
reconsider p1 = p, q1 = q as Polynomial of E by FIELD_4:9;
p is Element of the carrier of Polynom-Ring F &
p1 is Element of the carrier of Polynom-Ring E by POLYNOM3:def 10; then
deg p > 0 & deg p = deg p1 by RATFUNC1:def 2,FIELD_4:20; then
reconsider p1 as non constant Polynomial of E by RATFUNC1:def 2;
q <> 0_.(F) & 0_.(E) = 0_.(F) by B,C0SP1:def 3;
then reconsider q1 as non zero Polynomial of E by UPROOTS:def 5;
p *' q = p1 *' q1 by FIELD_4:17;
then p1 splits_in E by A,FIELD_4:def 5,FIELD_8:11;
then consider a being non zero Element of E, r being Ppoly of E such that
C: p1 = a * r by FIELD_4:def 5;
thus thesis by C,FIELD_4:def 5;
end;
theorem field426a:
for n being Nat
for F being Field, E being FieldExtension of F,
p being Polynomial of n,F, q being Polynomial of n,E
st p = q holds Support q = Support p
proof
let n be Nat, F be Field, E be FieldExtension of F,
p be Polynomial of n,F, q be Polynomial of n,E;
assume AS: p = q;
H1: F is Subring of E by FIELD_4:def 1;
A: now let o be object;
assume A1: o in Support p; then
reconsider b = o as Element of Bags n;
p.b <> 0.F by A1,POLYNOM1:def 4; then
p.b <> 0.E by H1,C0SP1:def 3;
hence o in Support q by AS,POLYNOM1:def 4;
end;
now let o be object;
assume A1: o in Support q; then
reconsider b = o as Element of Bags n;
q.b <> 0.E by A1,POLYNOM1:def 4; then
q.b <> 0.F by H1,C0SP1:def 3;
hence o in Support p by AS,POLYNOM1:def 4;
end;
hence thesis by A,TARSKI:2;
end;
theorem field426:
for n being Nat
for F being Field, E being FieldExtension of F,
p being Polynomial of n,F, q being Polynomial of n,E,
x being Function of n,E
st p = q holds Ext_eval(p,x) = eval(q,x)
proof
let n be Nat;
let R be Field; let S be FieldExtension of R;
let p be Polynomial of n,R, q be Polynomial of n,S;
let x being Function of n,S;
assume
A1: p = q;
R is Subring of S by FIELD_4:def 1; then
A2: the carrier of R c= the carrier of S by C0SP1:def 3;
consider Fp being FinSequence of the carrier of S such that
A6: Ext_eval(p,x) = Sum Fp & len Fp = len SgmX(BagOrder n, Support p) &
for i being Element of NAT st 1 <= i & i <= len Fp
holds Fp.i = In( (p * SgmX(BagOrder n, Support p)).i, S) *
eval(SgmX(BagOrder n, Support p)/.i,x) by FIELD_11:def 4;
consider Fq being FinSequence of the carrier of S such that
A7: len Fq = len SgmX(BagOrder n, Support q) & eval(q,x) = Sum Fq &
for i being Element of NAT st 1 <= i & i <= len Fq
holds Fq/.i = (q * SgmX(BagOrder n, Support q))/.i *
eval(((SgmX(BagOrder n, Support q))/.i),x)
by POLYNOM2:def 4;
A11: dom Fq = Seg(len SgmX(BagOrder n, Support q)) by A7,FINSEQ_1:def 3
.= Seg(len SgmX(BagOrder n, Support p)) by A1,field426a
.= dom Fp by A6,FINSEQ_1:def 3;
for i being Nat st i in dom Fp holds Fq.i = Fp.i
proof
let i be Nat;
assume
A12: i in dom Fp; then
i in Seg(len Fp) & i in Seg(len Fq) by A11,FINSEQ_1:def 3; then
A13: 1 <= i & i <= len Fp & i <= len Fq by FINSEQ_1:1;
A14: i is Element of NAT by ORDINAL1:def 12;
A15: eval(SgmX(BagOrder n, Support p)/.i,x)
= eval(SgmX(BagOrder n, Support q)/.i,x) by A1,field426a;
A19: dom Fq = Seg(len SgmX(BagOrder n, Support q)) by A7,FINSEQ_1:def 3
.= dom SgmX(BagOrder n, Support q) by FINSEQ_1:def 3; then
A18: i in dom SgmX(BagOrder n, Support q) &
i in dom SgmX(BagOrder n, Support p) by A11,A12,A1,field426a;
dom q = Bags n by FUNCT_2:def 1; then
SgmX(BagOrder n, Support q)/.i in dom q; then
A17: i in dom(q * SgmX(BagOrder n, Support q)) by A19,A11,A12,PARTFUN2:3;
dom p = Bags n by FUNCT_2:def 1; then
SgmX(BagOrder n, Support p)/.i in dom p; then
SgmX(BagOrder n, Support p).i in dom p by A18,PARTFUN1:def 6; then
p.(SgmX(BagOrder n, Support p).i) in rng p by FUNCT_1:3; then
A20: (p * SgmX(BagOrder n, Support p)).i in rng p by A18,FUNCT_1:13;
A21: rng p c= the carrier of R by RELAT_1:def 19;
A16: In( (p * SgmX(BagOrder n, Support p)).i, S)
= (p * SgmX(BagOrder n, Support p)).i by A20,A21,A2,SUBSET_1:def 8
.= (q * SgmX(BagOrder n, Support q)).i by A1,field426a
.= (q * SgmX(BagOrder n, Support q))/.i by A17,PARTFUN1:def 6;
thus Fp.i
= In( (p * SgmX(BagOrder n, Support p)).i, S) *
eval(SgmX(BagOrder n, Support p)/.i,x) by A6,A13,A14
.= Fq/.i by A7,A13,A14,A15,A16
.= Fq.i by A11,A12,PARTFUN1:def 6;
end;
hence thesis by A6,A7,A11,FINSEQ_1:13;
end;
theorem field427:
for n being Nat
for F being Field, E being FieldExtension of F,
a being Element of F, b being Element of E st a = b holds a|(n,F) = b|(n,E)
proof
let n be Nat, F be Field, E be FieldExtension of F,
a be Element of F, b be Element of E;
assume AS: a = b;
set ap = a|(n,F), bp = b|(n,E);
H: F is Subring of E by FIELD_4:def 1;
now let u be bag of n;
per cases;
suppose A: u = EmptyBag n;
hence ap.u = a by POLYNOM7:18 .= bp.u by AS,A,POLYNOM7:18;
end;
suppose A: u <> EmptyBag n;
hence ap.u = 0.F by POLYNOM7:def 7 .= 0.E by H,C0SP1:def 3
.= bp.u by A,POLYNOM7:def 7;
end;
end;
hence thesis;
end;
theorem lemNor1cu:
for F being Field,
E1 being FieldExtension of F
for E2 being Field st E1 == E2 holds E2 is FieldExtension of F
proof
let F be Field, E1 be FieldExtension of F, E2 be Field;
assume E1 == E2; then
A: E1 is Subfield of E2 by FIELD_7:def 2;
F is Subfield of E1 by FIELD_4:7;
then F is Subfield of E2 by A,EC_PF_1:5;
hence thesis by FIELD_4:7;
end;
theorem lemNor1cx:
for F1,F2 being Field
for p being Ppoly of F1 st F1 == F2 holds p is Ppoly of F2
proof
let F1,F2 be Field, p be Ppoly of F1;
assume F1 == F2; then
F1 is Subfield of F2 by FIELD_7:def 2; then
F2 is FieldExtension of F1 by FIELD_4:7;
hence thesis by FIELD_8:24;
end;
theorem lemNor1cv:
for F being Field,
E being FieldExtension of F
for p being Polynomial of F for q being Polynomial of E
for a being Element of F, b being Element of E
st p = q & a = b holds a * p = b * q
proof
let F be Field, E be FieldExtension of F;
let p be Polynomial of F; let q be Polynomial of E;
let a be Element of F, b be Element of E;
assume AS: p = q & a = b; then
A: (a|F) = (b|E) by FIELD_6:23;
thus a * p = (a|F) *' p by FIELD_8:2
.= (b|E) *' q by A,AS,FIELD_4:17
.= b * q by FIELD_8:2;
end;
theorem lemNor1cy:
for F1,F2 being Field
for p being Polynomial of F1 for a being Element of F1
for q being Polynomial of F2 for b being Element of F2
st F1 == F2 holds p = q & a = b implies a * p = b * q
proof
let F1,F2 be Field;
let p be Polynomial of F1; let a be Element of F1;
let q be Polynomial of F2; let b be Element of F2;
assume F1 == F2; then
F1 is Subfield of F2 by FIELD_7:def 2; then
A: F2 is FieldExtension of F1 by FIELD_4:7;
assume p = q & a = b;
hence thesis by A,lemNor1cv;
end;
theorem lemNor1c:
for F being Field,
E1,E2 being FieldExtension of F
for p being Polynomial of F
st E1 == E2 holds p splits_in E1 implies p splits_in E2
proof
let F be Field, E1,E2 be FieldExtension of F, p be Polynomial of F;
assume AS: E1 == E2; then
A: the doubleLoopStr of E1 = the doubleLoopStr of E2 by FIELD_7:def 1;
assume p splits_in E1; then
consider a being non zero Element of E1, q being Ppoly of E1 such that
C: p = a * q by FIELD_4:def 5;
reconsider q1 = q as Ppoly of E2 by AS,lemNor1cx;
reconsider a1 = a as Element of E2 by A;
now assume a1 = 0.E2;
then a1 = 0.E1 by A;
hence contradiction;
end; then
reconsider a1 = a as non zero Element of E2 by STRUCT_0:def 12;
p = a1 * q1 by AS,C,lemNor1cy;
hence p splits_in E2 by FIELD_4:def 5;
end;
helpb:
for R1,R2,R3 being Ring st R1 == R2 & R2 == R3 holds R1 == R3
proof
let R1,R2,R3 be Ring;
assume R1 == R2 & R2 == R3; then
the doubleLoopStr of R1 = the doubleLoopStr of R2 &
the doubleLoopStr of R2 = the doubleLoopStr of R3 by FIELD_7:def 1;
hence thesis by FIELD_7:def 1;
end;
theorem lemNor1d:
for F being Field,
E1,E2 being FieldExtension of F
for p being non constant Element of the carrier of Polynom-Ring F
st E1 == E2 holds E1 is SplittingField of p implies E2 is SplittingField of p
proof
let F be Field, E1,E2 be FieldExtension of F;
let p be non constant Element of the carrier of Polynom-Ring F;
assume AS: E1 == E2;
assume B: E1 is SplittingField of p; then
C: p splits_in E1 by FIELD_8:def 1;
now let E be FieldExtension of F;
assume D: p splits_in E & E is Subfield of E2; then
E2 is FieldExtension of E by FIELD_4:7; then
E1 is FieldExtension of E by AS,lemNor1cu; then
E is Subfield of E1 by FIELD_4:7; then
E == E1 by B,D,FIELD_8:def 1;
hence E == E2 by AS,helpb;
end;
hence thesis by AS,lemNor1c,C,FIELD_8:def 1;
end;
theorem lemNor1e:
for F being Field
for p being linear Element of the carrier of Polynom-Ring F
holds F is SplittingField of p
proof
let F be Field, p be linear Element of the carrier of Polynom-Ring F;
reconsider K = F as FieldExtension of F by FIELD_4:6;
A: deg p = 1 by FIELD_5:def 1;
now let E be FieldExtension of F;
assume p splits_in E & E is Subfield of F; then
E is Subfield of F & F is Subfield of E by FIELD_4:7;
hence E == F by FIELD_7:def 2;
end;
then K is SplittingField of p by A,FIELD_8:def 1,FIELD_4:29;
hence thesis;
end;
registration
let F be Field;
let E be FieldExtension of F;
cluster non empty finite F-algebraic for Subset of E;
existence
proof
set a = the F-algebraic Element of E;
take T = {a};
thus T is non empty;
thus T is finite;
for x being Element of E st x in T holds x is F-algebraic by TARSKI:def 1;
hence thesis by FIELD_7:def 12;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let a be F-algebraic Element of E;
cluster {a} -> F-algebraic for Subset of E;
coherence
proof
for x being Element of E st x in {a} holds x is F-algebraic by TARSKI:def 1;
hence thesis by FIELD_7:def 12;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let T1,T2 be F-algebraic Subset of E;
cluster T1 \/ T2 -> F-algebraic for Subset of E;
coherence
proof
now let x be Element of E;
assume x in T1 \/ T2; then
per cases by XBOOLE_0:def 3;
suppose x in T1;
hence x is F-algebraic by FIELD_7:def 12;
end;
suppose x in T2;
hence x is F-algebraic by FIELD_7:def 12;
end;
end;
hence thesis by FIELD_7:def 12;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
let T1 be F-algebraic Subset of E;
let T2 be Subset of E;
cluster T1 /\ T2 -> F-algebraic for Subset of E;
coherence
proof
now let x be Element of E;
assume x in T1 /\ T2;
then x in T1 by XBOOLE_0:def 4;
hence x is F-algebraic by FIELD_7:def 12;
end;
hence thesis by FIELD_7:def 12;
end;
cluster T1 \ T2 -> F-algebraic for Subset of E;
coherence
proof
now let x be Element of E;
assume x in T1 \ T2;
then x in T1 by XBOOLE_0:def 5;
hence x is F-algebraic by FIELD_7:def 12;
end;
hence thesis by FIELD_7:def 12;
end;
end;
definition
let F be Field,
E be FieldExtension of F;
let T be non empty F-algebraic Subset of E;
redefine mode Element of T -> Element of E; :: redefines Element (SUBSET_1, definition)
coherence by TARSKI:def 3;
end;
registration
let F be Field,
E be FieldExtension of F;
let T be non empty F-algebraic Subset of E;
cluster -> F-algebraic for Element of T;
coherence by FIELD_7:def 12;
end;
definition
let F be Field,
E1,E2 be FieldExtension of F;
let h be Function of E1,E2;
let T be Subset of E1;
redefine func h.:T -> Subset of E2; :: redefines .: (FUNCT_1, redefinition) → .: (RELAT_1, definition)
coherence
proof
now let o be object;
assume o in h.:T; then
consider x being object such that
B: x in dom h & x in T & o = h.x by FUNCT_1:def 6;
thus o in the carrier of E2 by B,FUNCT_2:5;
end;
then h.:T c= the carrier of E2;
hence thesis;
end;
end;
theorem ug1:
for F being Field,
E being FieldExtension of F
for T1 being Subset of E, T2 being Subset of E
for E1 being FieldExtension of FAdj(F,T2), T3 being Subset of E1
st E1 = E & T1 = T3 holds FAdj(F,T1\/T2) = FAdj(FAdj(F,T2),T3)
proof
let F be Field, E be FieldExtension of F;
let T1 be Subset of E, T2 be Subset of E;
let E1 be FieldExtension of FAdj(F,T2), T3 be Subset of E1;
assume AS: E1 = E & T1 = T3;
A1: F is Subfield of FAdj(FAdj(F,T2),T3) by FIELD_4:7;
T1 \/ T2 c= the carrier of FAdj(FAdj(F,T2),T3)
proof
now let o be object;
assume o in T1 \/ T2; then
per cases by XBOOLE_0:def 3;
suppose B1: o in T1;
T1 is Subset of FAdj(FAdj(F,T2),T3) by AS,FIELD_6:35;
hence o in the carrier of FAdj(FAdj(F,T2),T3) by B1;
end;
suppose B1: o in T2;
B2: T2 is Subset of FAdj(F,T2) by FIELD_6:35;
FAdj(F,T2) is Subfield of FAdj(FAdj(F,T2),T3) by FIELD_6:36; then
the carrier of FAdj(F,T2) c= the carrier of FAdj(FAdj(F,T2),T3)
by EC_PF_1:def 1;
hence o in the carrier of FAdj(FAdj(F,T2),T3) by B2,B1;
end;
end;
hence thesis;
end; then
A: FAdj(F,T1\/T2) is Subfield of FAdj(FAdj(F,T2),T3) by AS,A1,FIELD_6:37;
A1: FAdj(F,T2) is Subfield of FAdj(F,T1\/T2) by FIELD_7:10,XBOOLE_1:7;
T2\/T3 is Subset of FAdj(F,T1\/T2) by AS,FIELD_6:35; then
T3 c= the carrier of FAdj(F,T1\/T2) by XBOOLE_1:11; then
FAdj(FAdj(F,T2),T3) is Subfield of FAdj(F,T1\/T2) by A1,AS,FIELD_6:37;
hence thesis by A,EC_PF_1:4;
end;
theorem lemh1:
for F being Field,
E being FieldExtension of F,
K being E-extending FieldExtension of F
for T1 being finite F-algebraic Subset of E,
T2 being Subset of K st T1 = T2 holds FAdj(F,T1) = FAdj(F,T2)
proof
let F be Field, E be FieldExtension of F,
K be E-extending FieldExtension of F;
let T1 be finite F-algebraic Subset of E, T2 be Subset of K;
assume AS: T1 = T2;
defpred P[Nat] means
for T1 being finite F-algebraic Subset of E, T2 be Subset of K
st card T1 = $1 & T1 = T2 holds FAdj(F,T1) = FAdj(F,T2);
A: P[0]
proof
now let T1 be finite F-algebraic Subset of E, T2 be Subset of K;
assume card T1 = 0 & T1 = T2; then
T1 = {} & T2 = {}; then
A1: T1 is Subset of F & T2 is Subset of F by XBOOLE_1:2; then
the doubleLoopStr of FAdj(F,T1)
= the doubleLoopStr of F by FIELD_7:def 1,FIELD_7:3
.= the doubleLoopStr of FAdj(F,T2) by A1,FIELD_7:def 1,FIELD_7:3;
hence FAdj(F,T1) = FAdj(F,T2);
end;
hence thesis;
end;
B: now let k be Nat;
assume B0: P[k];
B1: E is Subfield of K by FIELD_4:7; then
B2: the carrier of E c= the carrier of K by EC_PF_1:def 1;
now let T1 be finite F-algebraic Subset of E, T2 be Subset of K;
assume C0: card T1 = k+1 & T1 = T2; then
reconsider U1 = T1 as non empty finite Subset of E;
set a = the Element of U1;
reconsider V1 = T1 \ {a} as finite F-algebraic Subset of E;
reconsider V2 = T2 \ {a} as Subset of K;
now let o be object;
assume o in {a}; then
o = a by TARSKI:def 1;
hence o in T1;
end; then
{a} c= T1; then
C1: T1 = V1 \/ {a} by XBOOLE_1:45;
a in {a} by TARSKI:def 1; then
not a in V1 by XBOOLE_0:def 5; then
C2: card T1 = card V1 + 1 by C1,CARD_2:41;
now let o be object;
assume o in {a}; then
o = a by TARSKI:def 1;
hence o in T2 by C0;
end; then
{a} c= T2; then
C3: T2 = V2 \/ {a} by XBOOLE_1:45;
C4: FAdj(F,V1) = FAdj(F,V2) by B0,C0,C2;
reconsider b = a as Element of K by B2;
consider p being non zero Polynomial of F such that
B: Ext_eval(p,a) = 0.E by FIELD_6:43;
reconsider p as non zero Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
Ext_eval(p,b) = 0.E by B,FIELD_6:11
.= 0.K by B1,EC_PF_1:def 1; then
reconsider b as F-algebraic Element of K by FIELD_6:43;
reconsider E1 = E as F-extending FieldExtension of FAdj(F,V1)
by FIELD_4:7;
reconsider E2 = K as F-extending FieldExtension of FAdj(F,V2)
by FIELD_4:7;
consider p being non zero Polynomial of F such that
B: Ext_eval(p,a) = 0.E by FIELD_6:43;
reconsider p as non zero Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
the carrier of Polynom-Ring F
c= the carrier of Polynom-Ring FAdj(F,V1) by FIELD_4:10; then
reconsider q = p as Element of the carrier of Polynom-Ring FAdj(F,V1);
C: Polynom-Ring F is Subring of Polynom-Ring FAdj(F,V1) by FIELD_4:def 1;
now assume q is zero;
then q = 0_.FAdj(F,V1) by UPROOTS:def 5
.= 0.(Polynom-Ring FAdj(F,V1)) by POLYNOM3:def 10
.= 0.(Polynom-Ring F) by C,C0SP1:def 3
.= 0_.(F) by POLYNOM3:def 10;
hence contradiction;
end; then
reconsider q as non zero Element of
the carrier of Polynom-Ring FAdj(F,V1);
Ext_eval(q,a) = 0.E1 by B,FIELD_7:15; then
reconsider a1 = a as FAdj(F,V1)-algebraic Element of E1 by FIELD_6:43;
consider p being non zero Polynomial of F such that
B: Ext_eval(p,b) = 0.K by FIELD_6:43;
reconsider p as non zero Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
the carrier of Polynom-Ring F
c= the carrier of Polynom-Ring FAdj(F,V2) by FIELD_4:10; then
reconsider q = p as Element of the carrier of Polynom-Ring FAdj(F,V2);
C: Polynom-Ring F is Subring of Polynom-Ring FAdj(F,V2) by FIELD_4:def 1;
now assume q is zero;
then q = 0_.FAdj(F,V2) by UPROOTS:def 5
.= 0.(Polynom-Ring FAdj(F,V2)) by POLYNOM3:def 10
.= 0.(Polynom-Ring F) by C,C0SP1:def 3
.= 0_.(F) by POLYNOM3:def 10;
hence contradiction;
end; then
reconsider q as non zero Element of
the carrier of Polynom-Ring FAdj(F,V2);
Ext_eval(q,b) = 0.E2 by B,FIELD_7:15; then
reconsider b1 = b as FAdj(F,V2)-algebraic Element of E2 by FIELD_6:43;
thus FAdj(F,T1) = FAdj(FAdj(F,V1),{a1}) by C1,FIELD_7:34
.= FAdj(FAdj(F,V2),{b1}) by C4,FIELD_10:9
.= FAdj(F,T2) by C3,FIELD_7:34;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(A,B);
consider n being Nat such that H: card T1 = n;
thus thesis by H,AS,I;
end;
theorem lemNor3z:
for F1,F2 being Field,
p1 being Element of the carrier of Polynom-Ring F1
for p2 being Element of the carrier of Polynom-Ring F2
for E1 being FieldExtension of F1,
E2 being FieldExtension of F2
st E1 = E2 & p1 = p2 holds Roots(E1,p1) = Roots(E2,p2)
proof
let F1,F2 be Field,
p1 be Element of the carrier of Polynom-Ring F1;
let p2 be Element of the carrier of Polynom-Ring F2;
let E1 be FieldExtension of F1, E2 be FieldExtension of F2;
assume AS: E1 = E2 & p1 = p2;
the carrier of Polynom-Ring F1 c= the carrier of Polynom-Ring E1 by FIELD_4:10;
then reconsider p1a = p1 as Element of the carrier of Polynom-Ring E1;
the carrier of Polynom-Ring F2 c= the carrier of Polynom-Ring E2 by FIELD_4:10;
then
reconsider p2a = p2 as Element of the carrier of Polynom-Ring E2;
H: Roots(E1,p1) = {a where a is Element of E1 : a is_a_root_of p1,E1} &
Roots(E2,p2) = {a where a is Element of E2 : a is_a_root_of p2,E2}
by FIELD_4:def 4;
A: now let o be object;
assume o in Roots(E1,p1);
then consider a1 being Element of E1 such that
B: o = a1 & a1 is_a_root_of p1,E1 by H;
reconsider a2 = a1 as Element of E2 by AS;
0.E2 = Ext_eval(p1,a1) by AS,B,FIELD_4:def 2
.= eval(p1a,a1) by FIELD_4:26
.= Ext_eval(p2,a2) by AS,FIELD_4:26;
then a2 is_a_root_of p2,E2 by FIELD_4:def 2;
hence o in Roots(E2,p2) by B,H;
end;
now let o be object;
assume o in Roots(E2,p2);
then consider a2 being Element of E2 such that
B: o = a2 & a2 is_a_root_of p2,E2 by H;
reconsider a1 = a2 as Element of E1 by AS;
0.E1 = Ext_eval(p2,a2) by AS,B,FIELD_4:def 2
.= eval(p2a,a2) by FIELD_4:26
.= Ext_eval(p1,a1) by AS,FIELD_4:26;
then a1 is_a_root_of p1,E1 by FIELD_4:def 2;
hence o in Roots(E1,p1) by B,H;
end;
hence thesis by A,TARSKI:2;
end;
theorem lemNor3xx:
for F being Field,
E,K being FieldExtension of F,
U1 being FieldExtension of E, U2 being FieldExtension of K
for T1 being Subset of U1, T2 being Subset of U2
st U1 = U2 & T1 = T2 & E == K holds FAdj(E,T1) = FAdj(K,T2)
proof
let F be Field, E,K be FieldExtension of F;
let U1 be FieldExtension of E, U2 be FieldExtension of K;
let T1 be Subset of U1, T2 be Subset of U2;
assume AS: U1 = U2 & T1 = T2 & E == K;
A: FAdj(E,T1) is Subfield of FAdj(K,T2)
proof
FAdj(K,T2) is FieldExtension of E by AS,FIELD_12:37; then
A1: E is Subfield of FAdj(K,T2) by FIELD_4:7;
T1 is Subset of FAdj(K,T2) by AS,FIELD_6:35;
hence thesis by AS,A1,FIELD_6:37;
end;
FAdj(K,T2) is Subfield of FAdj(E,T1)
proof
FAdj(E,T1) is FieldExtension of K by AS,FIELD_12:37; then
A1: K is Subfield of FAdj(E,T1) by FIELD_4:7;
T2 is Subset of FAdj(E,T1) by AS,FIELD_6:35;
hence thesis by AS,A1,FIELD_6:37;
end;
hence thesis by A,EC_PF_1:4;
end;
theorem
for F being Field,
E being FieldExtension of F,
K being E-extending FieldExtension of F
for T1 being Subset of K,
T2 being finite Subset of K
st T1 c= T2 & E == FAdj(F,T1) holds FAdj(E,T2) = FAdj(F,T2)
proof
let F be Field, E be FieldExtension of F, K be E-extending FieldExtension of F;
let T1 be Subset of K, T2 be finite Subset of K;
assume AS: T1 c= T2 & E == FAdj(F,T1); then
reconsider T1 as finite Subset of K;
reconsider K1 = K as FieldExtension of FAdj(F,T1) by FIELD_4:7;
reconsider T3 = T2 as Subset of K1;
FAdj(E,T2) = FAdj(FAdj(F,T1),T3) by AS,lemNor3xx .= FAdj(F,T1\/T2) by ug1;
hence thesis by AS,XBOOLE_1:12;
end;
theorem lemNor32:
for F1 being Field,
p1 being non constant Element of the carrier of Polynom-Ring F1
for F2 being FieldExtension of F1,
p2 being non constant Element of the carrier of Polynom-Ring F2
for E being SplittingField of p2
for T being F1-algebraic Subset of F2 st T c= Roots(E,p2) & F2 == FAdj(F1,T)
holds p1 = p2 implies E is SplittingField of p1
proof
let F1 be Field,
p1 be non constant Element of the carrier of Polynom-Ring F1;
let F2 be FieldExtension of F1,
p2 be non constant Element of the carrier of Polynom-Ring F2;
let E be SplittingField of p2;
let T be F1-algebraic Subset of F2;
assume AS: T c= Roots(E,p2) & F2 == FAdj(F1,T);
reconsider E as F2-extending FieldExtension of F1;
reconsider T as finite F1-algebraic Subset of F2 by AS;
assume A: p2 = p1;
p2 splits_in E by FIELD_8:def 1; then
consider a being non zero Element of E, q being Ppoly of E such that
C: p2 = a * q by FIELD_4:def 5;
D: p1 splits_in E by A,C,FIELD_4:def 5;
E: now let K be Field;
assume p1 splits_in K; then
consider a being non zero Element of K, q being Ppoly of K such that
E: p1 = a * q by FIELD_4:def 5;
thus p2 splits_in K by A,E,FIELD_4:def 5;
end;
now let U being FieldExtension of F1;
assume F1: p1 splits_in U & U is Subfield of E; then
E is FieldExtension of U by FIELD_4:7; then
F3: Roots(E,p1) c= the carrier of U by D,F1,FIELD_8:27;
F1 is Subfield of U by FIELD_4:7; then
F4: FAdj(F1,Roots(E,p1)) is Subfield of U by F1,F3,FIELD_6:37;
reconsider T1 = T as Subset of E by AS,XBOOLE_1:1;
T c= Roots(E,p1) by AS,A,FIELD_8:7; then
F5: FAdj(F1,T1) is Subfield of FAdj(F1,Roots(E,p1)) by FIELD_7:10;
FAdj(F1,T1) = FAdj(F1,T) by lemh1; then
FAdj(F1,T) is Subfield of U by F4,F5,EC_PF_1:5; then
U is FieldExtension of FAdj(F1,T) by FIELD_4:7; then
F6: U is FieldExtension of F2 by AS,FIELD_12:37;
p2 splits_in U by F1,E;
hence E == U by F1,F6,FIELD_8:def 1;
end;
hence thesis by A,C,FIELD_4:def 5,FIELD_8:def 1;
end;
theorem lemNor2bb:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for p being non constant Element of the carrier of Polynom-Ring F
st p splits_in E holds Roots(K,p) = Roots(E,p)
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let p be non constant Element of the carrier of Polynom-Ring F;
assume AS: p splits_in E; then
p splits_in K by FIELD_8:19;
hence thesis by AS,FIELD_8:29;
end;
theorem lemNor3d:
for F1 being Field,
F2 being F1-homomorphic Field
for h being Homomorphism of F1,F2
for a being Element of F1 holds (PolyHom h).(X-a) = X-(h.a)
proof
let F1 be Field, F2 be F1-homomorphic Field;
let h be Homomorphism of F1,F2; let a be Element of F1;
H: X-a = rpoly(1,a) & X-(h.a) = rpoly(1,h.a)by FIELD_9:def 2;
now let i be Element of NAT;
per cases;
suppose A: i = 0;
set g1 = power(F1), g2 = power(F2);
thus ((PolyHom h).(X-a)).i
= h.((X-a).i) by FIELD_1:def 2
.= h.(-g1.(a,0+1)) by A,H,HURWITZ:25
.= h.(-(g1.(a,0) * a)) by GROUP_1:def 7
.= h.(-(1_F1 * a)) by GROUP_1:def 7
.= -(1_F2 * h.a) by RING_2:7
.= -(g2.(h.a,0) * h.a) by GROUP_1:def 7
.= -g2.(h.a,0+1) by GROUP_1:def 7
.= (X-(h.a)).i by A,H,HURWITZ:25;
end;
suppose A: i = 1;
thus ((PolyHom h).(X-a)).i
= h.((X-a).i) by FIELD_1:def 2
.= h.(1_F1) by A,H,HURWITZ:25
.= 1_F2 by GROUP_1:def 13
.= (X-(h.a)).i by A,H,HURWITZ:25;
end;
suppose A: i <> 0 & i <> 1;
thus ((PolyHom h).(X-a)).i
= h.((X-a).i) by FIELD_1:def 2
.= h.(0.F1) by A,H,HURWITZ:26
.= 0.F2 by RING_2:6
.= (X-(h.a)).i by A,H,HURWITZ:26;
end;
end;
hence thesis;
end;
theorem lemNor3e:
for F1 being Field,
F2 being F1-isomorphic F1-homomorphic Field
for h being Isomorphism of F1,F2
for E1 being FieldExtension of F1, E2 be FieldExtension of F2
for a being Element of E1, b be Element of E2
for p being irreducible Element of the carrier of Polynom-Ring F1
st Ext_eval(p,a) = 0.E1 & Ext_eval((PolyHom h).p,b) = 0.E2
holds Psi(a,b,h,p).a = b
proof
let F1 be Field,
F2 be F1-isomorphic F1-homomorphic Field;
let h be Isomorphism of F1,F2;
let E1 be FieldExtension of F1, E2 be FieldExtension of F2;
let a be Element of E1, b be Element of E2;
let p be irreducible Element of the carrier of Polynom-Ring F1;
assume AS: Ext_eval(p,a) = 0.E1 & Ext_eval((PolyHom h).p,b) = 0.E2;
F1 is Subfield of E1 by FIELD_4:7; then
I1: 0.E1 = 0.F1 by EC_PF_1:def 1;
H1: X-(0.F1) = rpoly(1,0.F1) by FIELD_9:def 2
.= rpoly(1,0.E1) by I1,FIELD_4:21
.= X-(0.E1) by FIELD_9:def 2;
F2 is Subfield of E2 by FIELD_4:7; then
I2: 0.E2 = 0.F2 by EC_PF_1:def 1;
H2: X-(0.F2) = rpoly(1,0.F2) by FIELD_9:def 2
.= rpoly(1,0.E2) by I2,FIELD_4:21
.= X-(0.E2) by FIELD_9:def 2;
A: (PolyHom h).(X-(0.F1)) = X-(h.(0.F1)) by lemNor3d .= X-(0.F2) by RING_2:6;
B: Ext_eval(X-(0.F1),a)
= eval(X-(0.E1),a) by H1,FIELD_4:26
.= eval(rpoly(1,0.E1),a) by FIELD_9:def 2
.= a - 0.E1 by HURWITZ:29;
Psi(a,b,h,p).Ext_eval(X-(0.F1),a)
= Ext_eval(X-(0.F2),b) by A,AS,FIELD_8:def 10
.= eval(X-(0.E2),b) by H2,FIELD_4:26
.= eval(rpoly(1,0.E2),b) by FIELD_9:def 2
.= b - 0.E2 by HURWITZ:29;
hence thesis by B;
end;
begin :: Preliminaries about Ring Adjunctions
definition
let R1,R2 be Ring;
redefine pred R1 == R2 means :: redefines == (FIELD_7, definition)
R1 is Subring of R2 & R2 is Subring of R1;
correctness
proof
Th0: for F1,F2 being Ring
st F1 is Subring of F2 & F2 is Subring of F1 holds F1 == F2
proof
let F1,F2 be Ring;
assume AS1: F1 is Subring of F2 & F2 is Subring of F1; then
B: 1.F1 = 1.F2 & 0.F1 = 0.F2 by C0SP1:def 3;
D: the carrier of F1 c= the carrier of F2 &
the carrier of F2 c= the carrier of F1 by AS1,C0SP1:def 3; then
E: the carrier of F1 = the carrier of F2 by TARSKI:2;
C: the addF of F1
= (the addF of F2) || the carrier of F1 by AS1,C0SP1:def 3
.= the addF of F2 by E;
the multF of F1
= (the multF of F2) || the carrier of F1 by AS1,C0SP1:def 3
.= the multF of F2 by E; then
the doubleLoopStr of F1 = the doubleLoopStr of F2 by B,C,D,TARSKI:2;
hence thesis by FIELD_7:def 1;
end;
now assume R1 == R2; then
the doubleLoopStr of R1 = the doubleLoopStr of R2
by FIELD_7:def 1; then
A: the carrier of R1 = the carrier of R2 &
the addF of R1 = (the addF of R2) || (the carrier of R1) &
the multF of R1 = (the multF of R2) || (the carrier of R1) &
1.R1 = 1.R2 & 0.R1 = 0.R2;
hence R1 is Subring of R2 by C0SP1:def 3;
thus R2 is Subring of R1 by A,C0SP1:def 3;
end;
hence thesis by Th0;
end;
end;
theorem
for R being Ring holds R == R;
theorem
for R1,R2 being Ring st R1 == R2 holds R2 == R1;
theorem
for R1,R2,R3 being Ring st R1 == R2 & R2 == R3 holds R1 == R3
by helpb;
theorem ext0:
for R being Ring,
S being RingExtension of R
for T1,T2 being Subset of S
st T1 c= T2 holds RAdj(R,T1) is Subring of RAdj(R,T2)
proof
let F be Ring, E be RingExtension of F; let T1,T2 be Subset of E;
assume AS: T1 c= T2;
H: T2 is Subset of RAdj(F,T2) by FIELD_6:30;
now let o be object;
assume o in T1;
then o in T2 by AS;
hence o in the carrier of RAdj(F,T2) by H;
end; then
A: T1 c= the carrier of RAdj(F,T2);
F is Subring of RAdj(F,T2) by FIELD_4:def 1;
hence RAdj(F,T1) is Subring of RAdj(F,T2) by A,FIELD_6:32;
end;
theorem ug:
for R being Ring,
S being RingExtension of R
for T1,T2 being Subset of S
for S1 being RingExtension of RAdj(R,T2), T3 being Subset of S1
st S1 = S & T1 = T3 holds RAdj(R,T1\/T2) = RAdj(RAdj(R,T2),T3)
proof
let F be Ring, E be RingExtension of F; let T1,T2 be Subset of E;
let E1 be RingExtension of RAdj(F,T2), T3 be Subset of E1;
assume AS: E1 = E & T1 = T3;
A1: F is Subring of RAdj(RAdj(F,T2),T3) by FIELD_4:def 1;
T1 \/ T2 c= the carrier of RAdj(RAdj(F,T2),T3)
proof
now let o be object;
assume o in T1 \/ T2; then
per cases by XBOOLE_0:def 3;
suppose B1: o in T1;
T1 is Subset of RAdj(RAdj(F,T2),T3) by AS,FIELD_6:30;
hence o in the carrier of RAdj(RAdj(F,T2),T3) by B1;
end;
suppose B1: o in T2;
B2: T2 is Subset of RAdj(F,T2) by FIELD_6:30;
RAdj(F,T2) is Subring of RAdj(RAdj(F,T2),T3) by FIELD_6:31; then
the carrier of RAdj(F,T2) c= the carrier of RAdj(RAdj(F,T2),T3)
by C0SP1:def 3;
hence o in the carrier of RAdj(RAdj(F,T2),T3) by B2,B1;
end;
end;
hence thesis;
end; then
A: RAdj(F,T1\/T2) is Subring of RAdj(RAdj(F,T2),T3) by AS,A1,FIELD_6:32;
A1: RAdj(F,T2) is Subring of RAdj(F,T1\/T2) by ext0,XBOOLE_1:7;
T2\/T3 is Subset of RAdj(F,T1\/T2) by AS,FIELD_6:30; then
T3 c= the carrier of RAdj(F,T1\/T2) by XBOOLE_1:11; then
RAdj(RAdj(F,T2),T3) is Subring of RAdj(F,T1\/T2) by A1,AS,FIELD_6:32;
hence thesis by A,FIELD_6:12;
end;
theorem helpa:
for R being Ring
for S being RingExtension of R
for T being Subset of S holds RAdj(R,T) == R iff T is Subset of R
proof
let R be Ring, S be RingExtension of R; let T be Subset of S;
set P = RAdj(R,T);
X0: R is Subring of S by FIELD_4:def 1;
X1: R is Subring of R by 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 X0,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 FIELD_6:def 4;
end;
G:now assume B0: T is Subset of R;
now let o be object;
assume o in the carrier of P;
then o in carrierRA(T) by FIELD_6:def 4;
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 X0,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 FIELD_6:def 4 .= 1.R by X0,C0SP1:def 3;
B3: 0.P = 0.S by FIELD_6:def 4 .= 0.R by X0,C0SP1:def 3;
B4: the addF of P = (the addF of S)||carrierRA(T) by FIELD_6:def 4
.= (the addF of S)||the carrier of R by B1,FIELD_6:def 4
.= (the addF of R)||the carrier of R by X0,C0SP1:def 3;
the multF of P = (the multF of S)||carrierRA(T) by FIELD_6:def 4
.= (the multF of S)||the carrier of R by B1,FIELD_6:def 4
.= (the multF of R)||the carrier of R by X0,C0SP1:def 3;
hence RAdj(R,T) == R by B1,B2,B3,B4,FIELD_7:def 1;
end;
now assume RAdj(R,T) == R; then
the doubleLoopStr of RAdj(R,T) = the doubleLoopStr of R by FIELD_7:def 1;
hence T is Subset of R by FIELD_6:30;
end;
hence thesis by G;
end;
definition
let n be Nat;
let R,S be non degenerated comRing;
let x be Function of n,S;
func hom_Ext_eval(x,R) -> Function of Polynom-Ring(n,R),S means :dh:
for p being Polynomial of n,R holds it.p = Ext_eval(p,x);
existence
proof
defpred P[set,set] means ex p be Polynomial of n,R st p = $1 &
$2 = Ext_eval(p,x);
A1: for y be Element of the carrier of Polynom-Ring(n,R)
ex z be Element of S st P[y,z]
proof
let y be Element of the carrier of Polynom-Ring(n,R);
reconsider p = y as Polynomial of n,R by POLYNOM1:def 11;
take Ext_eval(p,x);
take p;
thus thesis;
end;
consider f be Function of Polynom-Ring(n,R), S such that
A2: for y be Element of Polynom-Ring(n,R) holds P[y,f.y]
from FUNCT_2:sch 3 (A1);
reconsider f as Function of Polynom-Ring(n,R), S;
take f;
let p be Polynomial of n,R;
p in Polynom-Ring(n,R) by POLYNOM1:def 11; then
ex q be Polynomial of n,R st q = p & f.p = Ext_eval(q,x) by A2;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function of Polynom-Ring(n,R), S such that
A3: for p be Polynomial of n,R holds f1.p = Ext_eval(p,x) and
A4: for p be Polynomial of n,R holds f2.p = Ext_eval(p,x);
now
let y be Element of Polynom-Ring(n,R);
reconsider p=y as Polynomial of n,R by POLYNOM1:def 11;
thus f1.y = Ext_eval(p,x) by A3 .= f2.y by A4;
end;
hence f1 = f2;
end;
end;
registration
let n be Nat;
let R be non degenerated comRing,
S be comRingExtension of R;
let x be Function of n,S;
cluster hom_Ext_eval(x,R) -> additive multiplicative unity-preserving;
coherence
proof
set g = hom_Ext_eval(x,R);
H: R is Subring of S by FIELD_4:def 1;
now let x1,x2 be Element of Polynom-Ring(n,R);
reconsider p = x1, q = x2 as Polynomial of n,R by POLYNOM1:def 11;
thus g.(x1+x2) = g.(p+q) by POLYNOM1:def 11
.= Ext_eval(p+q,x) by dh
.= Ext_eval(p,x) + Ext_eval(q,x) by H,FIELD_11:19
.= g.x1 + Ext_eval(q,x) by dh
.= g.x1 + g.x2 by dh;
end;
hence g is additive;
now let x1,x2 be Element of Polynom-Ring(n,R);
reconsider p = x1, q = x2 as Polynomial of n,R by POLYNOM1:def 11;
thus g.(x1*x2) = g.(p*'q) by POLYNOM1:def 11
.= Ext_eval(p*'q,x) by dh
.= Ext_eval(p,x) * Ext_eval(q,x) by H,FIELD_11:20
.= g.x1 * Ext_eval(q,x) by dh
.= g.x1 * g.x2 by dh;
end;
hence g is multiplicative;
g.(1_(Polynom-Ring(n,R)))
= g.(1_(n,R)) by POLYNOM1:def 11
.= Ext_eval(1_(n,R),x) by dh
.= 1_S by H,FIELD_11:17;
hence g is unity-preserving;
end;
end;
theorem helpp:
for n being Nat
for F being Field
for E being FieldExtension of F holds E is (Polynom-Ring(n,F))-homomorphic
proof
let n be Nat, F be Field, E be FieldExtension of F;
set x = the Function of n,E;
hom_Ext_eval(x,F) is RingHomomorphism;
hence thesis;
end;
registration
let n be Nat;
let F be Field;
cluster (Polynom-Ring(n,F))-homomorphic for FieldExtension of F;
existence
proof
set E = the FieldExtension of F;
E is (Polynom-Ring(n,F))-homomorphic by helpp;
hence thesis;
end;
end;
theorem lemphi1:
for n being Nat
for F,E being Field
for x being Function of n,E
holds rng hom_Ext_eval(x,F)
= the set of all Ext_eval(p,x) where p is Polynomial of n,F
proof
let n be Nat, F,E be Field, x be Function of n,E;
set g = hom_Ext_eval(x,F);
A: now let o be object;
assume o in rng g; then
consider p being object such that A1: p in dom g & o = g.p
by FUNCT_1:def 3;
reconsider p as Element of the carrier of Polynom-Ring(n,F) by A1;
reconsider p as Polynomial of n,F by POLYNOM1:def 11;
o = Ext_eval(p,x) by A1,dh;
hence o in the set of all Ext_eval(p,x) where p is Polynomial of n,F;
end;
now let o be object;
assume o in the set of all Ext_eval(p,x)
where p is Polynomial of n,F;
then consider p being Polynomial of n,F such that
A2: o = Ext_eval(p,x);
A3: g.p = o by A2,dh;
A4: dom g = the carrier of Polynom-Ring(n,F) by FUNCT_2:def 1;
p is Element of the carrier of Polynom-Ring(n,F)
by POLYNOM1:def 11;
hence o in rng g by A3,A4,FUNCT_1:3;
end;
hence thesis by A,TARSKI:2;
end;
T0: for n be Nat, F be Field, E be FieldExtension of F,
x be Function of n,E holds 0.E in rng hom_Ext_eval(x,F)
proof
let n be Nat, F be Field, E be FieldExtension of F, x be Function of n,E;
set f = hom_Ext_eval(x,F);
A: f.(0.Polynom-Ring(n,F)) = 0.E by RING_2:6;
dom f = the carrier of Polynom-Ring(n,F) by FUNCT_2:def 1;
hence 0.E in rng hom_Ext_eval(x,F) by A,FUNCT_1:def 3;
end;
T1: for n be Nat, F be Field, E be FieldExtension of F,
x be Function of n,E holds 1.E in rng hom_Ext_eval(x,F)
proof
let n be Nat, F be Field, E be FieldExtension of F, x be Function of n,E;
set f = hom_Ext_eval(x,F);
A: f.(1_Polynom-Ring(n,F)) = 1_E by GROUP_1:def 13 .= 1.E;
dom f = the carrier of Polynom-Ring(n,F) by FUNCT_2:def 1;
hence 1.E in rng f by A,FUNCT_1:def 3;
end;
T3: for n be Nat, F be Field, E be FieldExtension of F,
x be Function of n,E
holds rng hom_Ext_eval(x,F) is Preserv of the addF of E
proof
let n be Nat, F be Field, E be FieldExtension of F, x be Function of n,E;
set f = hom_Ext_eval(x,F);
set A = the addF of E;
reconsider K = rng f as Subset of E by RELAT_1:def 19;
now let x be set;
assume x in [:K,K:];
then consider a,b being object such that
A2: a in K and
A3: b in K and
A4: x = [a,b] by ZFMISC_1:def 2;
consider a1 being Element of E such that
A5: a1 = a & a1 in rng f by A2;
consider x1 being object such that
A6: x1 in dom f & f.x1 = a1 by A5,FUNCT_1:def 3;
reconsider x1 as Element of Polynom-Ring(n,F) by A6;
consider a2 being Element of E such that
A7: a2 = b & a2 in rng f by A3;
consider x2 being object such that
A8: x2 in dom f & f.x2 = a2 by A7,FUNCT_1:def 3;
reconsider x2 as Element of Polynom-Ring(n,F) by A8;
A9: dom f = the carrier of Polynom-Ring(n,F) by FUNCT_2:def 1;
f.(x1+x2) = a1 + a2 by A8,A6,VECTSP_1:def 20
.= A.x by A4,A5,A7;
hence A.x in rng f by A9,FUNCT_1:def 3;
end;
hence thesis by REALSET1:def 1;
end;
T4: for n be Nat, F be Field, E be FieldExtension of F,
x be Function of n,E
holds rng hom_Ext_eval(x,F) is Preserv of the multF of E
proof
let n be Nat, F be Field, E be FieldExtension of F, x be Function of n,E;
set f = hom_Ext_eval(x,F);
set A = the multF of E;
reconsider K = rng f as Subset of E by RELAT_1:def 19;
now let x be set;
assume x in [:K,K:];
then consider a,b being object such that
A2: a in K and
A3: b in K and
A4: x = [a,b] by ZFMISC_1:def 2;
consider a1 being Element of E such that
A5: a1 = a & a1 in rng f by A2;
consider x1 being object such that
A6: x1 in dom f & f.x1 = a1 by A5,FUNCT_1:def 3;
reconsider x1 as Element of Polynom-Ring(n,F) by A6;
consider a2 being Element of E such that
A7: a2 = b & a2 in rng f by A3;
consider x2 being object such that
A8: x2 in dom f & f.x2 = a2 by A7,FUNCT_1:def 3;
reconsider x2 as Element of Polynom-Ring(n,F) by A8;
A9: dom f = the carrier of Polynom-Ring(n,F) by FUNCT_2:def 1;
f.(x1*x2) = a1 * a2 by A8,A6,GROUP_6:def 6
.= A.x by A4,A5,A7;
hence A.x in rng f by A9,FUNCT_1:def 3;
end;
hence thesis by REALSET1:def 1;
end;
definition
let n be Nat;
let F be Field, E be FieldExtension of F;
let x be Function of n,E;
func Image_hom_Ext_eval(x,F) -> strict doubleLoopStr means :defIm:
the carrier of it = rng hom_Ext_eval(x,F) &
the addF of it = (the addF of E)||(rng hom_Ext_eval(x,F)) &
the multF of it = (the multF of E)||(rng hom_Ext_eval(x,F)) &
the OneF of it = 1.E &
the ZeroF of it = 0.E;
existence
proof
set A = the addF of E;
set M = the multF of E;
reconsider P = rng hom_Ext_eval(x,F) as Preserv of A by T3;
reconsider R = rng hom_Ext_eval(x,F) as Preserv of M by T4;
reconsider O = 1.E as Element of P by T1;
reconsider Z = 0.E as Element of P by T0;
reconsider MP = M||R as BinOp of P;
take doubleLoopStr(#P,A||P,MP,O,Z#);
thus thesis;
end;
uniqueness;
end;
registration
let n be Nat;
let F be Field, E be FieldExtension of F;
let x be Function of n,E;
cluster Image_hom_Ext_eval(x,F) -> non degenerated;
coherence
proof
set R = Image_hom_Ext_eval(x,F);
1.E <> 0.E & 1.R = 1.E & 0.R = 0.E by defIm;
hence thesis;
end;
end;
T5: for n be Nat, F be Field, E be FieldExtension of F,
x be Function of n,E
for a,b be Element of Image_hom_Ext_eval(x,F), x1,x2 be Element of E
st a = x1 & b = x2 holds a + b = x1 + x2 & a * b = x1 * x2
proof
let n be Nat, F be Field, E be FieldExtension of F, x be Function of n,E;
let a,b be Element of Image_hom_Ext_eval(x,F),
x1,x2 be Element of E;
set I = Image_hom_Ext_eval(x,F), f = hom_Ext_eval(x,F);
the carrier of I = rng f by defIm;
then A1: [a,b] in [:rng f,rng f:];
assume AS: a = x1 & b = x2;
(the addF of I).(a,b)
= ((the addF of E)||(rng f)).(a,b) by defIm
.= (the addF of E).(x1,x2) by AS,A1,FUNCT_1:49;
hence a + b = x1 + x2;
(the multF of I).(a,b)
= ((the multF of E)||(rng f)).(a,b) by defIm
.= (the multF of E).(x1,x2) by AS,A1,FUNCT_1:49;
hence a * b = x1 * x2;
end;
T6: for n be Nat, F be Field, E be FieldExtension of F,
x be Function of n,E
for a be Element of Image_hom_Ext_eval(x,F)
ex y being Element of the carrier of Polynom-Ring(n,F)
st hom_Ext_eval(x,F).y = a
proof
let n be Nat, F be Field, E be FieldExtension of F, x be Function of n,E;
let a be Element of Image_hom_Ext_eval(x,F);
set f = hom_Ext_eval(x,F);
the carrier of Image_hom_Ext_eval(x,F) = rng f by defIm;
then ex y being object st y in dom f & f.y = a by FUNCT_1:def 3;
hence thesis;
end;
registration
let n be Nat;
let F be Field, E be FieldExtension of F;
let x be Function of n,E;
cluster Image_hom_Ext_eval(x,F)
-> Abelian add-associative right_zeroed right_complementable;
coherence
proof
set I = Image_hom_Ext_eval(x,F), f = hom_Ext_eval(x,F),
R = Polynom-Ring(n,F);
now let v,w be Element of I;
consider a being Element of R such that A1: f.a = v by T6;
consider b being Element of R such that A2: f.b = w by T6;
thus v + w = f.a + f.b by A1,A2,T5
.= w + v by A1,A2,T5;
end;
hence I is Abelian;
now let u,v,w be Element of I;
consider a being Element of R such that A1: f.a = u by T6;
consider b being Element of R such that A2: f.b = v by T6;
consider c being Element of R such that A3: f.c = w by T6;
A4: v + w = f.b + f.c by A2,A3,T5;
u + v = f.a + f.b by A1,A2,T5;
hence (u + v) + w = (f.a + f.b) + f.c by A3,T5
.= f.a + (f.b + f.c) by RLVECT_1:def 3
.= u + (v + w) by A1,A4,T5;
end;
hence I is add-associative;
now let v be Element of I;
consider a being Element of R such that A1: f.a = v by T6;
0.I = 0.E by defIm; then
v + 0.I = f.a + 0.E by A1,T5
.= f.a;
hence v + 0.I = v by A1;
end;
hence I is right_zeroed;
now let x be Element of I;
consider a being Element of R such that A1: f.a = x by T6;
consider b being Element of R such that A2: a + b = 0.R by ALGSTR_0:def 11;
dom f = the carrier of R by FUNCT_2:def 1;
then f.b in rng f by FUNCT_1:3; then
reconsider y = f.b as Element of I by defIm;
0.I = 0.E by defIm
.= f.(0.R) by RING_2:6
.= f.a + f.b by A2,VECTSP_1:def 20
.= x + y by T5,A1;
hence x is right_complementable;
end;
hence I is right_complementable;
end;
end;
registration
let n be Nat;
let F be Field, E be FieldExtension of F;
let x be Function of n,E;
cluster Image_hom_Ext_eval(x,F)
-> commutative associative well-unital distributive;
coherence
proof
set I = Image_hom_Ext_eval(x,F), f = hom_Ext_eval(x,F),
R = Polynom-Ring(n,F);
now let u,v be Element of I;
consider a being Element of R such that A1: f.a = u by T6;
consider b being Element of R such that A2: f.b = v by T6;
thus u * v = f.a * f.b by A1,A2,T5
.= f.b * f.a by GROUP_1:def 12
.= v * u by A1,A2,T5;
end;
hence I is commutative;
now let u,v,w be Element of I;
consider a being Element of R such that A1: f.a = u by T6;
consider b being Element of R such that A2: f.b = v by T6;
consider c being Element of R such that A3: f.c = w by T6;
A4: v * w = f.b * f.c by A2,A3,T5;
u * v = f.a * f.b by A1,A2,T5;
hence (u * v) * w = (f.a * f.b) * f.c by A3,T5
.= f.a * (f.b * f.c) by GROUP_1:def 3
.= u * (v * w) by A1,A4,T5;
end;
hence I is associative;
now let x be Element of I;
consider a being Element of R such that A1: f.a = x by T6;
A2: 1.E = 1.I by defIm;
thus x * 1.I = f.a * 1.E by A1,A2,T5
.= x by A1;
thus 1.I * x = 1.E * f.a by A1,A2,T5
.= x by A1;
end;
hence I is well-unital;
now let u,v,w be Element of I;
consider a being Element of R such that A1: f.a = u by T6;
consider b being Element of R such that A2: f.b = v by T6;
consider c being Element of R such that A3: f.c = w by T6;
A4: v + w = f.b + f.c by A2,A3,T5;
A5: u * v = f.a * f.b by A1,A2,T5;
A6: u * w = f.a * f.c by A1,A3,T5;
thus u * (v + w) = f.a * (f.b + f.c) by A1,A4,T5
.= f.a * f.b + f.a * f.c by VECTSP_1:def 7
.= u * v + u * w by A5,A6,T5;
A7: v * u = f.b * f.a by A1,A2,T5;
A8: w * u = f.c * f.a by A1,A3,T5;
thus (v + w) * u = (f.b + f.c) * f.a by A1,A4,T5
.= f.b * f.a + f.c * f.a by VECTSP_1:def 7
.= v * u + w * u by A7,A8,T5;
end;
hence I is distributive;
end;
end;
theorem lemphi3:
for n being Nat
for F being Field,
E being FieldExtension of F
for x being Function of n,E holds F is Subring of Image_hom_Ext_eval(x,F)
proof
let n be Nat, F be Field, E be FieldExtension of F, x be Function of n,E;
set R = Image_hom_Ext_eval(x,F), f = hom_Ext_eval(x,F);
U: 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 o be object;
assume o in the carrier of F;
then reconsider b = o as Element of F;
reconsider c = b as Element of E by Y;
reconsider p = b|(n,F) as Element of the carrier of Polynom-Ring(n,F)
by POLYNOM1:def 11;
reconsider q = c|(n,E) as Element of the carrier of Polynom-Ring(n,E)
by POLYNOM1:def 11;
Ext_eval(b|(n,F),x) = eval(c|(n,E),x) by field427,field426
.= b by POLYNOM7:25;
then b in the set of all Ext_eval(p,x) where p is Polynomial of n,F;
hence o in rng hom_Ext_eval(x,F) by lemphi1;
end; then
ZZ: the carrier of F c= rng f;
now let o be object;
assume o in the carrier of F;
then o in rng hom_Ext_eval(x,F) by Z;
hence o in the carrier of R by defIm;
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 defIm
.= (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,U;
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 defIm
.= (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 defIm
.= (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,U;
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 defIm
.= (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 U,C0SP1:def 3 .= 0.R by defIm;
1.F = 1.E by U,C0SP1:def 3 .= 1.R by defIm;
hence thesis by A,B,C,D,C0SP1:def 3;
end;
definition
let F be Field;
let T be finite Subset of F;
let x be Function of (card T),F;
attr x is T-evaluating means :tev:
x is one-to-one & rng x = T;
end;
registration
let F be Field;
let T be finite Subset of F;
cluster T-evaluating for Function of (card T),F;
existence
proof
defpred P[object,object] means
ex n being Nat st $1 = n & $2 = (canFS T).(n+1);
A: now let x be object;
assume A1: x in card T; then
reconsider n = x as Ordinal;
card n in card T by A1,CARD_1:9; then
n is finite by CARD_2:49; then
reconsider n as Nat;
0 <= n & n < card T by A1,FIELD_5:3; then
1 <= n + 1 & n + 1 <= card T by NAT_1:11,NAT_1:13; then
n + 1 in Seg(card T) by FINSEQ_1:1; then
n + 1 in Seg(len(canFS T)) by FINSEQ_1:93; then
n + 1 in dom(canFS T) by FINSEQ_1:def 3; then
A2: (canFS T).(n+1) in rng(canFS T) by FUNCT_1:3;
rng(canFS T) c= T & T c= the carrier of F by FINSEQ_1:def 4; then
reconsider a = (canFS T).(n+1) as Element of F by A2;
thus ex y being object st y in the carrier of F & P[x,y]
proof
take a;
thus thesis;
end;
end;
consider f being Function of card T,the carrier of F such that
B: for n being object st n in card T holds P[n,f.n]
from FUNCT_2:sch 1(A);
C: now let n be Nat;
assume n in dom f;
then consider i being Nat such that
C1: i = n & f.n = (canFS T).(i+1) by B;
thus f.n = (canFS T).(n+1) by C1;
end;
D: now let n being object;
assume n in dom f;
then consider i being Nat such that
D1: i = n & f.n = (canFS T).(i+1) by B;
thus n is Nat by D1;
end;
take f;
G: rng f c= T
proof
now let o be object;
assume o in rng f; then
consider n being object such that
D1: n in dom f & f.n = o by FUNCT_1:def 3;
reconsider n as Nat by D1,D;
D2: f.n = (canFS T).(n+1) by D1,C;
D3: dom(canFS T) = Seg(len(canFS T)) by FINSEQ_1:def 3
.= Seg(card T) by FINSEQ_1:93;
n < card T by D1,FIELD_5:3; then
1 <= n + 1 & n + 1 <= card T by NAT_1:12,NAT_1:13; then
D4: (canFS T).(n+1) in rng(canFS T) by D3,FINSEQ_1:1,FUNCT_1:3;
rng(canFS T) c= T by FINSEQ_1:def 4;
hence o in T by D1,D2,D4;
end;
hence thesis;
end;
E: f is one-to-one
proof
now let x1,x2 be object;
assume E1: x1 in dom f & x2 in dom f & f.x1 = f.x2; then
reconsider n1 = x1, n2 = x2 as Nat by D;
E2: (canFS T).(n1+1) = f.n2 by E1,C .= (canFS T).(n2+1) by E1,C;
E3: dom(canFS T) = Seg(len(canFS T)) by FINSEQ_1:def 3
.= Seg(card T) by FINSEQ_1:93;
n1 < card T by E1,FIELD_5:3; then
1 <= n1 + 1 & n1 + 1 <= card T by NAT_1:12,NAT_1:13; then
E4: n1 + 1 in dom(canFS T) by E3,FINSEQ_1:1;
n2 < card T by E1,FIELD_5:3; then
1 <= n2 + 1 & n2 + 1 <= card T by NAT_1:12,NAT_1:13; then
n2 + 1 in dom(canFS T) by E3,FINSEQ_1:1; then
n1 + 1 = n2 + 1 by E4,E2,FUNCT_1:def 4;
hence x1 = x2;
end;
hence thesis;
end;
now let o be object;
assume o in T; then
o in rng(canFS T) by FUNCT_2:def 3; then
consider n being object such that
F2: n in dom(canFS T) & (canFS T).n = o by FUNCT_1:def 3;
F3: dom(canFS T) = Seg(len(canFS T)) by FINSEQ_1:def 3
.= Seg(card T) by FINSEQ_1:93;
reconsider n as Nat by F2;
F4: 1 <= n & n <= card T by F2,F3,FINSEQ_1:1; then
reconsider n1 = n - 1 as Nat;
n1 + 1 = n; then
n1 < card T by F4,NAT_1:13; then
n1 in card T by FIELD_5:3; then
F5: n1 in dom f by FUNCT_2:def 1; then
f.n1 = (canFS T).(n1+1) by C .= o by F2;
hence o in rng f by F5,FUNCT_1:def 3;
end;
then T c= rng f;
hence thesis by E,G,XBOOLE_0:def 10;
end;
end;
registration
let F be Field;
let T be finite Subset of F;
cluster T-evaluating -> T-valued one-to-one for Function of (card T),F;
coherence by RELAT_1:def 19;
end;
lemphi2ax:
for F being Field,
E being FieldExtension of F
for T being non empty finite Subset of E
for b being bag of (card T)
st ex o being set st support b = {o}
for x being T-evaluating Function of (card T),E
holds eval(b,x) in the carrier of RAdj(F,T)
proof
let F be Field, E be FieldExtension of F, T be non empty finite Subset of E,
b be bag of (card T);
assume AS: ex o being set st support b = {o};
let x be T-evaluating Function of (card T),E;
consider o being set such that A: support b = {o} by AS;
B: T is Subset of RAdj(F,T) by FIELD_6:30;
C: rng x c= T by RELAT_1:def 19;
D: o in support b & support b c= dom b by A,TARSKI:def 1,PRE_POLY:37;
dom b = card T by PARTFUN1:def 2 .= dom x by FUNCT_2:def 1; then
x.o in T by C,D,FUNCT_1:3; then
reconsider a = x.o as Element of RAdj(F,T) by B;
reconsider c = x.o as Element of E by D,FUNCT_2:5;
eval(b,x) = power(E).(x.o,b.o) by A,POLYNOM2:15
.= c|^(b.o) by BINOM:def 2
.= a|^(b.o) by FIELD_6:19
.= power(RAdj(F,T)).(a,b.o) by BINOM:def 2;
hence thesis;
end;
theorem lemphi2a:
for F being Field,
E being FieldExtension of F
for T being non empty finite Subset of E
for b being bag of (card T)
for x being T-evaluating Function of (card T),E
holds eval(b,x) in the carrier of RAdj(F,T)
proof
let F be Field, E be FieldExtension of F, T be non empty finite Subset of E;
let b be bag of (card T), x be T-evaluating Function of (card T),E;
defpred P[Nat] means
for b being bag of (card T) st card(support b) = $1
for x being T-evaluating Function of (card T),E
holds eval(b,x) in the carrier of RAdj(F,T);
set n = card T, R = RAdj(F,T);
H0: 0.E = 0.R & 1.E = 1.R by FIELD_6:def 4;
A: P[0]
proof
now let b be bag of n;
assume A0: card(support b) = 0;
let x be T-evaluating Function of n,E;
now let o be object;
assume o in n;
not o in support b by A0;
hence b.o = {} by PRE_POLY:def 7 .= (EmptyBag n).o by PBOOLE:5;
end; then
b = EmptyBag n by PBOOLE:def 10; then
eval(b,x) = 1.E by POLYNOM2:14;
hence eval(b,x) in the carrier of RAdj(F,T) by H0;
end;
hence thesis;
end;
B: now let k be Nat;
assume IV: P[k];
now let b be bag of n;
assume B0: card(support b) = k+1;
let x be T-evaluating Function of n,E;
set a = the Element of support b;
B3: support b <> {} by B0; then
B1: a in support b & support b c= dom b & dom b c= n by PRE_POLY:37; then
reconsider a as Element of n;
set b1 = b \ a; set b2 = ({a},b.a)-bag;
B2: support b1 = support b \ {a} by RING_5:29;
{a} c= support b by B1,TARSKI:def 1; then
card(support b1)
= card(support b) - card {a} by B2,CARD_2:44
.= (k + 1) - 1 by B0,CARD_2:42; then
reconsider u = eval(b1,x) as Element of RAdj(F,T) by IV;
b.a <> 0 by B3,PRE_POLY:def 7; then
support b2 = {a} by UPROOTS:8; then
reconsider v = eval(b2,x) as Element of RAdj(F,T) by lemphi2ax;
eval(b,x) = eval(b1 + b2,x) by RING_5:30
.= eval(b1,x) * eval(b2,x) by POLYNOM2:16
.= u * v by FIELD_6:16;
hence eval(b,x) in the carrier of RAdj(F,T);
end;
hence P[k+1];
end;
C: for k being Nat holds P[k] from NAT_1:sch 2(A,B);
consider n being Nat such that D: card(support b) = n;
thus thesis by C,D;
end;
Lm7:
for F being Field,
E being FieldExtension of F
for T being non empty finite Subset of E
for p being Polynomial of (card T),F
st (ex b being bag of (card T) st Support p = {b})
for x being T-evaluating Function of (card T),E
holds Ext_eval(p,x) in the carrier of RAdj(F,T)
proof
let F be Field, E be FieldExtension of F, T be non empty finite Subset of E;
let p be Polynomial of (card T),F;
assume AS: (ex b being bag of (card T) st Support p = {b});
let x be T-evaluating Function of (card T),E;
set n = card T;
A0: F is Subring of E by FIELD_4:def 1;
consider y being FinSequence of the carrier of E such that
A2: Ext_eval(p,x) = Sum y & len y = len SgmX(BagOrder n, Support p) &
for i being Element of NAT st 1 <= i & i <= len y
holds y.i = In( (p * SgmX(BagOrder n, Support p)).i, E) *
eval(SgmX(BagOrder n, Support p)/.i,x) by FIELD_11:def 4;
A3: len(SgmX(BagOrder n, Support p))
= card(Support p) by PRE_POLY:11,POLYNOM2:18
.= 1 by AS,CARD_2:42; then
H: 1 in Seg(len y) by A2,FINSEQ_1:1; then
1 in dom y by FINSEQ_1:def 3; then
A5: y.1 = y/.1 by PARTFUN1:def 6;
F is Subring of RAdj(F,T) by FIELD_6:31; then
A8: the carrier of F c= the carrier of RAdj(F,T) by C0SP1:def 3;
dom SgmX(BagOrder n, Support p)
= Seg(len y) by A2,FINSEQ_1:def 3 .= dom y by FINSEQ_1:def 3; then
A9: 1 in dom SgmX(BagOrder n, Support p) by H,FINSEQ_1:def 3;
dom p = Bags n by FUNCT_2:def 1; then
SgmX(BagOrder n, Support p)/.1 in dom p; then
SgmX(BagOrder n, Support p).1 in dom p by A9,PARTFUN1:def 6; then
p.(SgmX(BagOrder n, Support p).1) in rng p by FUNCT_1:3; then
A4: (p * SgmX(BagOrder n, Support p)).1 in rng p by A9,FUNCT_1:13;
A7: rng p c= the carrier of F by RELAT_1:def 19;
the carrier of F c= the carrier of E by A0,C0SP1:def 3; then
A6: In( (p * SgmX(BagOrder n, Support p)).1, E)
= (p * SgmX(BagOrder n, Support p)).1 by A4,A7,SUBSET_1:def 8;
reconsider c = (p * SgmX(BagOrder n, Support p)).1
as Element of RAdj(F,T) by A4,A7,A8;
reconsider a = eval(SgmX(BagOrder n, Support p)/.1,x)
as Element of RAdj(F,T) by lemphi2a;
y = <*y.1*> by A2,A3,FINSEQ_1:40; then
Ext_eval(p,x) = y/.1 by A2,A5,RLVECT_1:44
.= In( (p * SgmX(BagOrder n, Support p)).1, E) *
eval(SgmX(BagOrder n, Support p)/.1,x) by A5,A3,A2
.= c * a by A6,FIELD_6:16;
hence thesis;
end;
theorem lemphi2b:
for F being Field,
E being FieldExtension of F
for T being non empty finite Subset of E
for p being Polynomial of (card T),F
for x being T-evaluating Function of (card T),E
holds Ext_eval(p,x) in the carrier of RAdj(F,T)
proof
let F be Field, E be FieldExtension of F, T be non empty finite Subset of E,
p being Polynomial of (card T),F;
let x be T-evaluating Function of (card T),E;
set n = card T, R = F;
A0: F is Subring of E by FIELD_4:def 1;
defpred P[Nat] means
for p being Polynomial of (card T),F st card(Support p) = $1
holds Ext_eval(p,x) in the carrier of RAdj(F,T);
A1: ex k being Element of NAT st card(Support p) = k;
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3: P[k];
let p be Polynomial of n,R;
assume
A4: card(Support p) = k + 1;
set sgp = SgmX(BagOrder n, Support p);
set bg = sgp/.(len sgp);
A5: BagOrder n linearly_orders Support p by POLYNOM2:18;
Support p <> {} by A4;
then 1 <= len sgp by NAT_1:14;
then len sgp in Seg(len sgp) by FINSEQ_1:1;
then
A6: len sgp in dom sgp by FINSEQ_1:def 3;
then sgp/.(len sgp) = sgp.(len sgp) by PARTFUN1:def 6;
then bg in rng sgp by A6,FUNCT_1:def 3;
then
A7: bg in Support p by A5,PRE_POLY:def 2;
then
A8: p.bg <> 0.R by POLYNOM1:def 4;
set r2 = 0_(n,R)+*(bg,p.bg);
set r1 = p+*(bg,0.R);
reconsider bg as bag of n;
dom p = Bags n by FUNCT_2:def 1;
then
A9: r1 = p+*(bg.-->0.R) by FUNCT_7:def 3;
reconsider r1 as Function of Bags n,the carrier of R;
for u being object holds u in Support r1 implies u in Support p
proof
let u be object;
assume
A10: u in Support r1;
then reconsider u as Element of Bags n;
now
assume
A11: u = bg;
then u in dom(bg.-->0.R) by TARSKI:def 1;
then r1.u = (bg.-->0.R).bg by A9,A11,FUNCT_4:13;
then r1.u = 0.R by FUNCOP_1:72;
hence contradiction by A10,POLYNOM1:def 4;
end;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then p.u = r1.u by A9,FUNCT_4:11;
then p.u <> 0.R by A10,POLYNOM1:def 4;
hence thesis by POLYNOM1:def 4;
end;
then Support r1 c= Support p;
then reconsider r1 as Polynomial of n,R by POLYNOM1:def 5;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being object holds u in Support p implies u in Support r1 \/ {bg}
proof
let u be object;
assume
A14: u in Support p;
then reconsider u as Element of Bags n;
A15: p.u <> 0.R by A14,POLYNOM1:def 4;
per cases;
suppose
u = bg;
then u in {bg} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
u <> bg;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then r1.u = p.u by A9,FUNCT_4:11;
then u in Support r1 by A15,POLYNOM1:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
bg in dom(bg.-->0.R) by TARSKI:def 1;
then r1.bg = (bg.-->0.R).bg by A9,FUNCT_4:13;
then
A16: r1.bg = 0.R by FUNCOP_1:72;
then
A17: not bg in Support r1 by POLYNOM1:def 4;
for u being object holds u in Support r1 \/ {bg} implies u in Support p
proof
let u be object;
assume
A18: u in Support r1 \/ {bg};
per cases by A18,XBOOLE_0:def 3;
suppose
A19: u in Support r1;
then reconsider u as Element of Bags n;
u <> bg by A16,A19,POLYNOM1:def 4;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then
A20: r1.u = p.u by A9,FUNCT_4:11;
r1.u <> 0.R by A19,POLYNOM1:def 4;
hence thesis by A20,POLYNOM1:def 4;
end;
suppose
u in {bg};
hence thesis by A7,TARSKI:def 1;
end;
end;
then Support p = Support r1 \/ {bg} by A13,TARSKI:2;
then
A21: k + 1 = card(Support r1) + 1 by A4,A17,CARD_2:41;
dom 0_(n,R) = Bags n by FUNCT_2:def 1;
then
A22: r2 = 0_(n,R)+*(bg.-->p.bg) by FUNCT_7:def 3;
reconsider r2 as Function of Bags n,the carrier of R;
A23: for u being object holds u in Support r2 implies u in {bg}
proof
let u be object;
assume
A24: u in Support r2;
then reconsider u as Element of Bags n;
A25: r2.u <> 0.R by A24,POLYNOM1:def 4;
now
assume u <> bg;
then not u in dom(bg.-->p.bg) by TARSKI:def 1;
then r2.u = 0_(n,R).u by A22,FUNCT_4:11;
hence contradiction by A25,POLYNOM1:22;
end;
hence thesis by TARSKI:def 1;
end;
A50: for u being object holds u in {bg} implies u in Support r2
proof
let u be object;
bg in dom(bg.-->p.bg) by TARSKI:def 1;
then r2.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A26: r2.bg = p.bg by FUNCOP_1:72;
assume u in {bg};
then u = bg by TARSKI:def 1;
hence thesis by A8,A26,POLYNOM1:def 4;
end;
then Support r2 = {bg} by A23,TARSKI:2;
then reconsider r2 as Polynomial of n,R by POLYNOM1:def 5;
A28: for u being object st u in Bags n holds (r1+r2).u = p.u
proof
let u be object;
assume u in Bags n;
then reconsider u as bag of n;
per cases;
suppose
A29: u = bg;
bg in dom(bg.-->p.bg) by TARSKI:def 1;
then r2.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A30: r2.bg = p.bg by FUNCOP_1:72;
u in dom(bg.-->0.R) by A29,TARSKI:def 1;
then
A31: r1.u = (bg.-->0.R).bg by A9,A29,FUNCT_4:13;
(r1+r2).u = r1.u + r2.u by POLYNOM1:15
.= 0.R + p.bg by A29,A31,A30,FUNCOP_1:72
.= p.bg;
hence thesis by A29;
end;
suppose
A32: u <> bg;
then
A33: not u in dom(bg.-->0.R) by TARSKI:def 1;
not u in dom(bg.-->p.bg) by A32,TARSKI:def 1;
then r2.u = 0_(n,R).u by A22,FUNCT_4:11;
then
A34: r2.u = 0.R by POLYNOM1:22;
(r1+r2).u = r1.u + r2.u by POLYNOM1:15
.= p.u by A9,A33,A34,FUNCT_4:11;
hence thesis;
end;
end;
reconsider a = Ext_eval(r1,x) as Element of RAdj(F,T) by A3,A21;
reconsider c = Ext_eval(r2,x) as Element of RAdj(F,T) by A50,A23,TARSKI:2,Lm7;
dom(r1 + r2) = Bags n by FUNCT_2:def 1; then
Ext_eval(p,x)
= Ext_eval(r1+r2,x) by A12,A28,FUNCT_1:2
.= Ext_eval(r1,x) + Ext_eval(r2,x) by A0,FIELD_11:19
.= a + c by FIELD_6:15;
hence Ext_eval(p,x) in the carrier of RAdj(F,T);
end;
A36: P[0]
proof
let p be Polynomial of n,R;
assume card(Support p) = 0;
then Support p = {};
then p = 0_(n,R) by FIELD_11:5;
then Ext_eval(p,x) = 0.E by FIELD_11:16
.= 0.RAdj(F,T) by FIELD_6:def 4;
hence Ext_eval(p,x) in the carrier of RAdj(F,T);
end;
for k being Nat holds P[k] from NAT_1:sch 2(A36,A2);
hence thesis by A1;
end;
lemphi2:
for F being Field,
E being FieldExtension of F
for T being non empty finite Subset of E
for x being T-evaluating Function of (card T),E
holds rng hom_Ext_eval(x,F) c= the carrier of RAdj(F,T)
proof
let F be Field, E be FieldExtension of F, T be non empty finite Subset of E,
x be T-evaluating Function of (card T),E;
now let o be object;
assume A: o in rng hom_Ext_eval(x,F);
rng hom_Ext_eval(x,F) =
the set of all Ext_eval(p,x) where p is Polynomial of (card T),F
by lemphi1; then
consider p being Polynomial of (card T),F such that
B: o = Ext_eval(p,x) by A;
thus o in the carrier of RAdj(F,T) by B,lemphi2b;
end;
hence thesis;
end;
lemphi4aa:
for F being Field,
E being FieldExtension of F
for T being non empty finite Subset of E
for x being T-evaluating Function of (card T),E
holds Image_hom_Ext_eval(x,F) is Subring of RAdj(F,T)
proof
let F be Field, E be FieldExtension of F, T be non empty finite Subset of E;
let x be T-evaluating Function of (card T),E;
set S = Image_hom_Ext_eval(x,F), R = RAdj(F,T);
A: the carrier of S = rng hom_Ext_eval(x,F) by defIm; then
the carrier of S c= the carrier of R by lemphi2; then
J: [:the carrier of S,the carrier of S:] c=
[:the carrier of R,the carrier of R:] by ZFMISC_1:96;
B: the addF of S
= (the addF of E)||rng hom_Ext_eval(x,F) by defIm
.= (the addF of E)||the carrier of S by defIm
.= ((the addF of E)||(the carrier of R))||the carrier of S
by J,FUNCT_1:51
.= ((the addF of E)||(carrierRA(T)))||the carrier of S
by FIELD_6:def 4
.= (the addF of R)||the carrier of S by FIELD_6:def 4;
C: the multF of S
= (the multF of E)||rng hom_Ext_eval(x,F) by defIm
.= (the multF of E)||the carrier of S by defIm
.= ((the multF of E)||(the carrier of R))||the carrier of S
by J,FUNCT_1:51
.= ((the multF of E)||(carrierRA(T)))||the carrier of S
by FIELD_6:def 4
.= (the multF of R)||the carrier of S by FIELD_6:def 4;
D: 1.S = 1.E by defIm .= 1.R by FIELD_6:def 4;
0.S = 0.E by defIm .= 0.R by FIELD_6:def 4;
hence thesis by A,B,C,D,C0SP1:def 3,lemphi2;
end;
lemphi4ab:
for F being Field,
E being FieldExtension of F
for T being non empty finite Subset of E
for x being T-evaluating Function of (card T),E
holds T is Subset of the carrier of Image_hom_Ext_eval(x,F)
proof
let F be Field, E be FieldExtension of F, T be non empty finite Subset of E;
let x be T-evaluating Function of (card T),E;
set R = Image_hom_Ext_eval(x,F), S = RAdj(F,T), f = hom_Ext_eval(x,F);
set n = card T;
now let o be object;
assume A1: o in T; then
reconsider a = o as Element of E;
rng x = T by tev; then
consider i being object such that
A2: i in dom x & x.i = a by A1,FUNCT_1:def 3;
reconsider i as Element of n by A2;
set b = ({i},1)-bag;
defpred P[Element of Bags n,Element of the carrier of F] means
($1 = b & $2 = 1.F) or ($1 <> b & $2 = 0.F);
A: for x being Element of Bags n
ex y being Element of the carrier of F st P[x,y]
proof
let x be Element of Bags n;
per cases;
suppose x = b;
hence thesis;
end;
suppose x <> b;
hence thesis;
end;
end;
consider p being Function of Bags n, the carrier of F such that
B: for x being Element of Bags n holds P[x,p.x] from FUNCT_2:sch 3(A);
C: Support p = {b}
proof
C1: now let o be object;
assume o in {b}; then
C2: o = b by TARSKI:def 1;
p.b <> 0.F by B;
hence o in Support p by C2,POLYNOM1:def 4;
end;
now let o be object;
assume C3: o in Support p; then
reconsider b1 = o as Element of Bags n;
now assume b1 <> b; then
p.b1 = 0.F by B;
hence contradiction by C3,POLYNOM1:def 4;
end;
hence o in {b} by TARSKI:def 1;
end;
hence thesis by C1,TARSKI:2;
end; then
reconsider p as Polynomial of n,F by POLYNOM1:def 5;
dom f = the carrier of Polynom-Ring(n,F) by FUNCT_2:def 1; then
D: p in dom f by POLYNOM1:def 11;
K: F is Subring of E by FIELD_4:def 1; then
J: the carrier of F c= the carrier of E by C0SP1:def 3;
I: 1.E = 1.F by K,C0SP1:def 3
.= In(1.F,E) by J,SUBSET_1:def 8
.= In(p.b,E) by B;
H: i in {i} & support b = {i} by UPROOTS:8,TARSKI:def 1; then
E: eval(b,x) = power(E).(a,b.i) by A2,POLYNOM2:15
.= power(E).(a,0+1) by H,UPROOTS:7
.= power(E).(a,0) * a by GROUP_1:def 7
.= 1_E * a by GROUP_1:def 7;
f.p = Ext_eval(p,x) by dh
.= a by I,C,E,FIELD_11:18; then
a in rng f by D,FUNCT_1:def 3;
hence o in the carrier of R by defIm;
end;
then T c= the carrier of Image_hom_Ext_eval(x,F);
hence thesis;
end;
lemring:
now let R,S,T be Ring;
assume AS: R is Subring of S & S is Subring of T; then
H: the carrier of R c= the carrier of S &
the carrier of S c= the carrier of T by C0SP1:def 3; then
J: [:the carrier of R,the carrier of R:] c=
[:the carrier of S,the carrier of S:] by ZFMISC_1:96;
A: the carrier of R c= the carrier of T by H;
B: the addF of R
= (the addF of S)||the carrier of R by AS,C0SP1:def 3
.= ((the addF of T)||the carrier of S)||the carrier of R
by AS,C0SP1:def 3
.= (the addF of T)||the carrier of R by J,FUNCT_1:51;
C: the multF of R
= (the multF of S)||the carrier of R by AS,C0SP1:def 3
.= ((the multF of T)||the carrier of S)||the carrier of R
by AS,C0SP1:def 3
.= (the multF of T)||the carrier of R by J,FUNCT_1:51;
D: 1.R = 1.S by AS,C0SP1:def 3 .= 1.T by AS,C0SP1:def 3;
0.R = 0.S by AS,C0SP1:def 3 .= 0.T by AS,C0SP1:def 3;
hence R is Subring of T by A,B,C,D,C0SP1:def 3;
end;
theorem lemphi4:
for F being Field,
E being FieldExtension of F
for T being non empty finite Subset of E
for x being T-evaluating Function of (card T),E
holds RAdj(F,T) = Image_hom_Ext_eval(x,F)
proof
let F be Field, E be FieldExtension of F, T be non empty finite Subset of E;
let x be T-evaluating Function of (card T),E;
set R = Image_hom_Ext_eval(x,F), S = RAdj(F,T), f = hom_Ext_eval(x,F);
set n = card T;
A: T is Subset of the carrier of R by lemphi4ab;
B: F is Subring of R by lemphi3;
R is Subring of S & S is Subring of E by lemphi4aa; then
R is Subring of E by lemring; then
C: RAdj(F,T) is Subring of Image_hom_Ext_eval(x,F) by A,B,FIELD_6:32;
Image_hom_Ext_eval(x,F) is Subring of RAdj(F,T) by lemphi4aa;
hence thesis by C,FIELD_6:12;
end;
theorem help2m:
for F being Field,
E being FieldExtension of F
for T being non empty finite Subset of E
for x being T-evaluating Function of (card T),E
holds the carrier of RAdj(F,T) =
the set of all Ext_eval(p,x) where p is Polynomial of (card T),F
proof
let F be Field, E be FieldExtension of F, T be non empty finite Subset of E,
x be T-evaluating Function of (card T),E;
thus the carrier of RAdj(F,T)
= the carrier of Image_hom_Ext_eval(x,F) by lemphi4
.= rng hom_Ext_eval(x,F) by defIm
.= the set of all Ext_eval(p,x) where p is Polynomial of (card T),F
by lemphi1;
end;
help2:
for F being Field,
E being FieldExtension of F
for T being non empty finite Subset of E
for o being object
holds o in the carrier of RAdj(F,T) implies
ex p being Polynomial of (card T),F,
x being T-evaluating Function of (card T),E st o = Ext_eval(p,x)
proof
let F be Field, E be FieldExtension of F, T be finite non empty Subset of E;
let o be object;
assume A: o in the carrier of RAdj(F,T);
set x = the T-evaluating Function of (card T),E;
the carrier of RAdj(F,T) =
the set of all Ext_eval(p,x) where p is Polynomial of (card T),F by help2m;
then consider p being Polynomial of (card T),F such that
B: o = Ext_eval(p,x) by A;
thus thesis by B;
end;
theorem help1:
for F being Field,
E being FieldExtension of F
for T being finite Subset of E
holds T is F-algebraic implies FAdj(F,T) = RAdj(F,T)
proof
let F be Field, E be FieldExtension of F, T be finite Subset of E;
assume AS: T is F-algebraic;
defpred P[Nat] means
for F being Field, E being FieldExtension of F
for T being finite Subset of E st card T = $1
holds T is F-algebraic implies FAdj(F,T) = RAdj(F,T);
A: P[0]
proof
now let F be Field, E be FieldExtension of F;
let T be finite Subset of E;
assume card T = 0; then
T = {}; then
A1: T is Subset of F by XBOOLE_1:2; then
A2: FAdj(F,T) == F by FIELD_7:3;
F == RAdj(F,T) by A1,helpa;
hence FAdj(F,T) = RAdj(F,T) by A2,helpb,FIELD_7:2;
end;
hence thesis;
end;
B: now let k be Nat;
assume B0: P[k];
now let F be Field, E be FieldExtension of F;
let T be finite Subset of E;
assume C0: card T = k + 1;
assume T is F-algebraic; then
reconsider T1 = T as non empty finite F-algebraic Subset of E by C0;
set a = the Element of T1;
reconsider a as F-algebraic Element of E;
reconsider T2 = T1 \ {a} as finite F-algebraic Subset of E;
a in T1; then
{a} c= T1 by TARSKI:def 1; then
C4: T1 = T2 \/ {a} by XBOOLE_1:45;
a in {a} by TARSKI:def 1; then
not a in T2 by XBOOLE_0:def 5; then
card T1 = card T2 + 1 by C4,CARD_2:41; then
C6: FAdj(F,T2) = RAdj(F,T2) by B0,C0;
reconsider E1 = E as FieldExtension of FAdj(F,T2) by FIELD_4:7;
reconsider a1 = a as Element of E1;
reconsider E2 = E1 as RingExtension of RAdj(F,T2) by FIELD_4:def 1;
reconsider a2 = a1 as Element of E2;
C7: a1 is FAdj(F,T2)-algebraic
proof
consider p being non zero Polynomial of F such that
C8: Ext_eval(p,a) = 0.E by FIELD_6:43;
p <> 0_.F; then
C9: p <> 0.(Polynom-Ring F) by POLYNOM3:def 10;
reconsider p as non zero Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
the carrier of Polynom-Ring F
c= the carrier of Polynom-Ring FAdj(F,T2) by FIELD_4:10; then
reconsider q = p as
Element of the carrier of Polynom-Ring FAdj(F,T2);
now assume q is zero;
then q = 0_.FAdj(F,T2) by UPROOTS:def 5;
then q = 0.(Polynom-Ring FAdj(F,T2)) by POLYNOM3:def 10;
hence contradiction by C9,FIELD_4:11;
end; then
reconsider q as
non zero Element of the carrier of Polynom-Ring FAdj(F,T2);
E1 is FAdj(F,T2)-extending FieldExtension of F; then
Ext_eval(q,a) = Ext_eval(p,a) by FIELD_7:15;
hence thesis by C8,FIELD_6:43;
end;
FAdj(F,{a}\/T2) = FAdj(FAdj(F,T2),{a1}) by FIELD_7:34
.= RAdj(RAdj(F,T2),{a2}) by C6,C7,FIELD_6:56
.= RAdj(F,{a}\/T2) by ug;
hence FAdj(F,T) = RAdj(F,T) by C4;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(A,B);
consider n being Nat such that H: card T = n;
thus FAdj(F,T) = RAdj(F,T) by AS,H,I;
end;
begin :: On Fixing Monomorphisms
registration
let R be Ring;
let S be RingExtension of R;
cluster R-fixing for Homomorphism of S;
existence
proof
reconsider h = id S as Homomorphism of S;
now let a be Element of R;
R is Subring of S by FIELD_4:def 1;
then the carrier of R c= the carrier of S by C0SP1:def 3;
hence h.a = a by FUNCT_1:18;
end;
then h is R-fixing by FIELD_8:def 2;
hence thesis;
end;
cluster R-fixing for Monomorphism of S;
existence
proof
reconsider h = id S as Monomorphism of S;
now let a be Element of R;
R is Subring of S by FIELD_4:def 1;
then the carrier of R c= the carrier of S by C0SP1:def 3;
hence h.a = a by FUNCT_1:18;
end;
then h is R-fixing by FIELD_8:def 2;
hence thesis;
end;
cluster R-fixing for Automorphism of S;
existence
proof
reconsider h = id S as Automorphism of S;
now let a be Element of R;
R is Subring of S by FIELD_4:def 1;
then the carrier of R c= the carrier of S by C0SP1:def 3;
hence h.a = a by FUNCT_1:18;
end;
then h is R-fixing by FIELD_8:def 2;
hence thesis;
end;
end;
theorem fixp:
for F being Field,
E being FieldExtension of F, K being FieldExtension of E
for p being Element of the carrier of Polynom-Ring F
for h being F-fixing Homomorphism of E,K holds (PolyHom h).p = p
proof
let F be Field, E be FieldExtension of F, K be FieldExtension of E;
let p be Element of the carrier of Polynom-Ring F,
h be F-fixing Homomorphism of E,K;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of Polynom-Ring E;
set g = (PolyHom h).p1;
H: dom g = NAT by FUNCT_2:def 1 .= dom p by FUNCT_2:def 1;
now let o be object;
assume o in dom g; then
reconsider i = o as Nat;
g.i = h.(p1.i) by FIELD_1:def 2 .= p.i by FIELD_8:def 2;
hence g.o = p.o;
end;
hence thesis by H,FUNCT_1:2;
end;
theorem fixeval:
for F being Field,
E being FieldExtension of F, K being FieldExtension of E
for p being Element of the carrier of Polynom-Ring F
for a being Element of E, h being F-fixing Homomorphism of E,K
holds h.(Ext_eval(p,a)) = Ext_eval(p,h.a)
proof
let F be Field, E be FieldExtension of F, K be FieldExtension of E;
let p be Element of the carrier of Polynom-Ring F;
let a be Element of E, h be F-fixing Homomorphism of E,K;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E by FIELD_4:10;
then reconsider p1 = p as Element of the carrier of Polynom-Ring E;
reconsider p2 = (PolyHom h).p as Element of the carrier of Polynom-Ring F
by fixp;
thus h.(Ext_eval(p,a)) = h.eval(p1,a) by FIELD_4:26
.= eval((PolyHom h).p1,h.a) by FIELD_1:27
.= Ext_eval(p2,h.a) by FIELD_4:26
.= Ext_eval(p,h.a) by fixp;
end;
theorem fixrr:
for F being Field,
E being FieldExtension of F
for h being F-fixing Monomorphism of E
for p being non zero Element of the carrier of Polynom-Ring F
holds h .: Roots(E,p) = Roots(E,p)
proof
let F be Field, E being FieldExtension of F,
h be F-fixing Monomorphism of E;
let p be non zero Element of the carrier of Polynom-Ring F;
reconsider g = h|Roots(E,p) as bijective Function of Roots(E,p),Roots(E,p)
by FIELD_8:39;
A: g is onto;
Y: now let o be object;
assume o in Roots(E,p); then
consider b being object such that
C: b in dom(h|Roots(E,p)) & (h|Roots(E,p)).b = o by A,FUNCT_1:def 3;
D: b in dom h by C,RELAT_1:57;
h.b = o by C,FUNCT_1:49;
hence o in h.:Roots(E,p) by C,D,FUNCT_1:def 6;
end;
now let o be object;
assume o in h.:Roots(E,p); then
consider x being object such that
B: x in dom h & x in Roots(E,p) & o = h.x by FUNCT_1:def 6;
C: x in dom(h|Roots(E,p)) by B,RELAT_1:57;
o = (h|Roots(E,p)).x by B,FUNCT_1:49;
hence o in Roots(E,p) by A,C,FUNCT_1:def 3;
end;
hence thesis by Y,TARSKI:2;
end;
theorem fixr:
for F being Field,
E being F-algebraic FieldExtension of F
for h being F-fixing Monomorphism of E holds the carrier of E c= rng h
proof
let F be Field, E being F-algebraic FieldExtension of F,
h be F-fixing Monomorphism of E;
now let o be object;
assume o in the carrier of E; then
reconsider a = o as Element of E;
set p = MinPoly(a,F), M = Roots(E,MinPoly(a,F));
H: M = {a where a is Element of E : a is_a_root_of p,E} by FIELD_4:def 4;
Ext_eval(p,a) = 0.E by FIELD_6:52;
then a is_a_root_of p,E by FIELD_4:def 2;
then a in M by H;
then a in h.:M by fixrr;
then consider x being object such that
A: x in dom h & x in M & a = h.x by FUNCT_1:def 6;
thus o in rng h by A,FUNCT_1:def 3;
end;
hence thesis;
end;
theorem iso:
for F being Field,
E being F-algebraic FieldExtension of F
for h being F-fixing Monomorphism of E holds h is Automorphism of E
proof
let F be Field, E being F-algebraic FieldExtension of F,
h be F-fixing Monomorphism of E;
the carrier of E c= rng h & rng h c= the carrier of E by fixr,RELAT_1:def 19;
then h is onto by XBOOLE_0:def 10;
hence thesis;
end;
registration
let F be Field,
E be F-algebraic FieldExtension of F;
cluster -> isomorphism for F-fixing Monomorphism of E;
coherence by iso;
end;
theorem ll:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for h being F-fixing Monomorphism of E,K
for T being F-algebraic Subset of E holds h .: T is F-algebraic
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let h be F-fixing Monomorphism of E,K, T be F-algebraic Subset of E;
now let a be Element of K;
assume a in h.:T; then
consider x being object such that
A: x in dom h & x in T & a = h.x by FUNCT_1:def 6;
reconsider x as Element of E by A;
consider p being non zero Polynomial of F such that
B: Ext_eval(p,x) = 0.E by A,FIELD_6:43;
p is Element of the carrier of Polynom-Ring F by POLYNOM3:def 10; then
Ext_eval(p,a) = h.(0.E) by A,B,fixeval .= 0.K by RING_2:6;
hence a is F-algebraic by FIELD_6:43;
end;
hence thesis by FIELD_7:def 12;
end;
Lm10:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for h being F-fixing Monomorphism of E,K
for T being non empty finite Subset of E
for b being bag of (card T)
st ex o being set st support b = {o}
for x being T-evaluating Function of (card T),E
holds h.eval(b,x) in the carrier of RAdj(F,h.:T)
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let h be F-fixing Monomorphism of E,K, T be non empty finite Subset of E;
let b be bag of (card T);
assume AS: ex o being set st support b = {o};
let x be T-evaluating Function of (card T),E;
consider o being set such that A: support b = {o} by AS;
o in {o} by TARSKI:def 1; then
reconsider o as Element of (card T) by A;
B: h.:T is Subset of RAdj(F,h.:T) by FIELD_6:30;
C: rng x c= T by RELAT_1:def 19;
D: o in support b & support b c= dom b by A,TARSKI:def 1,PRE_POLY:37;
dom b = card T by PARTFUN1:def 2 .= dom x by FUNCT_2:def 1; then
E: x.o in T by C,D,FUNCT_1:3;
dom h = the carrier of E by FUNCT_2:def 1; then
h.(x.o) in h.:T by E,FUNCT_1:def 6; then
reconsider a = h.(x.o) as Element of RAdj(F,h.:T) by B;
reconsider c = x.o as Element of E;
h.eval(b,x) = h.(power(E).(x.o,b.o)) by A,POLYNOM2:15
.= h.(c|^(b.o)) by BINOM:def 2
.= (h.c)|^(b.o) by FIELD_1:13
.= a|^(b.o) by FIELD_6:19
.= power(RAdj(F,h.:T)).(a,b.o) by BINOM:def 2;
hence thesis;
end;
theorem Lm9:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for h being F-fixing Monomorphism of E,K
for T being non empty finite Subset of E
for b being bag of (card T)
for x being T-evaluating Function of (card T),E
holds h.eval(b,x) in the carrier of RAdj(F,h.:T)
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let h be F-fixing Monomorphism of E,K, T be non empty finite Subset of E;
let b be bag of (card T), x be T-evaluating Function of (card T),E;
defpred P[Nat] means
for b being bag of (card T) st card(support b) = $1
for x being T-evaluating Function of (card T),E
holds h.eval(b,x) in the carrier of RAdj(F,h.:T);
set n = card T, R = RAdj(F,h.:T);
H0: 0.K = 0.R & 1.K = 1.R by FIELD_6:def 4;
A: P[0]
proof
now let b be bag of n;
assume A0: card(support b) = 0;
let x be T-evaluating Function of n,E;
now let o be object;
assume o in n;
not o in support b by A0;
hence b.o = {} by PRE_POLY:def 7 .= (EmptyBag n).o by PBOOLE:5;
end; then
b = EmptyBag n by PBOOLE:def 10; then
h.eval(b,x) = h.(1_E) by POLYNOM2:14 .= 1_K by GROUP_1:def 13;
hence h.eval(b,x) in the carrier of RAdj(F,h.:T) by H0;
end;
hence thesis;
end;
B: now let k be Nat;
assume IV: P[k];
now let b be bag of n;
assume B0: card(support b) = k+1;
let x be T-evaluating Function of n,E;
set a = the Element of support b;
B3: support b <> {} by B0; then
B1: a in support b & support b c= dom b & dom b c= n by PRE_POLY:37; then
reconsider a as Element of n;
set b1 = b \ a; set b2 = ({a},b.a)-bag;
B2: support b1 = support b \ {a} by RING_5:29;
{a} c= support b by B1,TARSKI:def 1; then
card(support b1)
= card(support b) - card {a} by B2,CARD_2:44
.= (k + 1) - 1 by B0,CARD_2:42; then
reconsider u = h.eval(b1,x) as Element of RAdj(F,h.:T) by IV;
b.a <> 0 by B3,PRE_POLY:def 7; then
support b2 = {a} by UPROOTS:8; then
reconsider v = h.eval(b2,x) as Element of RAdj(F,h.:T) by Lm10;
h.eval(b,x) = h.eval(b1 + b2,x) by RING_5:30
.= h.(eval(b1,x) * eval(b2,x)) by POLYNOM2:16
.= h.eval(b1,x) * h.eval(b2,x) by GROUP_6:def 6
.= u * v by FIELD_6:16;
hence h.eval(b,x) in the carrier of RAdj(F,h.:T);
end;
hence P[k+1];
end;
C: for k being Nat holds P[k] from NAT_1:sch 2(A,B);
consider n being Nat such that D: card(support b) = n;
thus thesis by C,D;
end;
Lm8:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for h being F-fixing Monomorphism of E,K
for T being non empty finite Subset of E
for p being Polynomial of (card T),F
st (ex b being bag of (card T) st Support p = {b})
for x being T-evaluating Function of (card T),E
holds h.Ext_eval(p,x) in the carrier of RAdj(F,h.:T)
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let h be F-fixing Monomorphism of E,K, T be non empty finite Subset of E,
p be Polynomial of (card T),F;
assume AS: (ex b being bag of (card T) st Support p = {b});
let x be T-evaluating Function of (card T),E;
set n = card T;
A0: F is Subring of E by FIELD_4:def 1;
consider y being FinSequence of the carrier of E such that
A2: Ext_eval(p,x) = Sum y & len y = len SgmX(BagOrder n, Support p) &
for i being Element of NAT st 1 <= i & i <= len y
holds y.i = In( (p * SgmX(BagOrder n, Support p)).i, E) *
eval(SgmX(BagOrder n, Support p)/.i,x) by FIELD_11:def 4;
A3: len(SgmX(BagOrder n, Support p))
= card(Support p) by PRE_POLY:11,POLYNOM2:18
.= 1 by AS,CARD_2:42; then
H: 1 in Seg(len y) by A2,FINSEQ_1:1; then
1 in dom y by FINSEQ_1:def 3; then
A5: y.1 = y/.1 by PARTFUN1:def 6;
dom SgmX(BagOrder n, Support p)
= Seg(len y) by A2,FINSEQ_1:def 3 .= dom y by FINSEQ_1:def 3; then
A9: 1 in dom SgmX(BagOrder n, Support p) by H,FINSEQ_1:def 3;
dom p = Bags n by FUNCT_2:def 1; then
SgmX(BagOrder n, Support p)/.1 in dom p; then
U: SgmX(BagOrder n, Support p).1 in dom p by A9,PARTFUN1:def 6; then
p.(SgmX(BagOrder n, Support p).1) in rng p by FUNCT_1:3; then
A4: (p * SgmX(BagOrder n, Support p)).1 in rng p by A9,FUNCT_1:13;
A7: rng p c= the carrier of F by RELAT_1:def 19;
A6: the carrier of F c= the carrier of E by A0,C0SP1:def 3;
set b = SgmX(BagOrder n, Support p)/.1;
reconsider a = h.eval(b,x) as Element of RAdj(F,h.:T) by Lm9;
F is Subring of RAdj(F,h.:T) by FIELD_6:31; then
Y: the carrier of F c= the carrier of RAdj(F,h.:T) by C0SP1:def 3;
Z: 1 in dom(p * SgmX(BagOrder n, Support p)) by U,A9,FUNCT_1:11;
h.(In( (p * SgmX(BagOrder n, Support p)).1, E))
= h.((p * SgmX(BagOrder n, Support p)).1) by A4,A6,A7,SUBSET_1:def 8
.= h.((p * SgmX(BagOrder n, Support p))/.1) by Z,PARTFUN1:def 6
.= (p * SgmX(BagOrder n, Support p))/.1 by FIELD_8:def 2; then
reconsider c = h.(In( (p * SgmX(BagOrder n, Support p)).1, E))
as Element of RAdj(F,h.:T) by Y;
y = <*y.1*> by A2,A3,FINSEQ_1:40; then
h.Ext_eval(p,x)
= h.(y/.1) by A2,A5,RLVECT_1:44
.= h.((In( (p * SgmX(BagOrder n, Support p)).1, E) * eval(b,x)))
by A5,A3,A2
.= h.(In( (p * SgmX(BagOrder n, Support p)).1, E)) * h.eval(b,x)
by GROUP_6:def 6
.= c * a by FIELD_6:16;
hence thesis;
end;
theorem help3:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for h being F-fixing Monomorphism of E,K
for T being non empty finite Subset of E
for p being Polynomial of (card T),F
for x being T-evaluating Function of (card T),E
holds h.Ext_eval(p,x) in the carrier of RAdj(F,h.:T)
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let h be F-fixing Monomorphism of E,K, T be non empty finite Subset of E,
p be Polynomial of (card T),F, x be T-evaluating Function of (card T),E;
set n = card T, R = F;
defpred P[Nat] means
for p being Polynomial of (card T),F st card(Support p) = $1
holds h.Ext_eval(p,x) in the carrier of RAdj(F,h.:T);
A0: E is Subring of K & F is Subring of E by FIELD_4:def 1;
A1: ex k being Element of NAT st card(Support p) = k;
A2: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A3: P[k];
let p be Polynomial of n,R;
assume
A4: card(Support p) = k + 1;
set sgp = SgmX(BagOrder n, Support p);
set bg = sgp/.(len sgp);
A5: BagOrder n linearly_orders Support p by POLYNOM2:18;
Support p <> {} by A4;
then 1 <= len sgp by NAT_1:14;
then len sgp in Seg(len sgp) by FINSEQ_1:1;
then
A6: len sgp in dom sgp by FINSEQ_1:def 3;
then sgp/.(len sgp) = sgp.(len sgp) by PARTFUN1:def 6;
then bg in rng sgp by A6,FUNCT_1:def 3;
then
A7: bg in Support p by A5,PRE_POLY:def 2;
then
A8: p.bg <> 0.R by POLYNOM1:def 4;
set r2 = 0_(n,R)+*(bg,p.bg);
set r1 = p+*(bg,0.R);
reconsider bg as bag of n;
dom p = Bags n by FUNCT_2:def 1;
then
A9: r1 = p+*(bg.-->0.R) by FUNCT_7:def 3;
reconsider r1 as Function of Bags n,the carrier of R;
for u being object holds u in Support r1 implies u in Support p
proof
let u be object;
assume
A10: u in Support r1;
then reconsider u as Element of Bags n;
now
assume
A11: u = bg;
then u in dom(bg.-->0.R) by TARSKI:def 1;
then r1.u = (bg.-->0.R).bg by A9,A11,FUNCT_4:13;
then r1.u = 0.R by FUNCOP_1:72;
hence contradiction by A10,POLYNOM1:def 4;
end;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then p.u = r1.u by A9,FUNCT_4:11;
then p.u <> 0.R by A10,POLYNOM1:def 4;
hence thesis by POLYNOM1:def 4;
end;
then Support r1 c= Support p;
then reconsider r1 as Polynomial of n,R by POLYNOM1:def 5;
A12: dom p = Bags n by FUNCT_2:def 1;
A13: for u being object holds u in Support p implies u in Support r1 \/ {bg}
proof
let u be object;
assume
A14: u in Support p;
then reconsider u as Element of Bags n;
A15: p.u <> 0.R by A14,POLYNOM1:def 4;
per cases;
suppose
u = bg;
then u in {bg} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
suppose
u <> bg;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then r1.u = p.u by A9,FUNCT_4:11;
then u in Support r1 by A15,POLYNOM1:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
bg in dom(bg.-->0.R) by TARSKI:def 1;
then r1.bg = (bg.-->0.R).bg by A9,FUNCT_4:13;
then
A16: r1.bg = 0.R by FUNCOP_1:72;
then
A17: not bg in Support r1 by POLYNOM1:def 4;
for u being object holds u in Support r1 \/ {bg} implies u in Support p
proof
let u be object;
assume
A18: u in Support r1 \/ {bg};
per cases by A18,XBOOLE_0:def 3;
suppose
A19: u in Support r1;
then reconsider u as Element of Bags n;
u <> bg by A16,A19,POLYNOM1:def 4;
then not u in dom(bg.-->0.R) by TARSKI:def 1;
then
A20: r1.u = p.u by A9,FUNCT_4:11;
r1.u <> 0.R by A19,POLYNOM1:def 4;
hence thesis by A20,POLYNOM1:def 4;
end;
suppose
u in {bg};
hence thesis by A7,TARSKI:def 1;
end;
end;
then Support p = Support r1 \/ {bg} by A13,TARSKI:2;
then
A21: k + 1 = card(Support r1) + 1 by A4,A17,CARD_2:41;
dom 0_(n,R) = Bags n by FUNCT_2:def 1;
then
A22: r2 = 0_(n,R)+*(bg.-->p.bg) by FUNCT_7:def 3;
reconsider r2 as Function of Bags n,the carrier of R;
A23: for u being object holds u in Support r2 implies u in {bg}
proof
let u be object;
assume
A24: u in Support r2;
then reconsider u as Element of Bags n;
A25: r2.u <> 0.R by A24,POLYNOM1:def 4;
now
assume u <> bg;
then not u in dom(bg.-->p.bg) by TARSKI:def 1;
then r2.u = 0_(n,R).u by A22,FUNCT_4:11;
hence contradiction by A25,POLYNOM1:22;
end;
hence thesis by TARSKI:def 1;
end;
A50: for u being object holds u in {bg} implies u in Support r2
proof
let u be object;
bg in dom(bg.-->p.bg) by TARSKI:def 1;
then r2.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A26: r2.bg = p.bg by FUNCOP_1:72;
assume u in {bg};
then u = bg by TARSKI:def 1;
hence thesis by A8,A26,POLYNOM1:def 4;
end;
then Support r2 = {bg} by A23,TARSKI:2;
then reconsider r2 as Polynomial of n,R by POLYNOM1:def 5;
A28: for u being object st u in Bags n holds (r1+r2).u = p.u
proof
let u be object;
assume u in Bags n;
then reconsider u as bag of n;
per cases;
suppose
A29: u = bg;
bg in dom(bg.-->p.bg) by TARSKI:def 1;
then r2.bg = (bg.-->p.bg).bg by A22,FUNCT_4:13;
then
A30: r2.bg = p.bg by FUNCOP_1:72;
u in dom(bg.-->0.R) by A29,TARSKI:def 1;
then
A31: r1.u = (bg.-->0.R).bg by A9,A29,FUNCT_4:13;
(r1+r2).u = r1.u + r2.u by POLYNOM1:15
.= 0.R + p.bg by A29,A31,A30,FUNCOP_1:72
.= p.bg;
hence thesis by A29;
end;
suppose
A32: u <> bg;
then
A33: not u in dom(bg.-->0.R) by TARSKI:def 1;
not u in dom(bg.-->p.bg) by A32,TARSKI:def 1;
then r2.u = 0_(n,R).u by A22,FUNCT_4:11;
then
A34: r2.u = 0.R by POLYNOM1:22;
(r1+r2).u = r1.u + r2.u by POLYNOM1:15
.= p.u by A9,A33,A34,FUNCT_4:11;
hence thesis;
end;
end;
reconsider a = h.Ext_eval(r1,x) as Element of RAdj(F,h.:T) by A3,A21;
reconsider c = h.Ext_eval(r2,x) as Element of RAdj(F,h.:T)
by A50,A23,TARSKI:2,Lm8;
dom(r1 + r2) = Bags n by FUNCT_2:def 1; then
h.Ext_eval(p,x)
= h.Ext_eval(r1+r2,x) by A12,A28,FUNCT_1:2
.= h.(Ext_eval(r1,x) + Ext_eval(r2,x)) by A0,FIELD_11:19
.= h.Ext_eval(r1,x) + h.Ext_eval(r2,x) by VECTSP_1:def 20
.= a + c by FIELD_6:15;
hence h.Ext_eval(p,x) in the carrier of RAdj(F,h.:T);
end;
A36: P[0]
proof
let p be Polynomial of n,R;
assume card(Support p) = 0;
then Support p = {};
then p = 0_(n,R) by FIELD_11:5;
then Ext_eval(p,x) = 0.E by FIELD_11:16;
then h.Ext_eval(p,x) = 0.K by RING_2:6
.= 0.RAdj(F,h.:T) by FIELD_6:def 4;
hence h.Ext_eval(p,x) in the carrier of RAdj(F,h.:T);
end;
for k being Nat holds P[k] from NAT_1:sch 2(A36,A2);
hence thesis by A1;
end;
theorem lemNor2ch:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for h being F-fixing Monomorphism of E,K
for T being non empty finite F-algebraic Subset of E
holds h.:(the carrier of FAdj(F,T)) c= the carrier of FAdj(F,h.:T)
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let h be F-fixing Monomorphism of E,K;
let T be finite non empty F-algebraic Subset of E;
h .: T is F-algebraic by ll; then
A0: FAdj(F,h.:T) = RAdj(F,h.:T) by help1;
now let o be object;
assume o in h.:(the carrier of FAdj(F,T)); then
consider a being object such that
A1: a in dom h & a in the carrier of FAdj(F,T) & o = h.a by FUNCT_1:def 6;
reconsider a as Element of FAdj(F,T) by A1;
FAdj(F,T) = RAdj(F,T) by help1; then
consider p being Polynomial of (card T),F,
x being T-evaluating Function of (card T),E such that
A2: a = Ext_eval(p,x) by help2;
thus o in the carrier of FAdj(F,h.:T) by A0,A1,A2,help3;
end;
hence thesis;
end;
theorem
for F being Field,
E being FieldExtension of F,
K being E-extending FieldExtension of F
for T being finite F-algebraic Subset of K
st T c= the carrier of E holds FAdj(F,T) is Subfield of E
proof
let F be Field, E be FieldExtension of F,
K be E-extending FieldExtension of F;
let T be finite F-algebraic Subset of K;
assume T c= the carrier of E; then
reconsider T1 = T as finite Subset of E;
now let a being Element of E;
assume A: a in T1; then
reconsider b = a as Element of K;
consider p being non zero Polynomial of F such that
B: Ext_eval(p,b) = 0.K by A,FIELD_6:43;
reconsider p as non zero Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
C: E is Subfield of K by FIELD_4:7;
Ext_eval(p,a) = Ext_eval(p,b) by FIELD_6:11
.= 0.E by B,C,EC_PF_1:def 1;
hence a is F-algebraic by FIELD_6:43;
end; then
reconsider T1 as finite F-algebraic Subset of E by FIELD_7:def 12;
FAdj(F,T1) = FAdj(F,T) by lemh1;
hence thesis;
end;
theorem lemh:
for F being Field,
E being FieldExtension of F,
K being E-extending FieldExtension of F
for h being F-fixing Homomorphism of E,(K qua FieldExtension of E)
for T being finite F-algebraic Subset of E
st h.:T c= the carrier of E holds FAdj(F,h.:T) is Subfield of E
proof
let F be Field, E be FieldExtension of F,
K be E-extending FieldExtension of F;
let h be F-fixing Homomorphism of E,(K qua FieldExtension of E);
let T be finite F-algebraic Subset of E;
assume AS: h.:T c= the carrier of E;
reconsider T1 = h.:T as finite Subset of E by AS;
now let a be Element of E;
assume a in T1; then
consider x being object such that
A: x in dom h & x in T & a = h.x by FUNCT_1:def 6;
reconsider x as F-algebraic Element of E by A;
consider p being non zero Polynomial of F such that
B: Ext_eval(p,x) = 0.E by FIELD_6:43;
reconsider p as non zero Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
C: E is Subfield of K by FIELD_4:7;
Ext_eval(p,a) = Ext_eval(p,h.x) by A,FIELD_6:11
.= h.(0.E) by B,fixeval
.= 0.K by RING_2:6
.= 0.E by C,EC_PF_1:def 1;
hence a is F-algebraic by FIELD_6:43;
end; then
reconsider T1 as finite F-algebraic Subset of E by FIELD_7:def 12;
FAdj(F,T1) = FAdj(F,h.:T) by lemh1;
hence thesis;
end;
theorem lemNor2c:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for h being F-fixing Monomorphism of E,K
for T being non empty finite F-algebraic Subset of E
st h.:T c= the carrier of E
holds h.:(the carrier of FAdj(F,T)) c= the carrier of E
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let h be F-fixing Monomorphism of E,K,
T be non empty finite F-algebraic Subset of E;
assume h.:T c= the carrier of E; then
FAdj(F,h.:T) is Subfield of E by lemh; then
A: the carrier of FAdj(F,h.:T) c= the carrier of E by EC_PF_1:def 1;
h.:(the carrier of FAdj(F,T)) c= the carrier of FAdj(F,h.:T) by lemNor2ch;
hence thesis by A;
end;
theorem lemNor2b:
for F being Field,
E being FieldExtension of F,
K being F-extending FieldExtension of E
for h being F-fixing Monomorphism of E,K
for p being non constant Element of the carrier of Polynom-Ring F
st p splits_in E holds h .: Roots(E,p) c= the carrier of E
proof
let F be Field, E be FieldExtension of F,
K be F-extending FieldExtension of E;
let h be F-fixing Monomorphism of E,K;
let p be non constant Element of the carrier of Polynom-Ring F;
assume AS: p splits_in E;
H: Roots(E,p) = {a where a is Element of E : a is_a_root_of p,E} &
Roots(K,p) = {a where a is Element of K : a is_a_root_of p,K}
by FIELD_4:def 4;
now let o be object;
assume o in h.:Roots(E,p); then
consider x being object such that
B: x in dom h & x in Roots(E,p) & o = h.x by FUNCT_1:def 6;
consider a being Element of E such that
C: a = x & a is_a_root_of p,E by B,H;
Ext_eval(p,a) = 0.E by C,FIELD_4:def 2; then
0.K = h.(Ext_eval(p,a)) by RING_2:6 .= Ext_eval(p,h.a) by fixeval; then
h.a is_a_root_of p,K by FIELD_4:def 2; then
h.a in Roots(K,p) by H; then
h.a in Roots(E,p) by AS,lemNor2bb;
hence o in the carrier of E by C,B;
end;
hence thesis;
end;
begin :: Normal Extensions
definition
let F be Field;
let E be FieldExtension of F;
attr E is F-normal means
E is F-algebraic &
for p being irreducible Element of the carrier of Polynom-Ring F
st p is_with_roots_in E holds p splits_in E;
end;
registration
let F be Field;
cluster F-normal -> F-algebraic for FieldExtension of F;
coherence;
end;
lemmin:
for F being Field,
E being F-algebraic FieldExtension of F
holds E is F-normal iff
for a being Element of E holds MinPoly(a,F) splits_in E
proof
let F be Field, E be F-algebraic FieldExtension of F;
A: now assume AS: E is F-normal;
thus for a being Element of E holds MinPoly(a,F) splits_in E
proof
let a be Element of E;
0.E = Ext_eval(MinPoly(a,F),a) by FIELD_6:52;
then MinPoly(a,F) is_with_roots_in E by FIELD_4:def 3,FIELD_4:def 2;
hence thesis by AS;
end;
end;
now assume AS: for a being Element of E holds MinPoly(a,F) splits_in E;
now let p be irreducible Element of the carrier of Polynom-Ring F;
assume p is_with_roots_in E; then
consider a being Element of E such that
B: a is_a_root_of p,E by FIELD_4:def 3;
Ext_eval(p,a) = 0.E by B,FIELD_4:def 2; then
consider q being Polynomial of F such that
C: p = MinPoly(a,F) *' q by FIELD_6:53,RING_4:1;
reconsider q1 = q as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
q <> 0_.(F) by C; then
deg p = deg MinPoly(a,F) + deg q by C,HURWITZ:23; then
deg p - deg q + deg q > 0 + deg q by RING_4:def 4,XREAL_1:8; then
deg q1 < 1 by C,RING_4:1,RING_4:40; then
deg q1 + 1 <= 1 by INT_1:7; then
deg q1 + 1 - 1 <= 1 - 1 by XREAL_1:9; then
consider b being Element of F such that
G: q1 = b|F by RING_4:def 4,RING_4:20;
H: F is Subring of E by FIELD_4:def 1; then
the carrier of F c= the carrier of E by C0SP1:def 3; then
reconsider d = b as Element of E;
q <> (0.F)|F by C; then
d <> 0.E by G,H,C0SP1:def 3; then
reconsider d as non zero Element of E by STRUCT_0:def 12;
reconsider q2 = d|E as Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
H: d|E = b|F by FIELD_6:23;
consider c being non zero Element of E, r being Ppoly of E such that
I: MinPoly(a,F) = c * r by AS,FIELD_4:def 5;
p = (c * r) *' (d|E) by C,I,G,H,FIELD_4:17
.= (c * r) *' (d * 1_.(E)) by RING_4:16
.= d * ((c * r) *' 1_.(E)) by RING_4:10
.= (d * c) * r by RING_4:11;
hence p splits_in E by FIELD_4:def 5;
end;
hence E is F-normal;
end;
hence thesis by A;
end;
registration
let F be Field;
cluster F-quadratic -> F-normal for FieldExtension of F;
coherence
proof
let E be FieldExtension of F;
assume AS: E is F-quadratic; then
reconsider E as F-finite FieldExtension of F;
now 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 p = MinPoly(a,F) as Element of the carrier of Polynom-Ring E;
reconsider p1 = p as Polynomial of E;
H: deg MinPoly(a,F) <= deg(E,F) & deg MinPoly(a,F) = deg p
by FIELD_10:11,INT_2:27,FIELD_4:20;
0.E = Ext_eval(MinPoly(a,F),a) by FIELD_6:52
.= eval(p,a) by FIELD_4:26; then
consider r being Polynomial of E such that
B: rpoly(1,a) *' r = p1 by RING_5:11,RING_4:1;
MinPoly(a,F) <> 0_.(F); then
C: r <> 0_.(E) by B,FIELD_4:12;
reconsider r1 = r as Element of the carrier of Polynom-Ring E
by POLYNOM3:def 10;
deg p <= 2 implies deg p = 0 or ... or deg p = 2 by H; then
per cases by H,AS,FIELD_9:def 26;
suppose deg p = 0;
hence MinPoly(a,F) splits_in E by H,RING_4:def 4;
end;
suppose deg p = 1; then
H: 1 = deg rpoly(1,a) + deg r by B,C,HURWITZ:23
.= 1 + deg r by HURWITZ:27; then
consider b being Element of E such that
D: r1 = b|E by RING_4:def 4,RING_4:20;
r1 = b * 1_.(E) by D,RING_4:16; then
F: p = b * ((1_.(E)) *' rpoly(1,a)) by B,RING_4:10;
G: b is non zero by H,D,RING_4:21;
rpoly(1,a) is Ppoly of E by RING_5:51;
hence MinPoly(a,F) splits_in E by G,F,FIELD_4:def 5;
end;
suppose deg p = 2; then
2 = deg rpoly(1,a) + deg r by B,C,HURWITZ:23
.= 1 + deg r by HURWITZ:27; then
consider c,b being Element of E such that
D: c <> 0.E & r = c * rpoly(1,b) by HURWITZ:28;
E: c is non zero by D;
F: p = c * (rpoly(1,b) *' rpoly(1,a)) by B,D,RING_4:10;
rpoly(1,a) is Ppoly of E & rpoly(1,b) is Ppoly of E by RING_5:51; then
rpoly(1,b) *' rpoly(1,a) is Ppoly of E by RING_5:52;
hence MinPoly(a,F) splits_in E by E,F,FIELD_4:def 5;
end;
end;
hence thesis by lemmin;
end;
cluster -> F-normal for AlgebraicClosure of F;
coherence
proof
let A be AlgebraicClosure of F;
now let p be irreducible Element of the carrier of Polynom-Ring F;
reconsider q = p as Polynomial of A by FIELD_4:8;
reconsider q1 = q as Element of the carrier of Polynom-Ring A
by POLYNOM3:def 10;
now assume q = 0_.(A);
then p = 0_.(F) by FIELD_4:12;
hence contradiction;
end; then
reconsider q as non zero Polynomial of A by UPROOTS:def 5;
reconsider degq = deg q as Element of NAT;
assume p is_with_roots_in A; then
consider b being Element of A such that
H: b is_a_root_of p,A by FIELD_4:def 3;
C: 0.A = Ext_eval(p,b) by H,FIELD_4:def 2 .= eval(q1,b) by FIELD_4:26;
now assume q is constant;
then degq <= 0 by RATFUNC1:def 2;
then consider a being Element of A such that
F: q1 = a|A by RING_4:def 4,RING_4:20;
eval(q,b) = eval(a * 1_.(A),b) by F,RING_4:16
.= a * eval(1_.(A),b) by RING_5:7
.= a * 1.A by POLYNOM4:18;
hence contradiction by C,F;
end;
then ex a being non zero Element of A, r being Ppoly of A st q = a * r
by FIELD_12:22,FIELD_4:def 5;
hence p splits_in A by FIELD_4:def 5;
end;
hence thesis;
end;
end;
registration
let F be Field;
cluster F-algebraic F-normal for FieldExtension of F;
existence
proof
set A = the AlgebraicClosure of F;
take A;
thus thesis;
end;
end;
registration
cluster FAdj(F_Rat,{3-Root(2)}) -> non F_Rat-normal;
coherence
proof
set E = FAdj(F_Rat,{3-Root(2)}), p = X^3-2;
H: {3-Root(2)} is Subset of E & 3-Root(2) in {3-Root(2)}
by FIELD_6:35,TARSKI:def 1;
{3-Root(2)} = {a where a is Element of E : a is_a_root_of X^3-2,E}
by FIELD_10:64,FIELD_4:def 4; then
consider a being Element of E such that
A: a = 3-Root(2) & a is_a_root_of X^3-2,E by H;
thus thesis by A,FIELD_4:def 3,FIELD_10:65;
end;
end;
theorem
for F being Field,
E being F-algebraic FieldExtension of F
holds E is F-normal iff
for a being Element of E holds MinPoly(a,F) splits_in E by lemmin;
lemNor1:
for F being Field,
E being F-finite FieldExtension of F
holds E is F-normal implies
ex p being non constant Element of the carrier of Polynom-Ring F
st E is SplittingField of p
proof
let F be Field, E be F-finite FieldExtension of F;
assume AS: E is F-normal;
consider T being finite F-algebraic Subset of E such that
A: E == FAdj(F,T) by FIELD_7:37;
per cases;
suppose T is empty; then
for o being object st o in T holds o in the carrier of F; then
T is Subset of the carrier of F by TARSKI:def 3; then
H: FAdj(F,T) == F by FIELD_7:3;
reconsider p = rpoly(1,0.F) as
Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
deg rpoly(1,0.F) = 1 by HURWITZ:27; then
reconsider p as
linear Element of the carrier of Polynom-Ring F by FIELD_5:def 1;
F is SplittingField of p by lemNor1e; then
FAdj(F,T) is SplittingField of p by H,lemNor1d; then
E is SplittingField of p by A,lemNor1d;
hence thesis;
end;
suppose T is non empty;
then reconsider T as non empty finite F-algebraic Subset of E;
set M = the set of all MinPoly(a,F) where a is Element of T;
set x = the Element of T;
E: MinPoly(x,F) in M;
now let o be object;
assume o in the set of all MinPoly(a,F) where a is Element of T;
then consider a being Element of T such that
F: o = MinPoly(a,F);
thus o in the carrier of Polynom-Ring F by F;
end; then
reconsider M as non empty Subset of the carrier of Polynom-Ring F
by E,TARSKI:def 3;
defpred Q[object,object] means
ex a being Element of T st a = $1 & $2 = MinPoly(a,F);
E1: for a being Element of T ex y being Element of M st Q[a,y]
proof
let a be Element of T;
MinPoly(a,F) in the set of all MinPoly(a,F) where a is Element of T;
then reconsider y = MinPoly(a,F) as Element of M;
take y;
thus Q[a,y];
end;
consider f being Function of T,M such that
E2: for a being Element of T holds Q[a,f.a] from FUNCT_2:sch 3(E1);
E3: dom f = T by FUNCT_2:def 1;
rng f = M
proof
E4: now let o be object;
assume o in M; then
consider a being Element of T such that
E5: o = MinPoly(a,F);
Q[a,f.a] by E2;
hence o in rng f by E5,E3,FUNCT_1:def 3;
end;
now let o be object;
assume o in rng f; then
consider a be object such that
E4: a in dom f & f.a = o by FUNCT_1:def 3;
reconsider a as Element of T by E4;
Q[a,o] by E2,E4;
hence o in M;
end;
hence thesis by E4,TARSKI:2;
end; then
reconsider M as non empty finite Subset of the carrier of Polynom-Ring F;
rng(canFS M) c= M & M c= the carrier of Polynom-Ring F by FINSEQ_1:def 4; then
len canFS M = card M & rng(canFS M) c= the carrier of Polynom-Ring F
by FINSEQ_1:93; then
reconsider G = canFS M as
non empty FinSequence of the carrier of Polynom-Ring F by FINSEQ_1:def 4;
reconsider p = Product G as Element of the carrier of Polynom-Ring F;
F: ex i being Element of dom G st G.i = MinPoly(x,F)
proof
rng(canFS M) = M by FUNCT_2:def 3; then
MinPoly(x,F) in rng(canFS M); then
consider i being object such that
H: i in dom(canFS M) & (canFS M).i = MinPoly(x,F) by FUNCT_1:def 3;
thus thesis by H;
end;
Product G is non constant
proof
now let i be Element of dom G;
H1: G.i in rng G by FUNCT_1:def 3;
rng(canFS M) c= M by FINSEQ_1:def 4; then
G.i in M by H1; then
consider a being Element of T such that
H2: G.i = MinPoly(a,F);
thus G.i <> 0_.F by H2;
end;
then H: deg p >= deg MinPoly(x,F) by F,lemNor1deg;
deg MinPoly(x,F) > 0 by RING_4:def 4;
hence thesis by H,RING_4:def 4;
end; then
reconsider p = Product G
as non constant Element of the carrier of Polynom-Ring F;
D: p splits_in E
proof
deg p > 0 by RING_4:def 4; then
reconsider q = p as non constant Polynomial of F by RATFUNC1:def 2;
now let i be Element of dom G, p be Polynomial of F;
assume D1: p = G.i;
rng G c= M & G.i in rng G by FUNCT_1:3,FINSEQ_1:def 4; then
G.i in M; then
consider a being Element of T such that
D2: G.i = MinPoly(a,F);
thus p is constant or p splits_in E by D1,D2,AS,lemmin;
end;
then q splits_in E by lemNor1a;
hence thesis;
end;
now let K being FieldExtension of F;
assume E1: p splits_in K & K is Subfield of E; then
E2: F is Subfield of K & E is K-extending by FIELD_4:7; then
E3: Roots(K,p) = Roots(E,p) by D,E1,FIELD_8:29;
E4: Roots(E,p) = {a where a is Element of E : a is_a_root_of p,E}
by FIELD_4:def 4;
T is Subset of K
proof
now let o be object;
assume o in T; then
reconsider a = o as Element of T;
rng G = M by FUNCT_2:def 3; then
MinPoly(a,F) in rng G; then
consider i being object such that
E5: i in dom G & G.i = MinPoly(a,F) by FUNCT_1:def 3;
Ext_eval(MinPoly(a,F),a) = 0.E by FIELD_6:52; then
Ext_eval(p,a) = 0.E by E5,lemNor1b; then
a is_a_root_of p,E by FIELD_4:def 2; then
a in Roots(E,p) by E4;
hence o in the carrier of K by E3;
end;
hence thesis by TARSKI:def 3;
end; then
FAdj(F,T) is Subfield of K by E1,E2,FIELD_6:37; then
K is FAdj(F,T)-extending by FIELD_4:7; then
K is E-extending by A,FIELD_12:37; then
E is Subfield of K by FIELD_4:7;
hence K == E by E1,FIELD_7:def 2;
end;
then E is SplittingField of p by D,FIELD_8:def 1;
hence thesis;
end;
end;
lemNor2:
for F being Field,
E being F-finite FieldExtension of F
holds (ex p being non constant Element of the carrier of Polynom-Ring F
st E is SplittingField of p)
implies
for K being FieldExtension of E
for h being F-fixing Monomorphism of E,K holds h is Automorphism of E
proof
let F be Field, E be F-finite FieldExtension of F;
assume ex p being non constant Element of the carrier of Polynom-Ring F
st E is SplittingField of p; then
consider p being non constant Element of the carrier of Polynom-Ring F
such that AS: E is SplittingField of p;
reconsider U = E as SplittingField of p by AS;
B: the doubleLoopStr of E = the doubleLoopStr of FAdj(F,Roots(E,p))
by AS,FIELD_8:34,FIELD_7:def 1;
now let K1 be FieldExtension of E, h be F-fixing Monomorphism of E,K1;
reconsider K = K1 as E-extending FieldExtension of F;
p splits_in E by AS,FIELD_8:def 1; then
h .: Roots(U,p) c= the carrier of E by lemNor2b; then
C: h.:(the carrier of FAdj(F,Roots(E,p))) c= the carrier of E by lemNor2c;
reconsider g = h|(the carrier of E) as Function of E,E by B,C,FUNCT_2:101;
D: E is Subfield of K by FIELD_4:7;
g is additive multiplicative unity-preserving
proof
now let x,y be Element of E;
dom h = the carrier of E by FUNCT_2:def 1; then
h.x in h.:(the carrier of E) & h.y in h.:(the carrier of E)
by FUNCT_1:def 6; then
reconsider a = h.x, b = h.y as Element of E by B,C;
E: [a,b] in [:the carrier of E,the carrier of E:];
thus g.(x+y) = h.x + h.y by VECTSP_1:def 20
.= ((the addF of K) || the carrier of E).(a,b) by E,FUNCT_1:49
.= g.x + g.y by D,EC_PF_1:def 1;
end;
hence g is additive;
now let x,y be Element of E;
dom h = the carrier of E by FUNCT_2:def 1; then
h.x in h.:(the carrier of E) & h.y in h.:(the carrier of E)
by FUNCT_1:def 6; then
reconsider a = h.x, b = h.y as Element of E by B,C;
E: [a,b] in [:the carrier of E,the carrier of E:];
thus g.(x*y) = h.x * h.y by GROUP_6:def 6
.= ((the multF of K) || the carrier of E).(a,b) by E,FUNCT_1:49
.= g.x * g.y by D,EC_PF_1:def 1;
end;
hence g is multiplicative;
g.(1_E) = 1_K by GROUP_1:def 13 .= 1.E by D,EC_PF_1:def 1;
hence thesis;
end; then
reconsider g as Monomorphism of E;
for a being Element of F holds g.a = a by FIELD_8:def 2;
then g is F-fixing by FIELD_8:def 2;
hence h is Automorphism of E;
end;
hence thesis;
end;
lemNor31:
for F being Field,
E being FieldExtension of F
for T being Subset of E,
a being Element of E
st a in the carrier of FAdj(F,T) holds FAdj(F,T\/{a}) = FAdj(F,T)
proof
let F be Field, E be FieldExtension of F,
T be Subset of E, a be Element of E;
assume a in the carrier of FAdj(F,T); then
A: {a} c= the carrier of FAdj(F,T) by TARSKI:def 1;
reconsider E1 = E as FieldExtension of FAdj(F,T) by FIELD_4:7;
reconsider a1 = a as Element of E1;
FAdj(F,T\/{a}) = FAdj(FAdj(F,T),{a1}) by FIELD_7:34;
hence thesis by A,FIELD_6:38;
end;
lemNor3:
for F being Field,
E being F-finite FieldExtension of F
st for K being FieldExtension of E
for h being F-fixing Monomorphism of E,K holds h is Automorphism of E
holds E is F-normal
proof
let F be Field, E be F-finite FieldExtension of F;
assume AS:
for K being FieldExtension of E
for h being F-fixing Monomorphism of E,K holds h is Automorphism of E;
consider T being finite F-algebraic Subset of E such that
A: E == FAdj(F,T) by FIELD_7:37;
B: the doubleLoopStr of E = the doubleLoopStr of FAdj(F,T) by A,FIELD_7:def 1;
now let a be Element of E;
set T1 = T \/ {a};
reconsider T1 as non empty finite F-algebraic Subset of E;
Z: E == FAdj(F,T1) by A,B,lemNor31;
set M = the set of all MinPoly(a,F) where a is Element of T1;
a in {a} by TARSKI:def 1; then
H: a in T1 by XBOOLE_0:def 3; then
E: MinPoly(a,F) in M;
now let o be object;
assume o in the set of all MinPoly(a,F) where a is Element of T1;
then consider a being Element of T1 such that
F: o = MinPoly(a,F);
thus o in the carrier of Polynom-Ring F by F;
end; then
reconsider M as non empty Subset of the carrier of Polynom-Ring F
by E,TARSKI:def 3;
defpred Q[object,object] means
ex a being Element of T1 st a = $1 & $2 = MinPoly(a,F);
E1: for a being Element of T1 ex y being Element of M st Q[a,y]
proof
let a be Element of T1;
MinPoly(a,F) in the set of all MinPoly(a,F) where a is Element of T1;
then reconsider y = MinPoly(a,F) as Element of M;
take y;
thus Q[a,y];
end;
consider f being Function of T1,M such that
E2: for a being Element of T1 holds Q[a,f.a] from FUNCT_2:sch 3(E1);
E3: dom f = T1 by FUNCT_2:def 1;
rng f = M
proof
E4: now let o be object;
assume o in M; then
consider a being Element of T1 such that
E5: o = MinPoly(a,F);
Q[a,f.a] by E2;
hence o in rng f by E5,E3,FUNCT_1:def 3;
end;
now let o be object;
assume o in rng f; then
consider a be object such that
E4: a in dom f & f.a = o by FUNCT_1:def 3;
reconsider a as Element of T1 by E4;
Q[a,o] by E2,E4;
hence o in M;
end;
hence thesis by E4,TARSKI:2;
end; then
reconsider M as non empty finite Subset of the carrier of Polynom-Ring F;
rng(canFS M) c= M & M c= the carrier of Polynom-Ring F by FINSEQ_1:def 4; then
len canFS M = card M & rng(canFS M) c= the carrier of Polynom-Ring F
by FINSEQ_1:93; then
reconsider G = canFS M as
non empty FinSequence of the carrier of Polynom-Ring F by FINSEQ_1:def 4;
reconsider p = Product G as Element of the carrier of Polynom-Ring F;
F: ex i being Element of dom G st G.i = MinPoly(a,F)
proof
rng(canFS M) = M by FUNCT_2:def 3; then
MinPoly(a,F) in rng(canFS M) by H; then
consider i being object such that
H: i in dom(canFS M) & (canFS M).i = MinPoly(a,F) by FUNCT_1:def 3;
thus thesis by H;
end;
Product G is non constant
proof
now let i be Element of dom G;
H1: G.i in rng G by FUNCT_1:def 3;
rng(canFS M) c= M by FINSEQ_1:def 4; then
G.i in M by H1; then
consider a being Element of T1 such that
H2: G.i = MinPoly(a,F);
thus G.i <> 0_.F by H2;
end;
then H: deg p >= deg MinPoly(a,F) by F,lemNor1deg;
deg MinPoly(a,F) > 0 by RING_4:def 4;
hence thesis by H,RING_4:def 4;
end;
then reconsider pF = Product G as
non constant Element of the carrier of Polynom-Ring F;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E
by FIELD_4:10; then
reconsider p = pF as Element of the carrier of Polynom-Ring E;
deg pF > 0 & deg pF = deg p by FIELD_4:20,RING_4:def 4; then
reconsider p as non constant Element of the carrier of Polynom-Ring E
by RING_4:def 4;
L1: for u being Element of T1 ex i being Element of dom G st G.i = MinPoly(u,F)
proof
let u be Element of T1;
rng(canFS M) = M by FUNCT_2:def 3; then
MinPoly(u,F) in rng(canFS M); then
consider i being object such that
H: i in dom(canFS M) & (canFS M).i = MinPoly(u,F) by FUNCT_1:def 3;
thus thesis by H;
end;
L2: p = MinPoly(a,F) or
ex q being non zero Polynomial of F st p = MinPoly(a,F) *' q
proof
assume p <> MinPoly(a,F);
set x = the Element of T;
consider j being Element of dom G such that
K1: G.j = MinPoly(a,F) by H,L1;
dom G = Seg(len G) by FINSEQ_1:def 3; then
1 <= j & j <= len G by FINSEQ_1:1; then
G = (G|(j-'1)) ^ <*G.j*> ^ (G/^j) by FINSEQ_5:84; then
K2: Product G
= Product(G|(j-'1)^<*G.j*>) * Product((G/^j)) by GROUP_4:5
.= (Product(G|(j-'1)) * Product(<*G.j*>)) * Product(G/^j) by GROUP_4:5
.= (Product(<*G.j*>) * Product(G|(j-'1))) * Product(G/^j)
by GROUP_1:def 12
.= Product(<*G.j*>) *(Product(G|(j-'1)) * Product(G/^j))
by GROUP_1:def 3;
reconsider r1 = Product(G|(j-'1)),
r2 = Product(G/^j) as Polynomial of F by POLYNOM3:def 10;
K3: r1 *' r2 = Product(G|(j-'1)) * Product(G/^j) by POLYNOM3:def 10;
Product <*G.j*> = MinPoly(a,F) by K1,GROUP_4:9; then
K4: p = MinPoly(a,F) *' (r1 *' r2) by K2,K3,POLYNOM3:def 10; then
r1 *' r2 is non zero Polynomial of F;
hence ex q being non zero Polynomial of F st p = MinPoly(a,F) *' q by K4;
end;
L3: for u being Element of T1 holds u in Roots p
proof
let u be Element of T1;
M0: Ext_eval(MinPoly(u,F),u) = 0.E by FIELD_6:51;
consider i being Element of dom G such that
M1: G.i = MinPoly(u,F) by L1;
0.E = Ext_eval(pF,u) by M0,M1,lemNor1b
.= eval(p,u) by FIELD_4:26;
then u is_a_root_of p by POLYNOM5:def 7;
hence thesis by POLYNOM5:def 10;
end;
deg MinPoly(a,F) > 0 by RING_4:def 4; then
L4: MinPoly(a,F) is non constant Polynomial of F by RATFUNC1:def 2;
set U = the SplittingField of p;
reconsider U as E-extending FieldExtension of F;
E is Subfield of U by FIELD_4:7; then
the carrier of E c= the carrier of U by EC_PF_1:def 1; then
T1 c= the carrier of U; then
reconsider T2 = T1 as Subset of U;
G0: MinPoly(a,F) splits_in U
proof
p splits_in U by FIELD_8:def 1; then
consider x being non zero Element of U, r being Ppoly of U such that
G2: p = x * r by FIELD_4:def 5;
per cases by L2;
suppose p = MinPoly(a,F);
hence thesis by G2,FIELD_4:def 5;
end;
suppose ex q being non zero Polynomial of F st p = MinPoly(a,F) *' q;
then consider q being non zero Polynomial of F such that
G3: pF = MinPoly(a,F) *' q;
thus thesis by L4,G3,F811,G2,FIELD_4:def 5;
end;
end;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring FAdj(F,{a})
by FIELD_4:10; then
reconsider pa = p as Element of the carrier of Polynom-Ring FAdj(F,{a});
E is FieldExtension of FAdj(F,{a}) by FIELD_4:7; then
deg p > 0 & deg pa = deg p by FIELD_4:20,RING_4:def 4; then
reconsider pa as non constant
Element of the carrier of Polynom-Ring FAdj(F,{a})
by RING_4:def 4;
G1: U is SplittingField of pa
proof
reconsider E1 = E as FieldExtension of FAdj(F,{a}) by FIELD_4:7;
reconsider T2 = T as Subset of E1;
P0: FAdj(F,T1) = FAdj(FAdj(F,{a}),T2) by FIELD_7:35;
now let x be Element of E1;
assume x in T2;
consider p being non zero Polynomial of F such that
H: Ext_eval(p,x) = 0.E by FIELD_6:43;
reconsider p1 = p as Polynomial of FAdj(F,{a}) by FIELD_4:8;
p <> 0_.F; then
p1 <> 0_.FAdj(F,{a}) by FIELD_4:12; then
reconsider p1 as non zero Polynomial of FAdj(F,{a}) by UPROOTS:def 5;
p is Element of the carrier of Polynom-Ring F &
p1 is Element of the carrier of Polynom-Ring FAdj(F,{a})
by POLYNOM3:def 10; then
Ext_eval(p1,x) = 0.E by H,FIELD_7:15;
hence x is FAdj(F,{a})-algebraic by FIELD_6:43;
end; then
P1: T is FAdj(F,{a})-algebraic Subset of E1 by FIELD_7:def 12;
T c= T1 by XBOOLE_1:7; then
T c= Roots p & Roots p c= Roots(U,p) by L3,FIELD_4:28; then
T c= Roots(U,p);
hence thesis by Z,P0,P1,lemNor32;
end;
now let o be object;
assume LL: o in Roots(U,MinPoly(a,F)); then
reconsider b = o as Element of U;
Roots(U,MinPoly(a,F))
= {x where x is Element of U : x is_a_root_of MinPoly(a,F),U}
by FIELD_4:def 4; then
consider c being Element of U such that
LK: c = b & c is_a_root_of MinPoly(a,F),U by LL;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring FAdj(F,{b})
by FIELD_4:10; then
reconsider pb = pF as Element of the carrier of Polynom-Ring FAdj(F,{b});
deg pF > 0 & deg pb = deg pF by FIELD_4:20,RING_4:def 4; then
reconsider pb as non constant
Element of the carrier of Polynom-Ring FAdj(F,{b})
by RING_4:def 4;
G2: U is SplittingField of pb
proof
G0: U is FieldExtension of FAdj(F,{b}) by FIELD_4:7;
reconsider U1 = U as FieldExtension of FAdj(F,{b}) by FIELD_4:7;
p splits_in U by FIELD_8:def 1; then
consider x being non zero Element of U, r being Ppoly of U such that
G3: p = x * r by FIELD_4:def 5;
G4: pb splits_in U by G3,FIELD_4:def 5;
GG: Roots(U1,pb) = Roots(U,p) by lemNor3z;
L6: FAdj(F,T2) == FAdj(F,T1) by lemh1;
now let V be FieldExtension of FAdj(F,{b});
assume G5: pb splits_in V & V is Subfield of U; then
consider y being non zero Element of V, s being Ppoly of V such that
K2: pb = y * s by FIELD_4:def 5;
G9: U is V-extending by G5,FIELD_4:7;
G6: p splits_in V by K2,FIELD_4:def 5;
GH: Roots(U1,pb) c= the carrier of V by G9,G4,G5,FIELD_8:27;
F is Subfield of V by FIELD_4:7; then
G8: FAdj(F,Roots(U,p)) is Subfield of V by G5,GG,GH,FIELD_6:37;
Roots p c= Roots(U,p) by FIELD_4:28; then
T1 c= Roots(U,p) by L3; then
FAdj(F,T2) is Subfield of FAdj(F,Roots(U,p)) by FIELD_7:10; then
FAdj(F,T2) is Subfield of V by G8,EC_PF_1:5; then
V is FieldExtension of FAdj(F,T2) by FIELD_4:7; then
V is FieldExtension of E by FIELD_12:37,L6,Z,helpb;
hence V == U by G5,G6,FIELD_8:def 1;
end;
hence thesis by G0,G3,FIELD_4:def 5,FIELD_8:def 1;
end;
id F is isomorphism; then
reconsider F1 = F
as F-isomorphic F-homomorphic Field by RING_2:def 4,RING_3:def 4;
reconsider U1 = U as FieldExtension of F1;
reconsider b1 = b as Element of U1;
reconsider f = id F as Isomorphism of F,F1;
G3: Ext_eval(MinPoly(a,F),a) = 0.E by FIELD_6:51;
K1: now let p be Element of the carrier of Polynom-Ring F;
now let i be Nat;
thus ((PolyHom f).p).i = f.(p.i) by FIELD_1:def 2 .= p.i;
end;
hence (PolyHom f).p = p;
end;
G4: Ext_eval((PolyHom f).MinPoly(a,F),b1)
= Ext_eval(MinPoly(a,F),b1) by K1
.= 0.U1 by LK,FIELD_4:def 2; then
G5: Psi(a,b1,f,MinPoly(a,F)) is f-extending isomorphism by G3,FIELD_8:55; then
reconsider Fb = FAdj(F,{b})
as FAdj(F,{a})-homomorphic FAdj(F,{a})-isomorphic Field
by RING_2:def 4,RING_3:def 4;
reconsider i = Psi(a,b1,f,MinPoly(a,F)) as Isomorphism of FAdj(F,{a}),Fb by G5;
(PolyHom i).pa = (PolyHom f).pF
proof
now let j be Nat;
thus ((PolyHom i).pa).j
= i.(pa.j) by FIELD_1:def 2
.= f.(pF.j) by G4,G3,FIELD_8:55,FIELD_8:def 6
.= ((PolyHom f).pF).j by FIELD_1:def 2;
end;
hence thesis;
end; then
reconsider U1 as SplittingField of (PolyHom i).pa by K1,G2;
reconsider U as SplittingField of pa by G1;
consider h being Function of U,U1 such that
G6: h is i-extending isomorphism by FIELD_8:57;
G7: h is additive multiplicative unity-preserving by G6;
reconsider U as FieldExtension of E;
reconsider h as Function of U,U;
E is Subfield of U by FIELD_4:7; then
the carrier of E c= the carrier of U by EC_PF_1:def 1; then
reconsider g = h|(the carrier of E) as Function of E,U by FUNCT_2:32;
g is additive multiplicative unity-preserving
proof
C: E is Subfield of U by FIELD_4:7; then
D: the carrier of E c= the carrier of U by EC_PF_1:def 1;
E: E is Subring of U by C,FIELD_5:12;
now let x,y be Element of E;
reconsider a = x, b = y as Element of U by D;
x + y = a + b by E,FIELD_6:15;
hence g.(x+y) = h.(a+b) by FUNCT_1:49
.= h.a + h.b by G7
.= h.a + g.y by FUNCT_1:49
.= g.x + g.y by FUNCT_1:49;
end;
hence g is additive;
now let x,y be Element of E;
reconsider a = x, b = y as Element of U by D;
x * y = a * b by E,FIELD_6:16;
hence g.(x*y) = h.(a*b) by FUNCT_1:49
.= h.a * h.b by G7
.= h.a * g.y by FUNCT_1:49
.= g.x * g.y by FUNCT_1:49;
end;
hence g is multiplicative;
1.E = 1.U by C,EC_PF_1:def 1;
hence thesis by G7,FUNCT_1:49;
end; then
reconsider g as Monomorphism of E,U;
now let x be Element of F;
F is Subfield of FAdj(F,{a}) by FIELD_6:36; then
the carrier of F c= the carrier of FAdj(F,{a}) by EC_PF_1:def 1; then
reconsider y = x as Element of FAdj(F,{a});
F is Subfield of E by FIELD_4:7; then
the carrier of F c= the carrier of E by EC_PF_1:def 1;
hence g.x = h.y by FUNCT_1:49
.= i.y by G6,FIELD_8:def 6
.= f.x by G4,G3,FIELD_8:55,FIELD_8:def 6
.= x;
end;
then g is F-fixing by FIELD_8:def 2; then
reconsider g as Automorphism of E by AS;
g.a = b
proof
a in {a} & {a} is Subset of FAdj(F,{a}) by TARSKI:def 1,FIELD_6:35;
then reconsider c = a as Element of FAdj(F,{a});
thus g.a = h.c by FUNCT_1:49
.= Psi(a,b1,f,MinPoly(a,F)).c by G6,FIELD_8:def 6
.= b by G3,G4,lemNor3e;
end;
hence o in the carrier of E;
end; then
Roots(U,MinPoly(a,F)) c= the carrier of E;
hence MinPoly(a,F) splits_in E by G0,FIELD_8:27;
end;
hence thesis by lemmin;
end;
theorem main1:
for F being Field,
E being F-finite FieldExtension of F
holds E is F-normal iff
ex p being non constant Element of the carrier of Polynom-Ring F
st E is SplittingField of p
proof
let F be Field, E be F-finite FieldExtension of F;
now assume ex p being non constant Element of the carrier of Polynom-Ring F
st E is SplittingField of p; then
for K being FieldExtension of E
for h being F-fixing Monomorphism of E,K holds h is Automorphism of E
by lemNor2;
hence E is F-normal by lemNor3;
end;
hence thesis by lemNor1;
end;
theorem
for F being Field,
E being F-finite FieldExtension of F
holds E is F-normal iff
for K being FieldExtension of E
for h being F-fixing Monomorphism of E,K holds h is Automorphism of E
proof
let F be Field, E be F-finite FieldExtension of F;
now assume E is F-normal; then
ex p being non constant Element of the carrier of Polynom-Ring F
st E is SplittingField of p by lemNor1;
hence for K being FieldExtension of E
for h being F-fixing Monomorphism of E,K holds h is Automorphism of E
by lemNor2;
end;
hence thesis by lemNor3;
end;
registration
let F be Field;
let p be non constant Element of the carrier of Polynom-Ring F;
cluster -> F-normal for SplittingField of p;
coherence by main1;
end;
theorem
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
holds FAdj(F,{a}) is F-normal iff MinPoly(a,F) splits_in FAdj(F,{a})
proof
let F be Field, E be FieldExtension of F, a be F-algebraic Element of E;
set K = FAdj(F,{a});
{a} is Subset of K & a in {a} by FIELD_6:35,TARSKI:def 1; then
reconsider a1 = a as Element of K;
E is K-extending by FIELD_4:7; then
Ext_eval(MinPoly(a,F),a1)
= Ext_eval(MinPoly(a,F),a) by FIELD_6:11
.= 0.E by FIELD_6:52
.= 0.K by EC_PF_1:def 1; then
H1: a1 is_a_root_of MinPoly(a,F),K by FIELD_4:def 2;
Roots(K,MinPoly(a,F))
= {b where b is Element of K : b is_a_root_of MinPoly(a,F),K}
by FIELD_4:def 4; then
H2: a in Roots(K,MinPoly(a,F)) by H1;
now assume AS: MinPoly(a,F) splits_in K;
now let U be FieldExtension of F;
assume B: MinPoly(a,F) splits_in U & U is Subfield of K;
then K is U-extending by FIELD_4:7;
then Roots(K,MinPoly(a,F)) c= the carrier of U by AS,B,FIELD_8:27;
then a in the carrier of U by H2;
then {a} c= the carrier of U by TARSKI:def 1;
then {a} is Subset of U & F is Subfield of U & U is Subfield of E
by FIELD_4:7,B,EC_PF_1:5;
then K is Subfield of U by FIELD_6:37;
hence U == K by B,FIELD_7:def 2;
end;
then K is SplittingField of MinPoly(a,F) by AS,FIELD_8:def 1;
hence K is F-normal;
end;
hence thesis by H1,FIELD_4:def 3;
end;
theorem
for F being Field,
E being FieldExtension of F
for T being non empty finite F-algebraic Subset of E
holds FAdj(F,T) is F-normal iff
for a being Element of T holds MinPoly(a,F) splits_in FAdj(F,T)
proof
let F be Field, E be FieldExtension of F,
T be non empty finite F-algebraic Subset of E;
set V = FAdj(F,T);
A: now assume B: V is F-normal;
now let a be Element of T;
T is Subset of V & a in T by FIELD_6:35; then
reconsider a1 = a as Element of V;
E is V-extending by FIELD_4:7; then
Ext_eval(MinPoly(a,F),a1)
= Ext_eval(MinPoly(a,F),a) by FIELD_6:11
.= 0.E by FIELD_6:52
.= 0.V by EC_PF_1:def 1; then
a1 is_a_root_of MinPoly(a,F),V by FIELD_4:def 2;
hence MinPoly(a,F) splits_in V by B,FIELD_4:def 3;
end;
hence for a being Element of T holds MinPoly(a,F) splits_in V;
end;
now assume BB:
for a being Element of T holds MinPoly(a,F) splits_in V;
set M = the set of all MinPoly(a,F) where a is Element of T;
set x = the Element of T;
E: MinPoly(x,F) in M;
now let o be object;
assume o in the set of all MinPoly(a,F) where a is Element of T;
then consider a being Element of T such that
F: o = MinPoly(a,F);
thus o in the carrier of Polynom-Ring F by F;
end; then
reconsider M as non empty Subset of the carrier of Polynom-Ring F
by E,TARSKI:def 3;
defpred Q[object,object] means
ex a being Element of T st a = $1 & $2 = MinPoly(a,F);
E1: for a being Element of T ex y being Element of M st Q[a,y]
proof
let a be Element of T;
MinPoly(a,F) in the set of all MinPoly(a,F) where a is Element of T;
then reconsider y = MinPoly(a,F) as Element of M;
take y;
thus Q[a,y];
end;
consider f being Function of T,M such that
E2: for a being Element of T holds Q[a,f.a] from FUNCT_2:sch 3(E1);
E3: dom f = T by FUNCT_2:def 1;
rng f = M
proof
E4: now let o be object;
assume o in M; then
consider a being Element of T such that
E5: o = MinPoly(a,F);
Q[a,f.a] by E2;
hence o in rng f by E5,E3,FUNCT_1:def 3;
end;
now let o be object;
assume o in rng f; then
consider a be object such that
E4: a in dom f & f.a = o by FUNCT_1:def 3;
reconsider a as Element of T by E4;
Q[a,o] by E2,E4;
hence o in M;
end;
hence thesis by E4,TARSKI:2;
end; then
reconsider M as non empty finite Subset of the carrier of Polynom-Ring F;
rng(canFS M) c= M & M c= the carrier of Polynom-Ring F by FINSEQ_1:def 4; then
len canFS M = card M & rng(canFS M) c= the carrier of Polynom-Ring F
by FINSEQ_1:93; then
reconsider G = canFS M as
non empty FinSequence of the carrier of Polynom-Ring F by FINSEQ_1:def 4;
reconsider p = Product G as Element of the carrier of Polynom-Ring F;
F: ex i being Element of dom G st G.i = MinPoly(x,F)
proof
rng(canFS M) = M by FUNCT_2:def 3; then
MinPoly(x,F) in rng(canFS M); then
consider i being object such that
H: i in dom(canFS M) & (canFS M).i = MinPoly(x,F) by FUNCT_1:def 3;
thus thesis by H;
end;
Product G is non constant
proof
now let i be Element of dom G;
H1: G.i in rng G by FUNCT_1:def 3;
rng(canFS M) c= M by FINSEQ_1:def 4; then
G.i in M by H1; then
consider a being Element of T such that
H2: G.i = MinPoly(a,F);
thus G.i <> 0_.F by H2;
end;
then H: deg p >= deg MinPoly(x,F) by F,lemNor1deg;
deg MinPoly(x,F) > 0 by RING_4:def 4;
hence thesis by H,RING_4:def 4;
end; then
reconsider p = Product G
as non constant Element of the carrier of Polynom-Ring F;
D: p splits_in V
proof
deg p > 0 by RING_4:def 4; then
reconsider q = p as non constant Polynomial of F by RATFUNC1:def 2;
now let i be Element of dom G, p be Polynomial of F;
assume D1: p = G.i;
rng G c= M & G.i in rng G by FUNCT_1:3,FINSEQ_1:def 4; then
G.i in M; then
consider a being Element of T such that
D2: G.i = MinPoly(a,F);
thus p is constant or p splits_in V by D1,D2,BB;
end;
then q splits_in V by lemNor1a;
hence thesis;
end;
now let K be FieldExtension of F;
assume E1: p splits_in K & K is Subfield of V; then
E2: F is Subfield of K & V is K-extending by FIELD_4:7; then
E3: Roots(K,p) = Roots(V,p) by D,E1,FIELD_8:29;
E4: Roots(V,p) = {a where a is Element of V : a is_a_root_of p,V}
by FIELD_4:def 4;
E8: E is V-extending & K is Subfield of E by E1,EC_PF_1:5,FIELD_4:7;
T is Subset of K
proof
now let o be object;
assume Y: o in T; then
reconsider a = o as Element of T;
T is Subset of V by FIELD_6:35; then
reconsider a1 = a as Element of V by Y;
rng G = M by FUNCT_2:def 3; then
MinPoly(a,F) in rng G; then
consider i being object such that
E5: i in dom G & G.i = MinPoly(a,F) by FUNCT_1:def 3;
Ext_eval(MinPoly(a,F),a) = 0.E by FIELD_6:52; then
0.E = Ext_eval(p,a) by E5,lemNor1b
.= Ext_eval(p,a1) by E8,FIELD_7:14; then
Ext_eval(p,a1) = 0.V by EC_PF_1:def 1; then
a1 is_a_root_of p,V by FIELD_4:def 2; then
a1 in Roots(V,p) by E4;
hence o in the carrier of K by E3;
end;
hence thesis by TARSKI:def 3;
end; then
V is Subfield of K by E2,E8,FIELD_6:37;
hence K == V by E1,FIELD_7:def 2;
end;
then V is SplittingField of p by D,FIELD_8:def 1;
hence V is F-normal;
end;
hence thesis by A;
end;