:: {Z}ariski {T}opology
:: by Yasushige Watase
::
:: Received October 16, 2018
:: Copyright (c) 2018-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, FUNCT_1, RELAT_1, WELLORD1, CARD_3, XBOOLE_0, TARSKI,
XCMPLX_0, STRUCT_0, SUBSET_1, SUPINF_2, NAT_1, CARD_1, MESFUNC1, GROUP_1,
ARYTM_1, FINSEQ_1, SETFAM_1, INT_2, QUOFIELD, MSSUBFAM, BINOP_1, GROUP_4,
NUMBERS, IDEAL_1, C0SP1, ZFMISC_1, FUNCSDOM, CARD_FIL, RING_1, SQUARE_1,
BCIALG_2, NEWTON, RING_2, ORDERS_1, XXREAL_0, FINSET_1, WELLORD2,
PRE_TOPC, RCOMP_1, TEX_1, ORDINAL2, TOPZARI1, ALGSTR_0, LATTICEA;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, RELAT_1,
ORDINAL1, WELLORD1, FUNCT_1, FUNCT_2, FINSET_1, STRUCT_0, PRE_TOPC,
ALGSTR_0, RLVECT_1, ORDERS_1, GROUP_1, VECTSP_1, IDEAL_1, RING_1, RING_2,
TEX_1, RELSET_1, XCMPLX_0, XXREAL_0, NUMBERS, BINOM, GROUP_6, QUOFIELD,
C0SP1, FINSEQ_1;
constructors ARYTM_3, TDLAT_3, ORDERS_1, RINGCAT1, RING_2, BINOM, RELSET_1,
GCD_1, ALGSTR_0, TEX_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, NAT_1, STRUCT_0, CARD_1,
VECTSP_1, ALGSTR_1, SUBSET_1, FUNCT_2, ALGSTR_0, RLVECT_1, IDEAL_1,
RINGCAT1, RING_1, PRE_TOPC, SCMRINGI;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, IDEAL_1, XBOOLE_0;
equalities STRUCT_0, WELLORD1, TEX_1;
expansions TARSKI, STRUCT_0, GROUP_1, VECTSP_1, IDEAL_1, XBOOLE_0, GROUP_6,
ORDERS_1, RING_1, SUBSET_1, PBOOLE;
theorems GROUP_1, GROUP_6, VECTSP_1, RLVECT_1, IDEAL_1, SUBSET_1, FUNCT_2,
TARSKI, FUNCT_1, C0SP1, RING_1, TOPGEN_3, ZFMISC_1, XBOOLE_0, FINSEQ_1,
ORDINAL1, XXREAL_0, XBOOLE_1, BINOM, RELAT_2, WELLORD2, RING_2, ORDERS_1,
RELAT_1, SETFAM_1, PRE_TOPC, T_0TOPSP;
schemes NAT_1, FUNCT_2, XFAMILY, TOPGEN_3;
begin :: Preliminaries: Some Properties of Ideals
reserve R for commutative Ring;
reserve A,B for non degenerated commutative Ring;
reserve h for Function of A,B;
reserve I0,I,I1,I2 for Ideal of A;
reserve J,J1,J2 for proper Ideal of A;
reserve p for prime Ideal of A;
reserve S,S1 for non empty Subset of A;
reserve E,E1,E2 for Subset of A;
reserve a,b,f for Element of A;
reserve n for Nat;
reserve x,o,o1 for object;
Lm1:
x in Ideals A iff x is Ideal of A
proof
thus x in Ideals A implies x is Ideal of A
proof
assume x in Ideals A; then
x in the set of all I where I is Ideal of A by RING_2:def 3; then
consider x0 be Ideal of A such that
A3: x0 = x;
thus thesis by A3;
end;
assume x is Ideal of A; then
x in the set of all I where I is Ideal of A;
hence thesis by RING_2:def 3;
end;
definition let A,S;
func Ideals(A,S) -> Subset of Ideals A equals
{ I where I is Ideal of A: S c= I };
coherence
proof
set C = {I where I is Ideal of A: S c= I };
now let x be object;
assume x in C;
then ex I being Ideal of A st x = I & S c= I;
hence x in Ideals A by Lm1;
end;
then C c= Ideals A;
hence thesis;
end;
end;
registration let A,S;
cluster Ideals(A,S) -> non empty;
coherence
proof
set I = [#]A;
reconsider I as Subset of A;
I in Ideals(A,S);
hence thesis;
end;
end;
theorem Th2:
Ideals(A,S) = Ideals(A,S-Ideal)
proof
thus Ideals(A,S) c= Ideals(A,S-Ideal)
proof
let x be object;
assume x in Ideals(A,S); then
consider y being Ideal of A such that
A2: x = y and
A3: S c= y;
S-Ideal c= y-Ideal by A3,IDEAL_1:57; then
S-Ideal c= y by IDEAL_1:44;
hence thesis by A2;
end;
let x be object;
assume x in Ideals(A,S-Ideal); then
consider y being Ideal of A such that
A8: x = y and
A9: S-Ideal c= y;
S c= S-Ideal by IDEAL_1:def 14; then
S c= y by A9;
hence thesis by A8;
end;
:: Some Properties of power of an element of a ring
:: Definition of Nilpotency
definition
let A be unital non empty multLoopStr_0, a be Element of A;
attr a is nilpotent means
ex k being non zero Nat st a|^k = 0.A;
end;
registration
let A be unital non empty multLoopStr_0;
cluster 0.A -> nilpotent;
coherence
proof
(0.A)|^1 = 0.A by BINOM:8;
hence thesis;
end;
end;
registration
let A be unital non empty multLoopStr_0;
cluster nilpotent for Element of A;
existence
proof
take 0.A;
thus thesis;
end;
end;
registration let A;
cluster 1.A -> non nilpotent;
coherence
proof
set a = 1.A;
for n be Nat holds a|^n = a
proof
defpred P[Nat] means a|^$1 = 1.A;
A1: now
let n be Nat;
assume
A2: P[n];
a|^(n+1) = a|^n * a|^1 by BINOM:10
.= a by BINOM:8,A2;
hence P[n+1];
end;
a|^0 = 1_A by BINOM:8 .= a; then
A3: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
end;
hence thesis;
end;
end;
:: Definition of a multiplicatively closed set generated by an element
:: which does not meet a proper Ideal J
definition
let A,J,f;
func multClSet(J,f) -> Subset of A equals
the set of all f|^i where i is Nat;
coherence
proof
the set of all f|^i where i is Nat c= the carrier of A
proof
let x be object;
assume x in the set of all f|^i where i is Nat; then
consider k being Nat such that
A2: x = f|^k;
thus thesis by A2;
end;
hence thesis;
end;
end;
registration let A,J,f;
cluster multClSet(J,f) -> multiplicatively-closed;
coherence
proof
A2: f|^0 = 1_A by BINOM:8;
A4: 1.A in multClSet(J,f) by A2;
for v,u be Element of A st v in multClSet(J,f) & u in multClSet(J,f) holds
v * u in multClSet(J,f)
proof
let v,u be Element of A;
assume that
A5: v in multClSet(J,f) and
A6: u in multClSet(J,f);
consider n1 be Nat such that
A7: v = f|^n1 by A5;
consider n2 be Nat such that
A8: u = f|^n2 by A6;
v * u = f|^(n1+n2) by BINOM:10,A8,A7;
hence thesis;
end;
hence thesis by A4,C0SP1:def 4;
end;
end;
theorem Lm4:
for n be Nat holds (1.A)|^n = 1.A
proof
defpred P[Nat] means (1.A)|^$1 = 1.A;
A1: now
let n be Nat;
assume
A2: P[n];
(1.A)|^(n+1) = (1.A)|^n * (1.A)|^1 by BINOM:10
.= 1.A by BINOM:8,A2;
hence P[n+1];
end;
(1.A)|^0 = 1_A by BINOM:8; then
A3: P[0];
thus for n be Nat holds P[n] from NAT_1:sch 2(A3,A1);
end;
theorem Lm5:
not 1.A in sqrt J
proof
assume 1.A in sqrt J; then
1.A in {a where a is Element of A: ex n be Element of NAT st a|^n in J}
by IDEAL_1:def 24; then
consider a be Element of A such that
A3: 1.A = a and
A4: ex n be Element of NAT st a|^n in J;
consider n1 be Element of NAT such that
A5: a|^n1 in J by A4;
1.A = a|^n1 by A3,Lm4;
hence contradiction by IDEAL_1:19, A5;
end;
theorem Lm6:
multClSet(J,1.A) = {1.A}
proof
thus multClSet(J,1.A) c= {1.A}
proof
let x be object;
assume x in multClSet(J,1.A); then
consider n1 be Nat such that
A3: x = (1.A)|^n1;
x = 1.A by A3,Lm4;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {1.A}; then
x = 1.A by TARSKI:def 1;
hence thesis by C0SP1:def 4;
end;
definition let A,J,f;
func Ideals(A,J,f) -> Subset of Ideals A equals
{I where I is Subset of A: I is proper Ideal of A &
J c= I & I /\ multClSet(J,f) = {} };
coherence
proof
set C={I where I is Subset of A: I is proper Ideal of A &
J c= I & I /\ multClSet(J,f) = {} };
C c= Ideals A
proof let x be object;
assume x in C; then
consider I being Subset of A such that
A1: x = I and
A2: I is proper Ideal of A and
J c= I & I /\ multClSet(J,f) = {};
thus x in Ideals A by A1,A2,Lm1;
end;
hence thesis;
end;
end;
theorem Th7:
for A, J, f st not f in sqrt J holds J in Ideals(A,J,f)
proof
let A,J,f;
assume
A1: not f in sqrt J;
set I = J;
I /\ multClSet(J,f) = {}
proof
assume I /\ multClSet(J,f) <> {}; then
consider x be object such that
A4: x in I /\ multClSet(J,f) by XBOOLE_0:def 1;
x in I & x in multClSet(J,f) by A4,XBOOLE_0:def 4; then
consider n1 be Nat such that
A5: x = f|^n1;
reconsider n1 as Element of NAT by ORDINAL1:def 12;
sqrt J = {a where a is Element of A:
ex n being Element of NAT st a|^n in J} by IDEAL_1:def 24;
then not f|^n1 in J by A1;
hence contradiction by A4,A5,XBOOLE_0:def 4;
end;
hence thesis;
end;
::[AM] Theorem 1.3
theorem Th8:
for A, J, f st not f in sqrt J holds
Ideals(A,J,f) has_upper_Zorn_property_wrt RelIncl(Ideals(A,J,f) )
proof
let A,J,f;
assume
A1: not f in sqrt J;
set S = Ideals(A,J,f);
set P = RelIncl(S);
A2: field P = S by WELLORD2:def 1;
for Y be set st Y c= S & P|_2 Y is being_linear-order
ex x be set st x in S & for y be set st y in Y holds [y,x] in P
proof
let Y be set such that
A3: Y c= S and
A4: P |_2 Y is being_linear-order;
per cases;
suppose
A5: Y is empty;
take x = J;
thus thesis by A5,A1,Th7;
end;
suppose
Y is non empty; then
consider e being object such that
A6: e in Y;
take x = union Y;
for a be object st a in x holds a in the carrier of A
proof
let a be object;
assume a in x; then
consider Z being set such that
A7: a in Z and
A8: Z in Y by TARSKI:def 4;
Z in S by A3,A8; then
ex A1 be Subset of A st Z = A1 &
A1 is proper Ideal of A & J c= A1 & A1 /\ multClSet(J,f) = {};
hence thesis by A7;
end; then
x c= the carrier of A; then
reconsider B = x as Subset of A;
A9: B is left-ideal
proof
let p, a be Element of A;
assume a in B; then
consider Aa being set such that
A10: a in Aa and
A11: Aa in Y by TARSKI:def 4;
Aa in S by A3,A11; then
consider Ia be Subset of A such that
A12: Aa = Ia and
A13: Ia is proper Ideal of A and
J c= Ia and
Ia /\ multClSet(J,f) = {};
p*a in Ia & Ia c= B by A10,A11,A12,A13,IDEAL_1:def 2,ZFMISC_1:74;
hence thesis;
end;
A14: B is proper
proof
assume B is non proper; then
consider Aa being set such that
A16: 1.A in Aa and
A17: Aa in Y by TARSKI:def 4;
Aa in S by A3,A17; then
ex Ia be Subset of A st Aa = Ia &
Ia is proper Ideal of A & J c= Ia & Ia /\ multClSet(J,f) = {};
hence contradiction by A16,IDEAL_1:19;
end;
A18: B is add-closed
proof
A19: field (P |_2 Y) = Y by A2,A3,ORDERS_1:71;
let a, b be Element of A;
A20: now
let A1 be Ideal of A;
assume a in A1 & b in A1;
then
A21: a+b in A1 by IDEAL_1:def 1;
assume A1 in Y;
hence a+b in B by A21,TARSKI:def 4;
end;
assume a in B; then
consider Aa being set such that
A22: a in Aa and
A23: Aa in Y by TARSKI:def 4;
Aa in S by A3,A23; then
A24: ex Ia be Subset of A st Aa = Ia &
Ia is proper Ideal of A & J c= Ia & Ia /\ multClSet(J,f) = {};
assume b in B; then
consider Ab being set such that
A25: b in Ab and
A26: Ab in Y by TARSKI:def 4;
[Aa,Ab] in P |_2 Y or [Ab,Aa] in P |_2 Y or Aa = Ab
by A4, A23, A26, A19, RELAT_2:def 6,def 14; then
[Aa,Ab] in P or [Ab,Aa] in P or Aa = Ab by XBOOLE_0:def 4; then
A27: Aa c= Ab or Ab c= Aa by A3,A23,A26,WELLORD2:def 1;
Ab in S by A3,A26; then
ex Ib be Subset of A st Ab = Ib &
Ib is proper Ideal of A & J c= Ib & Ib /\ multClSet(J,f) = {};
hence a+b in B by A22,A23,A25,A26,A20,A24,A27;
end;
e in S by A3,A6; then
consider A1 be Subset of A such that
A28: A1 = e and
A29: A1 is proper Ideal of A and
A30: J c= A1 and
A1 /\ multClSet(J,f) = {};
ex q being object st q in A1 by XBOOLE_0:def 1,A29; then
A32: B is non empty & J c= B by A6,A28,A30,TARSKI:def 4;
A33: B /\ multClSet(J,f) = {}
proof
assume B /\ multClSet(J,f) <> {}; then
consider y be object such that
A35: y in B /\ multClSet(J,f) by XBOOLE_0:def 1;
y in B & y in multClSet(J,f) by A35,XBOOLE_0:def 4; then
consider Aa being set such that
A36: y in Aa and
A37: Aa in Y by TARSKI:def 4;
Aa in S by A3,A37; then
consider Ia be Subset of A such that
A38: Aa = Ia and
Ia is proper Ideal of A & J c= Ia and
A39: Ia /\ multClSet(J,f) = {};
y in multClSet(J,f) by A35, XBOOLE_0:def 4;
hence contradiction by A39, A38, A36, XBOOLE_0:def 4;
end;
thus
A41: x in S by A9,A14,A18,A32,A33;
let y be set;
assume
A42: y in Y; then
y c= x by ZFMISC_1:74;
hence thesis by A3,A41,A42,WELLORD2:def 1;
end;
end;
hence thesis;
end;
theorem Th9:
for f,J st not f in sqrt J holds
ex m be prime Ideal of A st not f in m & J c= m
proof
let f,J;
assume
A1: not f in sqrt J;
set S = Ideals(A,J,f);
set P = RelIncl(S);
A2: field P = S by WELLORD2:def 1;
P partially_orders S by WELLORD2:19,21,20; then
consider I being set such that
A3: I is_maximal_in P by A1,A2,Th8,ORDERS_1:63;
I in S by WELLORD2:def 1, A3; then
consider p be Subset of A such that
A4: p = I and
A6: p is proper Ideal of A and
A7: J c= p and
A8: p /\ multClSet(J,f) = {};
f|^1 = f by BINOM:8; then
f in multClSet(J,f); then
A11: not f in p by A8,XBOOLE_0:def 4;
p is quasi-prime Ideal of A
proof
for x,y be Element of A st not x in p & not y in p holds not x*y in p
proof
let x,y be Element of A;
assume that
A12: not x in p and
A13: not y in p;
assume
A14: x*y in p;
A15: p c< p + {x}-Ideal
proof
{x}-Ideal c= p + {x}-Ideal by A6,IDEAL_1:74;
hence thesis by A6,A12,IDEAL_1:66,73;
end;
A17: p c< p + {y}-Ideal
proof
{y}-Ideal c= p + {y}-Ideal by A6,IDEAL_1:74;
hence thesis by A6,A13,IDEAL_1:66,73;
end;
set J2 = p + {x}-Ideal;
A19: not (p + {x}-Ideal in Ideals(A,J,f) )
proof
assume
A20: p + {x}-Ideal in Ideals(A,J,f); then
A21: J2 in field P by WELLORD2:def 1;
J2 <> I & [I,J2] in P by A2,A3,A4,A15,A20,WELLORD2:def 1;
hence contradiction by A3,A21;
end;
A22: not (p + {y}-Ideal in Ideals(A,J,f) )
proof
assume
A23: p + {y}-Ideal in Ideals(A,J,f);
set J2 = p + {y}-Ideal;
A24: J2 in field P by WELLORD2:def 1,A23;
J2 <> I & [I,J2] in P by A2,A3,A4,A17,A23,WELLORD2:def 1;
hence contradiction by A3,A24;
end;
reconsider q = p + {x}-Ideal as Subset of A;
A26: p c= p + {x}-Ideal by A6,IDEAL_1:73;
A27: not(q is proper Ideal of A) or not (J c= q) or
not (q /\ multClSet(J,f) = {}) by A19;
A28: ex n be Nat st f|^n in p + {x}-Ideal
proof
per cases by A7,A26,A27;
suppose
A29: not(p + {x}-Ideal is proper Ideal of A);
reconsider q1 = p + {x}-Ideal as Ideal of A by A6;
A30: q1 = the carrier of A by A29, SUBSET_1:def 6;
reconsider n = 1 as Nat;
f|^n in q by A30;
hence thesis;
end;
suppose not (q /\ multClSet(J,f) = {}); then
consider h be object such that
A32: h in q /\ multClSet(J,f) by XBOOLE_0:def 1;
h in q & h in multClSet(J,f) by A32,XBOOLE_0:def 4;
then consider n1 be Nat such that
A33: h = f|^n1;
f|^n1 in q by A33,A32,XBOOLE_0:def 4;
hence thesis;
end;
end;
reconsider q = p + {y}-Ideal as Subset of A;
p c= p + {y}-Ideal by A6,IDEAL_1:73; then
A36: J c= q by A7;
A37: ex m be Nat st f|^m in p + {y}-Ideal
proof
per cases by A22,A36;
suppose
A38: not(p + {y}-Ideal is proper Ideal of A);
reconsider q1 = p + {y}-Ideal as Ideal of A by A6;
A39: q1 = the carrier of A by A38,SUBSET_1:def 6;
reconsider m = 1 as Nat;
f|^m in q by A39;
hence thesis;
end;
suppose q /\ multClSet(J,f) <> {}; then
consider h be object such that
A41: h in q /\ multClSet(J,f) by XBOOLE_0:def 1;
h in q & h in multClSet(J,f) by A41,XBOOLE_0:def 4;
then
consider n1 be Nat such that
A42: h = f|^n1;
f|^n1 in q by A41,XBOOLE_0:def 4,A42;
hence thesis;
end;
end;
reconsider p as Ideal of A by A6;
consider n be Nat such that
A43: f|^n in p + {x}-Ideal by A28;
consider m be Nat such that
A44: f|^m in p + {y}-Ideal by A37;
f|^n in {a + b where a,b is Element of A :
a in p & b in {x}-Ideal} by A43,IDEAL_1:def 19; then
consider p1,x1 be Element of A such that
A45: f|^n = p1+x1 and
A46: p1 in p and
A47: x1 in {x}-Ideal;
f|^m in {a + b where a,b is Element of A :
a in p & b in {y}-Ideal} by A44,IDEAL_1:def 19; then
consider p2,y2 be Element of A such that
A48: f|^m = p2+y2 and
A49: p2 in p and
A50: y2 in {y}-Ideal;
x1 in the set of all x*a where a is Element of A by A47,IDEAL_1:64;
then
consider a be Element of A such that
A51: x1 = x*a;
y2 in the set of all y*a where a is Element of A by A50,IDEAL_1:64;
then
consider b be Element of A such that
A52: y2 = y*b;
A53: (p1 + x1) * p2 + (p1 * y2) in p
proof
reconsider a = p1 + x1 as Element of A;
A54: a * p2 in p by A49,IDEAL_1:def 2;
p1 * y2 in p by A46,IDEAL_1:def 3;
hence thesis by A54,IDEAL_1:def 1;
end;
A56a: x1 * y2 in {x*y}-Ideal
proof
A57: x1 * y2 = a*(x*(y*b)) by GROUP_1:def 3,A52,A51
.= ((x*y)*b)*a by GROUP_1:def 3
.= (x*y)*(b*a) by GROUP_1:def 3;
(x*y)*(b*a) in the set of all (x*y)*r where r is Element of A;
hence thesis by A57,IDEAL_1:64;
end;
A59: f|^(n+m) = (f|^n) * (f|^m) by BINOM:10
.= (p1 + x1) * p2 + ((p1 + x1) * y2) by VECTSP_1:def 7,A45,A48
.= (p1 + x1) * p2 + (p1 * y2 + x1 * y2) by VECTSP_1:def 7
.= ((p1 + x1) * p2 + (p1 * y2)) + (x1 * y2) by RLVECT_1:def 3;
reconsider s = (p1 + x1) * p2 + (p1 * y2), t = x1 * y2 as Element of A;
s+t in {u+v where u,v is Element of A:u in p & v in {x*y}-Ideal}
by A53,A56a; then
A61: f|^(n+m) in p + {x*y}-Ideal by A59,IDEAL_1:def 19;
reconsider n1 = n + m as Nat;
A63: f|^(n+m) in multClSet(J,f);
A64: not p + {x*y}-Ideal in Ideals(A,J,f)
proof
assume p + {x*y}-Ideal in Ideals(A,J,f); then
consider q be Subset of A such that
A66: q = p + {x*y}-Ideal and
q is proper Ideal of A & J c= q and
A67: q /\ multClSet(J,f) = {};
thus contradiction by A61,A63,XBOOLE_0:def 4,A67,A66;
end;
p-Ideal = p by IDEAL_1:44; then
{x*y}-Ideal c= p by IDEAL_1:67, A14; then
p = p + {x*y}-Ideal by IDEAL_1:74,75;
hence contradiction by A3,A4,A64,WELLORD2:def 1;
end; then
for a, b being Element of A st a*b in p holds a in p or b in p;
hence thesis by A6,RING_1:def 1;
end;
hence thesis by A6,A7,A11;
end;
::[AM] Cor 1.4
theorem Th10:
ex m be maximal Ideal of A st J c= m
proof
A1: not 1.A in sqrt J by Lm5;
set S = Ideals(A,J,1.A);
set P = RelIncl(S);
A2: field P = S by WELLORD2:def 1;
P partially_orders S by WELLORD2:19,20, 21; then
consider I being set such that
A3: I is_maximal_in P by A1,A2,Th8, ORDERS_1:63;
I in S by WELLORD2:def 1,A3; then
consider p be Subset of A such that
A4: p = I and
A5: p is proper Ideal of A and
A6: J c= p and
p /\ multClSet(J,1.A) = {};
for q being Ideal of A st p c= q holds q = p or q is non proper
proof
let q be Ideal of A;
assume
A7: p c= q;
per cases;
suppose
A8: q is proper;
A9: multClSet(J,1.A) = {1.A} by Lm6;
A10: q /\ multClSet(J,1.A) = {}
proof
assume q /\ multClSet(J,1.A) <> {}; then
consider y be object such that
A12: y in q /\ multClSet(J,1.A) by XBOOLE_0:def 1;
A13: y in q & y in multClSet(J,1.A) by A12,XBOOLE_0:def 4;
1.A in q by A9,A13,TARSKI:def 1;
hence contradiction by A8,IDEAL_1:19;
end;
J c= q by A6,A7; then
A14: q in S by A8,A10;
[p,q] in P by A2,A3,A4,A7,A14,WELLORD2:def 1;
hence thesis by A2,A3,A4,A14;
end;
suppose q is non proper;
hence thesis;
end;
end; then
p is quasi-maximal;
hence thesis by A5,A6;
end;
theorem Th11:
ex m be prime Ideal of A st J c= m
proof
ex m be maximal Ideal of A st J c= m by Th10;
hence thesis;
end;
::[AM] Cor 1.5
theorem
a is NonUnit of A implies ex m be maximal Ideal of A st a in m
proof
assume a is NonUnit of A; then
{a}-Ideal <> [#] A by RING_2:20; then
{a}-Ideal is proper; then
consider m be maximal Ideal of A such that
A2: {a}-Ideal c= m by Th10;
a in m by A2,IDEAL_1:66;
hence thesis;
end;
begin :: Spectrum of Prime Ideals and Maximal Ideal
definition
let R be commutative Ring;
func Spectrum R -> Subset-Family of R equals :Def3:
{I where I is Ideal of R: I is quasi-prime & I <> [#]R}
if R is non degenerated
otherwise {};
coherence
proof
thus R is non degenerated implies
{I where I is Ideal of R: I is quasi-prime & I <> [#]R}
is Subset of bool the carrier of R
proof
set X = {I where I is Ideal of R: I is quasi-prime & I <> [#]R};
X c= bool the carrier of R
proof
let x be object;
assume x in X;
then ex I being Ideal of R st x = I & I is quasi-prime & I <> [#]R;
hence thesis;
end;
hence thesis;
end;
thus thesis by XBOOLE_1:2;
end;
consistency;
end;
definition
let A;
redefine func Spectrum A -> Subset-Family of A equals :: redefines Spectrum (TOPZARI1, definition)
the set of all I where I is prime Ideal of A;
correctness
proof
set C = {I where I is Ideal of A: I is quasi-prime & I <> [#]A};
A1: x in Spectrum A implies x in the set of all I where I is prime Ideal of A
proof
assume x in Spectrum A; then
x in C by Def3; then
consider I being Ideal of A such that
A3: x = I and
A4: I is quasi-prime and
A5: I <> [#]A;
A6: I is proper Ideal of A by A5,SUBSET_1:def 6;
reconsider I as quasi-prime Ideal of A by A4;
I in the set of all I where I is prime Ideal of A by A6;
hence thesis by A3;
end;
x in the set of all I where I is prime Ideal of A implies x in Spectrum A
proof
assume x in the set of all I where I is prime Ideal of A; then
consider I be prime Ideal of A such that
A8: I = x;
reconsider I as non empty Subset of A;
I in C;
hence thesis by A8,Def3;
end;
hence thesis by TARSKI:2,A1;
end;
end;
registration
let A;
cluster Spectrum A -> non empty;
coherence
proof
set m = the maximal Ideal of A;
reconsider m as Subset of A;
m in Spectrum A;
hence thesis;
end;
end;
definition
let R;
func m-Spectrum R -> Subset-Family of R equals :Def4:
{I where I is Ideal of R: I is quasi-maximal & I <> [#]R}
if R is non degenerated
otherwise {};
coherence
proof
thus R is non degenerated implies
{I where I is Ideal of R: I is quasi-maximal & I <> [#]R}
is Subset of bool the carrier of R
proof
set X = {I where I is Ideal of R: I is quasi-maximal & I <> [#]R};
X c= bool the carrier of R
proof
let x be object;
assume x in X; then
ex I being Ideal of R st x = I & I is quasi-maximal & I <> [#]R;
hence thesis;
end;
hence thesis;
end;
thus thesis by XBOOLE_1:2;
end;
consistency;
end;
definition
let A;
redefine func m-Spectrum A -> Subset-Family of the carrier of A equals :: redefines m-Spectrum (TOPZARI1, definition)
the set of all I where I is maximal Ideal of A;
correctness
proof
set C = {I where I is Ideal of A: I is quasi-maximal & I <> [#]A};
A2: x in m-Spectrum A implies
x in the set of all I where I is maximal Ideal of A
proof
assume x in m-Spectrum A; then
x in C by Def4; then
consider I being Ideal of A such that
A4: x = I and
A5: I is quasi-maximal and
A6: I <> [#]A;
I is proper by A6;
hence thesis by A4,A5;
end;
x in the set of all I where I is maximal Ideal of A implies
x in m-Spectrum A
proof
assume x in the set of all I where I is maximal Ideal of A; then
consider I be maximal Ideal of A such that
A9: I = x;
I in C;
hence thesis by A9,Def4;
end;
hence thesis by TARSKI:2,A2;
end;
end;
registration
let A;
cluster m-Spectrum A -> non empty;
coherence
proof
set m = the maximal Ideal of A;
m in m-Spectrum A;
hence thesis;
end;
end;
begin :: Local & Semi-Local Ring
definition
let A;
attr A is local means
ex m be Ideal of A st m-Spectrum A = {m};
end;
definition
let A;
attr A is semi-local means
m-Spectrum A is finite;
end;
theorem Th15:
x in I & I is proper Ideal of A implies x is NonUnit of A
proof
assume that
A1: x in I and
A2: I is proper Ideal of A;
assume
A3: not x is NonUnit of A;
reconsider x as Element of A by A1;
{x}-Ideal = [#]A by A3,RING_2:20; then
[#]A = I by A1,RING_2:4;
hence contradiction by A2;
end;
theorem Th16:
(for m1,m2 be object st m1 in m-Spectrum A & m2 in m-Spectrum A holds
m1 = m2)
implies A is local
proof
assume
A1: for m1,m2 be object st m1 in m-Spectrum A & m2 in m-Spectrum A holds
m1 = m2;
reconsider m = the maximal Ideal of A as maximal Ideal of A;
A3: o = m implies o in m-Spectrum A;
m in m-Spectrum A; then
o in m-Spectrum A implies o = m by A1; then
m-Spectrum A = {m} by A3,TARSKI:def 1;
hence thesis;
end;
::[AM] prop 1.6 i)
theorem Th17:
(for x holds x in [#]A \ J implies x is Unit of A) implies A is local
proof
assume
A1: (for x holds x in [#]A \ J implies x is Unit of A);
consider m1 be maximal Ideal of A such that
A2: J c= m1 by Th10;
:: claim any m st maximal implies m = m1
A3: for m be maximal Ideal of A holds m = m1
proof
let m be maximal Ideal of A;
o in m implies o in m1
proof
assume
A4: o in m; then
o is NonUnit of A by Th15; then
not o in [#]A \ J by A1; then
o in J by A4,XBOOLE_0:def 5;
hence thesis by A2;
end; then
m c= m1;
hence thesis by RING_1:def 3;
end;
for o1,o2 be object st o1 in m-Spectrum A & o2 in m-Spectrum A holds
o1 = o2
proof
let o1,o2 be object;
assume that
A8: o1 in m-Spectrum A and
A9: o2 in m-Spectrum A;
consider x1 being maximal Ideal of A such that
A10: x1 = o1 by A8;
consider x2 being maximal Ideal of A such that
A11: x2 = o2 by A9;
o1 = m1 by A10,A3 .= o2 by A3,A11;
hence thesis;
end;
hence thesis by Th16;
end;
reserve m for maximal Ideal of A;
theorem Th18:
a in [#]A \ m implies {a}-Ideal + m = [#]A
proof
assume
A1: a in [#]A \ m;
A2: a in {a}-Ideal by IDEAL_1:66;
0.A in m by IDEAL_1:3; then
A4: a+0.A in {x+y where x,y is Element of A :x in {a}-Ideal & y in m} by A2;
reconsider a as Element of A;
A5: a in {a}-Ideal + m by A4,IDEAL_1:def 19;
{a}-Ideal + m=m or {a}-Ideal+m is non proper by IDEAL_1:74,RING_1:def 3;
hence thesis by A1,A5,XBOOLE_0:def 5;
end;
::[AM] prop 1.6 ii)
theorem
(for a holds a in m implies 1.A + a is Unit of A) implies A is local
proof
assume
A1: (for a holds a in m implies 1.A + a is Unit of A);
for x holds x in [#]A \ m implies x is Unit of A
proof
let x;
assume
A2: x in [#]A \ m; then
reconsider a0=x as Element of A;
{a0}-Ideal + m = [#]A by A2,Th18; then
1.A in {a0}-Ideal + m; then
1.A in {p+q where p,q is Element of A:
p in {a0}-Ideal & q in m } by IDEAL_1:def 19; then
consider p,q be Element of A such that
A3: 1.A = p+q and
A4: p in {a0}-Ideal and
A5: q in m;
A6: {a0}-Ideal = the set of all a0*s where s is Element of A by IDEAL_1:64;
consider s be Element of A such that
A7: p = a0 * s by A4,A6;
1.A+(-q) = a0*s+(-q+q) by RLVECT_1:def 3,A3,A7
.= a0*s+0.A by RLVECT_1:5 .= a0*s; then
a0*s is Unit of A by A1,A5,IDEAL_1:13; then
{a0*s}-Ideal = [#]A by RING_2:20; then
A9: 1.A in {a0*s}-Ideal;
{a0*s}-Ideal = the set of all (a0*s)*t where t is Element of A
by IDEAL_1:64; then
consider t1 be Element of A such that
A11: 1.A = (a0*s)*t1 by A9;
A12: a0*(s*t1) = 1.A by A11,GROUP_1:def 3;
reconsider t = s*t1 as Element of A;
1.A in {a0}-Ideal by A6,A12; then
not {a0}-Ideal is proper by IDEAL_1:19; then
{a0}-Ideal = [#]A;
hence thesis by RING_2:20;
end;
hence thesis by Th17;
end;
definition
let R;
let E be Subset of R;
func PrimeIdeals(R,E) -> Subset of Spectrum R equals :Def5:
{p where p is Ideal of R: p is quasi-prime & p <> [#]R & E c= p}
if R is non degenerated
otherwise {};
coherence
proof
set X = {p where p is Ideal of R: p is quasi-prime & p <> [#]R & E c=p};
thus R is non degenerated implies
{p where p is Ideal of R: p is quasi-prime & p <> [#]R & E c=p}
is Subset of Spectrum R
proof
assume
A1: R is non degenerated;
X c= Spectrum R
proof
let x be object;
assume x in X; then
consider p be Ideal of R such that
A3: x = p and
A4: p is quasi-prime and
A5: p <> [#]R and
E c= p;
p in {p where p is Ideal of R: p is quasi-prime & p <> [#]R} by A4,A5;
hence thesis by A3,A1,Def3;
end;
hence thesis;
end;
thus thesis by XBOOLE_1:2;
end;
consistency;
end;
definition
let A;
let E be Subset of A;
redefine func PrimeIdeals(A,E) -> Subset of Spectrum A equals :: redefines PrimeIdeals (TOPZARI1, definition)
{p where p is prime Ideal of A: E c=p };
correctness
proof
set C = {p where p is Ideal of A: p is quasi-prime & p <> [#]A & E c=p};
A1: x in PrimeIdeals(A,E) implies x in {p where p is prime Ideal of A: E c=p }
proof
assume x in PrimeIdeals(A,E); then
A3: x in C by Def5;
consider I being Ideal of A such that
A4: x = I and
A5: I is quasi-prime and
A6: I <> [#]A and
A7: E c= I by A3;
reconsider I as prime Ideal of A by A5,A6,RING_1:def 2,SUBSET_1:def 6;
I in {p where p is prime Ideal of A: E c=p } by A7;
hence thesis by A4;
end;
x in {p where p is prime Ideal of A: E c=p } implies x in PrimeIdeals(A,E)
proof
assume x in {p where p is prime Ideal of A: E c=p }; then
consider I be prime Ideal of A such that
A9: I = x and
A10: E c= I;
I in C by A10;
hence thesis by A9,Def5;
end;
hence thesis by TARSKI:2,A1;
end;
end;
registration
let A,J;
cluster PrimeIdeals(A,J) -> non empty;
coherence
proof
consider m be prime Ideal of A such that
A1: J c= m by Th11;
m in PrimeIdeals(A,J) by A1;
hence thesis;
end;
end;
Th21:
PrimeIdeals(A,{0.A}) = Spectrum A
proof
Spectrum A c= PrimeIdeals(A,{0.A})
proof
let x;
assume x in Spectrum A; then
consider J being prime Ideal of A such that
A3: J = x;
{0.A} c= J by IDEAL_1:2, ZFMISC_1:31;
hence thesis by A3;
end;
hence thesis;
end;
Th22:
x in Spectrum A implies x is prime Ideal of A
proof
assume x in Spectrum A; then
consider x1 being prime Ideal of A such that
A2: x1 = x;
thus thesis by A2;
end;
reserve p for prime Ideal of A;
reserve k for non zero Nat;
theorem Th23:
not a in p implies not a|^k in p
proof
assume
A1: not a in p;
not a|^k in p
proof
defpred P[Nat] means not a|^$1 in p;
A2: P[1] by A1,BINOM:8;
A3: for k holds P[k] implies P[k+1]
proof
let k;
assume
A4: P[k];
A5: a|^(k+1) = (a|^k)*(a|^1) by BINOM:10;
not (a|^1) in p by A1,BINOM:8;
hence thesis by A4,A5,RING_1:def 1;
end;
for k holds P[k] from NAT_1:sch 10(A2,A3);
hence thesis;
end;
hence thesis;
end;
Lm24:
a|^n in p implies n <> 0
proof
assume
A1: a|^n in p;
assume n = 0; then
a|^n = 1_A by BINOM:8; then
A5: {1.A} c= p by A1,TARSKI:def 1;
p-Ideal = p by IDEAL_1:44; then
{1.A}-Ideal c= p by A5,IDEAL_1:57; then
the carrier of A = p by IDEAL_1:51; then
p is non proper;
hence contradiction;
end;
begin :: Nilradical & Jacobson Radical
definition
let A;
func nilrad A -> Subset of A equals
the set of all a where a is nilpotent Element of A;
coherence
proof
set M = the set of all a where a is nilpotent Element of A;
M c= the carrier of A
proof
let x be object;
assume x in M; then
ex a being nilpotent Element of A st a = x;
hence thesis;
end;
hence thesis;
end;
end;
Lm25:
a is nilpotent implies a in sqrt({0.A})
proof
set N = {a where a is Element of A:
ex n being Element of NAT st a|^n in {0.A}};
assume a is nilpotent; then
consider n being non zero Nat such that
A2: a|^n = 0.A;
A3: {0.A} = {0.A}-Ideal by IDEAL_1:47;
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider s = a as Element of A;
s|^n in {0.A} by A2,A3,IDEAL_1:66; then
a in N;
hence a in sqrt({0.A}) by IDEAL_1:def 24;
end;
Lm26:
a|^n in {0.A} implies n <> 0
proof
assume
A1: a|^n in {0.A};
assume n = 0; then
1_A in {0.A} by A1, BINOM:8;
hence contradiction by TARSKI:def 1;
end;
theorem Th27:
nilrad A = sqrt({0.A})
proof
set N ={a where a is Element of A: ex n being Element of NAT st a|^n in {0.A}};
A1: for a be object st a in nilrad A holds a in sqrt({0.A})
proof
let a be object;
assume a in nilrad A; then
consider s being nilpotent Element of A such that
A3: s = a;
thus thesis by A3, Lm25;
end;
for a be object st a in sqrt({0.A}) holds a in nilrad A
proof
let a be object;
assume a in sqrt({0.A}); then
a in N by IDEAL_1:def 24; then
consider s being Element of A such that
A7: s = a & ex n being Element of NAT st s|^n in {0.A};
consider n be Element of NAT such that
A8: s|^n in {0.A} by A7;
A9: s|^n = 0.A by A8,TARSKI:def 1;
n is non zero Nat by A8,Lm26; then
s is nilpotent by A9;
hence thesis by A7;
end;
hence thesis by A1,TARSKI:2;
end;
registration
let A;
cluster nilrad A -> non empty;
coherence
proof
sqrt({0.A}) is non empty;
hence thesis by Th27;
end;
end;
registration
let A;
cluster nilrad A -> add-closed for Subset of A;
coherence
proof
reconsider S = sqrt({0.A}) as Ideal of A;
S = nilrad A by Th27;
hence thesis;
end;
end;
registration
let A;
cluster nilrad A -> left-ideal right-ideal for Subset of A;
coherence
proof
reconsider S = sqrt({0.A}) as Ideal of A;
S = nilrad A by Th27;
hence thesis;
end;
end;
::::: [AM] Prop 1.14
theorem Th28:
sqrt J = meet PrimeIdeals(A,J)
proof
for x be object st x in sqrt J holds x in meet PrimeIdeals(A,J)
proof
let x be object;
assume x in sqrt J; then
x in {a where a is Element of A: ex n be Element of NAT st a|^n in J}
by IDEAL_1:def 24; then
consider y be Element of A such that
A2: y = x and
A3: ex n being Element of NAT st y|^n in J;
consider k be Element of NAT such that
A4: y|^k in J by A3;
y in meet PrimeIdeals(A,J)
proof
for Y be set holds Y in PrimeIdeals(A,J) implies y in Y
proof
let Y be set;
Y in PrimeIdeals(A,J) implies y in Y
proof
assume Y in PrimeIdeals(A,J); then
consider Y1 be prime Ideal of A such that
A6: Y1 = Y and
A7: J c= Y1;
reconsider k as non zero Nat by A4,A7,Lm24;
y|^k in Y1 by A4,A7;
hence thesis by A6,Th23;
end;
hence thesis;
end;
hence thesis by SETFAM_1:def 1;
end;
hence thesis by A2;
end; then
A9: sqrt J c= meet PrimeIdeals(A,J);
set N1 = meet PrimeIdeals(A,J);
for x be object st not x in sqrt J holds not x in N1
proof
let x be object;
assume
A10: not x in sqrt J;
per cases;
suppose x in A; then
reconsider x1 = x as Element of A;
consider p be prime Ideal of A such that
A12: not x1 in p and
A13: J c= p by A10,Th9;
p in PrimeIdeals(A,J) by A13;
hence thesis by A12, SETFAM_1:def 1;
end;
suppose
A15: not x in A;
not x in N1
proof
assume
A16: x in N1;
consider m be prime Ideal of A such that
A17: J c= m by Th11;
m in PrimeIdeals(A,J) by A17; then
x in m by A16,SETFAM_1:def 1;
hence contradiction by A15;
end;
hence thesis;
end;
end; then
meet PrimeIdeals(A,J) c= sqrt J;
hence thesis by A9;
end;
::::: [AM] Prop 1.8
theorem
nilrad A = meet Spectrum A
proof
reconsider I = {0.A} as proper Ideal of A by SUBSET_1:def 6;
nilrad A = sqrt({0.A}) by Th27 .= meet PrimeIdeals(A,I) by Th28
.= meet Spectrum A by Th21;
hence thesis;
end;
:::[AM] Ex 1.13 i)
theorem Th30:
I c= sqrt I
proof
let x be object;
assume
A1: x in I; then
reconsider x as Element of A;
x|^1 in I by A1,BINOM:8; then
x in {a where a is Element of A: ex n being
Element of NAT st a|^n in I};
hence thesis by IDEAL_1:def 24;
end;
theorem
I c= J implies sqrt I c= sqrt J
proof
assume
A1: I c= J;
let s be object;
assume
A2: s in sqrt I; then
reconsider s as Element of A;
s in {a where a is Element of A:
ex n being Element of NAT st a|^n in I } by A2,IDEAL_1:def 24; then
consider s1 be Element of A such that
A3: s1 = s and
A4: ex n being Element of NAT st s1|^n in I;
consider n1 be Element of NAT such that
A5: s1|^n1 in I by A4;
n1 <> 0
proof
assume n1 = 0; then
s1|^n1 = 1_A by BINOM:8;
hence contradiction by A1,A5,IDEAL_1:19;
end; then
reconsider n1 as non zero Nat;
s1 in {a where a is Element of A:ex n being Element of NAT st a|^n in J}
by A1,A5;
hence thesis by A3,IDEAL_1:def 24;
end;
definition
let A;
func J-Rad A -> Subset of A equals
meet m-Spectrum A;
coherence;
end;
begin :: Construction of Zariski Topology of the Prime Spectrum of A (Spec A)
theorem Th32:
PrimeIdeals(A,S) c= Ideals(A,S)
proof
let x be object;
assume x in PrimeIdeals(A,S); then
consider x1 be prime Ideal of A such that
A2: x1 = x and
A3: S c= x1;
thus thesis by A2, A3;
end;
theorem Th33:
PrimeIdeals(A,S) = Ideals(A,S) /\ Spectrum A
proof
thus PrimeIdeals(A,S) c= Ideals(A,S) /\ Spectrum A
proof
let x be object;
assume
A2: x in PrimeIdeals(A,S); then
consider x1 be prime Ideal of A such that
A3: x1 = x and
S c= x1;
A4: x in Spectrum A by A3;
x in Ideals(A,S) by A2,Th32,TARSKI:def 3;
hence thesis by A4,XBOOLE_0:def 4;
end;
let x be object;
assume x in Ideals(A,S) /\ Spectrum A; then
A8: x in Ideals(A,S) & x in Spectrum A by XBOOLE_0:def 4; then
consider x1 be Ideal of A such that
A10: x1 = x and
A11: S c= x1;
x1 is prime Ideal of A by A8,Th22,A10;
hence thesis by A10,A11;
end;
:: [AM] p.12 Ex15 i)
theorem Th34:
PrimeIdeals(A,S) = PrimeIdeals(A,S-Ideal)
proof
PrimeIdeals(A,S) = Ideals(A,S) /\ Spectrum A by Th33
.= Ideals(A,S-Ideal) /\ Spectrum A by Th2
.= PrimeIdeals(A,S-Ideal) by Th33;
hence thesis;
end;
theorem Th35:
I c= p implies sqrt I c= p
proof
assume
A1: I c= p;
let s be object;
assume
A2: s in sqrt I; then
reconsider s as Element of A;
s in {a where a is Element of A:
ex n being Element of NAT st a|^n in I } by A2,IDEAL_1:def 24; then
consider s1 be Element of A such that
A3: s1 = s and
A4: ex n being Element of NAT st s1|^n in I;
consider n1 be Element of NAT such that
A5: s1|^n1 in I by A4;
n1 <> 0
proof
assume n1 = 0; then
s1|^n1 = 1_A by BINOM:8;
hence contradiction by A1,A5,IDEAL_1:19;
end; then
reconsider n1 as non zero Nat;
s1|^n1 in p by A1,A5;
hence thesis by A3,Th23;
end;
theorem Th36:
sqrt I c= p implies I c= p
proof
assume
A1: sqrt I c= p;
I c= sqrt I by Th30;
hence thesis by A1;
end;
:: [AM] p.12 Ex15 i)
theorem Th37:
PrimeIdeals(A,sqrt(S-Ideal)) = PrimeIdeals(A,S-Ideal)
proof
thus PrimeIdeals(A,sqrt(S-Ideal)) c= PrimeIdeals(A,S-Ideal)
proof
let p be object;
assume p in PrimeIdeals(A,sqrt(S-Ideal)); then
consider p1 be prime Ideal of A such that
A3: p1 = p and
A4: sqrt(S-Ideal) c= p1;
S-Ideal c= p1 by A4,Th36;
hence p in PrimeIdeals(A,S-Ideal) by A3;
end;
let p be object;
assume p in PrimeIdeals(A,S-Ideal); then
consider p1 be prime Ideal of A such that
A7: p1 = p and
A8: S-Ideal c= p1;
sqrt(S-Ideal) c= p1 by A8,Th35;
hence p in PrimeIdeals(A,sqrt(S-Ideal)) by A7;
end;
theorem Th38:
E2 c= E1 implies PrimeIdeals(A,E1) c= PrimeIdeals(A,E2)
proof
assume
A1: E2 c= E1;
let x;
assume x in PrimeIdeals(A,E1); then
consider x1 be prime Ideal of A such that
A3: x1 = x and
A4: E1 c= x1;
E2 c= x1 by A1,A4;
hence thesis by A3;
end;
::[AM] p.12 Ex.17 iv) not yet introduce X_f = PrimeIdeals(A,{f})
theorem
PrimeIdeals(A,J1) = PrimeIdeals(A,J2) iff sqrt J1 = sqrt J2
proof
thus PrimeIdeals(A,J1) = PrimeIdeals(A,J2) implies sqrt J1 = sqrt J2
proof
assume
A2: PrimeIdeals(A,J1) = PrimeIdeals(A,J2);
sqrt J1 = meet PrimeIdeals(A,J1) by Th28
.= sqrt J2 by Th28,A2;
hence thesis;
end;
assume
A3: sqrt J1 = sqrt J2;
PrimeIdeals(A,J1) = PrimeIdeals(A,J1-Ideal) by IDEAL_1:44
.= PrimeIdeals(A,sqrt(J1-Ideal)) by Th37
.= PrimeIdeals(A,sqrt J1) by IDEAL_1:44
.= PrimeIdeals(A,sqrt(J2-Ideal)) by A3,IDEAL_1:44
.= PrimeIdeals(A,J2-Ideal) by Th37
.= PrimeIdeals(A,J2) by IDEAL_1:44;
hence thesis;
end;
::[AM] Prop 1.11 ii) case of n=2
theorem Th40:
I1 *' I2 c= p implies I1 c= p or I2 c= p
proof
not(I1 c= p or I2 c= p) implies not(I1 *' I2 c= p)
proof
assume
A1: not (I1 c= p or I2 c= p); then
consider x1 be object such that
A2: x1 in I1 and
A3: not x1 in p;
consider x2 be object such that
A4: x2 in I2 and
A5: not x2 in p by A1;
reconsider x1 as Element of A by A2;
reconsider x2 as Element of A by A4;
reconsider x = x1*x2 as Element of the carrier of A;
reconsider seq=<* x *> as FinSequence of the carrier of A;
A6: Sum seq = x by BINOM:3;
A8: for i being Element of NAT st 1 <= i & i <= len seq
ex a,b being Element of A st seq.i = a*b & a in I1 & b in I2
proof
let i be Element of NAT;
assume that
A9: 1 <= i and
A10: i <= len seq;
A11: i <= 1 by A10,FINSEQ_1:40;
seq.i = seq.1 by A9,XXREAL_0:1, A11 .= x1*x2 by FINSEQ_1:40;
hence thesis by A2,A4;
end;
A12: Sum seq in
{Sum s where s is FinSequence of the carrier of A : for i being
Element of NAT st 1 <= i & i <= len s ex a,b be Element of A
st s.i = a*b & a in I1 & b in I2} by A8;
x1*x2 in I1 *' I2 by A6,A12,IDEAL_1:def 21;
hence thesis by A3,A5,RING_1:def 1;
end;
hence thesis;
end;
::[AM] p.12 Ex.15 ii)
theorem Th41A:
PrimeIdeals(A,{1.A}) = {}
proof
assume PrimeIdeals(A,{1.A}) <> {}; then
consider p be object such that
A2: p in PrimeIdeals(A,{1.A}) by XBOOLE_0:def 1;
consider p1 be prime Ideal of A such that
p1 = p and
A3: {1.A} c= p1 by A2;
1.A in {1.A} by TARSKI:def 1;
hence contradiction by A3,IDEAL_1:19;
end;
Th41:
ex E be non empty Subset of A st {} = PrimeIdeals(A,E)
proof
take {1.A};
thus thesis by Th41A;
end;
::[AM] p.12 Ex.15 ii)
theorem
Spectrum A = PrimeIdeals(A,{0.A}) by Th21;
Th42:
ex E be non empty Subset of A st Spectrum A = PrimeIdeals(A,E)
proof
take {0.A};
thus thesis by Th21;
end;
::[AM] p.12 Ex.15 iv)
theorem Th43:
for E1,E2 be non empty Subset of A holds
ex E3 be non empty Subset of A st
PrimeIdeals(A,E1) \/ PrimeIdeals(A,E2) = PrimeIdeals(A,E3)
proof
let E1,E2 be non empty Subset of A;
set F1 = PrimeIdeals(A,E1);
set F2 = PrimeIdeals(A,E2);
set I1 = E1-Ideal;
set I2 = E2-Ideal;
reconsider I3 = I1 *' I2 as Ideal of A;
A4: PrimeIdeals(A,E1) = PrimeIdeals(A,I1) by Th34;
A5: PrimeIdeals(A,I3) c= PrimeIdeals(A,I1) \/ PrimeIdeals(A,I2)
proof
let x be object;
assume x in PrimeIdeals(A,I3); then
consider x1 be prime Ideal of A such that
A7: x1 = x and
A8: I3 c= x1;
A9: I1 c= x1 or I2 c= x1 by A8,Th40;
x1 in {p where p is prime Ideal of A: I1 c= p } or
x1 in {p where p is prime Ideal of A: I2 c= p } by A9;
hence thesis by A7,XBOOLE_0:def 3;
end;
A11:PrimeIdeals(A,I1) \/ PrimeIdeals(A,I2) c= PrimeIdeals(A,I3)
proof
A12: I1*'I2 c= I1 /\ I2 by IDEAL_1:79;
I1 /\ I2 c= I1 by XBOOLE_1:17; then
A13: I1*'I2 c= I1 by A12;
I1 /\ I2 c= I2 by XBOOLE_1:17; then
I1*'I2 c= I2 by A12; then
A14: PrimeIdeals(A,I2) c= PrimeIdeals(A,I1*'I2) by Th38;
PrimeIdeals(A,I1) c= PrimeIdeals(A,I1*'I2) by A13,Th38;
hence thesis by A14,XBOOLE_1:8;
end;
PrimeIdeals(A,I3) =
PrimeIdeals(A,E1) \/ PrimeIdeals(A,E2) by A4,A5,A11,Th34;
hence thesis;
end;
::[AM] p.12 Ex.15 iii)
theorem Th44:
for G being Subset-Family of Spectrum A st
for S being set st S in G holds
(ex E be non empty Subset of A st S = PrimeIdeals(A,E))
holds ex F be non empty Subset of A st Intersect G = PrimeIdeals(A,F)
proof
let G be Subset-Family of Spectrum A;
assume
A1: for S being set st S in G holds
(ex E be non empty Subset of A st S = PrimeIdeals(A,E));
per cases;
suppose
A2: G <> {}; then
consider o such that
A3: o in G by XBOOLE_0:def 1;
reconsider o as set by A3;
consider E be non empty Subset of A such that
A4: o = PrimeIdeals(A,E) by A1,A3;
A5: meet G = Intersect G by A2,SETFAM_1:def 9;
defpred X[set] means ex Z being non empty Subset of A
st $1 = Z & ex D be set st D in G & D = PrimeIdeals(A,Z);
consider SFE being set such that
A6: for x being set holds x in SFE iff x in bool the carrier of A &
X[x] from XFAMILY:sch 1;
SFE c= bool the carrier of A by A6; then
reconsider SFE as non empty Subset-Family of the carrier of A
by A3,A4,A6;
E c= union SFE by ZFMISC_1:74,A3,A4,A6; then
A8: union SFE is non empty Subset of A;
A9: x in Intersect G implies x in PrimeIdeals(A,union SFE)
proof
assume
A10: x in Intersect G; then
A11: x in meet G by A2,SETFAM_1:def 9;
reconsider x as prime Ideal of A by A10,Th22;
union SFE c= x
proof
let o1;
assume o1 in union SFE; then
consider Y be set such that
A13: o1 in Y and
A14: Y in SFE by TARSKI:def 4;
consider Z being non empty Subset of A such that
A15: Z = Y and
A16: ex D be set st D in G & D = PrimeIdeals(A,Z) by A6,A14;
consider D be set such that
A17: D in G and
A18: D = PrimeIdeals(A,Z) by A16;
x in D by A17,A11,SETFAM_1:def 1; then
consider x1 be prime Ideal of A such that
A19: x1 = x and
A20: Z c= x1 by A18;
thus thesis by A13,A15,A20,A19;
end;
hence thesis;
end;
x in PrimeIdeals(A,union SFE) implies x in Intersect G
proof
assume
A23: x in PrimeIdeals(A,union SFE);
for Y be set holds Y in G implies x in Y
proof
let Y be set;
assume
A24: Y in G; then
consider E be non empty Subset of A such that
A25: Y = PrimeIdeals(A,E) by A1;
E c= union SFE by A6,A24,A25,ZFMISC_1:74; then
PrimeIdeals(A,union SFE) c= PrimeIdeals(A,E) by Th38;
hence thesis by A25,A23;
end;
hence thesis by A2,A5,SETFAM_1:def 1;
end;
hence thesis by A8,A9,TARSKI:2;
end;
suppose G = {}; then
Intersect G = Spectrum A by SETFAM_1:def 9;
hence thesis by Th42;
end;
end;
::[AM] p.12 Ex.15
definition
let A;
func ZariskiTS(A) -> strict TopSpace means :Def7:
the carrier of it = Spectrum A &
for F being Subset of it holds F is closed iff
(ex E be non empty Subset of A st F = PrimeIdeals(A,E));
existence
proof
defpred C[set] means
ex Z being non empty Subset of A st $1 = PrimeIdeals(A,Z);
A1: for F1,F2 being set st C[F1] & C[F2] holds C[F1 \/ F2] by Th43;
A2: for G being Subset-Family of Spectrum A st for S being set st S in G holds
C[S] holds C[Intersect G] by Th44;
A3: C[{}] & C[Spectrum A] by Th41,Th42;
consider T being strict TopSpace such that
A4: the carrier of T = Spectrum A & for E being Subset of T holds E is closed
iff C[E] from TOPGEN_3:sch 1(A3,A1,A2);
take T;
thus the carrier of T = Spectrum A by A4;
let F be Subset of T;
thus thesis by A4;
end;
correctness
proof
let T1,T2 be strict TopSpace such that
A5: the carrier of T1 = Spectrum A and
A6: for F being Subset of T1 holds F is closed iff
ex Z1 being non empty Subset of A st F = PrimeIdeals(A,Z1) and
A7: the carrier of T2 = Spectrum A and
A8: for F being Subset of T2 holds F is closed iff
ex Z2 being non empty Subset of A st F = PrimeIdeals(A,Z2);
now
let F be set;
F is closed Subset of T1 iff
ex Z1 be non empty Subset of A st F = PrimeIdeals(A,Z1) by A5,A6;
hence F is closed Subset of T1 iff F is closed Subset of T2 by A7,A8;
end;
hence thesis by TOPGEN_3:6;
end;
end;
registration
let A;
cluster ZariskiTS(A) -> non empty;
coherence
proof
[#]ZariskiTS(A) = Spectrum A by Def7;
hence thesis;
end;
end;
Lm44:
for P being Point of ZariskiTS A holds P is prime Ideal of A
proof
let P be Point of ZariskiTS A;
P in [#]ZariskiTS A; then
P in Spectrum A by Def7;
hence thesis by Th22;
end;
theorem Th45:
for P,Q being Point of ZariskiTS A st P <> Q holds
ex V being Subset of ZariskiTS A
st V is open & ( P in V & not Q in V or Q in V & not P in V )
proof
let P,Q be Point of ZariskiTS A;
reconsider P1=P, Q1=Q as prime Ideal of A by Lm44;
assume P <> Q; then
per cases;
suppose not Q c= P; then
Q \ P <> {} by XBOOLE_1:37; then
consider x such that
A3: x in Q \ P by XBOOLE_0:def 1;
x in Q1 by A3; then
reconsider x as Element of A;
PrimeIdeals(A,{x}-Ideal) is closed Subset of ZariskiTS A by Def7; then
reconsider W = [#]ZariskiTS A \ PrimeIdeals(A,{x}-Ideal) as
open Subset of ZariskiTS A by PRE_TOPC:def 3;
A5: not x in P by XBOOLE_0:def 5,A3;
A6: not P in PrimeIdeals(A,{x}-Ideal)
proof
assume P in PrimeIdeals(A,{x}-Ideal); then
consider P0 be prime Ideal of A such that
A8: P = P0 and
A9: {x}-Ideal c= P0;
thus contradiction by A5,IDEAL_1:66,A8,A9;
end;
{x}-Ideal c= Q1-Ideal by A3,ZFMISC_1:31,IDEAL_1:57; then
{x}-Ideal c= Q1 by IDEAL_1:44; then
Q in PrimeIdeals(A,{x}-Ideal); then
P in W & not Q in W by A6,XBOOLE_0:def 5;
hence thesis;
end;
suppose Q c= P & Q <> P; then
Q c< P; then
consider x such that
A13: x in P and
A14: not x in Q by XBOOLE_0:6;
x in P1 by A13; then
reconsider x as Element of A;
PrimeIdeals(A,{x}-Ideal) is closed Subset of ZariskiTS A by Def7; then
reconsider W = [#]ZariskiTS A \ PrimeIdeals(A,{x}-Ideal)
as open Subset of ZariskiTS A by PRE_TOPC:def 3;
A16: not Q in PrimeIdeals(A,{x}-Ideal)
proof
assume Q in PrimeIdeals(A,{x}-Ideal); then
consider Q0 be prime Ideal of A such that
A18: Q = Q0 and
A19: {x}-Ideal c= Q0;
thus contradiction by A14,IDEAL_1:66,A18,A19;
end;
{x}-Ideal c= P1-Ideal by A13,ZFMISC_1:31,IDEAL_1:57; then
{x}-Ideal c= P1 by IDEAL_1:44; then
P in PrimeIdeals(A,{x}-Ideal); then
Q in W & not P in W by A16,XBOOLE_0:def 5;
hence thesis;
end;
end;
registration
cluster degenerated for commutative Ring;
existence
proof
take the trivial commutative Ring;
thus thesis;
end;
end;
registration let R be degenerated commutative Ring;
cluster ADTS Spectrum R -> T_0;
coherence
proof
ADTS Spectrum R is empty by Def3;
hence thesis;
end;
end;
::[AM] p.13 Ex18 iv)
registration let A;
cluster ZariskiTS A -> T_0;
coherence
proof
for P,Q being Point of ZariskiTS(A) st P <> Q holds
ex V being Subset of ZariskiTS (A) st V is open &
( P in V & not Q in V or Q in V & not P in V ) by Th45;
hence thesis by T_0TOPSP:def 7;
end;
end;
begin :: Continuous Map ZariskiTS B -> ZariskiTS A
:: associated with a ring homomorphism.
reserve M0 for Ideal of B;
Lm48:
for x,y be Element of the carrier of A,h st h is RingHomomorphism &
x in h"M0 & y in h"M0 holds x + y in h"M0
proof
let x,y be Element of the carrier of A;
let h;
assume that
A1: h is RingHomomorphism and
A2: x in h"M0 and
A3: y in h"M0;
A4: h.x in M0 by A2,FUNCT_1:def 7;
A5: h.y in M0 by A3,FUNCT_1:def 7;
reconsider a=x,b=y as Element of A;
A6: h is additive by A1;
h.x + h.y in M0 by A4,A5,IDEAL_1:def 1; then
A8: h.(x+y) in M0 by A6;
x+y in A; then
x+y in dom h by FUNCT_2:def 1;
hence thesis by A8,FUNCT_1:def 7;
end;
Lm49:
for r,x be Element of A,h st h is RingHomomorphism &
x in h"M0 holds r*x in h"M0
proof
let r,x be Element of A;
let h;
assume that
A1: h is RingHomomorphism and
A2: x in h"M0;
h.x in M0 by A2,FUNCT_1:def 7; then
A5: h.r * h.x in M0 by IDEAL_1:def 2;
h is multiplicative by A1; then
A6: h.(r*x) in M0 by A5;
r*x in A; then
r*x in dom h by FUNCT_2:def 1;
hence thesis by A6,FUNCT_1:def 7;
end;
theorem Th50:
h is RingHomomorphism implies h"M0 is Ideal of A
proof
assume
A1: h is RingHomomorphism; then
A2: h"M0 is add-closed by Lm48;
A3: h"M0 is left-ideal by A1,Lm49;
A6: dom (h) = the carrier of A by FUNCT_2:def 1;
h.0.A = 0.B by A1,RING_2:6; then
h.0.A in M0 by IDEAL_1:2; then
0.A in h"M0 by A6,FUNCT_1:def 7;
hence thesis by A2,A3;
end;
reserve M0 for prime Ideal of B;
theorem Th51:
h is RingHomomorphism implies h"M0 is prime Ideal of A
proof
assume
A1: h is RingHomomorphism;
A2: for x,y be Element of A st x*y in h"M0 holds x in h"M0 or y in h"M0
proof
let x,y be Element of A;
assume x*y in h"M0; then
x*y in dom(h) & h.(x*y) in M0 by FUNCT_1:def 7; then
A4: h.x * h.y in M0 by A1,GROUP_6:def 6;
A5: dom(h)= the carrier of A by FUNCT_2:def 1;
x in h"M0 or y in h"M0
proof
per cases by A4,RING_1:def 1;
suppose h.x in M0;
hence thesis by A5,FUNCT_1:def 7;
end;
suppose h.y in M0;
hence thesis by A5,FUNCT_1:def 7;
end;
end;
hence thesis;
end;
h"M0 <> the carrier of A
proof
assume
A9: h"M0 = the carrier of A;
A10: h is unity-preserving by A1;
1.B in M0 by A9,FUNCT_1:def 7,A10;
hence contradiction by IDEAL_1:19;
end; then
h"M0 is proper quasi-prime by A2;
hence thesis by A1,Th50;
end;
:: Spec h is continuous map of ZariskiTS B -> ZariskiTS A
:: associated with a ring homomorphism h:A->B.
::[AM] p.13 Ex22
definition ::: similar to "f from FUNCT_3
let A, B, h;
assume
A0: h is RingHomomorphism;
func Spec h -> Function of ZariskiTS B, ZariskiTS A means :Def9:
for x be Point of ZariskiTS B holds it.x = h"x;
existence
proof
defpred P[Point of ZariskiTS B,object] means $2 = h"$1;
A1: for x be Point of ZariskiTS B ex y be Point of ZariskiTS A st P[x,y]
proof
let x be Point of ZariskiTS B;
x is prime Ideal of B by Lm44; then
h"x is prime Ideal of A by A0,Th51; then
h"x in Spectrum A; then
reconsider y =h"x as Point of ZariskiTS A by Def7;
P[x,y];
hence thesis;
end;
consider f being Function of ZariskiTS B, ZariskiTS A such that
A2: for x being Point of ZariskiTS B holds P[x,f.x] from FUNCT_2:sch 3(A1);
thus thesis by A2;
end;
uniqueness
proof
let f,g be Function of ZariskiTS B, ZariskiTS A;
assume that
A3: for x be Point of ZariskiTS B holds f.x = h"x and
A4: for x be Point of ZariskiTS B holds g.x = h"x;
now
let x be Point of ZariskiTS B;
f.x = h"x by A3;
hence f.x = g.x by A4;
end;
hence thesis;
end;
end;
::[AM] p.13 Ex22 ii)
theorem Th52:
h is RingHomomorphism implies
(Spec h)"PrimeIdeals(A,E) = PrimeIdeals(B,h.:E)
proof
assume
A1: h is RingHomomorphism;
thus (Spec h)"PrimeIdeals(A,E) c= PrimeIdeals(B,h.:E)
proof
let x;
assume
A3: x in (Spec h)"PrimeIdeals(A,E); then
A4: x in dom (Spec h) & (Spec h).x in PrimeIdeals(A,E) by FUNCT_1:def 7;
reconsider x1 = x as Point of ZariskiTS B by A3;
h"x1 in {p where p is prime Ideal of A: E c=p } by A1, Def9, A4; then
consider q be prime Ideal of A such that
A6: q = h"x1 and
A7: E c= q;
A8: h.:E c= h.:(h"x1) by A6,A7,RELAT_1:123;
h.:(h"x1) c= x1 by FUNCT_1:75; then
A9: h.:E c= x1 by A8;
x1 in the carrier of ZariskiTS B; then
x1 in Spectrum B by Def7; then
x1 is prime Ideal of B by Th22;
hence thesis by A9;
end;
let x;
assume x in PrimeIdeals(B,h.:E); then
consider q be prime Ideal of B such that
A12: x = q and
A13: h.:E c= q;
A14: h"(h.:E) c= h"q by A13,RELAT_1:143;
E c= h"(h.:E) by FUNCT_2:42; then
A15: E c= h"q by A14;
h"q is prime Ideal of A by A1,Th51; then
A17: h"q in PrimeIdeals(A,E) by A15;
A18: dom(Spec h) = the carrier of ZariskiTS B by FUNCT_2:def 1;
q in Spectrum B; then
reconsider q1 = q as Point of ZariskiTS B by Def7;
(Spec h).q1 in PrimeIdeals(A,E) by A17,A1,Def9;
hence thesis by A12,A18,FUNCT_1:def 7;
end;
::[AM] p.13 Ex22 i)
theorem
h is RingHomomorphism implies Spec h is continuous
proof
assume
A1: h is RingHomomorphism;
for P1 being Subset of ZariskiTS A st P1 is closed holds
(Spec h)" P1 is closed
proof
let P1 be Subset of ZariskiTS A;
assume P1 is closed; then
consider E be non empty Subset of A such that
A3: P1 = PrimeIdeals(A,E) by Def7;
A4: dom h = the carrier of A by FUNCT_2:def 1;
(Spec h)"P1 = PrimeIdeals(B,h.:E) by A3,A1,Th52; then
consider E1 be non empty Subset of B such that
E1 = h.:E and
A5: (Spec h)"P1 = PrimeIdeals(B,E1) by A4;
thus thesis by A5,Def7;
end;
hence thesis by PRE_TOPC:def 6;
end;