:: Existence and Uniqueness of Algebraic Closures
:: by Christoph Schwarzweller
::
:: Received December 27, 2022
:: Copyright (c) 2022-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, EQREL_1, STRUCT_0, NAT_1,
SUBSET_1, SUPINF_2, POLYNOM8, FUNCT_2, INT_2, MESFUNC1, C0SP1, CARD_1,
GROUP_6, POLYNOM1, POLYNOM3, FUNCSDOM, RLVECT_1, GROUP_2, EC_PF_1,
HURWITZ, FINSEQ_1, FINSET_1, FUNCT_1, RELAT_1, PRALG_1, BINOP_1,
XBOOLE_0, NUMBERS, POLYNOM5, GROUP_1, ZFMISC_1, VECTSP_2, MOD_4,
GLIB_000, REARRAN1, CAT_1, YELLOW_8, RATFUNC1, RING_2, RING_3, RING_4,
MSSUBFAM, LATTICES, IDEAL_1, GROEB_2, FDIFF_1, ALGNUM_1, ARYTM_1,
FIELD_4, FIELD_2, FOMODEL1, REALSET1, WELLORD1, XXREAL_0, QUOFIELD,
QC_LANG1, XCMPLX_0, FIELD_6, GCD_1, ORDERS_1, RING_5, FIELD_1, RLVECT_2,
POLYNOM2, FIELD_7, WAYBEL20, FIELD_8, FACIRC_1, SEQ_4, RELAT_2, MCART_1,
FIELD_12;
notations TARSKI, XBOOLE_0, SUBSET_1, BINOP_1, RELAT_1, RELSET_1, FUNCT_1,
ORDINAL1, FUNCT_2, ZFMISC_1, NUMBERS, CARD_1, PARTFUN1, REALSET1,
RELAT_2, XCMPLX_0, XXREAL_0, NAT_1, VFUNCT_1, FINSET_1, ALGSEQ_1,
XTUPLE_0, ORDERS_1, WELLORD1, POLYNOM3, POLYNOM5, POLYNOM4, STRUCT_0,
GROUP_1, GROUP_6, MOD_4, GCD_1, PRALG_1, ALGSTR_0, QUOFIELD, IDEAL_1,
RLVECT_1, VECTSP_2, HURWITZ, VECTSP_1, C0SP1, EC_PF_1, RATFUNC1,
RINGCAT1, EQREL_1, RING_1, RING_2, RING_3, RING_4, RING_5, ALGNUM_1,
FIELD_1, FIELD_2, FIELD_4, FIELD_6, FIELD_7, FIELD_8;
constructors ARYTM_1, POLYNOM4, VFUNCT_1, RATFUNC1, GCD_1, REALSET1, RINGCAT1,
ALGSEQ_1, EQREL_1, ALGNUM_1, TSEP_1, RING_5, ORDERS_1, PRALG_1, FIELD_2,
FIELD_7, FIELD_8;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, STRUCT_0,
VECTSP_1, EC_PF_1, XTUPLE_0, FUNCT_2, ALGSTR_0, MOD_4, RLVECT_1,
QUOFIELD, RELAT_2, FUNCT_1, VFUNCT_1, CARD_1, FINSET_1, RATFUNC1,
RELAT_1, RINGCAT1, RING_2, RING_3, RING_4, RING_5, REALSET1, INT_3,
POLYNOM3, POLYNOM5, FIELD_1, FIELD_2, FIELD_4, FIELD_6, FIELD_7;
requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
definitions ALGSTR_0, VECTSP_1, GROUP_1, RLVECT_1;
equalities STRUCT_0, REALSET1, BINOP_1, ALGSTR_0, POLYNOM3, FIELD_1;
expansions STRUCT_0, GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1, BINOP_1, RING_4,
TARSKI, GROUP_6, QUOFIELD, FUNCT_1, FUNCT_2, ORDERS_1, FIELD_1, FIELD_8;
theorems ALGSTR_0, GROUP_1, GROUP_6, VECTSP_1, VECTSP_2, RLVECT_1, NAT_1,
WELLORD1, C0SP1, FUNCT_2, TARSKI, FUNCT_1, RELAT_1, EC_PF_1, POLYNOM4,
RING_3, RATFUNC1, POLYNOM5, UPROOTS, RING_4, RING_5, ORDERS_1, HURWITZ,
XREAL_1, XBOOLE_0, FIELD_2, FIELD_4, RING_2, POLYNOM3, ALGNUM_1, CARD_2,
ZFMISC_1, XXREAL_0, XBOOLE_1, ORDINAL1, FIELD_1, XTUPLE_0, RINGCAT1,
RING_1, FIELD_6, FIELD_8, RELAT_2, FIELD_5, FIELD_7, PRALG_1, FIELD_11;
schemes BINOP_1, FUNCT_1, FUNCT_2, NAT_1, TARSKI, RECDEF_1;
begin :: Preliminaries
registration
let L be non empty doubleLoopStr;
cluster the doubleLoopStr of L -> non empty;
coherence;
end;
registration
let L be non trivial doubleLoopStr;
cluster the doubleLoopStr of L -> non trivial;
coherence;
end;
registration
let L be non degenerated doubleLoopStr;
cluster the doubleLoopStr of L -> non degenerated;
coherence
proof
0.L <> 1.L;
hence thesis;
end;
end;
registration
let L be add-associative doubleLoopStr;
cluster the doubleLoopStr of L -> add-associative;
coherence
proof
now let a,b,c be Element of the doubleLoopStr of L;
reconsider x = a, y = b, z = c as Element of L;
thus (a + b) + c = (x + y) + z
.= x + (y + z) by RLVECT_1:def 3 .= a + (b + c);
end;
hence thesis;
end;
end;
registration
let L be right_zeroed doubleLoopStr;
cluster the doubleLoopStr of L -> right_zeroed;
coherence
proof
set G = the doubleLoopStr of L;
now let a be Element of G;
reconsider x = a as Element of L;
thus a + 0.G = x + 0.L .= a by RLVECT_1:def 4;
end;
hence thesis;
end;
end;
registration
let L be right_complementable doubleLoopStr;
cluster the doubleLoopStr of L -> right_complementable;
coherence
proof
set G = the doubleLoopStr of L;
now let a be Element of G;
reconsider x = a as Element of L;
consider y being Element of L such that
E1: x + y = 0.L by ALGSTR_0:def 11;
reconsider b = y as Element of G;
a + b = 0.G by E1;
hence a is right_complementable;
end;
hence thesis;
end;
end;
registration
let L be Abelian doubleLoopStr;
cluster the doubleLoopStr of L -> Abelian;
coherence
proof
now let a,b be Element of the doubleLoopStr of L;
reconsider x = a, y = b as Element of L;
thus a + b = x + y .= y + x .= b + a;
end;
hence thesis;
end;
end;
registration
let L be associative doubleLoopStr;
cluster the doubleLoopStr of L -> associative;
coherence
proof
now let a,b,c be Element of the doubleLoopStr of L;
reconsider x = a, y = b, z = c as Element of L;
thus (a * b) * c = (x * y) * z
.= x * (y * z) by GROUP_1:def 3 .= a * (b * c);
end;
hence thesis;
end;
end;
registration
let L be well-unital non empty doubleLoopStr;
cluster the doubleLoopStr of L -> well-unital;
coherence
proof
set G = the doubleLoopStr of L;
now let a be Element of G;
reconsider x = a as Element of L;
A: a * 1.G = x * 1.L .= a;
1.G * a = 1.L * x .= a;
hence a * 1.G = a & 1.G * a = a by A;
end;
hence thesis;
end;
end;
registration
let L be left-distributive non empty doubleLoopStr;
cluster the doubleLoopStr of L -> left-distributive;
coherence
proof
now let a,b,c be Element of the doubleLoopStr of L;
reconsider x = a, y = b, z = c as Element of L;
thus (b+c)*a = (y+z)*x .= y*x + z*x by VECTSP_1:def 3 .= b*a + c*a;
end;
hence thesis;
end;
end;
registration
let L be right-distributive non empty doubleLoopStr;
cluster the doubleLoopStr of L -> right-distributive;
coherence
proof
now let a,b,c be Element of the doubleLoopStr of L;
reconsider x = a, y = b, z = c as Element of L;
thus a*(b+c) = x*(y+z) .= x*y + x*z by VECTSP_1:def 2 .= a*b + a*c;
end;
hence thesis;
end;
end;
registration
let L be commutative doubleLoopStr;
cluster the doubleLoopStr of L -> commutative;
coherence
proof
now let a,b be Element of the doubleLoopStr of L;
reconsider x = a, y = b as Element of L;
thus a * b = x * y .= y * x by GROUP_1:def 12 .= b * a;
end;
hence thesis;
end;
end;
registration
let L be domRing-like non empty doubleLoopStr;
cluster the doubleLoopStr of L -> domRing-like;
coherence
proof
set G = the doubleLoopStr of L;
now let a,b be Element of G;
reconsider x = a, y = b as Element of L;
assume a * b = 0.G;
then x * y = 0.L;
hence a = 0.G or b = 0.G by VECTSP_2:def 1;
end;
hence thesis by VECTSP_2:def 1;
end;
end;
registration
let L be almost_left_invertible doubleLoopStr;
cluster the doubleLoopStr of L -> almost_left_invertible;
coherence
proof
set G = the doubleLoopStr of L;
now let a be Element of G;
assume A: a <> 0.G;
reconsider x = a as Element of L;
x <> 0.L by A;
then x is left_invertible by ALGSTR_0:def 39;
then consider y being Element of L such that
B: y * x = 1.L;
reconsider b = y as Element of G;
b * a = 1.G by B;
hence a is left_invertible;
end;
hence thesis;
end;
end;
lemug:
for F being Field holds the doubleLoopStr of F is Subfield of F
proof
let F be Field;
set G = the doubleLoopStr of F;
the addF of G = (the addF of F) || the carrier of G &
the multF of G = (the multF of F) || the carrier of G &
1.F = 1.G & 0.F = 0.G;
hence thesis by EC_PF_1:def 1;
end;
theorem lemug1:
for F being Field holds the doubleLoopStr of F == F
proof
let F be Field;
set G = the doubleLoopStr of F;
the addF of F = (the addF of G) || the carrier of F &
the multF of F = (the multF of G) || the carrier of F &
1.F = 1.G & 0.F = 0.G;
then F is Subfield of G & G is Subfield of F by EC_PF_1:def 1;
hence thesis by FIELD_7:def 2;
end;
registration
let F be Field;
cluster strict for FieldExtension of F;
existence
proof
set E = the doubleLoopStr of F;
E == F by lemug1;
then F is Subfield of E by FIELD_7:def 2;
then reconsider E as FieldExtension of F by FIELD_4:7;
take E;
thus thesis;
end;
end;
registration
let F be Field;
let L be F-monomorphic Field;
cluster F-homomorphic F-monomorphic for FieldExtension of L;
existence
proof
reconsider L1 = L as FieldExtension of L by FIELD_4:6;
take L1;
thus thesis;
end;
end;
registration
let F be Field;
cluster monic irreducible for Element of the carrier of Polynom-Ring F;
existence
proof
set p = the irreducible Element of the carrier of Polynom-Ring F;
set q = NormPolynomial p;
take q;
thus thesis by RING_4:28;
end;
end;
registration
let F be non algebraic-closed Field;
cluster monic non constant non with_roots for
Element of the carrier of Polynom-Ring F;
existence
proof
now assume A: for p be monic non constant
Element of the carrier of Polynom-Ring F holds p is with_roots;
now let p be Polynomial of F;
reconsider q = NormPolynomial p as Element of
the carrier of Polynom-Ring F by POLYNOM3:def 10;
assume B: len p > 1; then
len p - 1 > 1 - 1 by XREAL_1:9; then
deg p > 0 by HURWITZ:def 2; then
D: p is non constant by RATFUNC1:def 2;
len q > 1 by B,POLYNOM5:57; then
len q - 1 > 1 - 1 by XREAL_1:9; then
q is non constant monic by D,HURWITZ:def 2; then
q is with_roots by A;
hence p is with_roots by B,POLYNOM5:60;
end;
hence F is algebraic-closed by POLYNOM5:def 9;
end;
hence thesis;
end;
end;
theorem F815:
for F1 being Field,
F2 being F1-monomorphic F1-homomorphic Field
for h being Monomorphism of F1,F2
for p being Element of the carrier of Polynom-Ring F1
holds (PolyHom h).(-p) = -(PolyHom h).p
proof
let F1 be Field, F2 be F1-monomorphic F1-homomorphic Field;
let h be Monomorphism of F1,F2;
let p be Element of the carrier of Polynom-Ring F1;
(PolyHom h).p + (PolyHom h).(-p)
= (PolyHom h).(p + -p) by FIELD_1:24
.= (PolyHom h).(0.(Polynom-Ring F1)) by RLVECT_1:5
.= (PolyHom h).(0_.F1) by POLYNOM3:def 10
.= 0_.F2 by FIELD_1:22
.= 0.(Polynom-Ring F2) by POLYNOM3:def 10;
hence thesis by RLVECT_1:6;
end;
theorem F814:
for F1 being Field,
F2 being F1-monomorphic F1-homomorphic Field
for h being Monomorphism of F1,F2
for p,q being Element of the carrier of Polynom-Ring F1
holds p divides q implies (PolyHom h).p divides (PolyHom h).q
proof
let F1 be Field, F2 be F1-monomorphic F1-homomorphic Field;
let h be Monomorphism of F1,F2;
let p,q be Element of the carrier of Polynom-Ring F1;
assume AS: p divides q;
reconsider pp = p, qq = q as Polynomial of F1;
consider rr being Polynomial of F1 such that
B: pp *' rr = qq by AS,RING_4:1;
reconsider r = rr as Element of the carrier of Polynom-Ring F1
by POLYNOM3:def 10;
p * r = q by B,POLYNOM3:def 10; then
C: (PolyHom h).q = (PolyHom h).p * (PolyHom h).r by FIELD_1:25;
reconsider pe = (PolyHom h).p, qe = (PolyHom h).q, re = (PolyHom h).r
as Polynomial of F2;
qe = pe *' re by C,POLYNOM3:def 10;
hence (PolyHom h).p divides (PolyHom h).q by RING_4:1;
end;
registration
let F1 be Field,
F2 be F1-monomorphic F1-homomorphic Field;
let h be Monomorphism of F1,F2;
let p be non constant Element of the carrier of Polynom-Ring F1;
cluster (PolyHom h).p -> non constant for
Element of the carrier of Polynom-Ring F2;
coherence
proof
let q be Element of the carrier of Polynom-Ring F2 such that
A: q = (PolyHom h).p;
deg p > 0 by RING_4:def 4;
hence q is non constant by A,FIELD_1:31;
end;
end;
definition
let R be gcdDomain;
let a,b be Element of R;
pred a,b are_coprime means
1.R is a_gcd of a,b;
end;
theorem copr1:
for F being Field
for p,q being Element of the carrier of Polynom-Ring F
holds p,q are_coprime iff p gcd q = 1_.(F)
proof
let F be Field, p,q be Element of the carrier of Polynom-Ring F;
set P = Polynom-Ring F;
reconsider o = 0_.(F), e = 1_.(F) as Element of the carrier of P
by POLYNOM3:def 10;
consider a,b being Element of Polynom-Ring F such that
H: a = p & b = q & p gcd q = a gcd b by RING_4:def 12;
Y: 1.P = 1_.(F) by POLYNOM3:def 10;
now assume AS: p,q are_coprime; then
AS1: 1.P divides p & 1.P divides q &
for r being Element of the carrier of P st r divides p & r divides q
holds r divides 1.P by RING_4:def 10;
now assume p = 0_.(F) & q = 0_.(F);
then p gcd q = o by H,RING_4:def 11;
then o divides p & o divides q &
for r being Element of the carrier of P
st r divides p & r divides q holds r divides o by H,RING_4:51;
then 0_.(F) divides 1_.(F) by AS1,Y;
then consider r2 being Polynomial of F such that
E: (0_.(F)) *' r2 = 1_.(F) by RING_4:1;
thus contradiction by E;
end;
hence p gcd q = 1_.(F) by H,AS,Y,RING_4:def 11;
end;
hence thesis by H,POLYNOM3:def 10;
end;
theorem copr2:
for F being Field
for p,q being Element of the carrier of Polynom-Ring F
st p,q are_coprime holds p,q have_no_common_roots
proof
let F be Field, p,q be Element of the carrier of Polynom-Ring F;
set P = Polynom-Ring F;
assume AS: p,q are_coprime;
Y: 1.P = 1_.(F) by POLYNOM3:def 10;
now assume p,q have_a_common_root; then
consider a being Element of F such that
A: a is_a_common_root_of p,q by RATFUNC1:def 4;
B: a is_a_root_of p & a is_a_root_of q by A,RATFUNC1:def 3; then
consider rp being Polynomial of F such that
C: p = rpoly(1,a) *' rp by HURWITZ:33;
consider rq being Polynomial of F such that
D: q = rpoly(1,a) *' rq by B,HURWITZ:33;
reconsider rpa = rpoly(1,a) as Element of the carrier of P
by POLYNOM3:def 10;
rpoly(1,a) divides p & rpoly(1,a) divides q by D,C,RING_4:1; then
rpa divides 1.P by AS,RING_4:def 10; then
rpoly(1,a) divides 1_.(F) by Y; then
deg rpoly(1,a) <= deg 1_.(F) by RING_5:13; then
1 <= deg 1_.(F) by HURWITZ:27;
hence contradiction by RATFUNC1:def 2;
end;
hence thesis;
end;
theorem mi1:
for F being Field
for p being Element of the carrier of Polynom-Ring F
holds (ex E being FieldExtension of F,
a being F-algebraic Element of E st p = MinPoly(a,F)) iff
(p is monic irreducible)
proof
let F be Field, p1 be Element of the carrier of Polynom-Ring F;
now assume p1 is irreducible monic;
then reconsider p = p1 as irreducible monic
Element of the carrier of Polynom-Ring F;
set KF = KroneckerField(F,p), u = KrRoot p;
consider FP being Field such that
X1: KF,FP are_isomorphic &
(the carrier of FP) /\ ((the carrier of KF) \/ (the carrier of F)) = {}
by FIELD_5:29;
X: [#] F = the carrier of F & [#] FP = the carrier of FP;
X2: F,FP are_disjoint
proof
now assume A: (the carrier of F) /\ (the carrier of FP) <> {};
set x = the Element of (the carrier of F) /\ (the carrier of FP);
B: x in the carrier of F & x in the carrier of FP by A,XBOOLE_0:def 4;
then x in (the carrier of KF) \/ (the carrier of F) by XBOOLE_0:def 3;
hence contradiction by B,X1,XBOOLE_0:def 4;
end;
hence thesis by X,FIELD_2:def 1;
end;
consider phi being Function of KF,FP such that
X3: phi is isomorphism by X1;
reconsider KroneckerIsop = (KroneckerIso p)" as
Isomorphism of KroneckerField(F,p),Polynom-Ring p by RING_3:73;
set h = phi * (emb p);
reconsider h as Function of F,FP;
X4: h is linear one-to-one by X3,RINGCAT1:1; then
reconsider FP as F-monomorphic Field by RING_3:def 3;
reconsider h as Monomorphism of F,FP by X4;
reconsider E = embField h as Field by X2,FIELD_2:12;
emb_iso h is onto by X2,FIELD_2:15; then
reconsider embisoh = (emb_iso h)" as Function of FP,E by FUNCT_2:25;
emb_iso h is additive multiplicative unity-preserving
by X2,FIELD_2:13,FIELD_2:14; then
Y: emb_iso h is linear one-to-one onto by X2,FIELD_2:15; then
reconsider FP as E-isomorphic Field by RING_3:def 4;
reconsider embisoh as Isomorphism of FP,E by Y,RING_3:73;
set iso = embisoh * phi;
reconsider iso as Function of KF,E;
X5: iso is RingHomomorphism by X3,RINGCAT1:1;
then reconsider E as KF-homomorphic Field by RING_2:def 4;
reconsider iso as Homomorphism of KF,E by X5;
u is_a_root_of emb(p,p) by FIELD_1:42; then
Z: eval((PolyHom iso).(emb(p,p)),iso.u) = 0.E by FIELD_1:33,POLYNOM5:def 7;
F is Subfield of E by FIELD_2:17;
then reconsider E as FieldExtension of F by FIELD_4:7;
take E;
reconsider a = iso.u as Element of E;
(PolyHom iso).(emb(p,p)) = p
proof
set g = (PolyHom iso).(emb(p,p));
A: for a being Element of F holds iso.((emb p).a) = a
proof
let a be Element of F;
reconsider b = a|F as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
reconsider v = Class(EqRel(Polynom-Ring F,{p}-Ideal),b)
as Element of KroneckerField(F,p) by RING_1:12;
dom(emb p) = the carrier of F by FUNCT_2:def 1; then
C: h.a = phi.((emb p).a) by FUNCT_1:13 .= phi.v by FIELD_1:39;
the carrier of (embField h) = carr h by FIELD_2:def 7
.= ([#]FP \ rng h) \/ [#]F by FIELD_2:def 2
.= ((the carrier of FP)\(rng h))\/(the carrier of F);
then reconsider a1 = a as Element of embField h by XBOOLE_0:def 3;
a in F; then
D: (emb_iso h).a1 = phi.v by C,FIELD_2:def 8;
A1: dom phi = the carrier of KF by FUNCT_2:def 1;
A3: dom(emb_iso h) = the carrier of E by FUNCT_2:def 1;
thus iso.((emb p).a) = (embisoh * phi).v by FIELD_1:39
.= ((emb_iso h)").(phi.v) by A1,FUNCT_1:13
.= a by D,A3,FUNCT_1:34;
end;
now let x be object;
assume x in NAT;
then reconsider i = x as Element of NAT;
g.i = iso.(emb(p,p).i) by FIELD_1:def 2
.= iso.(Class(EqRel(Polynom-Ring F,{p}-Ideal),(p.i)|F))
by FIELD_1:40
.= iso.((emb p).(p.i)) by FIELD_1:39;
hence g.x = p.x by A;
end;
hence thesis;
end;
then K: Ext_eval(p,a) = 0.E by Z,FIELD_4:26;
then reconsider a1 = a as F-algebraic Element of E by FIELD_6:43;
take a1;
p = MinPoly(a1,F) by K,FIELD_6:52;
hence thesis;
end;
hence thesis;
end;
theorem mi2:
for F being Field
for p being irreducible Element of the carrier of Polynom-Ring F
ex E being F-finite FieldExtension of F
st deg(E,F) = deg p & p is_with_roots_in E
proof
let F be Field;
let p1 be irreducible Element of the carrier of Polynom-Ring F;
set p = NormPolynomial p1;
consider E being FieldExtension of F,
a being F-algebraic Element of E such that
A: p = MinPoly(a,F) by mi1,RING_4:28;
reconsider L = FAdj(F,{a}) as F-finite FieldExtension of F;
take L;
p1 is non constant; then
len p1 - 1 > 0 by HURWITZ:def 2; then
B: len p1 <> 0;
deg p = len p - 1 by HURWITZ:def 2
.= len p1 - 1 by B,POLYNOM5:57
.= deg p1 by HURWITZ:def 2;
hence deg(L,F) = deg p1 by A,FIELD_6:67;
a in {a} & {a} is Subset of FAdj(F,{a}) by TARSKI:def 1,FIELD_6:35; then
reconsider a1 = a as Element of L;
L is Subring of E by FIELD_5:12; then
reconsider E as L-extending FieldExtension of F by FIELD_4:def 1;
for a being Element of E, b being Element of L st a = b
holds Ext_eval(p,a) = Ext_eval(p,b) by FIELD_7:14; then
Ext_eval(p,a1) = Ext_eval(p,a)
.= 0.E by A,FIELD_6:52
.= 0.L by EC_PF_1:def 1; then
Ext_eval(p1,a1) = 0.L by FIELD_6:25;
hence p1 is_with_roots_in L by FIELD_4:def 3,FIELD_4:def 2;
end;
theorem
for F being Field
for p being non constant Element of the carrier of Polynom-Ring F
ex E being F-finite FieldExtension of F
st p is_with_roots_in E & deg(E,F) <= deg p
proof
let F be Field, p be non constant Element of the carrier of Polynom-Ring F;
consider q being Element of Polynom-Ring F such that
A: q is_a_irreducible_factor_of p by FIELD_1:3;
reconsider q as Element of the carrier of Polynom-Ring F;
consider E being F-finite FieldExtension of F such that
C: deg(E,F) = deg q & q is_with_roots_in E by A,mi2;
take E;
reconsider p1 = p, q1 = q as Polynomial of F;
q1 divides p1 by A; then
consider r1 being Polynomial of F such that
D: q1 *' r1 = p1 by RING_4:1;
consider a being Element of E such that
E: a is_a_root_of q,E by C,FIELD_4:def 3;
F is Subring of E by FIELD_4:def 1; then
Ext_eval(p1,a) = Ext_eval(q1,a) * Ext_eval(r1,a) by D,ALGNUM_1:20
.= 0.E * Ext_eval(r1,a) by E,FIELD_4:def 2;
hence p is_with_roots_in E by FIELD_4:def 3,FIELD_4:def 2;
q1 divides p1 by A;
hence deg(E,F) <= deg p by C,RING_5:13;
end;
theorem lemA:
for F being Field
for E being F-algebraic FieldExtension of F
for K being E-extending FieldExtension of F
for a being Element of K st a is E-algebraic holds a is F-algebraic
proof
let F be Field, E be F-algebraic FieldExtension of F;
let K be E-extending FieldExtension of F, a be Element of K;
assume a is E-algebraic; then
consider p being non zero Polynomial of E such that
A: Ext_eval(p,a) = 0.K by FIELD_6:43;
reconsider T = Coeff p as finite Subset of E;
for a be Element of E st a in T holds a is F-algebraic; then
reconsider T as finite F-algebraic Subset of E by FIELD_7:def 12;
set B = FAdj(F,T);
E is FieldExtension of B by FIELD_4:7; then
reconsider K1 = K as FieldExtension of B;
E: K1 is B-extending & E is B-extending by FIELD_4:7;
reconsider a1 = a as Element of K1;
T is Subset of B by FIELD_6:35; then
reconsider p1 = p as non zero Polynomial of B by E,FIELD_7:12;
p1 is Element of the carrier of Polynom-Ring B &
p is Element of the carrier of Polynom-Ring E by POLYNOM3:def 10; then
Ext_eval(p1,a) = 0.K by A,E,FIELD_7:15;then
reconsider a1 = a as B-algebraic Element of K1 by FIELD_6:43;
reconsider B1 = FAdj(B,{a1}) as FieldExtension of F;
F: {a} is Subset of FAdj(B,{a1}) by FIELD_6:35;
G: K is B1-extending by FIELD_4:7;
a in {a} by TARSKI:def 1;
then a in FAdj(B,{a1}) by F;
hence a is F-algebraic by G,FIELD_7:33;
end;
theorem e1a:
for F1,F2,L being Field
for E1 being FieldExtension of F1,
K1 being E1-extending FieldExtension of F1
for h1 being Function of F1,L, h2 being Function of E1,L,
h3 being Function of K1,L
st h2 is h1-extending & h3 is h2-extending holds h3 is h1-extending
proof
let F1,F2,L be Field,
E1 be FieldExtension of F1, K1 be E1-extending FieldExtension of F1;
let h1 be Function of F1,L, h2 be Function of E1,L,
h3 be Function of K1,L;
assume AS: h2 is h1-extending & h3 is h2-extending;
now let a be Element of F1;
thus h3.a = h3.@(a,E1) by FIELD_7:def 4
.= h2.@(a,E1) by AS
.= h2.a by FIELD_7:def 4
.= h1.a by AS;
end;
hence thesis;
end;
registration
let F be Field;
cluster -> F-monomorphic F-homomorphic for FieldExtension of F;
coherence
proof
let E be FieldExtension of F;
H: F is Subring of E by FIELD_4:def 1; then
rng(id F) c= the carrier of E by C0SP1:def 3; then
reconsider f = id F as Function of F,E by FUNCT_2:6;
B: now let x,y be Element of F;
reconsider a = f.x, b = f.y as Element of E;
B1: [a,b] in [:the carrier of F,the carrier of F:] by ZFMISC_1:def 2;
thus f.(x+y)
= (the addF of E)||(the carrier of F).(a,b) by H,C0SP1:def 3
.= f.x + f.y by B1,FUNCT_1:49;
end;
C: now let x,y be Element of F;
reconsider a = f.x, b = f.y as Element of E;
B1: [a,b] in [:the carrier of F,the carrier of F:] by ZFMISC_1:def 2;
thus f.(x*y)
= (the multF of E)||(the carrier of F).(a,b) by H,C0SP1:def 3
.= f.x * f.y by B1,FUNCT_1:49;
end;
f is additive multiplicative unity-preserving by B,C,H,C0SP1:def 3;
hence thesis by RING_3:def 3;
end;
end;
registration
let F be Field,
E be FieldExtension of F;
cluster E-homomorphic E-monomorphic F-homomorphic F-monomorphic for Field;
existence
proof
take E;
id E is RingHomomorphism;
hence E is E-homomorphic by RING_2:def 4;
id E is RingHomomorphism monomorphism;
hence E is E-monomorphic by RING_3:def 3;
thus E is F-homomorphic;
thus E is F-monomorphic;
end;
end;
begin :: Sequences of fields
definition
mode sequence -> Function means :ds:
dom it = NAT;
existence
proof
set f = the Function of NAT,NAT;
take f;
thus thesis by FUNCT_2:def 1;
end;
end;
registration
cluster -> NAT-defined for sequence;
coherence
proof
let s be sequence;
dom s = NAT by ds;
hence thesis by RELAT_1:def 18;
end;
end;
definition
let f be Relation;
attr f is Field-yielding means :defFy:
for x being object st x in rng f holds x is Field;
end;
registration
cluster Field-yielding for sequence;
existence
proof
set F = the Field;
deffunc G(object) = F;
consider f being Function such that
A: dom f = NAT & for x being object st x in NAT holds f.x = G(x)
from FUNCT_1:sch 3;
reconsider f as sequence by A,ds;
take f;
now let x be object;
assume x in rng f;
then consider o being object such that
B: o in dom f & f.o = x by FUNCT_1:def 3;
thus x is Field by A,B;
end;
hence thesis;
end;
end;
registration
cluster Field-yielding -> 1-sorted-yielding for Function;
coherence
proof
let f be Function;
assume f is Field-yielding; then
for o being object st o in rng f holds o is 1-sorted;
hence thesis by PRALG_1:def 11;
end;
end;
definition
let f be Field-yielding sequence;
let i be Element of NAT;
redefine func f.i -> Field; :: redefines . (FUNCT_1, definition)
coherence
proof
dom f = NAT by ds;
then f.i in rng f by FUNCT_1:3;
hence f.i is Field by defFy;
end;
end;
definition
let f be Field-yielding sequence;
let i be Nat;
redefine func f.i -> Field; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
dom f = NAT by ds;
then f.i1 in rng f by FUNCT_1:3;
hence f.i is Field;
end;
end;
scheme
RecExField { A() -> Field, P[object,Field,Field] }:
ex f being Field-yielding sequence
st f.0 = A() & for n being Nat holds P[n,f.n,f.(n+1)]
provided
A1:for n being Nat for x being Field ex y being Field st P[n,x,y];
defpred Q[set,set,set] means
$2 is Field implies
ex K2,K3 being Field st K2 = $2 & K3 = $3 & P[$1,K2,K3];
A2: for n being Nat for x being set ex y being set st Q[n,x,y]
proof
let n being Nat, x be set;
thus ex y being set st Q[n,x,y]
proof
per cases;
suppose B0: not x is Field;
take y = 0;
thus Q[n,x,y] by B0;
end;
suppose x is Field;
then reconsider K2 = x as Field;
consider K3 being Field such that B1: P[n,K2,K3] by A1;
take y = K3;
thus Q[n,x,y] by B1;
end;
end;
end;
consider f being Function such that
A3: dom f = NAT & f.0 = A() &
for n being Nat holds Q[n,f.n,f.(n+1)] from RECDEF_1:sch 1(A2);
reconsider f as sequence by A3,ds;
A4: for i being Nat holds f.i is Field
proof
let i be Nat;
defpred R[Nat] means f.($1) is Field;
IA: R[0] by A3;
IS: now let k be Nat;
assume IV: R[k];
Q[k,f.k,f.(k+1)] by A3;
hence R[k+1] by IV;
end;
for k being Nat holds R[k] from NAT_1:sch 2(IA,IS);
hence thesis;
end;
now let x be object;
assume x in rng f; then
consider i being object such that
C1: i in dom f & f.i = x by FUNCT_1:def 3;
reconsider i as Element of NAT by C1;
thus x is Field by C1,A4;
end;
then reconsider f as Field-yielding sequence by defFy;
take f;
thus f.0 = A() by A3;
thus for n being Nat holds P[n,f.n,f.(n+1)]
proof
let n be Nat;
Q[n,f.n,f.(n+1)] by A3;
hence thesis;
end;
end;
definition
let f be Field-yielding sequence;
attr f is ascending means :defasc:
for i being Element of NAT holds f.(i+1) is FieldExtension of f.i;
end;
registration
cluster ascending for Field-yielding sequence;
existence
proof
set F = the Field;
deffunc G(object) = F;
consider f being Function such that
A: dom f = NAT & for x being object st x in NAT holds f.x = G(x)
from FUNCT_1:sch 3;
reconsider f as sequence by A,ds;
now let x be object;
assume x in rng f;
then consider o being object such that
B: o in dom f & f.o = x by FUNCT_1:def 3;
thus x is Field by A,B;
end;
then reconsider f as Field-yielding sequence by defFy;
take f;
now let i be Element of NAT;
f.i = F & f.(i+1) = F by A;
hence f.(i+1) is FieldExtension of f.i by FIELD_4:6;
end;
hence thesis;
end;
end;
definition
let f be Field-yielding sequence;
func Carrier f -> non empty set equals
union(the set of all the carrier of f.i where i is Element of NAT);
coherence
proof
the carrier of f.0 in
the set of all the carrier of f.i where i is Element of NAT; then
0.(f.0) in union (the set of all the carrier of f.i where i is Element of NAT)
by TARSKI:def 4;
hence thesis;
end;
end;
theorem lem1:
for f being ascending Field-yielding sequence
for i,j being Element of NAT
for a being Element of f.i holds i <= j implies a in the carrier of f.j
proof
let f be ascending Field-yielding sequence, i,j be Element of NAT;
let a be Element of f.i;
assume AS: i <= j;
defpred P[Nat] means
ex k being Element of NAT st k = i + $1 & a in the carrier of f.k;
IA: P[0];
IS: now let k be Nat;
assume P[k]; then
consider n being Element of NAT such that
IV: n = i + k & a in the carrier of f.n;
f.(n+1) is FieldExtension of f.n by defasc; then
f.n is Subring of f.(n+1) by FIELD_4:def 1; then
the carrier of f.n c= the carrier of f.(n+1) by C0SP1:def 3;
hence P[k+1] by IV;
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that H: i + n = j by AS,NAT_1:10;
P[n] by I;
hence thesis by H;
end;
theorem lem3:
for f being ascending Field-yielding sequence
for i,j being Element of NAT st i <= j holds f.j is FieldExtension of f.i
proof
let f be ascending Field-yielding sequence, i,j be Element of NAT;
assume AS: i <= j;
defpred P[Nat] means
ex k being Element of NAT st k = i + $1 & f.k is FieldExtension of f.i;
IA: P[0]
proof
take k = i;
thus thesis by FIELD_4:6;
end;
IS: now let k be Nat;
assume P[k]; then
consider n being Element of NAT such that
IV: n = i + k & f.n is FieldExtension of f.i;
f.(n+1) is FieldExtension of f.n by defasc;
hence P[k+1] by IV;
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that H: i + n = j by AS,NAT_1:10;
P[n] by I;
hence thesis by H;
end;
theorem lem2:
for f being ascending Field-yielding sequence
for i,j being Element of NAT
for xi,yi being Element of f.i
for xj,yj being Element of f.j
st xi = xj & yi = yj holds xi + yi = xj + yj & xi * yi = xj * yj
proof
let f be ascending Field-yielding sequence, i,j be Element of NAT;
let xi,yi be Element of f.i, xj,yj be Element of f.j;
assume AS2: xi = xj & yi = yj;
per cases;
suppose AS1: i <= j;
defpred P[Nat] means
ex k being Element of NAT st k = i + $1
& for xi,yi being Element of f.i
for xj,yj being Element of f.k
st xi = xj & yi = yj holds xi + yi = xj + yj & xi * yi = xj * yj;
IA: P[0]
proof
take k = i;
thus k = i + 0;
thus thesis;
end;
IS: now let k be Nat;
assume P[k]; then
consider n being Element of NAT such that
IV: n = i + k &
for xi,yi being Element of f.i
for xj,yj being Element of f.n
st xi = xj & yi = yj holds xi + yi = xj + yj & xi * yi = xj * yj;
now let xi,yi being Element of f.i;
let xj,yj being Element of f.(n+1);
assume B: xi = xj & yi = yj;
i <= i + k & i + k <= n + 1 by IV,NAT_1:11; then
f.(n+1) is FieldExtension of f.i by lem3,XXREAL_0:2; then
f.i is Subfield of f.(n+1) by FIELD_4:7; then
C: f.i is Subring of f.(n+1) by FIELD_5:12;
hence xi + yi = xj + yj by B,FIELD_6:15;
thus xi * yi = xj * yj by B,C,FIELD_6:16;
end;
hence P[k+1] by IV;
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that H: i + n = j by AS1,NAT_1:10;
P[n] by I;
hence thesis by H,AS2;
end;
suppose AS1: j <= i;
defpred P[Nat] means
ex k being Element of NAT st k = j + $1
& for xi,yi being Element of f.j
for xj,yj being Element of f.k
st xi = xj & yi = yj holds xi + yi = xj + yj & xi * yi = xj * yj;
IA: P[0]
proof
take k = j;
thus k = j + 0;
thus thesis;
end;
IS: now let k be Nat;
assume P[k]; then
consider n being Element of NAT such that
IV: n = j + k &
for xi,yi being Element of f.j
for xj,yj being Element of f.n
st xi = xj & yi = yj holds xi + yi = xj + yj & xi * yi = xj * yj;
now let xi,yi being Element of f.j;
let xj,yj being Element of f.(n+1);
assume B: xi = xj & yi = yj;
j <= j + k & j + k <= n + 1 by IV,NAT_1:11; then
f.(n+1) is FieldExtension of f.j by lem3,XXREAL_0:2; then
f.j is Subfield of f.(n+1) by FIELD_4:7; then
C: f.j is Subring of f.(n+1) by FIELD_5:12;
hence xi + yi = xj + yj by B,FIELD_6:15;
thus xi * yi = xj * yj by B,C,FIELD_6:16;
end;
hence P[k+1] by IV;
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that H: j + n = i by AS1,NAT_1:10;
P[n] by I;
hence thesis by H,AS2;
end;
end;
definition
let f be ascending Field-yielding sequence;
func addseq f -> BinOp of Carrier f means :defadd:
for a,b being Element of Carrier f
ex i being Element of NAT, x,y being Element of f.i
st x = a & y = b & it.(a,b) = x + y;
existence
proof
set C = Carrier f;
defpred P[object,object,object] means
ex i being Element of NAT, x,y being Element of f.i
st x = $1 & y = $2 & $3 = x + y;
A: for a,b being Element of C ex z being Element of C st P[a,b,z]
proof
let a,b being Element of C;
consider Y being set such that
A0: a in Y & Y in the set of all
the carrier of f.i where i is Element of NAT by TARSKI:def 4;
consider i being Element of NAT such that
A1: Y = the carrier of f.i by A0;
consider Z being set such that
A2: b in Z & Z in the set of all
the carrier of f.i where i is Element of NAT by TARSKI:def 4;
consider j being Element of NAT such that
A3: Z = the carrier of f.j by A2;
per cases;
suppose i <= j;
then reconsider x = a, y = b as Element of f.j by A0,A1,A2,A3,lem1;
x + y in the carrier of f.j &
the carrier of f.j in
the set of all the carrier of f.n where n is Element of NAT;
then reconsider z = x + y as Element of C by TARSKI:def 4;
take z;
thus thesis;
end;
suppose j <= i;
then reconsider x = a, y = b as Element of f.i by A0,A1,A2,A3,lem1;
x + y in the carrier of f.i &
the carrier of f.i in
the set of all the carrier of f.n where n is Element of NAT;
then reconsider z = x + y as Element of C by TARSKI:def 4;
take z;
thus thesis;
end;
end;
consider A being Function of [:C,C:],C such that
B: for x,y being Element of C holds P[x,y,A.(x,y)] from BINOP_1:sch 3(A);
reconsider A as BinOp of Carrier f;
take A;
thus thesis by B;
end;
uniqueness
proof
let f1,f2 be BinOp of Carrier f such that
A1: for a,b being Element of Carrier f
ex i being Element of NAT, x,y being Element of f.i
st x = a & y = b & f1.(a,b) = x + y
and
A2: for a,b being Element of Carrier f
ex i being Element of NAT, x,y being Element of f.i
st x = a & y = b & f2.(a,b) = x + y;
now let a,b be Element of Carrier f;
consider i being Element of NAT, xi,yi being Element of f.i such that
A3: xi = a & yi = b & f1.(a,b) = xi + yi by A1;
consider j being Element of NAT, xj,yj being Element of f.j such that
A4: xj = a & yj = b & f2.(a,b) = xj + yj by A2;
thus f1.(a,b) = f2.(a,b) by A3,A4,lem2;
end;
hence f1 = f2;
end;
end;
definition
let f be ascending Field-yielding sequence;
func multseq f -> BinOp of Carrier f means :defmult:
for a,b being Element of Carrier f
ex i being Element of NAT, x,y being Element of f.i
st x = a & y = b & it.(a,b) = x * y;
existence
proof
set C = Carrier f;
defpred P[object,object,object] means
ex i being Element of NAT, x,y being Element of f.i
st x = $1 & y = $2 & $3 = x * y;
A: for a,b being Element of C ex z being Element of C st P[a,b,z]
proof
let a,b being Element of C;
consider Y being set such that
A0: a in Y & Y in the set of all
the carrier of f.i where i is Element of NAT by TARSKI:def 4;
consider i being Element of NAT such that
A1: Y = the carrier of f.i by A0;
consider Z being set such that
A2: b in Z & Z in the set of all
the carrier of f.i where i is Element of NAT by TARSKI:def 4;
consider j being Element of NAT such that
A3: Z = the carrier of f.j by A2;
per cases;
suppose i <= j;
then reconsider x = a, y = b as Element of f.j by A0,A1,A2,A3,lem1;
x + y in the carrier of f.j &
the carrier of f.j in
the set of all the carrier of f.n where n is Element of NAT;
then reconsider z = x * y as Element of C by TARSKI:def 4;
take z;
thus thesis;
end;
suppose j <= i;
then reconsider x = a, y = b as Element of f.i by A0,A1,A2,A3,lem1;
x + y in the carrier of f.i &
the carrier of f.i in
the set of all the carrier of f.n where n is Element of NAT;
then reconsider z = x * y as Element of C by TARSKI:def 4;
take z;
thus thesis;
end;
end;
consider A being Function of [:C,C:],C such that
B: for x,y being Element of C holds P[x,y,A.(x,y)] from BINOP_1:sch 3(A);
reconsider A as BinOp of Carrier f;
take A;
thus thesis by B;
end;
uniqueness
proof
let f1,f2 be BinOp of Carrier f such that
A1: for a,b being Element of Carrier f
ex i being Element of NAT, x,y being Element of f.i
st x = a & y = b & f1.(a,b) = x * y
and
A2: for a,b being Element of Carrier f
ex i being Element of NAT, x,y being Element of f.i
st x = a & y = b & f2.(a,b) = x * y;
now let a,b be Element of Carrier f;
consider i being Element of NAT, xi,yi being Element of f.i such that
A3: xi = a & yi = b & f1.(a,b) = xi * yi by A1;
consider j being Element of NAT, xj,yj being Element of f.j such that
A4: xj = a & yj = b & f2.(a,b) = xj * yj by A2;
thus f1.(a,b) = f2.(a,b) by A3,A4,lem2;
end;
hence f1 = f2;
end;
end;
definition
let f be ascending Field-yielding sequence;
func SeqField f -> strict doubleLoopStr means :dsf:
the carrier of it = Carrier f &
the addF of it = addseq f &
the multF of it = multseq f &
the OneF of it = 1.(f.0) &
the ZeroF of it = 0.(f.0);
existence
proof
A: the carrier of f.0 in
the set of all the carrier of f.i where i is Element of NAT;
reconsider o = 1.(f.0) as Element of Carrier f by A,TARSKI:def 4;
reconsider z = 0.(f.0) as Element of Carrier f by A,TARSKI:def 4;
take doubleLoopStr(# Carrier f,addseq f,multseq f,o,z #);
thus thesis;
end;
uniqueness;
end;
theorem lem5:
for f being ascending Field-yielding sequence
for i being Element of NAT
holds 1.(SeqField f) = 1.(f.i) & 0.(SeqField f) = 0.(f.i)
proof
let f be ascending Field-yielding sequence, i be Element of NAT;
defpred P[Nat] means
ex k being Element of NAT st k = $1 & 1.(f.k) = 1.(f.0) & 0.(f.k) = 0.(f.0);
IA: P[0];
IS: now let k be Nat;
assume P[k]; then
consider n being Element of NAT such that
IV: k = n & 1.(f.n) = 1.(f.0) & 0.(f.n) = 0.(f.0);
f.(n+1) is FieldExtension of f.n by defasc; then
f.n is Subfield of f.(n+1) by FIELD_4:7; then
1.(f.n) = 1.(f.(n+1)) & 0.(f.n) = 0.(f.(n+1)) by EC_PF_1:def 1;
hence P[k+1] by IV;
end;
for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
then P[i] & 1.(SeqField f) = 1.(f.0) & 0.(SeqField f) = 0.(f.0) by dsf;
hence 1.(SeqField f) = 1.(f.i) & 0.(SeqField f) = 0.(f.i);
end;
theorem lem4:
for f being ascending Field-yielding sequence
for a,b being Element of SeqField f
for i being Element of NAT, x,y being Element of f.i
st x = a & y = b holds a + b = x + y & a * b = x * y
proof
let f be ascending Field-yielding sequence, a,b be Element of SeqField f;
let i be Element of NAT, x,y be Element of f.i;
assume AS: x = a & y = b;
H: a is Element of Carrier f & b is Element of Carrier f by dsf; then
consider j being Element of NAT, xj,yj being Element of f.j such that
A: xj = a & yj = b & (addseq f).(a,b) = xj + yj by defadd;
x + y = xj + yj by AS,A,lem2;
hence a + b = x + y by A,dsf;
consider j being Element of NAT, xj,yj being Element of f.j such that
A: xj = a & yj = b & (multseq f).(a,b) = xj * yj by H,defmult;
x * y = xj * yj by AS,A,lem2;
hence a * b = x * y by A,dsf;
end;
registration
let f be ascending Field-yielding sequence;
cluster SeqField f -> non degenerated;
coherence
proof
1.(SeqField f) = 1.(f.0) & 0.(SeqField f) = 0.(f.0) by dsf;
hence thesis;
end;
end;
registration
let f be ascending Field-yielding sequence;
cluster SeqField f -> Abelian
add-associative right_zeroed right_complementable;
coherence
proof
set F = SeqField f;
hereby
let x,y be Element of F;
reconsider a = x, b = y as Element of Carrier f by dsf;
consider i being Element of NAT, yi,xi being Element of f.i such that
A: yi = b & xi = a & (addseq f).(b,a) = yi + xi by defadd;
thus x + y = xi + yi by A,lem4 .= y + x by A,lem4;
end;
hereby
let x,y,z be Element of F;
reconsider a = x, b = y, c = z, ab = x + y as Element of Carrier f by dsf;
consider i being Element of NAT, xi,yi being Element of f.i such that
A: xi = a & yi = b & (addseq f).(a,b) = xi + yi by defadd;
consider j being Element of NAT, xj,zj being Element of f.j such that
B: xj = ab & zj = c & (addseq f).(ab,c) = xj + zj by defadd;
per cases;
suppose j <= i;
then reconsider zi = zj as Element of f.i by lem1;
C: yi + zi = y + z by A,B,lem4;
x + y = xi + yi by A,lem4;
hence (x + y) + z = (xi + yi) + zi by B,lem4
.= xi + (yi + zi) by RLVECT_1:def 3
.= x + (y + z) by A,C,lem4;
end;
suppose i <= j;
then reconsider xj = xi, yj = yi as Element of f.j by lem1;
C: yj + zj = y + z by A,B,lem4;
x + y = xj + yj by A,lem4;
hence (x + y) + z = (xj + yj) + zj by B,lem4
.= xj + (yj + zj) by RLVECT_1:def 3
.= x + (y + z) by A,C,lem4;
end;
end;
hereby
let x be Element of F;
x is Element of Carrier f by dsf; then
consider Y being set such that
A: x in Y & Y in the set of all the carrier of f.i where i is Element of NAT
by TARSKI:def 4;
consider i being Element of NAT such that
B: Y = the carrier of f.i by A;
reconsider a = x as Element of f.i by A,B;
0.F = 0.(f.i) by lem5;
hence x + 0.F = a + 0.(f.i) by lem4 .= x;
end;
let x be Element of F;
x is Element of Carrier f by dsf; then
consider Y being set such that
A: x in Y & Y in the set of all the carrier of f.i where i is Element of NAT
by TARSKI:def 4;
consider i being Element of NAT such that
B: Y = the carrier of f.i by A;
reconsider a = x as Element of f.i by A,B;
the carrier of f.i in
the set of all the carrier of f.i where i is Element of NAT; then
-a in Carrier f by TARSKI:def 4; then
reconsider y = -a as Element of F by dsf;
take y;
thus x + y = a + -a by lem4 .= 0.(f.i) by RLVECT_1:5 .= 0.F by lem5;
end;
end;
registration
let f be ascending Field-yielding sequence;
cluster SeqField f -> commutative associative well-unital distributive
almost_left_invertible;
coherence
proof
set F = SeqField f;
A: now let x,y be Element of F;
reconsider a = x, b = y as Element of Carrier f by dsf;
consider i being Element of NAT, yi,xi being Element of f.i such that
A: yi = b & xi = a & (multseq f).(b,a) = yi * xi by defmult;
thus x * y = xi * yi by A,lem4
.= yi * xi by GROUP_1:def 12 .= y * x by A,lem4;
end;
hence F is commutative;
hereby
let x,y,z be Element of F;
reconsider a = x, b = y, c = z, ab = x * y as Element of Carrier f by dsf;
consider i being Element of NAT, xi,yi being Element of f.i such that
A: xi = a & yi = b & (multseq f).(a,b) = xi * yi by defmult;
consider j being Element of NAT, xj,zj being Element of f.j such that
B: xj = ab & zj = c & (multseq f).(ab,c) = xj * zj by defmult;
per cases;
suppose j <= i;
then reconsider zi = zj as Element of f.i by lem1;
C: yi * zi = y * z by A,B,lem4;
x * y = xi * yi by A,lem4;
hence (x * y) * z = (xi * yi) * zi by B,lem4
.= xi * (yi * zi) by GROUP_1:def 3
.= x * (y * z) by A,C,lem4;
end;
suppose i <= j;
then reconsider xj = xi, yj = yi as Element of f.j by lem1;
C: yj * zj = y * z by A,B,lem4;
x * y = xj * yj by A,lem4;
hence (x * y) * z = (xj * yj) * zj by B,lem4
.= xj * (yj * zj) by GROUP_1:def 3
.= x * (y * z) by A,C,lem4;
end;
end;
hereby let x be Element of F;
x is Element of Carrier f by dsf; then
consider Y being set such that
A: x in Y & Y in the set of all the carrier of f.i where i is Element of NAT
by TARSKI:def 4;
consider i being Element of NAT such that
B: Y = the carrier of f.i by A;
reconsider a = x as Element of f.i by A,B;
C: 1.F = 1.(f.i) by lem5;
thus x * 1.F = a * 1.(f.i) by C,lem4 .= x;
thus 1.F * x = 1.(f.i) * a by C,lem4 .= x;
end;
hereby let x,y,z be Element of F;
reconsider a = x, b = y, c = z, bc = y + z as Element of Carrier f by dsf;
consider i being Element of NAT, yi,zi being Element of f.i such that
B: yi = b & zi = c & (addseq f).(b,c) = yi + zi by defadd;
consider j being Element of NAT, xj,pj being Element of f.j such that
C: xj = a & pj = bc & (multseq f).(a,bc) = xj * pj by defmult;
thus Z: x * (y + z) = x * y + x * z
proof
per cases;
suppose j <= i;
then reconsider xi = xj as Element of f.i by lem1;
D: x * y = xi * yi & x * z = xi * zi by B,C,lem4;
y + z = yi + zi by B,lem4;
hence x * (y + z) = xi * (yi + zi) by C,lem4
.= xi * yi + xi * zi by VECTSP_1:def 2
.= x * y + x * z by D,lem4;
end;
suppose i <= j;
then reconsider yj = yi, zj = zi as Element of f.j by lem1;
D: x * y = xj * yj & x * z = xj * zj by B,C,lem4;
y + z = yj + zj by B,lem4;
hence x * (y + z) = xj * (yj + zj) by C,lem4
.= xj * yj + xj * zj by VECTSP_1:def 2
.= x * y + x * z by D,lem4;
end;
end;
thus (y + z) * x = x * y + x * z by A,Z
.= x * y + z * x by A
.= y * x + z * x by A;
end;
let x be Element of F such that H: x <> 0.F;
x is Element of Carrier f by dsf; then
consider Y being set such that
A: x in Y & Y in the set of all the carrier of f.i where i is Element of NAT
by TARSKI:def 4;
consider i being Element of NAT such that
B: Y = the carrier of f.i by A;
reconsider a = x as Element of f.i by A,B;
the carrier of f.i in
the set of all the carrier of f.i where i is Element of NAT; then
a" in Carrier f by TARSKI:def 4; then
reconsider y = a" as Element of F by dsf;
C: a <> 0.(f.i) by H,lem5;
take y;
thus y * x = a" * a by lem4 .= 1.(f.i) by C,VECTSP_1:def 10 .= 1.F by lem5;
end;
end;
theorem Fsub:
for f being ascending Field-yielding sequence
for i being Element of NAT holds (f.i) is Subfield of (SeqField f)
proof
let f be ascending Field-yielding sequence, i be Element of NAT;
set F = f.i, K = SeqField f;
H: the carrier of K = Carrier f by dsf
.= union(the set of all the carrier of f.i where i is Element of NAT);
J: the carrier of F in
the set of all the carrier of f.i where i is Element of NAT; then
A: the carrier of F c= the carrier of K by H,ZFMISC_1:74;
B: the addF of F = (the addF of K) || the carrier of F
proof
set aF = the addF of F, aK = (the addF of K) || the carrier of F;
B1: dom aK
= dom(the addF of K) /\ [:the carrier of F,the carrier of F:] by RELAT_1:61
.= [:the carrier of K,the carrier of K:] /\
[:the carrier of F,the carrier of F:] by FUNCT_2:def 1
.= [:the carrier of F,the carrier of F:] by A,ZFMISC_1:96,XBOOLE_1:28;
now let x be object;
assume B2: x in dom aF; then
consider a,b being object such that
B3: a in the carrier of F & b in the carrier of F & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of F by B3;
reconsider y = a, z = b as Element of K by A;
thus aF.x = a + b by B3
.= y + z by lem4
.= aK.x by B3,B2,FUNCT_1:49;
end;
hence thesis by B1,FUNCT_2:def 1;
end;
C: the multF of F = (the multF of K) || the carrier of F
proof
set mF = the multF of F, mK = (the multF of K) || the carrier of F;
B1: dom mK
= dom(the multF of K) /\ [:the carrier of F,the carrier of F:]
by RELAT_1:61
.= [:the carrier of K,the carrier of K:] /\
[:the carrier of F,the carrier of F:] by FUNCT_2:def 1
.= [:the carrier of F,the carrier of F:] by A,ZFMISC_1:96,XBOOLE_1:28;
now let x be object;
assume B2: x in dom mF; then
consider a,b being object such that
B3: a in the carrier of F & b in the carrier of F & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of F by B3;
reconsider y = a, z = b as Element of K by A;
thus mF.x = a * b by B3
.= y * z by lem4
.= mK.x by B3,B2,FUNCT_1:49;
end;
hence thesis by B1,FUNCT_2:def 1;
end;
1.F = 1.K & 0.F = 0.K by lem5;
hence thesis by H,J,ZFMISC_1:74,B,C,EC_PF_1:def 1;
end;
theorem
for E being Field
for f being ascending Field-yielding sequence
st for i being Element of NAT holds (f.i) is Subfield of E
holds (SeqField f) is Subfield of E
proof
let K be Field, f be ascending Field-yielding sequence;
assume AS: for i being Element of NAT holds (f.i) is Subfield of K;
then X: f.0 is Subfield of K;
set F = SeqField f;
H: the carrier of F = Carrier f by dsf
.= union(the set of all the carrier of f.i where i is Element of NAT);
A: the carrier of F c= the carrier of K
proof
now let o be object;
assume o in the carrier of F; then
consider Y being set such that
A1: o in Y &
Y in the set of all the carrier of f.i where i is Element of NAT
by H,TARSKI:def 4;
consider i being Element of NAT such that
A2: Y = the carrier of f.i by A1;
f.i is Subfield of K by AS; then
the carrier of f.i c= the carrier of K by EC_PF_1:def 1;
hence o in the carrier of K by A1,A2;
end;
hence thesis;
end;
B: the addF of F = (the addF of K) || the carrier of F
proof
set aF = the addF of F, aK = (the addF of K) || the carrier of F;
B1: dom aK
= dom(the addF of K) /\
[:the carrier of F,the carrier of F:] by RELAT_1:61
.= [:the carrier of K,the carrier of K:] /\
[:the carrier of F,the carrier of F:] by FUNCT_2:def 1
.= [:the carrier of F,the carrier of F:] by A,XBOOLE_1:28,ZFMISC_1:96
.= dom aF by FUNCT_2:def 1;
now let x be object;
assume x in dom aF; then
consider a,b being object such that
B3: a in the carrier of F & b in the carrier of F & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of F by B3;
consider Y1 being set such that
C1: a in Y1 &
Y1 in the set of all the carrier of f.i where i is Element of NAT
by H,TARSKI:def 4;
consider j1 being Element of NAT such that
B4: Y1 = the carrier of f.j1 by C1;
consider Y2 being set such that
C2: b in Y2 &
Y2 in the set of all the carrier of f.i where i is Element of NAT
by H,TARSKI:def 4;
consider j2 being Element of NAT such that
B5: Y2 = the carrier of f.j2 by C2;
per cases;
suppose j1 <= j2; then
reconsider a1 = a, b1 = b as Element of f.j2 by C1,C2,B4,B5,lem1;
f.j2 is Subfield of K by AS; then
B4: the addF of (f.j2) = (the addF of K) || the carrier of (f.j2)
by EC_PF_1:def 1;
B5: [a1,b1] in [:the carrier of (f.j2),the carrier of (f.j2):]
by ZFMISC_1:def 2;
B6: [a1,b1] in [:the carrier of F,the carrier of F:]
by ZFMISC_1:def 2;
thus aF.x
= a + b by B3
.= a1 + b1 by lem4
.= (the addF of K).(a1,b1) by B4,B5,FUNCT_1:49
.= aK.x by B3,B6,FUNCT_1:49;
end;
suppose j2 <= j1;then
reconsider a1 = a, b1 = b as Element of f.j1 by C1,C2,B4,B5,lem1;
f.j1 is Subfield of K by AS; then
B4: the addF of (f.j1) = (the addF of K) || the carrier of (f.j1)
by EC_PF_1:def 1;
B5: [a1,b1] in [:the carrier of (f.j1),the carrier of (f.j1):]
by ZFMISC_1:def 2;
B6: [a1,b1] in [:the carrier of F,the carrier of F:]
by ZFMISC_1:def 2;
thus aF.x
= a + b by B3
.= a1 + b1 by lem4
.= (the addF of K).(a1,b1) by B4,B5,FUNCT_1:49
.= aK.x by B3,B6,FUNCT_1:49;
end;
end;
hence thesis by B1;
end;
C: the multF of F = (the multF of K) || the carrier of F
proof
set aF = the multF of F, aK = (the multF of K) || the carrier of F;
B1: dom aK
= dom(the multF of K) /\
[:the carrier of F,the carrier of F:] by RELAT_1:61
.= [:the carrier of K,the carrier of K:] /\
[:the carrier of F,the carrier of F:] by FUNCT_2:def 1
.= [:the carrier of F,the carrier of F:] by A,XBOOLE_1:28,ZFMISC_1:96
.= dom aF by FUNCT_2:def 1;
now let x be object;
assume x in dom aF; then
consider a,b being object such that
B3: a in the carrier of F & b in the carrier of F & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of F by B3;
consider Y1 being set such that
C1: a in Y1 &
Y1 in the set of all the carrier of f.i where i is Element of NAT
by H,TARSKI:def 4;
consider j1 being Element of NAT such that
B4: Y1 = the carrier of f.j1 by C1;
consider Y2 being set such that
C2: b in Y2 &
Y2 in the set of all the carrier of f.i where i is Element of NAT
by H,TARSKI:def 4;
consider j2 being Element of NAT such that
B5: Y2 = the carrier of f.j2 by C2;
per cases;
suppose j1 <= j2; then
reconsider a1 = a, b1 = b as Element of f.j2 by C1,C2,B4,B5,lem1;
f.j2 is Subfield of K by AS; then
B4: the multF of (f.j2) = (the multF of K) || the carrier of (f.j2)
by EC_PF_1:def 1;
B5: [a1,b1] in [:the carrier of (f.j2),the carrier of (f.j2):]
by ZFMISC_1:def 2;
B6: [a1,b1] in [:the carrier of F,the carrier of F:] by ZFMISC_1:def 2;
thus aF.x
= a * b by B3
.= a1 * b1 by lem4
.= (the multF of K).(a1,b1) by B4,B5,FUNCT_1:49
.= aK.x by B3,B6,FUNCT_1:49;
end;
suppose j2 <= j1;then
reconsider a1 = a, b1 = b as Element of f.j1 by C1,C2,B4,B5,lem1;
f.j1 is Subfield of K by AS; then
B4: the multF of (f.j1) = (the multF of K) || the carrier of (f.j1)
by EC_PF_1:def 1;
B5: [a1,b1] in [:the carrier of (f.j1),the carrier of (f.j1):]
by ZFMISC_1:def 2;
B6: [a1,b1] in [:the carrier of F,the carrier of F:] by ZFMISC_1:def 2;
thus aF.x
= a * b by B3
.= a1 * b1 by lem4
.= (the multF of K).(a1,b1) by B4,B5,FUNCT_1:49
.= aK.x by B3,B6,FUNCT_1:49;
end;
end;
hence thesis by B1;
end;
D: 1.F = 1.(f.0) by dsf .= 1.K by X,EC_PF_1:def 1;
0.F = 0.(f.0) by dsf .= 0.K by X,EC_PF_1:def 1;
hence thesis by A,B,C,D,EC_PF_1:def 1;
end;
theorem alg3a:
for f being ascending Field-yielding sequence
for X being finite Subset of (SeqField f)
ex i being Element of NAT st X c= the carrier of (f.i)
proof
let f be ascending Field-yielding sequence,
X be finite Subset of (SeqField f);
defpred P[Nat] means
for X being finite Subset of (SeqField f) st card X = $1
ex i being Element of NAT st X c= the carrier of f.i;
set F = SeqField f;
H: the carrier of F = Carrier f by dsf
.= union(the set of all the carrier of f.i where i is Element of NAT);
IA: P[0]
proof
now let X be finite Subset of (SeqField f);
assume card X = 0; then
X c= the carrier of f.0;
hence ex i being Element of NAT st X c= the carrier of f.i;
end;
hence thesis;
end;
I1: P[1]
proof
now let X be finite Subset of (SeqField f);
assume card X = 1; then
consider a being object such that A: X = {a} by CARD_2:42;
a in X by A,TARSKI:def 1; then
reconsider a as Element of F;
consider Y being set such that
B: a in Y &
Y in the set of all the carrier of f.i where i is Element of NAT
by H,TARSKI:def 4;
consider i being Element of NAT such that
C: Y = the carrier of f.i by B;
X c= the carrier of f.i by A,B,C,TARSKI:def 1;
hence ex i being Element of NAT st X c= the carrier of f.i;
end;
hence thesis;
end;
IS: now let k be Nat;
assume IV: P[k];
now let X be finite Subset of (SeqField f);
assume AS: card X = k + 1; then
A: X <> {};
set a = the Element of X;
A1: a in X by A; then
reconsider a as Element of F;
set X1 = X \ {a};
a in {a} by TARSKI:def 1; then
not a in X1 by XBOOLE_0:def 5; then
B: card (X1 \/ {a}) = card X1 + 1 by CARD_2:41;
{a} c= X by A1,TARSKI:def 1; then
C: X1 \/ {a} = X by FIELD_5:1; then
consider i1 being Element of NAT such that
D: X1 c= the carrier of f.i1 by AS,B,IV;
card {a} = 1 by CARD_2:42; then
consider i2 being Element of NAT such that
E: {a} c= the carrier of f.i2 by I1;
a in {a} by TARSKI:def 1; then
reconsider a as Element of f.i2 by E;
per cases;
suppose i1 <= i2; then
f.i2 is FieldExtension of f.i1 by lem3; then
f.i1 is Subfield of f.i2 by FIELD_4:7; then
the carrier of f.i1 c= the carrier of f.i2 by EC_PF_1:def 1; then
X1 c= the carrier of f.i2 by D; then
X1 \/ {a} c= (the carrier of f.i2) \/ (the carrier of f.i2)
by XBOOLE_1:13;
hence ex i being Element of NAT st X c= the carrier of f.i by C;
end;
suppose i2 <= i1; then
reconsider a as Element of f.i1 by lem1;
X1 \/ {a} c= (the carrier of f.i1) \/ (the carrier of f.i1)
by D,XBOOLE_1:13;
hence ex i being Element of NAT st X c= the carrier of f.i by C;
end;
end;
hence P[k+1];
end;
I: for k being Nat holds P[k] from NAT_1:sch 2(IA,IS);
consider n being Nat such that I2: card X = n;
consider i being Element of NAT such that
H: X c= the carrier of f.i by I,I2;
thus thesis by H;
end;
begin :: Maximal Algebraic and Algebraic Closed Fields
definition
let F be Field;
attr F is maximal_algebraic means
for E being F-algebraic FieldExtension of F holds E == F;
end;
al1: for F being Field holds
F is algebraic-closed iff
for p being irreducible Element of the carrier of Polynom-Ring F
holds deg p = 1
proof
let F be Field;
A: now assume B: F is algebraic-closed;
now let p being irreducible Element of the carrier of Polynom-Ring F;
set q = NormPolynomial p;
q is irreducible by RING_4:28;
then deg q = 1 by B,RING_4:46;
hence deg p = 1 by RING_4:27,RING_4:29;
end;
hence for p being irreducible Element of the carrier of Polynom-Ring F
holds deg p = 1;
end;
now assume for p being irreducible Element of the carrier of Polynom-Ring F
holds deg p = 1; then
for p being monic Element of the carrier of Polynom-Ring F
holds p is irreducible iff deg p = 1 by RING_4:42;
hence F is algebraic-closed by RING_4:46;
end;
hence thesis by A;
end;
theorem eq:
for F being Field holds F is maximal_algebraic iff F is algebraic-closed
proof
let F be Field;
A: now assume B: F is maximal_algebraic;
now let p be irreducible Element of the carrier of Polynom-Ring F;
consider E being F-finite FieldExtension of F such that
C: deg(E,F) = deg p & p is_with_roots_in E by mi2;
thus 1 = deg p by C,B,FIELD_7:8;
end;
hence F is algebraic-closed by al1;
end;
now assume not F is maximal_algebraic;
then consider E being F-algebraic FieldExtension of F such that
B: not E == F;
F is Subfield of E by FIELD_4:7; then
C: the carrier of F c= the carrier of E by EC_PF_1:def 1;
F: not deg(E,F) = 1 by B,FIELD_7:8;
now assume G: for a being Element of E holds a in F;
now let o be object;
assume o in the carrier of E; then
reconsider a = o as Element of E;
a in F by G;
hence o in the carrier of F;
end;
hence contradiction by F,FIELD_7:7,C,TARSKI:2;
end; then
consider a being Element of E such that D: not a in F;
set p = MinPoly(a,F);
E: deg(FAdj(F,{a}),F) = deg p by FIELD_6:67;
a in {a} by TARSKI:def 1; then
not {a} is Subset of F by D; then
not deg(FAdj(F,{a}),F) = 1 by FIELD_7:8,FIELD_7:3;
hence not F is algebraic-closed by E,al1;
end;
hence thesis by A;
end;
theorem alg2:
for F being Field holds
F is algebraic-closed iff
for p being non constant Polynomial of F holds p is with_roots
proof
let F be Field;
now assume B: for p being non constant Polynomial of F holds p is with_roots;
now let p be Polynomial of F;
assume C: len p > 1;
deg p = len p - 1 by HURWITZ:def 2;
then deg p + 1 - 1 > 1 - 1 by C,XREAL_1:9;
then p is non constant by RATFUNC1:def 2;
hence p is with_roots by B;
end;
hence F is algebraic-closed by POLYNOM5:def 9;
end;
hence thesis;
end;
theorem
for F being Field holds
F is algebraic-closed iff
for p being irreducible Element of the carrier of Polynom-Ring F
holds deg p = 1 by al1;
theorem
for F being Field holds
F is algebraic-closed iff
for p being non constant Polynomial of F holds p splits_in F
proof
let F be Field;
A: now assume B: F is algebraic-closed;
now let p be non constant Polynomial of F;
reconsider p1 = p as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
deg p1 > 0 by RATFUNC1:def 2; then
reconsider p1 = p as non constant
Element of the carrier of Polynom-Ring F
by RING_4:def 4;
set q = NormPolynomial p1;
deg q = deg p by RING_4:27,RING_4:29; then
reconsider q as non constant monic Polynomial of F
by RING_4:def 4,RATFUNC1:def 2;
reconsider q as Ppoly of F by B,RING_5:70;
C: LC p <> 0.F;
q = (LC p)" * p by RING_4:23; then
LC p * q = ((LC p) * (LC p)") * p by RING_4:11
.= ((LC p)" * (LC p)) * p by GROUP_1:def 12
.= (1.F) * p by C,VECTSP_1:def 10
.= p;
hence p splits_in F by FIELD_4:def 5;
end;
hence for p being non constant Polynomial of F holds p splits_in F;
end;
now assume B: for p being non constant Polynomial of F holds p splits_in F;
now let p be non constant monic Polynomial of F;
consider a being non zero Element of F, q being Ppoly of F such that
C: p = a * q by B,FIELD_4:def 5;
1.F = LC p by RATFUNC1:def 7
.= a * LC q by C,RING_5:5
.= a * 1.F by RING_5:50;
hence p is Ppoly of F by C;
end;
hence F is algebraic-closed by RING_5:70;
end;
hence thesis by A;
end;
theorem
for F being Field holds
F is algebraic-closed iff
for p being non constant monic Polynomial of F holds p is Ppoly of F
by RING_5:70;
theorem
for F being Field holds
F is algebraic-closed iff
for p,q being Element of the carrier of Polynom-Ring F
holds p,q are_coprime iff p,q have_no_common_roots
proof
let F be Field;
A: now assume Z: F is algebraic-closed;
now let p,q be Element of the carrier of Polynom-Ring F;
set g = p gcd q;
assume AS: not p,q are_coprime;
per cases;
suppose X: p = 0_.(F) & q = 0_.(F);
eval(0_.(F),0.F) = 0.F by POLYNOM4:17; then
0.F is_a_root_of p & 0.F is_a_root_of q by X,POLYNOM5:def 7;
hence p,q have_a_common_root by RATFUNC1:def 4,RATFUNC1:def 3;
end;
suppose K: p <> 0_.(F) or q <> 0_.(F);
now assume K0: g is constant;
per cases;
suppose K1: g = 0_.(F);
consider r1 being Polynomial of F such that
K2: (0_.(F)) *' r1 = p by K1,RING_4:52,RING_4:1;
consider r2 being Polynomial of F such that
K3: (0_.(F)) *' r2 = q by K1,RING_4:52,RING_4:1;
thus contradiction by K,K2,K3;
end;
suppose K1: g <> 0_.(F);
reconsider p1 = p ,q1 = q as Polynomial of F;
reconsider g1 = g as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
deg g <= 0 by K0,RATFUNC1:def 2; then
reconsider g1 as
non zero constant Element of the carrier of Polynom-Ring F
by K1,UPROOTS:def 5,RING_4:def 4;
consider a being Element of F such that
K3: g1 = a|F by RING_4:20;
per cases by K;
suppose p <> 0_.(F); then
p1 is non zero by UPROOTS:def 5; then
1.F = LC(a|F) by K3,RATFUNC1:def 7 .= a by RING_5:6;
then g = 1_.(F) by K3,RING_4:14;
hence contradiction by AS,copr1;
end;
suppose q <> 0_.(F); then
q1 is non zero by UPROOTS:def 5; then
1.F = LC(a|F) by K3,RATFUNC1:def 7 .= a by RING_5:6;
then g = 1_.(F) by K3,RING_4:14;
hence contradiction by AS,copr1;
end;
end;
end; then
consider a being Element of F such that
F: a is_a_root_of g by Z,POLYNOM5:def 8;
X: eval(g,a) = 0.F by F,POLYNOM5:def 7;
consider gp being Polynomial of F such that
G: g *' gp = p by RING_4:52,RING_4:1;
consider gq being Polynomial of F such that
J: g *' gq = q by RING_4:52,RING_4:1;
eval(p,a) = 0.F * eval(gp,a) &
eval(q,a) = 0.F * eval(gq,a) by J,G,X,POLYNOM4:24; then
a is_a_root_of p & a is_a_root_of q by POLYNOM5:def 7;
hence p,q have_a_common_root by RATFUNC1:def 4,RATFUNC1:def 3;
end;
end;
hence for p,q being Element of the carrier of Polynom-Ring F
holds p,q are_coprime iff p,q have_no_common_roots by copr2;
end;
now assume not F is algebraic-closed; then
reconsider F1 = F as non algebraic-closed Field;
set p = the non constant non with_roots monic
Element of the carrier of Polynom-Ring F1;
reconsider p1 = p as Element of Polynom-Ring F1;
reconsider e = 1.(Polynom-Ring F1) as Element of Polynom-Ring F1;
H: e = 1_.(F1) by POLYNOM3:def 10;
B: not p,p are_coprime
proof
D: p1 divides p1;
now assume 1.(Polynom-Ring F1) is a_gcd of p1,p1; then
p1 divides e by D,RING_4:def 10; then
p divides 1_.(F1) by H; then
deg p <= deg 1_.(F) by RING_5:13; then
deg p <= 0 by RATFUNC1:def 2;
hence contradiction by RING_4:def 4;
end;
hence thesis;
end;
now assume p,p have_a_common_root; then
consider a being Element of F1 such that
A: a is_a_common_root_of p,p by RATFUNC1:def 4;
a is_a_root_of p & a is_a_root_of p by A,RATFUNC1:def 3;
hence contradiction by POLYNOM5:def 8;
end;
hence ex p,q being Element of the carrier of Polynom-Ring F
st (not p,q are_coprime) & p,q have_no_common_roots by B;
end;
hence thesis by A;
end;
theorem ClA:
for F being Field holds
F is algebraic-closed iff
for E being F-algebraic FieldExtension of F holds E == F
proof
let F be Field;
A: now assume F is algebraic-closed;
then F is maximal_algebraic by eq;
hence for E being F-algebraic FieldExtension of F holds E == F;
end;
now assume for E being F-algebraic FieldExtension of F holds E == F;
then F is maximal_algebraic;
hence F is algebraic-closed by eq;
end;
hence thesis by A;
end;
theorem
for F being Field holds
F is algebraic-closed iff
for E being F-finite FieldExtension of F holds E == F
proof
let F be Field;
A: now assume F is algebraic-closed;
then F is maximal_algebraic by eq;
hence for E being F-finite FieldExtension of F holds E == F;
end;
now assume not F is algebraic-closed; then
not F is maximal_algebraic by eq;
then consider E being F-algebraic FieldExtension of F such that
B: not E == F;
F is Subfield of E by FIELD_4:7; then
C: the carrier of F c= the carrier of E by EC_PF_1:def 1;
F: not deg(E,F) = 1 by B,FIELD_7:8;
now assume G: for a being Element of E holds a in F;
now let o be object;
assume o in the carrier of E; then
reconsider a = o as Element of E;
a in F by G;
hence o in the carrier of F;
end;
hence contradiction by F,FIELD_7:7,C,TARSKI:2;
end; then
consider a being Element of E such that D: not a in F;
set p = MinPoly(a,F);
a in {a} by TARSKI:def 1; then
not {a} is Subset of F by D; then
not FAdj(F,{a}) == F by FIELD_7:3;
hence ex E being F-finite FieldExtension of F st not E == F;
end;
hence thesis by A;
end;
registration
cluster algebraic-closed -> infinite for Field;
coherence;
end;
begin :: Existence of Algebraic Closures
definition
let F be Field;
mode ClosureSequence of F -> ascending Field-yielding sequence means :dA:
it.0 = F &
for i being Element of NAT
for K being Field,
E being FieldExtension of K st K = it.i & E = it.(i+1)
holds for p being non constant Element of the carrier of Polynom-Ring K
holds p is_with_roots_in E;
existence
proof
defpred P[object,Field,Field] means
$3 is FieldExtension of $2 &
for K being FieldExtension of $2 st K = $3
for p being non constant Element of the carrier of Polynom-Ring $2
holds p is_with_roots_in K;
A: for n being Nat for x being Field ex y being Field st P[n,x,y]
proof
let n be Nat; let x be Field;
consider y being FieldExtension of x such that
A1: for p being non constant Element of the carrier of Polynom-Ring x
holds p is_with_roots_in y by FIELD_11:43;
take y;
thus P[n,x,y] by A1;
end;
consider f being Field-yielding sequence such that
B: f.0 = F & for n being Nat holds P[n,f.n,f.(n+1)] from RecExField(A);
for i be Element of NAT holds f.(i+1) is FieldExtension of f.i by B; then
reconsider f as ascending Field-yielding sequence by defasc;
take f;
thus f.0 = F by B;
thus thesis by B;
end;
end;
theorem alg3:
for f being ascending Field-yielding sequence
for p being Polynomial of (SeqField f)
ex i being Element of NAT st p is Polynomial of (f.i)
proof
let f be ascending Field-yielding sequence, p be Polynomial of (SeqField f);
consider i being Element of NAT such that
H: Coeff p c= the carrier of (f.i) by alg3a;
take i;
f.i is Subfield of SeqField f by Fsub;
then SeqField f is FieldExtension of f.i by FIELD_4:7;
hence thesis by H,FIELD_7:11;
end;
f12:
for f being ascending Field-yielding sequence
for p being non constant Polynomial of (SeqField f)
ex i being Element of NAT st p is non constant Polynomial of (f.i)
proof
let f be ascending Field-yielding sequence,
p be non constant Polynomial of (SeqField f);
consider i being Element of NAT such that H: p is Polynomial of (f.i)
by alg3;
reconsider p1 = p as Element of the carrier of Polynom-Ring f.i
by H,POLYNOM3:def 10;
reconsider q = p as Element of the carrier of Polynom-Ring (SeqField f)
by POLYNOM3:def 10;
f.i is Subfield of SeqField f by Fsub; then
SeqField f is FieldExtension of f.i by FIELD_4:7; then
deg p1 = deg q by FIELD_4:20; then
reconsider p1 as non constant Element of the carrier of Polynom-Ring f.i
by RING_4:def 4,RATFUNC1:def 2;
reconsider q1 = p1 as Polynomial of f.i;
H: deg q1 >= 0;
take i;
thus thesis by H,RING_4:def 4,RATFUNC1:def 2;
end;
registration
let F be Field;
let f be ClosureSequence of F;
cluster SeqField f -> F-extending;
coherence
proof
F = f.0 by dA;
then F is Subfield of (SeqField f) by Fsub;
hence thesis by FIELD_4:7;
end;
cluster SeqField f -> algebraic-closed;
coherence
proof
now let p be non constant Polynomial of SeqField f;
consider i being Element of NAT such that
A: p is non constant Polynomial of (f.i) by f12;
reconsider F = f.i as Field;
reconsider q = p as non constant Polynomial of F by A;
reconsider p1 = q as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
deg q >= 0; then
reconsider p1 as non constant Element of the carrier of Polynom-Ring F
by RING_4:def 4,RATFUNC1:def 2;
reconsider E = f.(i+1) as FieldExtension of F by defasc;
the carrier of Polynom-Ring F c= the carrier of Polynom-Ring E by FIELD_4:10;
then reconsider q1 = p1 as Element of the carrier of Polynom-Ring E;
consider a being Element of E such that
B: a is_a_root_of p1,E by dA,FIELD_4:def 3;
C: Ext_eval(p1,a) = 0.E by B,FIELD_4:def 2;
D: F is Subfield of SeqField f by Fsub;
reconsider pp = p as Element of the carrier of Polynom-Ring SeqField f
by POLYNOM3:def 10;
G: E is Subfield of SeqField f by Fsub; then
the carrier of E c= the carrier of SeqField f by EC_PF_1:def 1; then
reconsider a1 = a as Element of SeqField f;
F: SeqField f is E-extending FieldExtension of F by G,D,FIELD_4:7; then
Ext_eval(p1,a) = Ext_eval(p1,a1) by FIELD_7:14
.= eval(pp,a1) by F,FIELD_4:26
.= eval(p,a1);
then eval(p,a1) = 0.(SeqField f) by C,G,EC_PF_1:def 1;
hence p is with_roots by POLYNOM5:def 8,def 7;
end;
hence thesis by alg2;
end;
end;
theorem main1:
for F being Field ex E being FieldExtension of F st E is algebraic-closed
proof
let F be Field;
set f = the ClosureSequence of F;
take E = SeqField f;
thus thesis;
end;
definition
let F be Field;
mode AlgebraicClosure of F -> FieldExtension of F means :defAC:
it is F-algebraic &
it is algebraic-closed;
existence
proof
consider A being FieldExtension of F such that
A: A is algebraic-closed by main1;
take K = F_Alg A;
thus K is F-algebraic;
now let p being non constant Polynomial of K;
reconsider A as K-extending FieldExtension of F by FIELD_7:42;
K is Subfield of A by FIELD_4:7; then
H0: K is Subring of A by FIELD_5:12; then
reconsider p1 = p as Polynomial of A by FIELD_4:9;
H1: p1 is Element of Polynom-Ring A by POLYNOM3:def 10;
H2: p is Element of Polynom-Ring K by POLYNOM3:def 10;
B0: deg p > 0 by RATFUNC1:def 2;
deg p = deg p1 by H1,H2,FIELD_4:20; then
reconsider p1 as non constant Polynomial of A by B0,RATFUNC1:def 2;
consider a1 being Element of A such that
B1: a1 is_a_root_of p1 by A,POLYNOM5:def 8;
B2: 0.A = eval(p1,a1) by B1,POLYNOM5:def 7
.= Ext_eval(p,a1) by H1,H2,FIELD_4:26;
then a1 is F-algebraic by FIELD_6:43,lemA;
then a1 in the set of all a where a is F-algebraic Element of A;
then a1 in Alg_El A by FIELD_7:def 13;
then reconsider a = a1 as Element of K by FIELD_7:def 14;
eval(p,a) = Ext_eval(p,a1) by H2,FIELD_6:10 .= 0.K by B2,H0,C0SP1:def 3;
hence p is with_roots by POLYNOM5:def 7,def 8;
end;
hence thesis by alg2;
end;
end;
registration
let F be Field;
cluster -> F-algebraic algebraic-closed for AlgebraicClosure of F;
coherence by defAC;
end;
registration
let F be Field;
cluster F-homomorphic F-monomorphic for algebraic-closed Field;
existence
proof
set A = the AlgebraicClosure of F;
take A;
thus A is F-homomorphic;
thus A is F-monomorphic;
end;
end;
theorem
for F being Field ex E being Field st E is AlgebraicClosure of F
proof
let F be Field;
set A = the AlgebraicClosure of F;
take A;
thus thesis;
end;
theorem XX:
for F being Field
for E being F-algebraic FieldExtension of F
ex A being AlgebraicClosure of F st E is Subfield of A
proof
let F be Field, E be F-algebraic FieldExtension of F;
set K = the AlgebraicClosure of E;
reconsider K as FieldExtension of F;
reconsider K as E-extending FieldExtension of F;
K is F-algebraic by FIELD_7:39; then
reconsider K as AlgebraicClosure of F by defAC;
take K;
thus thesis by FIELD_4:7;
end;
registration
let F be Field;
let E be F-algebraic FieldExtension of F;
cluster E-extending for AlgebraicClosure of F;
existence
proof
consider A being AlgebraicClosure of F such that
B: E is Subfield of A by XX;
take A;
thus thesis by B,FIELD_4:7;
end;
end;
theorem
for F being Field
for E being F-algebraic FieldExtension of F
for A being AlgebraicClosure of E holds A is AlgebraicClosure of F
proof
let F be Field, E be F-algebraic FieldExtension of F;
let A be AlgebraicClosure of E;
reconsider B = A as FieldExtension of F;
B is F-algebraic by FIELD_7:39;
hence thesis by defAC;
end;
theorem
for F being Field
for E being FieldExtension of F
for A being AlgebraicClosure of F
st A is E-extending holds A is AlgebraicClosure of E
proof
let F be Field, E be FieldExtension of F;
let A be AlgebraicClosure of F;
assume A is E-extending; then
reconsider B = A as FieldExtension of E;
B is E-algebraic by FIELD_7:40;
hence thesis by defAC;
end;
theorem lift3a:
for F being Field
for A1,A2 being AlgebraicClosure of F st A1 is A2-extending holds A2 == A1
proof
let F be Field, E1,E2 be AlgebraicClosure of F;
assume E1 is E2-extending;
then reconsider K = E1 as E2-extending FieldExtension of F;
K is E2-algebraic by FIELD_7:40;
hence thesis by ClA;
end;
begin :: Some more Preliminaries
registration
let R being Ring,
S being R-homomorphic Ring;
cluster S-homomorphic R-homomorphic for Ring;
existence
proof
take S;
id S is RingHomomorphism;
hence S is S-homomorphic by RING_2:def 4;
thus S is R-homomorphic;
end;
end;
registration
let R being Ring,
S being R-homomorphic Ring,
T being S-homomorphic Ring;
let f being additive Function of R,S,
g being additive Function of S,T;
cluster g*f -> additive for Function of R,T;
coherence
proof
now let a,b be Element of R;
A: dom f = the carrier of R by FUNCT_2:def 1;
hence (g*f).(a+b) = g.(f.(a+b)) by FUNCT_1:13
.= g.(f.a + f.b) by VECTSP_1:def 20
.= g.(f.a) + g.(f.b) by VECTSP_1:def 20
.= (g*f).a + g.(f.b) by A,FUNCT_1:13
.= (g*f).a + (g*f).b by A,FUNCT_1:13;
end;
hence thesis;
end;
end;
registration
let R being Ring,
S being R-homomorphic Ring,
T being S-homomorphic Ring;
let f being multiplicative Function of R,S,
g being multiplicative Function of S,T;
cluster g*f -> multiplicative for Function of R,T;
coherence
proof
now let a,b be Element of R;
A: dom f = the carrier of R by FUNCT_2:def 1;
hence (g*f).(a*b) = g.(f.(a*b)) by FUNCT_1:13
.= g.(f.a * f.b) by GROUP_6:def 6
.= g.(f.a) * g.(f.b) by GROUP_6:def 6
.= (g*f).a * g.(f.b) by A,FUNCT_1:13
.= (g*f).a * (g*f).b by A,FUNCT_1:13;
end;
hence thesis;
end;
end;
registration
let R being Ring,
S being R-homomorphic Ring,
T being S-homomorphic Ring;
let f being unity-preserving Function of R,S,
g being unity-preserving Function of S,T;
cluster g*f -> unity-preserving for Function of R,T;
coherence;
end;
theorem lift5a:
for F being Field
for E being FieldExtension of F holds id F is Monomorphism of F,E
proof
let F be Field, E be FieldExtension of F;
I: F is Subfield of E by FIELD_4:7; then
H: the carrier of F c= the carrier of E by EC_PF_1:def 1;
rng(id F) c= the carrier of E by I,EC_PF_1:def 1; then
reconsider f = id F as Function of F,E by FUNCT_2:6;
f is additive multiplicative unity-preserving monomorphism
proof
now let a,b be Element of F;
reconsider a1 = a, b1 = b as Element of E by H;
K: [a,b] in [:the carrier of F,the carrier of F:] by ZFMISC_1:def 2;
thus f.(a+b) = ((the addF of E)||(the carrier of F)).(a,b)
by I,EC_PF_1:def 1
.= f.a + f.b by K,FUNCT_1:49;
end;
hence K1: f is additive;
now let a,b be Element of F;
reconsider a1 = a, b1 = b as Element of E by H;
K: [a,b] in [:the carrier of F,the carrier of F:] by ZFMISC_1:def 2;
thus f.(a*b) = ((the multF of E)||(the carrier of F)).(a,b)
by I,EC_PF_1:def 1
.= f.a * f.b by K,FUNCT_1:49;
end;
hence K2: f is multiplicative;
thus f is unity-preserving by I,EC_PF_1:def 1;
hence f is monomorphism by K1,K2;
end;
hence thesis;
end;
theorem ll:
for R being Ring,
S being R-homomorphic Ring, T being S-homomorphic R-homomorphic Ring
for f being additive Function of R,S, g being additive Function of S,T
holds PolyHom(g*f) = (PolyHom g) * (PolyHom f)
proof
let R be Ring, S be R-homomorphic Ring, T be R-homomorphic S-homomorphic Ring;
let f be additive Function of R,S, g be additive Function of S,T;
now let o be object;
assume o in the carrier of Polynom-Ring R;
then reconsider p = o as Element of the carrier of Polynom-Ring R;
now let i be Nat;
A: dom f = the carrier of R by FUNCT_2:def 1;
C: dom(PolyHom f) = the carrier of Polynom-Ring R by FUNCT_2:def 1;
thus ((PolyHom(g*f)).p).i
= (g*f).(p.i) by FIELD_1:def 2
.= g.(f.(p.i)) by A,FUNCT_1:13
.= g.( ((PolyHom f).p).i ) by FIELD_1:def 2
.= ((PolyHom g).((PolyHom f).p)).i by FIELD_1:def 2
.= (((PolyHom g) * (PolyHom f)).p).i by C,FUNCT_1:13;
end;
then (PolyHom(g*f)).p = ((PolyHom g) * (PolyHom f)).p;
hence (PolyHom(g*f)).o = ((PolyHom g) * (PolyHom f)).o;
end;
hence thesis;
end;
ll2:
for R being Ring,
S being R-homomorphic Ring, T being R-homomorphic S-homomorphic Ring
for f being additive Function of R,S, g being additive Function of S,T
st g * f = id R holds (PolyHom g) * (PolyHom f) = id(Polynom-Ring R)
proof
let R be Ring, S be R-homomorphic Ring, T be R-homomorphic S-homomorphic Ring;
let f be additive Function of R,S, g be additive Function of S,T;
assume AS: g * f = id R;
A: dom((PolyHom g) * (PolyHom f)) = the carrier of Polynom-Ring R
by FUNCT_2:def 1;
now let o be object;
assume o in dom((PolyHom g) * (PolyHom f)); then
reconsider p = o as Element of the carrier of Polynom-Ring R;
now let i be Nat;
thus ((PolyHom(g*f)).p).i = (g*f).(p.i) by FIELD_1:def 2 .= p.i by AS;
end;
then (PolyHom(g*f)).p = p;
hence o = ((PolyHom g) * (PolyHom f)).o by ll;
end;
hence thesis by A;
end;
theorem
for R being Ring,
S being R-homomorphic Ring, T being R-homomorphic S-homomorphic Ring
for f being additive Function of R,S, g being additive Function of S,T
st g * f = id R holds PolyHom(g*f) = id(Polynom-Ring R)
proof
let R be Ring, S be R-homomorphic Ring, T be R-homomorphic S-homomorphic Ring;
let f be additive Function of R,S, g be additive Function of S,T;
assume g * f = id R;
hence id(Polynom-Ring R) = (PolyHom g) * (PolyHom f) by ll2
.= PolyHom(g*f) by ll;
end;
theorem lift9:
for F1,F2 being Field,
E being FieldExtension of F1 st F1 == F2 holds E is FieldExtension of F2
proof
let F1,F2 be Field, E be FieldExtension of F1;
assume F1 == F2; then
A: F2 is Subfield of F1 by FIELD_7:def 2;
F1 is Subfield of E by FIELD_4:7; then
F2 is Subfield of E by A,EC_PF_1:5;
hence thesis by FIELD_4:7;
end;
theorem lift6b:
for F1,F2 being Field
st F1 == F2 holds 0_.(F1) = 0_.(F2) & 1_.(F1) = 1_.(F2)
proof
let F1,F2 be Field;
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;
hence 0_.(F1) = 0_.(F2) by FIELD_4:12;
thus 1_.(F1) = 1_.(F2) by A,FIELD_4:14;
end;
theorem lift6a:
for F1,F2 being Field
for p being Polynomial of F1 st F1 == F2 holds p is Polynomial of F2
proof
let F1,F2 be Field, p be Polynomial of F1;
assume F1 == F2; then
F1 is Subfield of F2 by FIELD_7:def 2; then
F1 is Subring of F2 by FIELD_5:12;
hence thesis by FIELD_4:9;
end;
theorem lift6:
for F1,F2 being Field
for p being non zero Polynomial of F1
st F1 == F2 holds p is non zero Polynomial of F2
proof
let F1,F2 be Field, p be non zero Polynomial of F1;
assume AS: F1 == F2; then
reconsider p1 = p as Polynomial of F2 by lift6a;
now assume p1 is zero;
then p1 = 0_.(F2) by UPROOTS:def 5
.= 0_.(F1) by AS,lift6b;
hence contradiction;
end;
hence thesis;
end;
theorem lift8:
for F1,F2 being Field
for p being Polynomial of F1 for q being Polynomial of F2
for a being Element of F1, b being Element of F2
st F1 == F2 & p = q & a = b holds eval(p,a) = eval(q,b)
proof
let F1,F2 be Field;
let p be Polynomial of F1; let q be Polynomial of F2;
let a be Element of F1, b be Element of F2;
assume AS: F1 == F2 & p = q & a = b; then
F1 is Subfield of F2 by FIELD_7:def 2; then
A: F2 is FieldExtension of F1 by FIELD_4:7;
p is Element of the carrier of Polynom-Ring F1 &
q is Element of the carrier of Polynom-Ring F2 by POLYNOM3:def 10;
hence thesis by A,AS,FIELD_4:27;
end;
theorem lift7:
for F1,F2 being Field,
E1 being FieldExtension of F1, E2 being FieldExtension of F2
for p being Polynomial of F1 for q being Polynomial of F2
for a being Element of E1, b being Element of E2
st F1 == F2 & E1 == E2 & p = q & a = b holds Ext_eval(p,a) = Ext_eval(q,b)
proof
let F1,F2 be Field,
E1 be FieldExtension of F1, E2 be FieldExtension of F2;
let p be Polynomial of F1; let q be Polynomial of F2;
let a be Element of E1, b be Element of E2;
assume AS: F1 == F2 & E1 == E2 & p = q & a = b;
B: p is Element of the carrier of Polynom-Ring F1 &
q is Element of the carrier of Polynom-Ring F2 by POLYNOM3:def 10;
p is Polynomial of E1 by FIELD_4:8; then
reconsider p1 = p as Element of the carrier of Polynom-Ring E1
by POLYNOM3:def 10;
q is Polynomial of E2 by FIELD_4:8; then
reconsider q1 = q as Element of the carrier of Polynom-Ring E2
by POLYNOM3:def 10;
thus Ext_eval(p,a) = eval(p1,a) by B,FIELD_4:26
.= eval(q1,b) by AS,lift8
.= Ext_eval(q,b) by B,FIELD_4:26;
end;
theorem lift5:
for F1,F2 being Field, E being F1-algebraic FieldExtension of F1
st F1 == F2 holds E is F2-algebraic FieldExtension of F2
proof
let F1,F2 be Field, E be F1-algebraic FieldExtension of F1;
assume AS: F1 == F2; then
reconsider E3 = E as FieldExtension of F2 by lift9;
now let a be Element of E3;
reconsider a1 = a as Element of E;
consider p being non zero Polynomial of F1 such that
B: Ext_eval(p,a1) = 0.E by FIELD_6:43;
reconsider p1 = p as non zero Polynomial of F2 by AS,lift6;
Ext_eval(p1,a1) = 0.E3 by B,AS,lift7;
hence a is F2-algebraic by FIELD_6:43;
end;
hence thesis by FIELD_7:def 11;
end;
theorem lift4:
for F1,F2 being Field, E being AlgebraicClosure of F1
st F1 == F2 holds E is AlgebraicClosure of F2
proof
let F1,F2 be Field, E be AlgebraicClosure of F1;
assume F1 == F2; then
reconsider E3 = E as F2-algebraic FieldExtension of F2 by lift5;
E3 is algebraic-closed;
hence thesis by defAC;
end;
definition
let X be set;
attr X is Field-membered means :defFm:
for x being object st x in X holds x is Field;
end;
registration
cluster Field-membered non empty for set;
existence
proof
set F = the Field;
take X = { F };
thus thesis by TARSKI:def 1;
end;
end;
definition
let X be non empty Field-membered set;
redefine mode Element of X -> Field; :: redefines Element (SUBSET_1, definition)
coherence by defFm;
end;
definition
let F be Field;
func SubFields F -> set means :defX:
for o being object holds
o in it iff (ex K being strict Field st o = K & K is Subfield of F);
existence
proof
set M = { S where S is Subset of the carrier of F :
ex K being strict Field st S = the carrier of K & K is Subfield of F };
defpred P[object,object] means
ex K being strict Field st K = $2 &
the carrier of K = $1 & K is Subfield of F;
A: for x,y,z being object st P[x,y] & P[x,z] holds y = z by EC_PF_1:8;
consider A being set such that
B: for x being object holds x in A iff
ex y being object st y in M & P[y,x] from TARSKI:sch 1(A);
take A;
C: now let x be object;
assume x in A;
then consider y being object such that
D: y in M & P[y,x] by B;
consider K being strict Field such that
E: K = x & the carrier of K = y & K is Subfield of F by D;
thus ex K being strict Field st x = K & K is Subfield of F by E;
end;
now let x be object;
assume ex K being strict Field st x = K & K is Subfield of F;
then consider K being strict Field such that
D: x = K & K is Subfield of F;
the carrier of K c= the carrier of F by D,EC_PF_1:def 1;
then the carrier of K in M by D;
hence x in A by B,D;
end;
hence thesis by C;
end;
uniqueness
proof
let A,B be set such that
A1: for x being object holds
x in A iff (ex K being strict Field st x = K & K is Subfield of F)
and
A2: for x being object holds
x in B iff (ex K being strict Field st x = K & K is Subfield of F);
A3: now let x be object;
assume x in A;
then ex K being strict Field st x = K & K is Subfield of F by A1;
hence x in B by A2;
end;
now let x be object;
assume x in B;
then ex K being strict Field st x = K & K is Subfield of F by A2;
hence x in A by A1;
end;
hence A = B by A3,TARSKI:2;
end;
end;
registration
let F be Field;
cluster SubFields F -> non empty Field-membered;
coherence
proof
set K = the doubleLoopStr of F;
K is Subfield of F by lemug;
hence SubFields(F) is non empty by defX;
now let x being object;
assume x in SubFields(F);
then consider K being strict Field such that
A: x = K & K is Subfield of F by defX;
thus x is Field by A;
end;
hence thesis;
end;
end;
theorem subfie:
for F,K being Field holds K in SubFields F iff K is strict Subfield of F
proof
let F,K be Field;
now assume K in SubFields(F);
then consider K1 being strict Field such that
B: K1 = K & K1 is Subfield of F by defX;
thus K is strict Subfield of F by B;
end;
hence thesis by defX;
end;
begin :: Uniqueness of Algebraic Closures
definition
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
func Ext_Set(f,E) -> non empty set equals
{ [K,g] where K is Element of SubFields(E), g is Function of K,L :
ex K1 being FieldExtension of F,
g1 being Function of K1,L
st K1 = K & g1 = g & g1 is monomorphism f-extending };
coherence
proof
set M = { [K,g] where K is Element of SubFields(E), g is Function of K,L :
ex K1 being FieldExtension of F,
g1 being Function of K1,L
st K1 = K & g1 = g & g1 is monomorphism f-extending };
set K1 = the doubleLoopStr of F;
H: K1 == F by lemug1; then
F is Subfield of K1 by FIELD_7:def 2; then
reconsider K1 as FieldExtension of F by FIELD_4:7;
J: F is Subfield of E by FIELD_4:7;
K1 is Subfield of F by H,FIELD_7:def 2; then
K1 is Subfield of E by J,EC_PF_1:5; then
reconsider K = K1 as Element of SubFields(E) by subfie;
reconsider g = f as Function of K,L;
reconsider g1 = f as Function of K1,L;
B: g1 is f-extending;
C: now let x,y be Element of K1;
reconsider a = x, b = y as Element of F;
thus g1.(x+y) = f.(a+b) .= g1.x + g1.y by VECTSP_1:def 20;
end;
D: now let x,y be Element of K1;
reconsider a = x, b = y as Element of F;
thus g1.(x*y) = f.(a*b) .= g1.x * g1.y by GROUP_6:def 6;
end;
g1.(1_K1) = f.(1_F) .= 1_L by GROUP_1:def 13; then
g1 is additive multiplicative unity-preserving by C,D; then
[K,g] in M by B;
hence thesis;
end;
end;
registration
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
cluster -> pair for Element of Ext_Set(f,E);
coherence
proof
let p be Element of Ext_Set(f,E);
p in Ext_Set(f,E); then
consider K be Element of SubFields(E), g be Function of K,L such that
A: p = [K,g] &
ex K1 being FieldExtension of F,
g1 being Function of K1,L
st K1 = K & g1 = g & g1 is monomorphism f-extending;
thus thesis by A;
end;
end;
definition
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let p be Element of Ext_Set(f,E);
redefine func p`1 -> strict FieldExtension of F; :: redefines `1 (XTUPLE_0, definition)
coherence
proof
p in Ext_Set(f,E); then
consider K be Element of SubFields(E), g be Function of K,L such that
A: p = [K,g] &
ex K1 being FieldExtension of F,
g1 being Function of K1,L
st K1 = K & g1 = g & g1 is monomorphism f-extending;
thus thesis by A,subfie;
end;
end;
definition
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let p be Element of Ext_Set(f,E);
redefine func p`2 -> Function of (p`1),L; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
p in Ext_Set(f,E); then
consider K be Element of SubFields(E), g be Function of K,L such that
A: p = [K,g] &
ex K1 being FieldExtension of F,
g1 being Function of K1,L
st K1 = K & g1 = g & g1 is monomorphism f-extending;
thus thesis by A;
end;
end;
theorem inS:
for F being Field, E being FieldExtension of F,
L being F-monomorphic Field,
f being Monomorphism of F,L
for K being strict FieldExtension of F,
g being Function of K,L st g is monomorphism
holds [K,g] in Ext_Set(f,E) iff
(E is FieldExtension of K & F is Subfield of K & g is f-extending)
proof
let F be Field, E be FieldExtension of F,
L be F-monomorphic Field, f be Monomorphism of F,L;
let K be strict FieldExtension of F, g be Function of K,L;
assume AS: g is monomorphism;
A: now assume [K,g] in Ext_Set(f,E); then
consider K2 be Element of SubFields(E), g2 be Function of K2,L such that
A1: [K,g] = [K2,g2] &
ex K1 being FieldExtension of F, g1 being Function of K1,L
st K1 = K2 & g1 = g2 & g1 is monomorphism f-extending;
consider K1 being FieldExtension of F, g1 being Function of K1,L such that
A2: K1 = K2 & g1 = g2 & g1 is monomorphism f-extending by A1;
A3: K2 = [K,g]`1 by A1,XTUPLE_0:def 2 .= K;
A7: g2 = [K,g]`2 by A1,XTUPLE_0:def 3 .= g;
K is strict Subfield of E by A3,subfie;
hence E is FieldExtension of K & F is Subfield of K &
g is f-extending by A2,A7,FIELD_4:7;
end;
now assume B0:
E is FieldExtension of K & F is Subfield of K & g is f-extending; then
K is Subfield of E by FIELD_4:7;
then K in SubFields(E) by subfie;
hence [K,g] in Ext_Set(f,E) by B0,AS;
end;
hence thesis by A;
end;
definition
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let p,q be Element of Ext_Set(f,E);
pred p <= q means
q`1 is FieldExtension of p`1 &
for K being FieldExtension of p`1, g being Function of K,L
st K = q`1 & g = q`2 holds g is (p`2)-extending;
end;
definition
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty Subset of Ext_Set(f,E);
attr S is ascending means :dasc:
for p,q being Element of S holds p <= q or q <= p;
end;
registration
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
cluster ascending for non empty Subset of Ext_Set(f,E);
existence
proof
set p = the Element of Ext_Set(f,E);
set S = { p };
now let o be object;
assume o in S;
then o = p by TARSKI:def 1;
hence o in Ext_Set(f,E);
end; then
S c= Ext_Set(f,E); then
reconsider S as non empty Subset of Ext_Set(f,E);
take S;
now let q1,q2 be Element of S;
B: q1 = p & q2 = p by TARSKI:def 1;
for K being FieldExtension of p`1, g being Function of K,L
st K = p`1 & g = p`2 holds g is (p`2)-extending;
hence q1 <= q2 or q2 <= q1 by B,FIELD_4:6;
end;
hence thesis;
end;
end;
theorem po1:
for F being Field, E being FieldExtension of F
for L being F-monomorphic Field,
f being Monomorphism of F,L
for p being Element of Ext_Set(f,E) holds p <= p
proof
let F be Field, E being FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L, p be Element of Ext_Set(f,E);
for K being FieldExtension of p`1, g being Function of K,L
st K = p`1 & g = p`2 holds g is (p`2)-extending;
hence thesis by FIELD_4:6;
end;
theorem po2:
for F being Field, E being FieldExtension of F
for L being F-monomorphic Field,
f being Monomorphism of F,L
for p,q being Element of Ext_Set(f,E) st p <= q & q <= p holds p = q
proof
let F be Field, E being FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L , p,q be Element of Ext_Set(f,E);
assume AS: p <= q & q <= p;
consider K1 being FieldExtension of p`1, g1 being Function of K1,L such that
B: K1 = q`1 & g1 = q`2 & g1 is (p`2)-extending by AS;
E: p`1 is Subfield of q`1 & q`1 is Subfield of p`1 by AS,FIELD_4:7;
p`2 = q`2 by B,E,EC_PF_1:4;
hence thesis by E,EC_PF_1:4,XTUPLE_0:2;
end;
theorem po3:
for F being Field, E being FieldExtension of F
for L being F-monomorphic Field,
f being Monomorphism of F,L
for p,q,r being Element of Ext_Set(f,E) st p <= q & q <= r holds p <= r
proof
let F be Field, E being FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L, p,q,r be Element of Ext_Set(f,E);
assume AS: p <= q & q <= r; then
consider K1 being FieldExtension of p`1, g1 being Function of K1,L such that
B: K1 = q`1 & g1 = q`2 & g1 is (p`2)-extending;
consider K2 being FieldExtension of q`1, g2 being Function of K2,L such that
D: K2 = r`1 & g2 = r`2 & g2 is (q`2)-extending by AS;
reconsider K = p`1 as Field;
reconsider K1 as FieldExtension of K;
reconsider K2 as K1-extending FieldExtension of K by B;
reconsider L1 = L as FieldExtension of L by FIELD_4:6;
reconsider g = p`2 as Function of K,L;
reconsider g2 as Function of K2,L1;
now let K be FieldExtension of p`1, h being Function of K,L;
assume F: K = r`1 & h = r`2;
g2 is g-extending by B,D,FIELD_8:41;
hence h is (p`2)-extending by F,D;
end;
hence thesis by AS;
end;
definition
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty Subset of Ext_Set(f,E);
func unionCarrier(S,f,E) -> non empty set equals
union(the set of all the carrier of p`1 where p is Element of S);
coherence
proof
set p = the Element of S;
0.(p`1) in the carrier of p`1 &
the carrier of p`1 in
the set of all the carrier of p`1 where p is Element of S;
hence thesis by TARSKI:def 4;
end;
end;
definition
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
func unionAdd(S,f,E) -> BinOp of unionCarrier(S,f,E) means :dua:
for a,b being Element of unionCarrier(S,f,E)
ex p being Element of S, x,y being Element of p`1
st x = a & y = b & it.(a,b) = x + y;
existence
proof
set C = unionCarrier(S,f,E);
defpred P[object,object,object] means
ex p being Element of S, x,y being Element of p`1
st x = $1 & y = $2 & $3 = x + y;
A: for a,b being Element of C ex z being Element of C st P[a,b,z]
proof
let a,b being Element of C;
consider Y being set such that
A0: a in Y & Y in the set of all
the carrier of p`1 where p is Element of S by TARSKI:def 4;
consider pa being Element of S such that
A1: Y = the carrier of pa`1 by A0;
consider Z being set such that
A2: b in Z & Z in the set of all
the carrier of p`1 where p is Element of S by TARSKI:def 4;
consider pb being Element of S such that
A3: Z = the carrier of pb`1 by A2;
per cases by dasc;
suppose pa <= pb;
then pa`1 is Subfield of pb`1 by FIELD_4:7;
then the carrier of pa`1 c= the carrier of pb`1 by EC_PF_1:def 1;
then reconsider x = a, y = b as Element of pb`1 by A0,A1,A2,A3;
x + y in the carrier of pb`1 &
the carrier of pb`1 in
the set of all the carrier of p`1 where p is Element of S;
then reconsider z = x + y as Element of C by TARSKI:def 4;
take z;
thus thesis;
end;
suppose pb <= pa;
then pb`1 is Subfield of pa`1 by FIELD_4:7;
then the carrier of pb`1 c= the carrier of pa`1 by EC_PF_1:def 1;
then reconsider x = a, y = b as Element of pa`1 by A0,A1,A2,A3;
x + y in the carrier of pa`1 &
the carrier of pa`1 in
the set of all the carrier of p`1 where p is Element of S;
then reconsider z = x + y as Element of C by TARSKI:def 4;
take z;
thus thesis;
end;
end;
consider A being Function of [:C,C:],C such that
B: for x,y being Element of C holds P[x,y,A.(x,y)] from BINOP_1:sch 3(A);
reconsider A as BinOp of unionCarrier(S,f,E);
take A;
thus thesis by B;
end;
uniqueness
proof
let f1,f2 be BinOp of unionCarrier(S,f,E) such that
A1: for a,b being Element of unionCarrier(S,f,E)
ex p1 being Element of S, x,y being Element of p1`1
st x = a & y = b & f1.(a,b) = x + y
and
A2: for a,b being Element of unionCarrier(S,f,E)
ex p2 being Element of S, x,y being Element of p2`1
st x = a & y = b & f2.(a,b) = x + y;
now let a,b be Element of unionCarrier(S,f,E);
consider p1 being Element of S, x1,y1 being Element of p1`1 such that
A3: x1 = a & y1 = b & f1.(a,b) = x1 + y1 by A1;
consider p2 being Element of S, x2,y2 being Element of p2`1 such that
A4: x2 = a & y2 = b & f2.(a,b) = x2 + y2 by A2;
per cases by dasc;
suppose p1 <= p2; then
p1`1 is Subfield of p2`1 by FIELD_4:7; then
A5: the addF of p1`1 = (the addF of p2`1) || (the carrier of p1`1)
by EC_PF_1:def 1;
[x2,y2] in [:the carrier of p1`1,the carrier of p1`1:]
by A3,A4,ZFMISC_1:def 2;
hence f1.(a,b) = f2.(a,b) by A3,A4,A5,FUNCT_1:49;
end;
suppose p2 <= p1; then
p2`1 is Subfield of p1`1 by FIELD_4:7;then
A5: the addF of p2`1 = (the addF of p1`1) || (the carrier of p2`1)
by EC_PF_1:def 1;
[x1,y1] in [:the carrier of p2`1,the carrier of p2`1:]
by A3,A4,ZFMISC_1:def 2;
hence f1.(a,b) = f2.(a,b) by A3,A4,A5,FUNCT_1:49;
end;
end;
hence f1 = f2;
end;
func unionMult(S,f,E) -> BinOp of unionCarrier(S,f,E) means :dum:
for a,b being Element of unionCarrier(S,f,E)
ex p being Element of S, x,y being Element of p`1
st x = a & y = b & it.(a,b) = x * y;
existence
proof
set C = unionCarrier(S,f,E);
defpred P[object,object,object] means
ex p being Element of S, x,y being Element of p`1
st x = $1 & y = $2 & $3 = x * y;
A: for a,b being Element of C ex z being Element of C st P[a,b,z]
proof
let a,b being Element of C;
consider Y being set such that
A0: a in Y & Y in the set of all
the carrier of p`1 where p is Element of S by TARSKI:def 4;
consider pa being Element of S such that
A1: Y = the carrier of pa`1 by A0;
consider Z being set such that
A2: b in Z & Z in the set of all
the carrier of p`1 where p is Element of S by TARSKI:def 4;
consider pb being Element of S such that
A3: Z = the carrier of pb`1 by A2;
per cases by dasc;
suppose pa <= pb;
then pa`1 is Subfield of pb`1 by FIELD_4:7;
then the carrier of pa`1 c= the carrier of pb`1 by EC_PF_1:def 1;
then reconsider x = a, y = b as Element of pb`1 by A0,A1,A2,A3;
x + y in the carrier of pb`1 &
the carrier of pb`1 in
the set of all the carrier of p`1 where p is Element of S;
then reconsider z = x * y as Element of C by TARSKI:def 4;
take z;
thus thesis;
end;
suppose pb <= pa;
then pb`1 is Subfield of pa`1 by FIELD_4:7;
then the carrier of pb`1 c= the carrier of pa`1 by EC_PF_1:def 1;
then reconsider x = a, y = b as Element of pa`1 by A0,A1,A2,A3;
x + y in the carrier of pa`1 &
the carrier of pa`1 in
the set of all the carrier of p`1 where p is Element of S;
then reconsider z = x * y as Element of C by TARSKI:def 4;
take z;
thus thesis;
end;
end;
consider A being Function of [:C,C:],C such that
B: for x,y being Element of C holds P[x,y,A.(x,y)] from BINOP_1:sch 3(A);
reconsider A as BinOp of unionCarrier(S,f,E);
take A;
thus thesis by B;
end;
uniqueness
proof
let f1,f2 be BinOp of unionCarrier(S,f,E) such that
A1: for a,b being Element of unionCarrier(S,f,E)
ex p1 being Element of S, x,y being Element of p1`1
st x = a & y = b & f1.(a,b) = x * y
and
A2: for a,b being Element of unionCarrier(S,f,E)
ex p2 being Element of S, x,y being Element of p2`1
st x = a & y = b & f2.(a,b) = x * y;
now let a,b be Element of unionCarrier(S,f,E);
consider p1 being Element of S, x1,y1 being Element of p1`1 such that
A3: x1 = a & y1 = b & f1.(a,b) = x1 * y1 by A1;
consider p2 being Element of S, x2,y2 being Element of p2`1 such that
A4: x2 = a & y2 = b & f2.(a,b) = x2 * y2 by A2;
per cases by dasc;
suppose p1 <= p2; then
p1`1 is Subfield of p2`1 by FIELD_4:7; then
A5: the multF of p1`1 = (the multF of p2`1) || (the carrier of p1`1)
by EC_PF_1:def 1;
[x2,y2] in [:the carrier of p1`1,the carrier of p1`1:]
by A3,A4,ZFMISC_1:def 2;
hence f1.(a,b) = f2.(a,b) by A3,A4,A5,FUNCT_1:49;
end;
suppose p2 <= p1; then
p2`1 is Subfield of p1`1 by FIELD_4:7;then
A5: the multF of p2`1 = (the multF of p1`1) || (the carrier of p2`1)
by EC_PF_1:def 1;
[x1,y1] in [:the carrier of p2`1,the carrier of p2`1:]
by A3,A4,ZFMISC_1:def 2;
hence f1.(a,b) = f2.(a,b) by A3,A4,A5,FUNCT_1:49;
end;
end;
hence f1 = f2;
end;
end;
definition
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
func unionOne(S,f,E) -> Element of unionCarrier(S,f,E) means :defone:
ex p being Element of S st it = 1.(p`1);
existence
proof
set p = the Element of S;
1.(p`1) in the carrier of p`1 &
the carrier of p`1 in
the set of all the carrier of p`1 where p is Element of S; then
reconsider e = 1.(p`1) as Element of unionCarrier(S,f,E) by TARSKI:def 4;
take e;
thus thesis;
end;
uniqueness
proof
let q1,q2 be Element of unionCarrier(S,f,E);
assume A1: (ex p1 being Element of S st q1 = 1.(p1`1)) &
(ex p2 being Element of S st q2 = 1.(p2`1)); then
consider p1 being Element of S such that A2: q1 = 1.(p1`1);
consider p2 being Element of S such that A3: q2 = 1.(p2`1) by A1;
per cases by dasc;
suppose p1 <= p2;
then p1`1 is Subfield of p2`1 by FIELD_4:7;
hence q1 = q2 by A2,A3,EC_PF_1:def 1;
end;
suppose p2 <= p1;
then p2`1 is Subfield of p1`1 by FIELD_4:7;
hence q1 = q2 by A2,A3,EC_PF_1:def 1;
end;
end;
func unionZero(S,f,E) -> Element of unionCarrier(S,f,E) means :defzero:
ex p being Element of S st it = 0.(p`1);
existence
proof
set p = the Element of S;
0.(p`1) in the carrier of p`1 &
the carrier of p`1 in
the set of all the carrier of p`1 where p is Element of S; then
reconsider e = 0.(p`1) as Element of unionCarrier(S,f,E) by TARSKI:def 4;
take e;
thus thesis;
end;
uniqueness
proof
let q1,q2 be Element of unionCarrier(S,f,E);
assume A1: (ex p1 being Element of S st q1 = 0.(p1`1)) &
(ex p2 being Element of S st q2 = 0.(p2`1)); then
consider p1 being Element of S such that A2: q1 = 0.(p1`1);
consider p2 being Element of S such that A3: q2 = 0.(p2`1) by A1;
per cases by dasc;
suppose p1 <= p2;
then p1`1 is Subfield of p2`1 by FIELD_4:7;
hence q1 = q2 by A2,A3,EC_PF_1:def 1;
end;
suppose p2 <= p1;
then p2`1 is Subfield of p1`1 by FIELD_4:7;
hence q1 = q2 by A2,A3,EC_PF_1:def 1;
end;
end;
end;
definition
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
func unionField(S,f,E) -> strict doubleLoopStr means :duf:
the carrier of it = unionCarrier(S,f,E) &
the addF of it = unionAdd(S,f,E) &
the multF of it = unionMult(S,f,E) &
the OneF of it = unionOne(S,f,E) &
the ZeroF of it = unionZero(S,f,E);
existence
proof
take doubleLoopStr(# unionCarrier(S,f,E),unionAdd(S,f,E),unionMult(S,f,E),
unionOne(S,f,E),unionZero(S,f,E) #);
thus thesis;
end;
uniqueness;
end;
theorem lem1a:
for F being Field, E being FieldExtension of F,
L being F-monomorphic Field
for f being Monomorphism of F,L,
S being non empty Subset of Ext_Set(f,E)
for p,q being Element of S
for a being Element of p`1 holds p <= q implies a in the carrier of q`1
proof
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be non empty Subset of Ext_Set(f,E);
let p,q be Element of S, a be Element of p`1;
assume p <= q; then
p`1 is Subfield of q`1 by FIELD_4:7; then
the carrier of p`1 c= the carrier of q`1 by EC_PF_1:def 1;
hence thesis;
end;
theorem lem5a:
for F being Field, E being FieldExtension of F,
L being F-monomorphic Field
for f being Monomorphism of F,L,
S being ascending non empty Subset of Ext_Set(f,E)
for p being Element of S
holds 1.unionField(S,f,E) = 1.(p`1) & 0.unionField(S,f,E) = 0.(p`1)
proof
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
let p be Element of S;
1.unionField(S,f,E) = unionOne(S,f,E) by duf; then
consider q being Element of S such that
A: 1.unionField(S,f,E) = 1.(q`1) by defone;
now per cases by dasc;
suppose p <= q;
then p`1 is Subfield of q`1 by FIELD_4:7;
hence 1.unionField(S,f,E) = 1.(p`1) by A,EC_PF_1:def 1;
end;
suppose q <= p;
then q`1 is Subfield of p`1 by FIELD_4:7;
hence 1.unionField(S,f,E) = 1.(p`1) by A,EC_PF_1:def 1;
end;
end;
hence 1.unionField(S,f,E) = 1.(p`1);
0.unionField(S,f,E) = unionZero(S,f,E) by duf; then
consider q being Element of S such that
A: 0.unionField(S,f,E) = 0.(q`1) by defzero;
now per cases by dasc;
suppose p <= q;
then p`1 is Subfield of q`1 by FIELD_4:7;
hence 0.unionField(S,f,E) = 0.(p`1) by A,EC_PF_1:def 1;
end;
suppose q <= p;
then q`1 is Subfield of p`1 by FIELD_4:7;
hence 0.unionField(S,f,E) = 0.(p`1) by A,EC_PF_1:def 1;
end;
end;
hence 0.unionField(S,f,E) = 0.(p`1);
end;
theorem lem4a:
for F being Field, E being FieldExtension of F,
L being F-monomorphic Field
for f being Monomorphism of F,L,
S being ascending non empty Subset of Ext_Set(f,E)
for a,b being Element of unionField(S,f,E)
for p being Element of S, x,y being Element of p`1
st x = a & y = b holds a + b = x + y & a * b = x * y
proof
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
let a,b be Element of unionField(S,f,E);
let p be Element of S, x,y being Element of p`1;
assume AS: x = a & y = b;
H: the carrier of unionField(S,f,E) = unionCarrier(S,f,E) by duf; then
consider q being Element of S, x1,y1 being Element of q`1 such that
A: x1 = a & y1 = b & unionAdd(S,f,E).(a,b) = x1 + y1 by dua;
now per cases by dasc;
suppose p <= q;
then p`1 is Subfield of q`1 by FIELD_4:7; then
B: the addF of p`1 = (the addF of q`1) || (the carrier of p`1)
by EC_PF_1:def 1;
C: [x1,y1] in [:the carrier of p`1,the carrier of p`1:]
by AS,A,ZFMISC_1:def 2;
thus a + b = x1 + y1 by A,duf .= x + y by AS,A,B,C,FUNCT_1:49;
end;
suppose q <= p;
then q`1 is Subfield of p`1 by FIELD_4:7; then
B: the addF of q`1 = (the addF of p`1) || (the carrier of q`1)
by EC_PF_1:def 1;
C: [x1,y1] in [:the carrier of q`1,the carrier of q`1:]
by ZFMISC_1:def 2;
thus a + b = x1 + y1 by A,duf .= x + y by AS,A,B,C,FUNCT_1:49;
end;
end;
hence a + b = x + y;
consider q being Element of S, x1,y1 being Element of q`1 such that
A: x1 = a & y1 = b & unionMult(S,f,E).(a,b) = x1 * y1 by H,dum;
now per cases by dasc;
suppose p <= q;
then p`1 is Subfield of q`1 by FIELD_4:7; then
B: the multF of p`1 = (the multF of q`1) || (the carrier of p`1)
by EC_PF_1:def 1;
C: [x1,y1] in [:the carrier of p`1,the carrier of p`1:]
by AS,A,ZFMISC_1:def 2;
thus a * b = x1 * y1 by A,duf .= x * y by AS,A,B,C,FUNCT_1:49;
end;
suppose q <= p;
then q`1 is Subfield of p`1 by FIELD_4:7; then
B: the multF of q`1 = (the multF of p`1) || (the carrier of q`1)
by EC_PF_1:def 1;
C: [x1,y1] in [:the carrier of q`1,the carrier of q`1:]
by ZFMISC_1:def 2;
thus a * b = x1 * y1 by A,duf .= x * y by AS,A,B,C,FUNCT_1:49;
end;
end;
hence a * b = x * y;
end;
registration
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
cluster unionField(S,f,E) -> non degenerated;
coherence
proof
set p = the Element of S;
1.unionField(S,f,E) = 1.(p`1) & 0.unionField(S,f,E) = 0.(p`1) by lem5a;
hence thesis;
end;
end;
registration
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
cluster unionField(S,f,E) -> Abelian
add-associative right_zeroed right_complementable;
coherence
proof
set K = unionField(S,f,E);
hereby
let x,y be Element of K;
reconsider a = x, b = y as Element of unionCarrier(S,f,E) by duf;
consider p being Element of S, xi,yi being Element of p`1 such that
A: xi = a & yi = b & unionAdd(S,f,E).(a,b) = xi + yi by dua;
thus x + y = xi + yi by A,lem4a .= y + x by A,lem4a;
end;
hereby
let x,y,z be Element of K;
reconsider a = x, b = y, c = z, ab = x + y as
Element of unionCarrier(S,f,E) by duf;
consider p being Element of S, xi,yi being Element of p`1 such that
A: xi = a & yi = b & unionAdd(S,f,E).(a,b) = xi + yi by dua;
consider q being Element of S, xj,zj being Element of q`1 such that
B: xj = ab & zj = c & unionAdd(S,f,E).(ab,c) = xj + zj by dua;
per cases by dasc;
suppose q <= p;
then reconsider zi = zj as Element of p`1 by lem1a;
C: yi + zi = y + z by A,B,lem4a;
x + y = xi + yi by A,lem4a;
hence (x + y) + z = (xi + yi) + zi by B,lem4a
.= xi + (yi + zi) by RLVECT_1:def 3
.= x + (y + z) by A,C,lem4a;
end;
suppose p <= q;
then reconsider xj = xi, yj = yi as Element of q`1 by lem1a;
C: yj + zj = y + z by A,B,lem4a;
x + y = xj + yj by A,lem4a;
hence (x + y) + z = (xj + yj) + zj by B,lem4a
.= xj + (yj + zj) by RLVECT_1:def 3
.= x + (y + z) by A,C,lem4a;
end;
end;
hereby
let x be Element of K;
x is Element of unionCarrier(S,f,E) by duf; then
consider Y being set such that
A: x in Y & Y in the set of all the carrier of p`1 where p is Element of S
by TARSKI:def 4;
consider p being Element of S such that
B: Y = the carrier of p`1 by A;
reconsider a = x as Element of p`1 by A,B;
0.K = 0.(p`1) by lem5a;
hence x + 0.K = a + 0.(p`1) by lem4a .= x;
end;
let x be Element of K;
x is Element of unionCarrier(S,f,E) by duf; then
consider Y being set such that
A: x in Y & Y in the set of all the carrier of p`1 where p is Element of S
by TARSKI:def 4;
consider p being Element of S such that
B: Y = the carrier of p`1 by A;
reconsider a = x as Element of p`1 by A,B;
the carrier of p`1 in
the set of all the carrier of p`1 where p is Element of S; then
-a in unionCarrier(S,f,E) by TARSKI:def 4; then
reconsider y = -a as Element of K by duf;
take y;
thus x + y = a + -a by lem4a .= 0.(p`1) by RLVECT_1:5 .= 0.K by lem5a;
end;
end;
registration
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
cluster unionField(S,f,E) -> commutative associative well-unital distributive
almost_left_invertible;
coherence
proof
set K = unionField(S,f,E);
H: the carrier of K = unionCarrier(S,f,E) by duf;
A: now let x,y be Element of K;
reconsider a = x, b = y as Element of unionCarrier(S,f,E) by duf;
consider p being Element of S, xi,yi being Element of p`1 such that
A: xi = a & yi = b & unionMult(S,f,E).(a,b) = xi * yi by dum;
thus x * y = xi * yi by A,lem4a
.= yi * xi by GROUP_1:def 12 .= y * x by A,lem4a;
end;
hence K is commutative;
hereby
let x,y,z be Element of K;
reconsider a = x, b = y, c = z, ab = x * y as
Element of unionCarrier(S,f,E) by duf;
consider p being Element of S, xi,yi being Element of p`1 such that
A: xi = a & yi = b & unionMult(S,f,E).(a,b) = xi * yi by dum;
consider q being Element of S, xj,zj being Element of q`1 such that
B: xj = ab & zj = c & unionMult(S,f,E).(ab,c) = xj * zj by dum;
per cases by dasc;
suppose q <= p;
then reconsider zi = zj as Element of p`1 by lem1a;
C: yi * zi = y * z by A,B,lem4a;
x * y = xi * yi by A,lem4a;
hence (x * y) * z = (xi * yi) * zi by B,lem4a
.= xi * (yi * zi) by GROUP_1:def 3
.= x * (y * z) by A,C,lem4a;
end;
suppose p <= q;
then reconsider xj = xi, yj = yi as Element of q`1 by lem1a;
C: yj * zj = y * z by A,B,lem4a;
x * y = xj * yj by A,lem4a;
hence (x * y) * z = (xj * yj) * zj by B,lem4a
.= xj * (yj * zj) by GROUP_1:def 3
.= x * (y * z) by A,C,lem4a;
end;
end;
hereby let x be Element of K;
x is Element of unionCarrier(S,f,E) by duf; then
consider Y being set such that
A: x in Y & Y in the set of all the carrier of p`1 where p is Element of S
by TARSKI:def 4;
consider p being Element of S such that
B: Y = the carrier of p`1 by A;
reconsider a = x as Element of p`1 by A,B;
C: 1.K = 1.(p`1) by lem5a;
thus x * 1.K = a * 1.(p`1) by C,lem4a .= x;
thus 1.K * x = 1.(p`1) * a by C,lem4a .= x;
end;
hereby let x,y,z be Element of K;
reconsider a = x, b = y, c = z, bc = y + z as
Element of unionCarrier(S,f,E) by duf;
consider p being Element of S, yi,zi being Element of p`1 such that
B: yi = b & zi = c & unionAdd(S,f,E).(b,c) = yi + zi by dua;
consider q being Element of S, xj,pj being Element of q`1 such that
C: xj = a & pj = bc & unionMult(S,f,E).(a,bc) = xj * pj by dum;
thus Z: x * (y + z) = x * y + x * z
proof
per cases by dasc;
suppose q <= p;
then reconsider xi = xj as Element of p`1 by lem1a;
D: x * y = xi * yi & x * z = xi * zi by B,C,lem4a;
y + z = yi + zi by B,lem4a;
hence x * (y + z) = xi * (yi + zi) by C,lem4a
.= xi * yi + xi * zi by VECTSP_1:def 2
.= x * y + x * z by D,lem4a;
end;
suppose p <= q;
then reconsider yj = yi, zj = zi as Element of q`1 by lem1a;
D: x * y = xj * yj & x * z = xj * zj by B,C,lem4a;
y + z = yj + zj by B,lem4a;
hence x * (y + z) = xj * (yj + zj) by C,lem4a
.= xj * yj + xj * zj by VECTSP_1:def 2
.= x * y + x * z by D,lem4a;
end;
end;
thus (y + z) * x = x * y + x * z by A,Z
.= x * y + z * x by A
.= y * x + z * x by A;
end;
let x be Element of K such that J: x <> 0.K;
x is Element of unionCarrier(S,f,E) by duf; then
consider Y being set such that
A: x in Y & Y in the set of all the carrier of p`1 where p is Element of S
by TARSKI:def 4;
consider p being Element of S such that
B: Y = the carrier of p`1 by A;
reconsider a = x as Element of p`1 by A,B;
the carrier of p`1 in
the set of all the carrier of p`1 where p is Element of S; then
reconsider y = a" as Element of K by H,TARSKI:def 4;
C: a <> 0.(p`1) by J,lem5a;
take y;
thus y * x = a" * a by lem4a .= 1.(p`1) by C,VECTSP_1:def 10 .= 1.K by lem5a;
end;
end;
theorem Fsubb:
for F being Field, E being FieldExtension of F,
L be F-monomorphic Field
for f being Monomorphism of F,L
for S being ascending non empty Subset of Ext_Set(f,E)
for p being Element of S
holds p`1 is Subfield of unionField(S,f,E)
proof
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
let p be Element of S;
set K = unionField(S,f,E);
H: the carrier of K = unionCarrier(S,f,E) by duf
.= union(the set of all the carrier of p`1 where p is Element of S);
J: the carrier of p`1 in
the set of all the carrier of p`1 where p is Element of S; then
A: the carrier of p`1 c= the carrier of K by H,ZFMISC_1:74;
B: the addF of p`1 = (the addF of K) || the carrier of p`1
proof
set aF = the addF of p`1, aK = (the addF of K) || the carrier of p`1;
B1: dom aK
= dom(the addF of K) /\ [:the carrier of p`1,the carrier of p`1:]
by RELAT_1:61
.= [:the carrier of K,the carrier of K:] /\
[:the carrier of p`1,the carrier of p`1:] by FUNCT_2:def 1
.= [:the carrier of p`1,the carrier of p`1:] by A,ZFMISC_1:96,XBOOLE_1:28;
now let x be object;
assume B2: x in dom aF; then
consider a,b being object such that
B3: a in the carrier of p`1 & b in the carrier of p`1 & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of p`1 by B3;
reconsider y = a, z = b as Element of K by A;
thus aF.x = a + b by B3
.= y + z by lem4a
.= aK.x by B3,B2,FUNCT_1:49;
end;
hence thesis by B1,FUNCT_2:def 1;
end;
C: the multF of p`1 = (the multF of K) || the carrier of p`1
proof
set mF = the multF of p`1, mK = (the multF of K) || the carrier of p`1;
B1: dom mK
= dom(the multF of K) /\ [:the carrier of p`1,the carrier of p`1:]
by RELAT_1:61
.= [:the carrier of K,the carrier of K:] /\
[:the carrier of p`1,the carrier of p`1:] by FUNCT_2:def 1
.= [:the carrier of p`1,the carrier of p`1:] by A,ZFMISC_1:96,XBOOLE_1:28;
now let x be object;
assume B2: x in dom mF; then
consider a,b being object such that
B3: a in the carrier of p`1 & b in the carrier of p`1 & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of p`1 by B3;
reconsider y = a, z = b as Element of K by A;
thus mF.x = a * b by B3
.= y * z by lem4a
.= mK.x by B3,B2,FUNCT_1:49;
end;
hence thesis by B1,FUNCT_2:def 1;
end;
1.(p`1) = 1.K & 0.K = 0.(p`1) by lem5a;
hence thesis by H,J,ZFMISC_1:74,B,C,EC_PF_1:def 1;
end;
theorem Fsuba:
for F being Field, E being FieldExtension of F,
L be F-monomorphic Field
for f being Monomorphism of F,L
for S being ascending non empty Subset of Ext_Set(f,E)
holds F is Subfield of unionField(S,f,E)
proof
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
set p = the Element of S;
A2: F is Subfield of p`1 by FIELD_4:7;
p`1 is Subfield of unionField(S,f,E) by Fsubb;
hence thesis by A2,EC_PF_1:5;
end;
theorem inSa:
for F being Field, E being FieldExtension of F,
L be F-monomorphic Field
for f being Monomorphism of F,L
for S being ascending non empty Subset of Ext_Set(f,E)
holds unionField(S,f,E) is Subfield of E
proof
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
set K = unionField(S,f,E);
H: the carrier of K = unionCarrier(S,f,E) by duf
.= union(the set of all the carrier of p`1 where p is Element of S);
A: the carrier of K c= the carrier of E
proof
now let o be object;
assume o in the carrier of K; then
consider Y being set such that
A1: o in Y &
Y in the set of all the carrier of p`1 where p is Element of S
by H,TARSKI:def 4;
consider p being Element of S such that
A2: Y = the carrier of p`1 by A1;
p in Ext_Set(f,E); then
consider K be Element of SubFields(E), g be Function of K,L such that
A3: p = [K,g] &
ex K1 being FieldExtension of F, g1 being Function of K1,L
st K1 = K & g1 = g & g1 is monomorphism f-extending;
p`1 is Subfield of E by A3,subfie; then
the carrier of p`1 c= the carrier of E by EC_PF_1:def 1;
hence o in the carrier of E by A1,A2;
end;
hence thesis;
end;
B: the addF of K = (the addF of E) || the carrier of K
proof
set aF = the addF of K, aK = (the addF of E) || the carrier of K;
B1: dom aK
= dom(the addF of E) /\
[:the carrier of K,the carrier of K:] by RELAT_1:61
.= [:the carrier of E,the carrier of E:] /\
[:the carrier of K,the carrier of K:] by FUNCT_2:def 1
.= [:the carrier of K,the carrier of K:] by A,XBOOLE_1:28,ZFMISC_1:96
.= dom aF by FUNCT_2:def 1;
now let x be object;
assume x in dom aF; then
consider a,b being object such that
B3: a in the carrier of K & b in the carrier of K & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of K by B3;
consider Y1 being set such that
C1: a in Y1 &
Y1 in the set of all the carrier of p`1 where p is Element of S
by H,TARSKI:def 4;
consider pa being Element of S such that
B4: Y1 = the carrier of pa`1 by C1;
consider Y2 being set such that
C2: b in Y2 &
Y2 in the set of all the carrier of p`1 where p is Element of S
by H,TARSKI:def 4;
consider pb being Element of S such that
B5: Y2 = the carrier of pb`1 by C2;
pa in Ext_Set(f,E); then
consider U be Element of SubFields(E), g be Function of U,L such that
A3: pa = [U,g] &
ex K1 being FieldExtension of F, g1 being Function of K1,L
st K1 = U & g1 = g & g1 is monomorphism f-extending;
AS1: pa`1 is Subfield of E by A3,subfie;
pb in Ext_Set(f,E); then
consider U be Element of SubFields(E), g be Function of U,L such that
A3: pb = [U,g] &
ex K1 being FieldExtension of F, g1 being Function of K1,L
st K1 = U & g1 = g & g1 is monomorphism f-extending;
AS2: pb`1 is Subfield of E by A3,subfie;
per cases by dasc;
suppose pa <= pb; then
reconsider a1 = a, b1 = b as Element of pb`1 by C1,C2,B4,B5,lem1a;
B4: the addF of pb`1 = (the addF of E) || the carrier of (pb`1)
by AS2,EC_PF_1:def 1;
B5: [a1,b1] in [:the carrier of pb`1,the carrier of pb`1:]
by ZFMISC_1:def 2;
B6: [a,b] in [:the carrier of K,the carrier of K:] by ZFMISC_1:def 2;
thus aF.x
= a + b by B3
.= a1 + b1 by lem4a
.= (the addF of E).(a,b) by B4,B5,FUNCT_1:49
.= aK.x by B3,B6,FUNCT_1:49;
end;
suppose pb <= pa; then
reconsider a1 = a, b1 = b as Element of pa`1 by C1,C2,B4,B5,lem1a;
B4: the addF of pa`1 = (the addF of E) || the carrier of (pa`1)
by AS1,EC_PF_1:def 1;
B5: [a1,b1] in [:the carrier of pa`1,the carrier of pa`1:]
by ZFMISC_1:def 2;
B6: [a1,b1] in [:the carrier of K,the carrier of K:]
by ZFMISC_1:def 2;
thus aF.x
= a + b by B3
.= a1 + b1 by lem4a
.= (the addF of E).(a1,b1) by B4,B5,FUNCT_1:49
.= aK.x by B3,B6,FUNCT_1:49;
end;
end;
hence thesis by B1;
end;
C: the multF of K = (the multF of E) || the carrier of K
proof
set aF = the multF of K, aK = (the multF of E) || the carrier of K;
B1: dom aK
= dom(the multF of E) /\
[:the carrier of K,the carrier of K:] by RELAT_1:61
.= [:the carrier of E,the carrier of E:] /\
[:the carrier of K,the carrier of K:] by FUNCT_2:def 1
.= [:the carrier of K,the carrier of K:] by A,XBOOLE_1:28,ZFMISC_1:96
.= dom aF by FUNCT_2:def 1;
now let x be object;
assume x in dom aF; then
consider a,b being object such that
B3: a in the carrier of K & b in the carrier of K & x = [a,b]
by ZFMISC_1:def 2;
reconsider a,b as Element of K by B3;
consider Y1 being set such that
C1: a in Y1 &
Y1 in the set of all the carrier of p`1 where p is Element of S
by H,TARSKI:def 4;
consider pa being Element of S such that
B4: Y1 = the carrier of pa`1 by C1;
consider Y2 being set such that
C2: b in Y2 &
Y2 in the set of all the carrier of p`1 where p is Element of S
by H,TARSKI:def 4;
consider pb being Element of S such that
B5: Y2 = the carrier of pb`1 by C2;
pa in Ext_Set(f,E); then
consider U be Element of SubFields(E), g be Function of U,L such that
A3: pa = [U,g] &
ex K1 being FieldExtension of F, g1 being Function of K1,L
st K1 = U & g1 = g & g1 is monomorphism f-extending;
AS1: pa`1 is Subfield of E by A3,subfie;
pb in Ext_Set(f,E); then
consider U be Element of SubFields(E), g be Function of U,L such that
A3: pb = [U,g] &
ex K1 being FieldExtension of F, g1 being Function of K1,L
st K1 = U & g1 = g & g1 is monomorphism f-extending;
AS2: pb`1 is Subfield of E by A3,subfie;
per cases by dasc;
suppose pa <= pb; then
reconsider a1 = a, b1 = b as Element of pb`1 by C1,C2,B4,B5,lem1a;
B4: the multF of pb`1 = (the multF of E) || the carrier of (pb`1)
by AS2,EC_PF_1:def 1;
B5: [a1,b1] in [:the carrier of pb`1,the carrier of pb`1:]
by ZFMISC_1:def 2;
B6: [a,b] in [:the carrier of K,the carrier of K:]
by ZFMISC_1:def 2;
thus aF.x
= a * b by B3
.= a1 * b1 by lem4a
.= (the multF of E).(a,b) by B4,B5,FUNCT_1:49
.= aK.x by B3,B6,FUNCT_1:49;
end;
suppose pb <= pa; then
reconsider a1 = a, b1 = b as Element of pa`1 by C1,C2,B4,B5,lem1a;
B4: the multF of pa`1 = (the multF of E) || the carrier of (pa`1)
by AS1,EC_PF_1:def 1;
B5: [a1,b1] in [:the carrier of pa`1,the carrier of pa`1:]
by ZFMISC_1:def 2;
B6: [a1,b1] in [:the carrier of K,the carrier of K:]
by ZFMISC_1:def 2;
thus aF.x
= a * b by B3
.= a1 * b1 by lem4a
.= (the multF of E).(a1,b1) by B4,B5,FUNCT_1:49
.= aK.x by B3,B6,FUNCT_1:49;
end;
end;
hence thesis by B1;
end;
set p = the Element of S;
p in Ext_Set(f,E); then
consider U be Element of SubFields(E), g be Function of U,L such that
A3: p = [U,g] &
ex K1 being FieldExtension of F, g1 being Function of K1,L
st K1 = U & g1 = g & g1 is monomorphism f-extending;
AS3: p`1 is Subfield of E by A3,subfie;
D: 1.K = 1.(p`1) by lem5a .= 1.E by AS3,EC_PF_1:def 1;
0.K = 0.(p`1) by lem5a .= 0.E by AS3,EC_PF_1:def 1;
hence thesis by A,B,C,D,EC_PF_1:def 1;
end;
registration
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
cluster unionField(S,f,E) -> F-extending;
coherence
proof
F is Subfield of unionField(S,f,E) by Fsuba;
hence thesis by FIELD_4:7;
end;
end;
definition
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
func unionExt(S,f,E) -> Function of unionField(S,f,E),L means :dufe:
for p being Element of S holds it|(the carrier of (p`1)) = p`2;
existence
proof
set K = unionField(S,f,E);
H: the carrier of K = unionCarrier(S,f,E) by duf
.= union(the set of all the carrier of p`1 where p is Element of S);
defpred P[object,object] means
ex p being Element of S st $1 is Element of p`1 & $2 = (p`2).$1;
A: now let x be object;
assume x in the carrier of K; then
consider Y being set such that
A1: x in Y &
Y in the set of all the carrier of p`1 where p is Element of S
by H,TARSKI:def 4;
consider p being Element of S such that
A2: Y = the carrier of p`1 by A1;
reconsider a = x as Element of p`1 by A1,A2;
thus ex y being object st y in the carrier of L & P[x,y]
proof
take b = (p`2).a;
thus thesis;
end;
end;
consider g being Function of the carrier of K, the carrier of L such that
B: for x being object st x in the carrier of K holds P[x,g.x]
from FUNCT_2:sch 1(A);
take g;
now let p be Element of S;
p`1 is Subfield of K by Fsubb; then
I: the carrier of p`1 c= the carrier of K by EC_PF_1:def 1;
B0: dom g /\ (the carrier of p`1)
= (the carrier of K) /\ (the carrier of p`1) by FUNCT_2:def 1
.= the carrier of p`1 by I,XBOOLE_1:28
.= dom p`2 by FUNCT_2:def 1;
now let o be object;
assume J: o in dom(p`2); then
consider q being Element of S such that
B1: o is Element of q`1 & g.o = (q`2).o by B,I;
per cases by dasc;
suppose p <= q;
hence (p`2).o = g.o by B1,J,FIELD_8:def 6;
end;
suppose q <= p;
hence (p`2).o = g.o by B1,FIELD_8:def 6;
end;
end;
hence g|(the carrier of (p`1)) = p`2 by B0,FUNCT_1:46;
end;
hence thesis;
end;
uniqueness
proof
let g1,g2 be Function of unionField(S,f,E),L;
assume AS:
(for p being Element of S holds g1|(the carrier of (p`1)) = p`2) &
(for p being Element of S holds g2|(the carrier of (p`1)) = p`2);
set K = unionField(S,f,E);
H: the carrier of K = unionCarrier(S,f,E) by duf
.= union(the set of all the carrier of p`1 where p is Element of S);
now let o be object;
assume o in the carrier of unionField(S,f,E); then
reconsider a = o as Element of K;
consider Y1 being set such that
A1: a in Y1 &
Y1 in the set of all the carrier of p`1 where p is Element of S
by H,TARSKI:def 4;
consider p being Element of S such that
A2: Y1 = the carrier of p`1 by A1;
reconsider a as Element of p`1 by A1,A2;
g1.a = (g1|(the carrier of p`1)).a by FUNCT_1:49
.= (p`2).a by AS
.= (g2|(the carrier of p`1)).a by AS
.= g2.a by FUNCT_1:49;
hence g1.o = g2.o;
end;
hence g1 = g2;
end;
end;
theorem inSb:
for F being Field, E being FieldExtension of F,
L be F-monomorphic Field
for f being Monomorphism of F,L
for S being ascending non empty Subset of Ext_Set(f,E)
holds unionExt(S,f,E) is monomorphism f-extending
proof
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
set K = unionField(S,f,E), h = unionExt(S,f,E);
set p = the Element of S;
H: the carrier of K = unionCarrier(S,f,E) by duf;
p in Ext_Set(f,E); then
consider U be Element of SubFields(E), g be Function of U,L such that
A3: p = [U,g] &
ex K1 being FieldExtension of F, g1 being Function of K1,L
st K1 = U & g1 = g & g1 is monomorphism f-extending;
consider K1 being FieldExtension of F, g1 being Function of K1,L such that
A4: K1 = U & g1 = g & g1 is monomorphism f-extending by A3;
AS3: p`1 = U by A3;
AS4: p`2 = g by A3;
D: 1.K = 1.K1 by A4,AS3,lem5a;
F: h|(the carrier of K1) = g by A4,AS4,dufe;
E: g is additive multiplicative unity-preserving by A4;
A: now let a,b be Element of K;
consider p being Element of S, x,y being Element of p`1 such that
A1: x = a & y = b & unionAdd(S,f,E).(a,b) = x + y by H,dua;
A2: h|(the carrier of p`1) = p`2 by dufe; then
A3: h.a = (p`2).x & h.b = (p`2).y by A1,FUNCT_1:49;
p in Ext_Set(f,E); then
consider U be Element of SubFields(E), g2 be Function of U,L such that
A7: p = [U,g2] &
ex K1 being FieldExtension of F, g1 being Function of K1,L
st K1 = U & g1 = g2 & g1 is monomorphism f-extending;
A4: p`2 is additive by A7;
A5: x + y = a + b by A1,duf;
thus h.a + h.b
= (p`2).(x + y) by A4,A3
.= h.(a + b) by A2,A5,FUNCT_1:49;
end;
B: now let a,b be Element of K;
consider p being Element of S, x,y being Element of p`1 such that
A1: x = a & y = b & unionMult(S,f,E).(a,b) = x * y by H,dum;
A2: h|(the carrier of p`1) = p`2 by dufe; then
A3: h.a = (p`2).x & h.b = (p`2).y by A1,FUNCT_1:49;
p in Ext_Set(f,E); then
consider U be Element of SubFields(E), g2 be Function of U,L such that
A7: p = [U,g2] &
ex K1 being FieldExtension of F, g1 being Function of K1,L
st K1 = U & g1 = g2 & g1 is monomorphism f-extending;
A4: p`2 is multiplicative by A7;
A5: x * y = a * b by A1,duf;
thus h.a * h.b
= (p`2).(x * y) by A4,A3
.= h.(a * b) by A2,A5,FUNCT_1:49;
end;
h is additive multiplicative unity-preserving by A,B,E,A4,D,F,FUNCT_1:49;
hence h is monomorphism;
set p = the Element of S;
p in Ext_Set(f,E); then
consider U be Element of SubFields(E), g be Function of U,L such that
A3: p = [U,g] &
ex K1 being FieldExtension of F, g1 being Function of K1,L
st K1 = U & g1 = g & g1 is monomorphism f-extending;
consider K1 being FieldExtension of F, g1 being Function of K1,L such that
A4: K1 = U & g1 = g & g1 is monomorphism f-extending by A3;
reconsider L1 = L as L-extending FieldExtension of L by FIELD_4:6;
p`1 is Subfield of K by Fsubb; then
reconsider K as K1-extending FieldExtension of F by A3,A4,FIELD_4:7;
reconsider h as Function of K,L1;
A7: p`2 = g1 by A3,A4;
now let a be Element of K1;
h|(the carrier of K1) = g1 by A7,dufe;
hence g1.a = h.a by FUNCT_1:49;
end;
then h is g1-extending;
hence thesis by A4,FIELD_8:41;
end;
definition
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
func upper_bound S -> Element of Ext_Set(f,E) equals
[ unionField(S,f,E), unionExt(S,f,E) ];
coherence
proof
set K = unionField(S,f,E), g = unionExt(S,f,E);
A: g is monomorphism by inSb;
K is Subfield of E by inSa; then
B: E is FieldExtension of K by FIELD_4:7;
C: F is Subfield of K by FIELD_4:7;
g is f-extending by inSb;
hence thesis by A,B,C,inS;
end;
end;
theorem up:
for F being Field, E being FieldExtension of F,
L being F-monomorphic Field,
f being Monomorphism of F,L
for S being ascending non empty Subset of Ext_Set(f,E)
for p being Element of S holds p <= upper_bound S
proof
let F be Field, E be FieldExtension of F;
let L be F-monomorphic Field;
let f be Monomorphism of F,L;
let S be ascending non empty Subset of Ext_Set(f,E);
let p be Element of S;
set q = upper_bound S, K = unionField(S,f,E), h = unionExt(S,f,E);
C: p`1 is Subfield of K by Fsubb;
now let K1 be FieldExtension of p`1, g1 be Function of K1,L;
assume K1 = q`1 & g1 = q`2; then
g1|(the carrier of p`1) = p`2 by dufe;
hence g1 is (p`2)-extending by FUNCT_1:49;
end;
hence thesis by C,FIELD_4:7;
end;
theorem lift1:
for F being Field,
E being FieldExtension of F
for a being F-algebraic Element of E
for L being F-monomorphic algebraic-closed Field,
f being Monomorphism of F,L
ex g being Function of FAdj(F,{a}),L st g is monomorphism f-extending
proof
let F be Field, E be FieldExtension of F, a be F-algebraic Element of E;
let L be F-monomorphic algebraic-closed Field;
let f be Monomorphism of F,L;
per cases;
suppose a in F; then
{a} c= the carrier of F by TARSKI:def 1; then
I: the doubleLoopStr of FAdj(F,{a}) = the doubleLoopStr of F
by FIELD_7:3,FIELD_7:def 1; then
reconsider f1 = f as Function of FAdj(F,{a}),L;
take f1;
f1 is additive multiplicative unity-preserving
proof
now let x,y be Element of FAdj(F,{a});
reconsider x1 = x, y1 = y as Element of F by I;
x + y = x1 + y1 by I;
hence f1.(x+y) = f1.x + f1.y by VECTSP_1:def 20;
end;
hence f1 is additive;
now let x,y be Element of FAdj(F,{a});
reconsider x1 = x, y1 = y as Element of F by I;
x * y = x1 * y1 by I;
hence f1.(x*y) = f1.x * f1.y by GROUP_6:def 6;
end;
hence f1 is multiplicative;
1_FAdj(F,{a}) = 1_F by I;
hence thesis by GROUP_1:def 13;
end;
hence thesis;
end;
suppose not a in F;
reconsider L1 = L as F-homomorphic F-monomorphic FieldExtension of L
by FIELD_4:6;
reconsider f1 = f as Monomorphism of F,L1;
reconsider p = MinPoly(a,F) as Element of the carrier of Polynom-Ring F;
reconsider q = (PolyHom f1).p as Polynomial of L;
deg q >= 0; then
reconsider q as non constant Polynomial of L by RATFUNC1:def 2,RING_4:def 4;
consider b being Element of L such that
A0: b is_a_root_of q by POLYNOM5:def 8;
eval(q,b) = 0.L by A0,POLYNOM5:def 7; then
B0: Ext_eval(q,b) = 0.L1 by FIELD_6:10; then
reconsider b as L-algebraic Element of L1 by FIELD_6:43;
H: FAdj(F,{a}) = RAdj(F,{a}) by FIELD_6:56;
set M = { [Ext_eval(p,a),Ext_eval(q,b)] where
p is (Polynomial of F), q is Polynomial of L : q = (PolyHom f1).p};
now let o be object;
assume o in M; then
consider p being (Polynomial of F), q being Polynomial of L such that
A: o = [Ext_eval(p,a),Ext_eval(q,b)] & q = (PolyHom f1).p;
Ext_eval(p,a) in the set of all Ext_eval(p,a) where p is Polynomial of F;
then B: Ext_eval(p,a) in the carrier of FAdj(F,{a}) by H,FIELD_6:45;
thus o in [:the carrier of FAdj(F,{a}),the carrier of L:]
by A,B,ZFMISC_1:def 2;
end;
then M c= [:the carrier of FAdj(F,{a}),the carrier of L:];
then reconsider M as Relation of the carrier of FAdj(F,{a}),the carrier of L;
now let x,y1,y2 be object;
assume A1: [x,y1] in M & [x,y2] in M; then
consider p1 being (Polynomial of F), q1 being Polynomial of L such that
A2: [x,y1] = [Ext_eval(p1,a),Ext_eval(q1,b)] & q1 = (PolyHom f1).p1;
A3: x = Ext_eval(p1,a) & y1 = Ext_eval(q1,b) by A2,XTUPLE_0:1;
consider p2 being (Polynomial of F), q2 being Polynomial of L such that
A4: [x,y2] = [Ext_eval(p2,a),Ext_eval(q2,b)] & q2 = (PolyHom f1).p2 by A1;
A5: x = Ext_eval(p2,a) & y2 = Ext_eval(q2,b) by A4,XTUPLE_0:1;
Ext_eval(p1,a) = Ext_eval(p2,a) by A2,XTUPLE_0:1,A5; then
A6: 0.E = Ext_eval(p1,a) - Ext_eval(p2,a) by RLVECT_1:15
.= Ext_eval(p1-p2,a) by FIELD_6:27;
reconsider pm = p1 - p2 as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
A7: (PolyHom f1).p divides (PolyHom f1).pm by A6,FIELD_6:53,F814;
A8: Ext_eval(q1-q2,b) = 0.L
proof
reconsider u = (PolyHom f1).p as Polynomial of L;
consider v being Polynomial of L such that
V: u *' v = (PolyHom f1).pm by A7,RING_4:1;
reconsider p1a = p1, p2a = p2 as
Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
-p2 = -p2a by FIELD_8:1; then
Z: p1 - p2 = p1a - p2a by POLYNOM3:def 10;
Y: -q2 = -(PolyHom f1).p2a by A4,FIELD_8:1;
X: q1-q2
= (PolyHom f1).p1a + -(PolyHom f1).p2a by Y,A2,POLYNOM3:def 10
.= (PolyHom f1).p1a + (PolyHom f1).(-p2a) by F815
.= (PolyHom f1).pm by Z,FIELD_1:24;
L is Subfield of L1 by FIELD_4:7; then
W: L is Subring of L1 by FIELD_5:12;
Ext_eval((PolyHom f1).pm,b)
= (0.L1) * Ext_eval(v,b) by B0,V,W,ALGNUM_1:20;
hence thesis by X;
end;
0.L = Ext_eval(q1,b) - Ext_eval(q2,b) by A8,FIELD_6:27;
hence y1 = y2 by A5,A3,RLVECT_1:21;
end; then
reconsider g = M as Function by FUNCT_1:def 1;
A1: for o being object st o in dom M holds o in the carrier of FAdj(F,{a});
now let o be object;
assume o in the carrier of FAdj(F,{a}); then
o in the set of all Ext_eval(p,a) where p is Polynomial of F
by H,FIELD_6:45; then
consider p being Polynomial of F such that A: o = Ext_eval(p,a);
ex y being object st [o,y] in g
proof
reconsider p1 = p as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
reconsider q = (PolyHom f1).p1 as Polynomial of L;
take y = Ext_eval(q,b);
thus thesis by A;
end;
hence o in dom g by XTUPLE_0:def 12;
end; then
A2: dom g = the carrier of FAdj(F,{a}) by A1,TARSKI:2;
rng M is Subset of the carrier of L; then
reconsider g as Function of the carrier of FAdj(F,{a}),the carrier of L
by A2,FUNCT_2:2;
U: for p being (Polynomial of F), q being Polynomial of L
st q = (PolyHom f1).p holds g.Ext_eval(p,a) = Ext_eval(q,b)
proof
let p be (Polynomial of F), q be Polynomial of L;
assume q = (PolyHom f1).p; then
[Ext_eval(p,a),Ext_eval(q,b)] in g;
hence thesis by FUNCT_1:1;
end;
take g;
I4: L is Subring of L1 by FIELD_4:def 1;
C1: now let x,y be Element of FAdj(F,{a});
x in the carrier of FAdj(F,{a}); then
x in the set of all Ext_eval(p,a) where p is Polynomial of F
by H,FIELD_6:45; then
consider p being Polynomial of F such that A1: x = Ext_eval(p,a);
y in the carrier of FAdj(F,{a}); then
y in the set of all Ext_eval(p,a) where p is Polynomial of F
by H,FIELD_6:45; then
consider q being Polynomial of F such that A2: y = Ext_eval(q,a);
reconsider pF = p, qF = q as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
reconsider f1p = (PolyHom f1).pF,f1q = (PolyHom f1).qF as Polynomial of L;
B: g.x = Ext_eval(f1p,b) & g.y = Ext_eval(f1q,b) by A1,A2,U;
D: x + y = Ext_eval(p+q,a) by A1,A2,FIELD_8:47;
reconsider pqF = p + q as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
reconsider f1pq = (PolyHom f1).(pF+qF) as Polynomial of L;
E: (PolyHom f1).(pF+qF)
= (PolyHom f1).pF + (PolyHom f1).qF by FIELD_1:24
.= f1p + f1q by POLYNOM3:def 10;
F: p + q = pF + qF by POLYNOM3:def 10;
thus g.(x+y) = Ext_eval(f1p+f1q,b) by D,U,E,F
.= g.x + g.y by B,I4,ALGNUM_1:15;
end;
C2: now let x,y be Element of FAdj(F,{a});
x in the carrier of FAdj(F,{a}); then
x in the set of all Ext_eval(p,a) where p is Polynomial of F
by H,FIELD_6:45; then
consider p being Polynomial of F such that A1: x = Ext_eval(p,a);
y in the carrier of FAdj(F,{a}); then
y in the set of all Ext_eval(p,a) where p is Polynomial of F
by H,FIELD_6:45; then
consider q being Polynomial of F such that A2: y = Ext_eval(q,a);
reconsider pF = p, qF = q as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
reconsider f1p = (PolyHom f1).pF,f1q = (PolyHom f1).qF as Polynomial of L;
B: g.x = Ext_eval(f1p,b) & g.y = Ext_eval(f1q,b) by A1,A2,U;
D: x * y = Ext_eval(p*'q,a) by A1,A2,FIELD_8:47;
reconsider pqF = p *' q as Element of the carrier of Polynom-Ring F
by POLYNOM3:def 10;
reconsider f1pq = (PolyHom f1).(pF*qF) as Polynomial of L;
E: (PolyHom f1).(pF*qF)
= (PolyHom f1).pF * (PolyHom f1).qF by FIELD_1:25
.= f1p *' f1q by POLYNOM3:def 10;
F: p *' q = pF * qF by POLYNOM3:def 10;
thus g.(x*y) = Ext_eval(f1p*'f1q,b) by D,U,E,F
.= g.x * g.y by B,I4,ALGNUM_1:20;
end;
C3: g.(1_FAdj(F,{a})) = 1_L1
proof
reconsider g1 = (1.F)|F as
Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
reconsider q = (1.L)|L as
Element of the carrier of Polynom-Ring L by POLYNOM3:def 10;
F: f.(1_F) = 1_L by GROUP_1:def 13;
1.FAdj(F,{a}) = Ext_eval(1_.F,a) by FIELD_8:46
.= Ext_eval(g1,a) by RING_4:14; then
g.(1.FAdj(F,{a}))
= Ext_eval((PolyHom f1).g1,b) by U
.= Ext_eval(q,b) by F,FIELD_8:13
.= LC((1.L)|L) by FIELD_6:28
.= 1.L1 by FIELD_8:3;
hence thesis;
end;
C: g is additive multiplicative unity-preserving by C1,C2,C3;
now let x be Element of F;
reconsider g1 = x|F as
Element of the carrier of Polynom-Ring F by POLYNOM3:def 10;
x = Ext_eval(x|F,a) by FIELD_8:48;
hence g.x = Ext_eval((PolyHom f1).g1,b) by U
.= Ext_eval((f.x)|L,b) by FIELD_8:13
.= LC((f.x)|L) by FIELD_6:28
.= f.x by FIELD_8:3;
end;
hence thesis by C;
end;
end;
theorem lift2:
for F being Field,
E being F-algebraic FieldExtension of F
for L being F-monomorphic algebraic-closed Field,
f being Monomorphism of F,L
ex g being Function of E,L st g is monomorphism f-extending
proof
let F be Field, E be F-algebraic FieldExtension of F;
let L be F-monomorphic algebraic-closed Field, f be Monomorphism of F,L;
set S = Ext_Set(f,E);
set R = { [p,q] where p,q is Element of S : p <= q };
now let o be object;
assume o in R;
then consider p,q being Element of S such that
A: o = [p,q] & p <= q;
thus ex y,z being object st o = [y,z] by A;
end; then
reconsider R as Relation by RELAT_1:def 1;
B: field R = S
proof
B1: now let o be object;
assume o in field R; then
o in dom R \/ rng R by RELAT_1:def 6; then
per cases by XBOOLE_0:def 3;
suppose o in dom R; then
consider y being object such that
B2: [o,y] in R by XTUPLE_0:def 12;
consider p,q being Element of S such that
B3: [o,y] = [p,q] & p <= q by B2;
o = p by B3,XTUPLE_0:1;
hence o in S;
end;
suppose o in rng R; then
consider y being object such that
B2: [y,o] in R by XTUPLE_0:def 13;
consider p,q being Element of S such that
B3: [y,o] = [p,q] & p <= q by B2;
o = q by B3,XTUPLE_0:1;
hence o in S;
end;
end;
now let o be object;
assume o in S;
then reconsider p = o as Element of S;
p <= p by po1;
then [p,p] in R;
then o in dom R by XTUPLE_0:def 12;
then o in dom R \/ rng R by XBOOLE_0:def 3;
hence o in field R by RELAT_1:def 6;
end;
hence thesis by B1,TARSKI:2;
end;
I1: R is_reflexive_in field R
proof
now let x be object;
assume x in field R;
then reconsider p = x as Element of S by B;
p <= p by po1;
hence [x,x] in R;
end;
hence thesis by RELAT_2:def 1;
end;
I2: R is_transitive_in field R
proof
now let x,y,z be object;
assume I3: x in field R & y in field R & z in field R &
[x,y] in R & [y,z] in R; then
consider p,q being Element of S such that
I4: [p,q] = [x,y] & p <= q;
consider q1,r being Element of S such that
I5: [q1,r] = [y,z] & q1 <= r by I3;
I6: p = x & q = y & q1 = y & r = z by I4,I5,XTUPLE_0:1;
then p <= r by I4,I5,po3;
hence [x,z] in R by I6;
end;
hence thesis by RELAT_2:def 8;
end;
I3: R is_antisymmetric_in field R
proof
now let x,y be object;
assume I3: x in field R & y in field R &
[x,y] in R & [y,x] in R; then
consider p,q being Element of S such that
I4: [p,q] = [x,y] & p <= q;
consider q1,p1 being Element of S such that
I5: [q1,p1] = [y,x] & q1 <= p1 by I3;
p = x & q = y & q1 = y & p1 = x by I4,I5,XTUPLE_0:1;
hence x = y by I4,I5,po2;
end;
hence thesis by RELAT_2:def 4;
end; then
reconsider R as reflexive transitive antisymmetric Relation
by I1,I2,RELAT_2:def 9,RELAT_2:def 16,RELAT_2:def 12;
A: R partially_orders S by I1,I2,I3,B;
now let Y be set;
assume C1: Y c= S & R|_2 Y is being_linear-order;
per cases;
suppose C2: Y is empty;
set p = the Element of S;
thus ex x being set
st x in S & for y being set st y in Y holds [y,x] in R
proof
take p;
thus thesis by C2;
end;
end;
suppose Y is non empty; then
reconsider Y1 = Y as non empty Subset of S by C1;
set O = R|_2 Y;
I: O = R /\ [:Y,Y:] by WELLORD1:def 6;
C3: field O = Y by C1,B,ORDERS_1:71;
now let p,q be Element of Y1;
per cases;
suppose p = q;
hence p <= q or q <= p by po1;
end;
suppose p <> q; then
[p,q] in O or [q,p] in O by C3,C1,RELAT_2:def 14,RELAT_2:def 6; then
per cases by I,XBOOLE_0:def 4;
suppose [p,q] in R;
then consider p1,q1 being Element of S such that
C7: [p1,q1] = [p,q] & p1 <= q1;
p1 = p & q1 = q by C7,XTUPLE_0:1;
hence p <= q or q <= p by C7;
end;
suppose [q,p] in R;
then consider q1,p1 being Element of S such that
C7: [q1,p1] = [q,p] & q1 <= p1;
p1 = p & q1 = q by C7,XTUPLE_0:1;
hence p <= q or q <= p by C7;
end;
end;
end;
then reconsider Y1 as ascending non empty Subset of S by dasc;
thus ex x being set st x in S & for y being set st y in Y holds [y,x] in R
proof
take p = upper_bound Y1;
thus p in S;
now let y be set;
assume y in Y;
then reconsider q = y as Element of Y1;
q <= p by up;
hence [y,p] in R;
end;
hence thesis;
end;
end;
end;
then S has_upper_Zorn_property_wrt R;
then consider U being set such that Z: U is_maximal_in R by A,B,ORDERS_1:63;
reconsider U as Element of S by Z,B;
U in Ext_Set(f,E); then
consider W be Element of SubFields(E), h be Function of W,L such that
H1: U = [W,h] &
ex W1 being FieldExtension of F, h1 being Function of W1,L
st W1 = W & h1 = h & h1 is monomorphism f-extending;
consider W1 be FieldExtension of F, h1 be Function of W1,L such that
H2: W1 = W & h1 = h & h1 is monomorphism f-extending by H1;
reconsider W as FieldExtension of F by H2;
I1: W is Subfield of E by subfie; then
I2: the carrier of W c= the carrier of E by EC_PF_1:def 1;
now let a be Element of E;
assume A1: not a in the carrier of W;
reconsider E1 = E as FieldExtension of F;
reconsider E1 as W-extending FieldExtension of F by I1,FIELD_4:7;
reconsider E1 as W-algebraic FieldExtension of W by FIELD_7:40;
reconsider a as W-algebraic Element of E1;
set V = FAdj(W,{a});
I3: V is Element of SubFields(E) by subfie;
reconsider L1 = L as W-monomorphic algebraic-closed Field by H2,RING_3:def 3;
reconsider h1 as Monomorphism of W,L1 by H2;
consider r being Function of V,L such that
A2: r is monomorphism h1-extending by lift1;
reconsider V as W-extending FieldExtension of F;
reconsider r as Function of V,L;
[V,r] in S
proof
r is f-extending by H2,A2,e1a;
hence thesis by I3,A2;
end; then
reconsider T = [V,r] as Element of S;
U <= T by H2,H1,A2; then
A5: [U,T] in R;
{a} is Subset of V & a in {a} by FIELD_6:35,TARSKI:def 1;
then the carrier of W <> the carrier of V by A1;
then U <> T by H1,XTUPLE_0:1;
hence contradiction by B,A5,Z;
end; then
C: the carrier of E c= the carrier of W; then
G: the carrier of E = the carrier of W by I2,XBOOLE_0:def 10;
set E1 = the doubleLoopStr of E;
M: E1 is strict & W is strict by subfie;
D: E1 = W
proof
D1: the addF of E1 = (the addF of E) || the carrier of E
.= the addF of W by I1,G,EC_PF_1:def 1;
D2: the multF of E1 = (the multF of E) || the carrier of E
.= the multF of W by I1,G,EC_PF_1:def 1;
D3: 1.E1 = 1.E .= 1.W by I1,EC_PF_1:def 1;
0.E1 = 0.E .= 0.W by I1,EC_PF_1:def 1;
hence thesis by C,M,D1,D2,D3,I2,XBOOLE_0:def 10;
end;
then reconsider h2 = h1 as Function of E1,L by H2;
E1 == E by lemug1; then
consider i being Function of E,E1 such that
E: i = id E & i is isomorphism by FIELD_7:1;
reconsider g = h2 * i as Function of E,L;
K: g is linear by E,H2,D,RINGCAT1:1;
now let a be Element of F;
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 a1 = a as Element of E;
g.a1 = h2.(i.a1) by E,FUNCT_1:13 .= f.a by E,H2;
hence g.a = f.a;
end;
then g is f-extending;
hence thesis by K;
end;
theorem lift3b:
for F being Field,
E being FieldExtension of F,
L being F-homomorphic E-homomorphic Field
for f being Homomorphism of F,L for g being Homomorphism of E,L
st g is f-extending holds (Image f) is Subfield of (Image g)
proof
let F be Field, E be FieldExtension of F,
L be F-homomorphic E-homomorphic Field;
let f be Homomorphism of F,L; let g be Homomorphism of E,L;
assume AS: g is f-extending;
set If = Image f, Ig = Image g;
H1: rng f = the carrier of If &
rng g = the carrier of Ig by RING_2:def 6;
F is Subfield of E by FIELD_4:7; then
H3: the carrier of F c= the carrier of E by EC_PF_1:def 1;
A: the carrier of If c= the carrier of Ig
proof
now let o be object;
assume o in the carrier of If;
then consider u being object such that
A1: u in dom f & f.u = o by H1,FUNCT_1:def 3;
reconsider a = u as Element of F by A1;
reconsider a1 = a as Element of E by H3;
A2: dom g = the carrier of E by FUNCT_2:def 1;
g.a1 = o by AS,A1;
hence o in the carrier of Ig by H1,A2,FUNCT_1:def 3;
end;
hence thesis;
end;
H4: [:the carrier of If,the carrier of If:] c=
[:the carrier of Ig,the carrier of Ig:] by A,ZFMISC_1:96;
B: the addF of If
= (the addF of L) || the carrier of If by EC_PF_1:def 1
.= ((the addF of L) || the carrier of Ig) || the carrier of If
by H4,FUNCT_1:51
.= (the addF of Ig) || the carrier of If by EC_PF_1:def 1;
C: the multF of If
= (the multF of L) || the carrier of If by EC_PF_1:def 1
.= ((the multF of L) || the carrier of Ig) || the carrier of If
by H4,FUNCT_1:51
.= (the multF of Ig) || the carrier of If by EC_PF_1:def 1;
D: 1.If = 1.L by RING_2:def 6 .= 1.Ig by RING_2:def 6;
0.If = 0.L by RING_2:def 6 .= 0.Ig by RING_2:def 6;
hence thesis by A,B,C,D,EC_PF_1:def 1;
end;
theorem lift3c:
for F being Field,
A being AlgebraicClosure of F,
L being A-monomorphic A-homomorphic Field
for g being Monomorphism of A,L holds (Image g) is algebraic-closed
proof
let F be Field, E be AlgebraicClosure of F;
let L be E-monomorphic E-homomorphic Field, g be Monomorphism of E,L;
H: rng g = the carrier of (Image g) by RING_2:def 6; then
reconsider f = g" as Function of (Image g),E;
A: f is additive multiplicative unity-preserving monomorphism
proof
B1: now let a,b be Element of Image g;
consider x being object such that
A1: x in dom g & g.x = a by H,FUNCT_1:def 3;
reconsider x as Element of E by A1;
consider y being object such that
A2: y in dom g & g.y = b by H,FUNCT_1:def 3;
reconsider y as Element of E by A2;
A3: dom g = the carrier of E by FUNCT_2:def 1;
A4: g".b = y by A2,FUNCT_1:34;
A5: [a,b] in [:the carrier of Image g,the carrier of Image g:]
by ZFMISC_1:def 2;
g.(x + y) = g.x + g.y by VECTSP_1:def 20
.= ((the addF of L)||(the carrier of Image g)).(a,b)
by A1,A2,A5,FUNCT_1:49
.= a + b by EC_PF_1:def 1;
hence f.(a+b) = x + y by A3,FUNCT_1:34
.= f.a + f.b by A1,A4,FUNCT_1:34;
end;
B2: now let a,b be Element of Image g;
consider x being object such that
A1: x in dom g & g.x = a by H,FUNCT_1:def 3;
reconsider x as Element of E by A1;
consider y being object such that
A2: y in dom g & g.y = b by H,FUNCT_1:def 3;
reconsider y as Element of E by A2;
A3: dom g = the carrier of E by FUNCT_2:def 1;
A4: g".b = y by A2,FUNCT_1:34;
A5: [a,b] in [:the carrier of Image g,the carrier of Image g:]
by ZFMISC_1:def 2;
g.(x * y) = g.x * g.y by GROUP_6:def 6
.= ((the multF of L)||(the carrier of Image g)).(a,b)
by A1,A2,A5,FUNCT_1:49
.= a * b by EC_PF_1:def 1;
hence f.(a*b) = x * y by A3,FUNCT_1:34
.= f.a * f.b by A1,A4,FUNCT_1:34;
end;
B3: dom g = the carrier of E by FUNCT_2:def 1;
g.(1_E) = 1_L by GROUP_1:def 13 .= 1_(Image g) by EC_PF_1:def 1;
then f is additive multiplicative unity-preserving by B1,B2,B3,FUNCT_1:34;
hence thesis;
end; then
reconsider E1 = E as (Image g)-monomorphic (Image g)-homomorphic Field
by RING_2:def 4,RING_3:def 3;
reconsider f as Monomorphism of (Image g),E1 by A;
now let p be non constant Polynomial of (Image g);
reconsider p1 = p as
Element of the carrier of Polynom-Ring (Image g) by POLYNOM3:def 10;
C: deg p > 0 by RATFUNC1:def 2; then
reconsider p1 as non constant
Element of the carrier of Polynom-Ring (Image g) by RING_4:def 4;
reconsider q = (PolyHom f).p1 as Polynomial of E;
deg p1 = deg (PolyHom f).p1 by FIELD_1:31; then
reconsider q = (PolyHom f).p1 as non constant Polynomial of E
by C,RATFUNC1:def 2;
consider a being Element of E such that
B: a is_a_root_of q by POLYNOM5:def 8;
reconsider r = q as Element of the carrier of Polynom-Ring E;
F: dom(PolyHom f) = the carrier of Polynom-Ring(Image g) by FUNCT_2:def 1;
E: (PolyHom g).((PolyHom f).p1) = p1
proof
dom g = the carrier of E1 by FUNCT_2:def 1; then
reconsider g1 = g as Function of E1,(Image g) by H,FUNCT_2:1;
Z: g1 is additive multiplicative unity-preserving
proof
now let a,b be Element of E1;
reconsider a1 = a, b1 = b as Element of E;
Z1: [g1.a,g1.b] in
[:the carrier of Image g,the carrier of Image g:]
by ZFMISC_1:def 2;
thus g1.(a+b)
= g.a1 + g.b1 by VECTSP_1:def 20
.= ((the addF of L)||(the carrier of Image g)).(g1.a,g1.b)
by Z1,FUNCT_1:49
.= g1.a + g1.b by EC_PF_1:def 1;
end;
hence g1 is additive;
now let a,b be Element of E1;
reconsider a1 = a, b1 = b as Element of E;
Z1: [g1.a,g1.b] in
[:the carrier of Image g,the carrier of Image g:]
by ZFMISC_1:def 2;
thus g1.(a*b)
= g.a1 * g.b1 by GROUP_6:def 6
.= ((the multF of L)||(the carrier of Image g)).(g1.a,g1.b)
by Z1,FUNCT_1:49
.= g1.a * g1.b by EC_PF_1:def 1;
end;
hence g1 is multiplicative;
g1.(1_E1) = 1_L by GROUP_1:def 13
.= 1_(Image g) by EC_PF_1:def 1;
hence thesis;
end;
reconsider Ig = (Image g) as E1-homomorphic Field by Z,RING_2:def 4;
reconsider g1 as additive Function of E1,Ig by Z;
G: g1 * f = id(Image g)
proof
now let o be object;
assume o in dom(g1 * f); then
reconsider a = o as Element of Image g;
(g1*f).a = a by H,FUNCT_1:35;
hence (g1*f).o = id(Image g).o;
end;
hence thesis by FUNCT_2:def 1;
end;
H: PolyHom g1 = PolyHom g
proof
now let o be object;
assume o in the carrier of Polynom-Ring E1;
then reconsider a = o as Element of the carrier of Polynom-Ring E1;
reconsider b = a as Element of the carrier of Polynom-Ring E;
now let i be Nat;
thus ((PolyHom g).b).i = g.(b.i) by FIELD_1:def 2
.= ((PolyHom g1).a).i by FIELD_1:def 2;
end;
then (PolyHom g1).a = (PolyHom g).b;
hence (PolyHom g1).o = (PolyHom g).o;
end;
hence thesis;
end;
thus (PolyHom g).((PolyHom f).p1)
= ((PolyHom g1) * (PolyHom f)).p1 by F,H,FUNCT_1:13
.= (id(Polynom-Ring (Image g))).p1 by G,ll2
.= p1;
end;
dom g = the carrier of E by FUNCT_2:def 1; then
reconsider ga = g.a as Element of (Image g) by H,FUNCT_1:3;
L is FieldExtension of (Image g) by FIELD_4:7; then
eval(p,ga) = eval((PolyHom g).r,g.a) by E,FIELD_4:27
.= 0.L by B,FIELD_1:34,POLYNOM5:def 7
.= 0.(Image g) by RING_2:def 6;
hence p is with_roots by POLYNOM5:def 8,POLYNOM5:def 7;
end;
hence thesis by alg2;
end;
theorem lift3:
for F being Field,
L being F-monomorphic F-homomorphic Field,
A being AlgebraicClosure of F
for f being Monomorphism of F,L st L is AlgebraicClosure of (Image f)
for g being Function of A,L
st g is monomorphism f-extending holds g is isomorphism
proof
let F be Field, L be F-monomorphic F-homomorphic Field,
E being AlgebraicClosure of F, f be Monomorphism of F,L;
assume AS1: L is AlgebraicClosure of (Image f);
let g be Function of E,L;
assume AS2: g is monomorphism f-extending; then
reconsider L1 = L as E-monomorphic E-homomorphic Field
by RING_3:def 3,RING_2:def 4;
reconsider g1 = g as Monomorphism of E,L1 by AS2;
B: Image g1 is algebraic-closed by lift3c;
reconsider If = Image f as Field;
If is Subfield of Image g1 by AS2,lift3b; then
reconsider Ig = Image g1 as FieldExtension of If by FIELD_4:7;
reconsider L1 as FieldExtension of If by AS1;
Ig is Subring of L1 by FIELD_5:12; then
reconsider L1 as Ig-extending FieldExtension of If by FIELD_4:def 1;
L1 is If-algebraic by AS1; then
Ig is AlgebraicClosure of If by B,defAC,FIELD_7:40; then
the doubleLoopStr of L1 = the doubleLoopStr of Ig
by AS1,lift3a,FIELD_7:def 1; then
g is onto by RING_2:def 6;
hence thesis by AS2;
end;
theorem
for F being Field
for A1,A2 being AlgebraicClosure of F holds A1,A2 are_isomorphic_over F
proof
let F be Field, E1,E2 be AlgebraicClosure of F;
reconsider L = E2 as F-monomorphic F-homomorphic algebraic-closed Field;
reconsider f = id F as Monomorphism of F,L by lift5a;
consider g being Function of E1,L such that
A: g is monomorphism f-extending by lift2;
C: the doubleLoopStr of F == F by lemug1;
Image f = the doubleLoopStr of F
proof
set If = Image f;
H: F is Subfield of E2 by FIELD_4:7;
B: the carrier of If = rng f by RING_2:def 6 .= the carrier of F;
C: the addF of If = (the addF of L)||(rng f) by RING_2:def 6
.= the addF of F by H,EC_PF_1:def 1;
D: the multF of If = (the multF of L)||(rng f) by RING_2:def 6
.= the multF of F by H,EC_PF_1:def 1;
E: the OneF of If = 1.L by RING_2:def 6 .= 1.F by H,EC_PF_1:def 1;
the ZeroF of If = 0.L by RING_2:def 6 .= 0.F by H,EC_PF_1:def 1;
hence thesis by B,C,D,E;
end; then
L is AlgebraicClosure of (Image f) by C,lift4;
then B: g is isomorphism by A,lift3;
now let a be Element of F;
thus g.a = f.a by A .= a;
end; then
g is F-fixing;
hence thesis by B,FIELD_8:def 5;
end;