begin
This file deals with the definition of the topology on the set of prime ideals. It defines the topology, computes the closed sets and the closure and interior operators.
Spectrum
The prime spectrum of a ring is the set of its prime ideals, which serves as the carrier set of the Zariski topology.
We define the spectrum as the collection of prime ideals of the ring.
definition (in ring0)
\( Spec \equiv \{I\in \mathcal{I} .\ I\triangleleft _pR\} \)
Zariski topology
The Zariski topology on the spectrum is generated by D-sets, one for each ideal of the ring.
The basic set that defines the topoogy is given by the D operator
definition (in ring0)
\( S\subseteq R \Longrightarrow D(S) \equiv \{I\in Spec.\ \neg (S\subseteq I)\} \)
The D operator preserves subsets
lemma (in ring0) D_operator_preserve_subset:
assumes \( S \subseteq T \), \( T\subseteq R \)
shows \( D(S) \subseteq D(T) \)proof from assms have S: \( S\subseteq R \)
fix \( x \)
assume \( x\in D(S) \)
then have x: \( x\in Spec \), \( \neg (S\subseteq x) \) using openBasic_def, S
with assms(1) have \( x\in Spec \), \( \neg (T\subseteq x) \)
then show \( x:D(T) \) using openBasic_def, assms(2)
qed
The D operator values can be obtained by considering only ideals. This is useful as we have operations on ideals that we do not have on subsets.
lemma (in ring0) D_operator_only_ideals:
assumes \( T\subseteq R \)
shows \( D(T) = D(\langle T\rangle _I) \)proof have T: \( T\subseteq \langle T\rangle _I \), \( \langle T\rangle _I \subseteq R \) using generated_ideal_contains_set, assms, generated_ideal_is_ideal, assms, ideal_dest_subset
with D_operator_preserve_subset show \( D(T) \subseteq D(\langle T\rangle _I) \)
{
fix \( t \)
assume \( t\in D(\langle T\rangle _I) \)
with T(2) have t: \( t\in Spec \), \( \neg (\langle T\rangle _I \subseteq t) \) using openBasic_def
{
assume as: \( T \subseteq t \)
from t(1) have \( t\triangleleft R \) unfolding Spec_def, primeIdeal_def
with as have \( \langle T\rangle _I \subseteq t \) using generated_ideal_small
with t(2) have \( False \)
then have \( \neg (T \subseteq t) \)
with t(1) have \( t\in D(T) \) using openBasic_def, assms
then show \( D(\langle T\rangle _I) \subseteq D(T) \)
qed
The intersection of to D-sets is the D-set on the product of ideals
lemma (in ring0) intersection_open_basic:
assumes \( I\triangleleft R \), \( J\triangleleft R \)
shows \( D(I)\cap D(J) = D(I\cdot _IJ) \)proof have S: \( I\cdot _IJ \subseteq R \) using product_in_intersection(2), ideal_dest_subset, assms
{
fix \( K \)
assume K: \( K\in D(I)\cap D(J) \)
then have \( K\triangleleft _pR \), \( \neg (I\subseteq K) \), \( \neg (J\subseteq K) \) using assms, ideal_dest_subset, openBasic_def unfolding Spec_def
then have \( \neg (I\subseteq K) \), \( \neg (J\subseteq K) \), \( \forall I\in \mathcal{I} .\ \forall J\in \mathcal{I} .\ I\cdot _IJ\subseteq K \longrightarrow I \subseteq K \vee J \subseteq K \) unfolding primeIdeal_def
then have \( \neg (I\cdot _IJ\subseteq K) \) using assms using ideal_dest_subset
moreover
note K, S
ultimately have \( K\in D(I\cdot _IJ) \) using openBasic_def, ideal_dest_subset, assms(1), openBasic_def unfolding Spec_def
then show \( D(I)\cap D(J) \subseteq D(I\cdot _IJ) \)
{
fix \( K \)
assume Kass: \( K\in D(I\cdot _IJ) \)
with S have K: \( K\triangleleft _pR \), \( \neg (I\cdot _IJ\subseteq K) \) using openBasic_def unfolding Spec_def
{
assume \( I \subseteq K \vee J \subseteq K \)
then have \( I\cap J \subseteq K \)
then have \( I\cdot _IJ\subseteq K \) using product_in_intersection, assms
with K(2) have \( False \)
then have \( \neg (I\subseteq K) \), \( \neg (J\subseteq K) \)
with Kass, S have \( K\in D(I)\cap D(J) \) using assms, ideal_dest_subset, openBasic_def unfolding Spec_def
then show \( D(I \cdot _I J) \subseteq D(I) \cap D(J) \)
qed
The union of D-sets is the D-set of the sum of the ideals
lemma (in ring0) union_open_basic:
assumes \( \mathcal{J} \subseteq \mathcal{I} \)
shows \( \bigcup \{D(I).\ I\in \mathcal{J} \} = D(\oplus _I\mathcal{J} ) \)proof from assms have sub: \( \bigcup \mathcal{J} \subseteq R \)
then have \( \langle \bigcup \mathcal{J} \rangle _I\triangleleft R \) using generated_ideal_is_ideal
then have S: \( (\oplus _I\mathcal{J} ) \subseteq R \) using sumArbitraryIdeals_def, assms, ideal_dest_subset
{
fix \( t \)
assume \( t\in \bigcup \{D(I).\ I\in \mathcal{J} \} \)
then obtain \( K \) where K: \( K\in \mathcal{J} \), \( t\in D(K) \)
then have t: \( t\triangleleft _pR \), \( \neg (K\subseteq t) \) using assms, openBasic_def unfolding Spec_def
{
assume \( (\oplus _I\mathcal{J} ) \subseteq t \)
then have \( \bigcup \mathcal{J} \subseteq t \) using generated_ideal_contains_set, sub, sumArbitraryIdeals_def, assms
with K(1) have \( K \subseteq t \)
with t(2) have \( False \)
then have \( \neg ((\oplus _I\mathcal{J} ) \subseteq t) \)
moreover
note K, S
ultimately have \( t\in D(\oplus _I\mathcal{J} ) \) using openBasic_def, assms
then show \( \bigcup \{D(I).\ I\in \mathcal{J} \} \subseteq D(\oplus _I\mathcal{J} ) \)
{
fix \( t \)
assume as: \( t\in D(\oplus _I\mathcal{J} ) \)
with S have t: \( t\in Spec \), \( \neg ((\oplus _I\mathcal{J} )\subseteq t) \) using openBasic_def
{
assume \( \bigcup \mathcal{J} \subseteq t \)
with t(1) have \( \langle \bigcup \mathcal{J} \rangle _I \subseteq t \) using generated_ideal_small unfolding Spec_def, primeIdeal_def
with t(2) have \( False \) using sumArbitraryIdeals_def, assms
then obtain \( J \) where J: \( \neg (J \subseteq t) \), \( J\in \mathcal{J} \)
moreover
from J(2) have \( J\subseteq R \) using assms
moreover note t(1), J(1)
ultimately have \( t\in D(J) \) using openBasic_def
then have \( t:\bigcup \{D(I).\ I\in \mathcal{J} \} \) using J(2)
then show \( D(\oplus _I\mathcal{J} ) \subseteq \bigcup \{D(I).\ I\in \mathcal{J} \} \)
qed
From the previous results on intersection and union, we conclude that the D-sets we computed form a topology
corollary (in ring0) zariski_top:
shows \( \{D(J).\ J\in \mathcal{I} }\text{ is a topology \} \)proof{
}
}
fix \( M \)
assume \( M \subseteq \{D(J).\ J\in \mathcal{I} \} \)
then have \( M = \{D(J).\ J\in \{K\in \mathcal{I} .\ D(K)\in M\}\} \)
then have union: \( \bigcup M = \bigcup \{D(J).\ J\in \{K\in \mathcal{I} .\ D(K)\in M\}\} \)
have sub: \( \{K \in \mathcal{I} .\ D(K) \in M\} \subseteq \mathcal{I} \)
then have subR: \( \bigcup \{K \in \mathcal{I} .\ D(K) \in M\} \subseteq R \)
from sub, union have \( \bigcup M = D(\oplus _I\{K\in \mathcal{I} .\ D(K)\in M\}) \) using union_open_basic
moreover
from sub, subR have \( (\oplus _I\{K\in \mathcal{I} .\ D(K)\in M\})\triangleleft R \) using generated_ideal_is_ideal, sumArbitraryIdeals_def
then have \( (\oplus _I\{K\in \mathcal{I} .\ D(K)\in M\})\in \mathcal{I} \) using ideal_dest_subset
ultimately have \( \bigcup M:\{D(J).\ J\in \mathcal{I} \} \)
then have A: \( \bigwedge M.\ M \subseteq \{D(J).\ J\in \mathcal{I} \} \Longrightarrow \bigcup M\in \{D(J).\ J\in \mathcal{I} \} \)
{
fix \( x \) \( xa \)
assume as: \( x\triangleleft R \), \( xa\triangleleft R \)
then have \( D(x) \cap D(xa) = D(x\cdot _Ixa) \) using intersection_open_basic
moreover
have \( (x\cdot _Ixa) \triangleleft R \) using product_in_intersection(2), as
then have \( (x\cdot _Ixa):\mathcal{I} \) using ideal_dest_subset
ultimately have \( D(x) \cap D(xa)\in \{D(J).\ J\in \mathcal{I} \} \)
then have B: \( \bigwedge x xa.\ x\triangleleft R \Longrightarrow xa\triangleleft R \Longrightarrow D(x) \cap D(xa)\in \{D(J).\ J\in \mathcal{I} \} \)
from A, B show \( thesis \) unfolding IsATopology_def
qed
We include all the results of topology0 into ring0 under the namespace "zariski"
abbreviation (in ring0)
\( int(U) \equiv \text{Interior}(U,\{D(J).\ J\in \mathcal{I} \}) \)
We define the Zariski closure operator.
abbreviation (in ring0)
\( cl(U) \equiv \text{Closure}(U,\{D(J).\ J\in \mathcal{I} \}) \)
We define the Zariski boundary operator.
abbreviation (in ring0)
\( \partial U \equiv \text{Boundary}(U,\{D(J).\ J\in \mathcal{I} \}) \)
The ring locale specializes the topology0 locale under the Zariski topology.
sublocale ring0 < zariski: topology0
unfolding topology0_def using zariski_top
The interior of a proper subset is given by the D-set of the intersection of all the prime ideals not in that subset
lemma (in ring0) interior_zariski:
assumes \( U \subseteq Spec \), \( U\neq Spec \)
shows \( int(U) = D(\bigcap (Spec-U)) \)proof{
}
}
}
}
}
}
fix \( t \)
assume t: \( t\in \bigcap (Spec-U) \)
then have \( \forall V\in Spec-U.\ t:V \)
moreover
from t have \( (Spec-U) \neq 0 \)
ultimately obtain \( V \) where \( V\in Spec-U \), \( t\in V \)
then have \( t\in \bigcup Spec \)
then have \( t\in R \) unfolding Spec_def
then have S: \( \bigcap (Spec-U) \subseteq R \)
{
fix \( t \)
assume \( t\in D(\bigcap (Spec-U)) \)
with S have t: \( t:Spec \), \( \neg (\bigcap (Spec-U) \subseteq t) \) using openBasic_def
{
assume \( t\notin U \)
with t(1) have \( t\in Spec-U \)
then have \( \bigcap (Spec-U) \subseteq t \)
then have \( False \) using t(2)
then have \( t\in U \)
then have \( D(\bigcap (Spec-U)) \subseteq U \)
moreover {
}
{
assume \( Spec-U = 0 \)
with assms(1) have \( U=Spec \)
with assms(2) have \( False \)
then have P: \( Spec-U \subseteq \mathcal{I} \), \( Spec-U \neq 0 \) unfolding Spec_def
then have \( (\bigcap (Spec-U))\triangleleft R \) using intersection_ideals
then have \( (\bigcap (Spec-U))\in \mathcal{I} \) using ideal_dest_subset
then have \( D(\bigcap (Spec-U)) \in \{D(J).\ J\in \mathcal{I} \} \)
ultimately show \( D(\bigcap (Spec-U)) \subseteq int(U) \) using Top_2_L5
fix \( V \)
assume V: \( V\in \{D(J).\ J\in \mathcal{I} \} \), \( V \subseteq U \)
from V(1) obtain \( J \) where J: \( J:\mathcal{I} \), \( V=D(J) \)
from V(2) have SS: \( Spec-U \subseteq Spec-V \)
{
fix \( K \)
assume K: \( K\in Spec-U \)
{
assume \( \neg (J\subseteq K) \)
with K have \( K\in D(J) \) using J(1) using openBasic_def
with SS, K, J(2) have \( False \)
then have \( J\subseteq K \)
then have \( J\subseteq \bigcap (Spec-U) \) using P(2)
then have \( D(J) \subseteq D(\bigcap (Spec-U)) \) using D_operator_preserve_subset, S
with J(2) have \( V \subseteq D(\bigcap (Spec-U)) \)
moreover
qed
from zariski.Top_2_L1 have \( int(U) \subseteq U \)
moreover from zariski.Top_2_L2 have \( int(U)\in RepFun(\mathcal{I} ,D) \)
ultimately show \( int(U) \subseteq D(\bigcap (Spec-U)) \)
Closed sets and boundary
We characterize the closed sets and study the closure operator in the Zariski topology.
The whole space is the D-set of the ring as an ideal of itself
lemma (in ring0) openBasic_total:
shows \( D(R) = Spec \)proof show \( D(R) \subseteq Spec \) using openBasic_def
{
fix \( t \)
assume t: \( t\in Spec \)
{
assume \( R \subseteq t \)
with t have \( False \) unfolding Spec_def, primeIdeal_def using ideal_dest_subset
with t have \( t\in D(R) \) using openBasic_def
then show \( Spec \subseteq D(R) \)
qed
The union of all D-sets equals the whole spectrum.
corollary (in ring0) total_spec:
shows \( \bigcup \{D(J).\ J\in \mathcal{I} \} = Spec \)proof show \( \bigcup \{D(J).\ J\in \mathcal{I} \} \subseteq Spec \) using openBasic_def
have \( D(R)\in \{D(J).\ J\in \mathcal{I} \} \) using ring_self_ideal
then have \( D(R) \subseteq \bigcup \{D(J).\ J\in \mathcal{I} \} \)
then show \( Spec \subseteq \bigcup \{D(J).\ J\in \mathcal{I} \} \) using openBasic_total
qed
The empty set is the D-set of the zero ideal
lemma (in ring0) openBasic_empty:
shows \( D(\{ 0 \}) = 0 \)proof{
}
fix \( t \)
assume t: \( t\in D(\{ 0 \}) \)
then have \( t\triangleleft _pR \), \( \neg (\{ 0 \} \subseteq t) \) using openBasic_def, Ring_ZF_1_L2(1) unfolding Spec_def
then have \( False \) using ideal_dest_zero unfolding primeIdeal_def
then show \( D(\{ 0 \}) =0 \)
qed
A closed set is a set of primes containing a given ideal
lemma (in ring0) closeBasic:
assumes \( U\{is closed in}\{D(J).\ J\in \mathcal{I} \\} \)
obtains \( J \) where \( J\in \mathcal{I} \) and \( U=\{K\in Spec.\ J\subseteq K\} \)proof assume rule: \( \bigwedge J.\ J \in \mathcal{I} \Longrightarrow U = \{K \in Spec .\ J \subseteq K\} \Longrightarrow thesis \)
from assms have U: \( U\subseteq Spec \), \( Spec-U \in \{D(J).\ J\in \mathcal{I} \} \) unfolding IsClosed_def using total_spec
then obtain \( J \) where J: \( J\in \mathcal{I} \), \( Spec-U = D(J) \)
moreover
qed
from U(1) have \( Spec-(Spec-U) = U \)
ultimately have \( U = Spec-\{K\in Spec.\ \neg (J\subseteq K)\} \) using openBasic_def
then have \( U = \{K\in Spec.\ J\subseteq K\} \)
with J show \( thesis \) using rule
We define the closed sets as V-sets
definition (in ring0)
\( S \subseteq R \Longrightarrow V(S) = \{K\in Spec.\ S\subseteq K\} \)
V-sets and D-sets are complementary
lemma (in ring0) V_is_closed:
assumes \( J\in \mathcal{I} \)
shows \( Spec-V(J) = D(J) \) and \( V(J)\{is closed in}\{D(J).\ J\in \mathcal{I} \\} \)proof from assms have \( V(J) \subseteq Spec \) using closeBasic_def
then have I: \( \bigwedge x.\ x \in V(J) \Longrightarrow x \in \bigcup RepFun(\mathcal{I} , D) \) using total_spec
show \( Spec-V(J) = D(J) \) using assms, closeBasic_def, openBasic_def
with assms have II: \( \bigcup RepFun(\mathcal{I} , D) - V(J) \in RepFun(\mathcal{I} , D) \) using total_spec
from I, II show \( V(J)\{is closed in}\{D(J).\ J\in \mathcal{I} \\} \) unfolding IsClosed_def
qed
As with D-sets, by De Morgan's Laws we get the same result for unions and intersections on V-sets
lemma (in ring0) V_union:
assumes \( J\in \mathcal{I} \), \( K\in \mathcal{I} \)
shows \( V(J)\cup V(K) = V(J\cdot _IK) \)proof{
}
fix \( t \)
assume \( t\in V(J) \)
then have \( t\in Spec \), \( J\subseteq t \) using closeBasic_def, assms(1)
moreover
have \( J\cdot _IK \subseteq J \) using product_in_intersection(1), assms
ultimately have \( t\in Spec \), \( J\cdot _IK \subseteq t \)
then have \( t: V(J\cdot _IK) \) using closeBasic_def, product_in_intersection(2), assms, ideal_dest_subset
moreover {
}
moreover {
}
ultimately show \( thesis \)
qed
fix \( t \)
assume \( t\in V(K) \)
then have \( t\in Spec \), \( K\subseteq t \) using closeBasic_def, assms(2)
moreover
have \( J\cdot _IK \subseteq K \) using product_in_intersection(1), assms
ultimately have \( t\in Spec \), \( J\cdot _IK \subseteq t \)
then have \( t: V(J\cdot _IK) \) using closeBasic_def, product_in_intersection(2), assms, ideal_dest_subset
fix \( t \)
assume \( t\in V(J\cdot _IK) \)
then have t: \( t\in Spec \), \( J\cdot _IK\subseteq t \) using closeBasic_def, assms, product_in_intersection(2), ideal_dest_subset
from this(1) have \( \forall Ia\in \mathcal{I} .\ \forall J\in \mathcal{I} .\ Ia \cdot _I J \subseteq t \longrightarrow Ia \subseteq t \vee J \subseteq t \) unfolding Spec_def, primeIdeal_def
with assms have \( J\cdot _IK\subseteq t \longrightarrow J\subseteq t \vee K\subseteq t \)
with t have \( t\in Spec \), \( J \subseteq t \vee K \subseteq t \)
then have \( t\in V(J)\cup V(K) \) using closeBasic_def, assms
The intersection of a family of V-sets is the V-set of the sum of the corresponding ideals.
lemma (in ring0) V_intersect:
assumes \( \mathcal{J} \subseteq \mathcal{I} \), \( \mathcal{J} \neq 0 \)
shows \( \bigcap \{V(I).\ I\in \mathcal{J} \} = V(\oplus _I\mathcal{J} ) \)proof have \( Spec - (\bigcap \{V(I).\ I\in \mathcal{J} \}) = \bigcup \{D(I).\ I\in \mathcal{J} \} \)proof
{
}
}
fix \( t \)
assume \( t:Spec - (\bigcap \{V(I).\ I\in \mathcal{J} \}) \)
then have t: \( t:Spec \), \( t\notin \bigcap \{V(I).\ I\in \mathcal{J} \} \)
from t(2) obtain \( K \) where \( (t\notin V(K) \wedge K\in \mathcal{J} ) \vee \mathcal{J} =0 \)
with assms(2) have tk: \( t\notin V(K) \), \( K\in \mathcal{J} \)
with t(1) have \( t\in Spec-V(K) \), \( K:\mathcal{J} \)
moreover
from tk(2) have \( Spec-V(K) = D(K) \) using assms(1), V_is_closed(1)
ultimately have \( t:D(K) \), \( K:\mathcal{J} \)
then have \( t\in \bigcup \{D(I).\ I\in \mathcal{J} \} \)
then show \( Spec - (\bigcap \{V(I).\ I\in \mathcal{J} \}) \subseteq \bigcup \{D(I).\ I\in \mathcal{J} \} \)
{
fix \( t \)
assume \( t\in \bigcup \{D(I).\ I\in \mathcal{J} \} \)
then obtain \( K \) where K: \( K:\mathcal{J} \), \( t:D(K) \) using assms(2)
from K(1) have \( Spec-V(K) = D(K) \) using assms(1), V_is_closed(1)
with K(2) have \( t:Spec-V(K) \)
with K(1) have \( t\in Spec-\bigcap \{V(I).\ I:\mathcal{J} \} \)
then show \( \bigcup \{D(I).\ I\in \mathcal{J} \} \subseteq Spec - (\bigcap \{V(I).\ I\in \mathcal{J} \}) \)
qed
then have \( Spec - (\bigcap \{V(I).\ I\in \mathcal{J} \}) = D(\oplus _I\mathcal{J} ) \) using union_open_basic, assms
then have \( Spec-(Spec - (\bigcap \{V(I).\ I\in \mathcal{J} \})) = Spec- D(\oplus _I\mathcal{J} ) \)
moreover
{
have \( \bigcup \mathcal{J} \subseteq R \) using assms(1)
then have \( \langle \bigcup \mathcal{J} \rangle _I\in \mathcal{I} \) using generated_ideal_is_ideal, ideal_dest_subset
then have JI: \( (\oplus _I\mathcal{J} ) \in \mathcal{I} \) using assms(1), sumArbitraryIdeals_def
then have \( Spec- V(\oplus _I\mathcal{J} ) = D(\oplus _I\mathcal{J} ) \) using V_is_closed(1)
then have \( Spec-(Spec-V(\oplus _I\mathcal{J} ) ) = Spec-D(\oplus _I\mathcal{J} ) \)
ultimately have R: \( Spec-(Spec - (\bigcap \{V(I).\ I\in \mathcal{J} \})) = Spec-(Spec-V(\oplus _I\mathcal{J} ) ) \)
fix \( t \)
assume t: \( t\in \bigcap \{V(I).\ I\in \mathcal{J} \} \)
with assms(2) obtain \( I \) where \( I:\mathcal{J} \), \( t:V(I) \)
then have \( t\in Spec \) using closeBasic_def, assms(1)
with t have \( t\in Spec-(Spec - (\bigcap \{V(I).\ I\in \mathcal{J} \})) \)
with R have \( t\in Spec-(Spec-V(\oplus _I\mathcal{J} ) ) \)
then have \( t\in V(\oplus _I\mathcal{J} ) \)
moreover {
}
ultimately show \( thesis \)
qed
fix \( t \)
assume t: \( t\in V(\oplus _I\mathcal{J} ) \)
with JI have \( t:Spec \) using closeBasic_def
with t have \( t\in Spec-(Spec-V(\oplus _I\mathcal{J} ) ) \)
then have \( t\in Spec-(Spec - (\bigcap \{V(I).\ I\in \mathcal{J} \})) \) using R
then have \( t\in \bigcap \{V(I).\ I\in \mathcal{J} \} \)
The closure of a set is the V-set of the intersection of all its points.
lemma (in ring0) closure_zariski:
assumes \( U \subseteq Spec \), \( U\neq 0 \)
shows \( cl(U) = V(\bigcap U) \)proof have \( U \subseteq \mathcal{I} \) using assms(1) unfolding Spec_def
then have ideal: \( (\bigcap U)\triangleleft R \) using intersection_ideals, assms(2)
{
fix \( t \)
assume t: \( t\in V(\bigcap U) \)
{
fix \( q \)
assume q: \( q\in \bigcap U \)
with q obtain \( M \) where \( M:U \), \( q:M \) using assms(2)
with assms have \( q\in \bigcup Spec \)
then have \( q:R \) unfolding Spec_def
then have sub: \( \bigcap U \subseteq R \)
with t have tt: \( t\in Spec \), \( \bigcap U \subseteq t \) using closeBasic_def
{
fix \( VV \)
assume VV: \( VV\in \{D(J).\ J\in \mathcal{I} \} \), \( t\in VV \)
then obtain \( J \) where J: \( VV= D(J) \), \( J\in \mathcal{I} \)
from VV(2), J have jt: \( \neg (J \subseteq t) \) using openBasic_def
{
assume \( U\cap D(J) = 0 \)
then have \( \forall x\in U.\ x\notin D(J) \)
with J(2) have \( \forall x\in U.\ J\subseteq x \) using openBasic_def, assms(1)
then have \( J\subseteq \bigcap U \vee U=0 \)
with tt(2), jt have \( False \) using assms(2)
then have \( U\cap VV \neq 0 \) using J(1)
then have R: \( \forall VV\in \{D(J).\ J\in \mathcal{I} \}.\ t\in VV \longrightarrow VV\cap U \neq 0 \)
from tt(1), assms(1) have RR: \( t\in \bigcup \{D(J).\ J\in \mathcal{I} \} \), \( U \subseteq \bigcup \{D(J).\ J\in \mathcal{I} \} \) using total_spec
have \( t\in cl(U) \) using inter_neigh_cl, RR(2,1), R
then show \( V(\bigcap U) \subseteq cl(U) \) by (rule subsetI )
{
fix \( p \)
assume p: \( p\in U \)
then have \( \bigcap U \subseteq p \)
moreover
from p, assms(1) have \( p\in Spec \), \( \bigcap U\subseteq \bigcup Spec \)
then have \( p\in Spec \), \( \bigcap U\subseteq R \) unfolding Spec_def
ultimately have \( p\in V(\bigcap U) \) using closeBasic_def
then have A: \( U\subseteq V(\bigcap U) \)
have B: \( V(\bigcap U)\{is closed in}\{D(J).\ J\in \mathcal{I} \\} \) using V_is_closed(2), ideal, ideal_dest_subset
show \( cl(U) \subseteq V(\bigcap U) \) using Top_3_L13, A, B
qed
Properties of Spec
In this section we study the topological properties of Spec related to the ring structure.
All Spec topologies are \(T_0\).
theorem (in ring0) zariski_t0:
shows \( \{D(I).\ I\in \mathcal{I} }\{is T_0\\} \)proof{
}
fix \( x \) \( y \)
assume ass: \( x:Spec \), \( y:Spec \), \( x\neq y \)
from ass(3) have \( \neg (x\subseteq y) \vee \neg (y\subseteq x) \)
then have \( y\in D(x) \vee x\in D(y) \) using ass(1,2), openBasic_def unfolding Spec_def
then have \( (x \in D(y) \wedge y \notin D(y)) \vee (y \in D(x) \wedge x \notin D(x)) \) using ass(1,2), openBasic_def unfolding Spec_def
then have \( \exists U\in \{D(I).\ I\in \mathcal{I} \}.\ (x \in U \wedge y \notin U) \vee (y \in U \wedge x \notin U) \) using ass(1,2) unfolding Spec_def
then have \( \forall x y.\ x \in \bigcup RepFun(\mathcal{I} , D) \wedge y \in \bigcup RepFun(\mathcal{I} , D) \wedge x \neq y \longrightarrow \)
\( (\exists U\in RepFun(\mathcal{I} , D).\ x \in U \wedge y \notin U \vee y \in U \wedge x \notin U) \) using total_spec
then show \( thesis \) unfolding isT0_def
qed
Noetherian rings have compact Zariski topology
theorem (in ring0) zariski_compact:
assumes \( \forall I\in \mathcal{I} .\ (I\text{ is finitely generated }) \)
shows \( Spec \text{ is compact in } \{D(I).\ I\in \mathcal{I} \} \)proof have I: \( \bigwedge x.\ x \in Spec \Longrightarrow x \in \bigcup RepFun(\mathcal{I} , D) \) using total_spec
{
fix \( M \)
assume M: \( M \subseteq RepFun(\mathcal{I} , D) \), \( Spec \subseteq \bigcup M \)
let \( J = \{J\in \mathcal{I} .\ D(J)\in M\} \)
have sub: \( J \subseteq \mathcal{I} \)
then have eq: \( \bigcup RepFun(J, D) = D(\oplus _IJ) \) using union_open_basic
have m: \( M = RepFun(J,D) \) using M(1)
then have mm: \( \bigcup M = D(\oplus _IJ) \) using eq
from assms(1), sub have \( \exists \mathcal{T} \in \text{FinPow}(J).\ (\oplus _IJ) = \oplus _I\mathcal{T} \) using sum_ideals_noetherian
then obtain \( T \) where T: \( T\in \text{FinPow}(J) \), \( (\oplus _IJ) = \oplus _IT \)
from T(2) have \( D(\oplus _IJ) = D(\oplus _IT) \)
moreover
have \( T\subseteq \mathcal{I} \) using T(1) unfolding FinPow_def
ultimately have \( D(\oplus _IJ) = \bigcup RepFun(T,D) \) using union_open_basic
with mm have \( \bigcup M = \bigcup RepFun(T,D) \)
then have \( Spec \subseteq \bigcup RepFun(T,D) \) using M(2)
moreover
from T(1) have \( RepFun(T,D) \subseteq RepFun(J,D) \) unfolding FinPow_def
with m have \( RepFun(T,D) \subseteq M \)
moreover from T(1) have \( Finite(RepFun(T,D)) \) unfolding FinPow_def using Finite_RepFun
ultimately have \( \exists N\in \text{FinPow}(M).\ Spec \subseteq \bigcup N \) unfolding FinPow_def
then have II: \( \bigwedge M.\ M\subseteq RepFun(\mathcal{I} ,D) \Longrightarrow Spec \subseteq \bigcup M \Longrightarrow \exists N\in \text{FinPow}(M).\ Spec \subseteq \bigcup N \)
from I, II show \( thesis \) unfolding IsCompact_def
qed
end
Definition of openBasic:
\( S\subseteq R \Longrightarrow D(S) \equiv \{I\in Spec.\ \neg (S\subseteq I)\} \)
corollary (in ring0) generated_ideal_contains_set:
assumes \( X\subseteq R \)
shows \( X\subseteq \langle X\rangle _I \) corollary (in ring0) generated_ideal_is_ideal:
assumes \( X\subseteq R \)
shows \( \langle X\rangle _I \triangleleft R \) lemma (in ring0) ideal_dest_subset:
assumes \( I \triangleleft R \)
shows \( I \subseteq R \)Definition of Spec:
\( Spec \equiv \{I\in \mathcal{I} .\ I\triangleleft _pR\} \)
Definition of primeIdeal:
\( P\triangleleft _pR \equiv P\triangleleft R \wedge P\neq R \wedge (\forall I\in \mathcal{I} .\ \forall J\in \mathcal{I} .\ I\cdot _IJ \subseteq P \longrightarrow (I\subseteq P \vee J\subseteq P)) \)
corollary (in ring0) generated_ideal_small:
assumes \( X\subseteq I \), \( I \triangleleft R \)
shows \( \langle X\rangle _I \subseteq I \) theorem (in ring0) product_in_intersection:
assumes \( I\triangleleft R \), \( J\triangleleft R \)
shows \( I\cdot _IJ \subseteq I\cap J \) and \( (I\cdot _IJ)\triangleleft R \) and \( M(I\times J) \subseteq I\cdot _IJ \) theorem (in ring0) product_in_intersection:
assumes \( I\triangleleft R \), \( J\triangleleft R \)
shows \( I\cdot _IJ \subseteq I\cap J \) and \( (I\cdot _IJ)\triangleleft R \) and \( M(I\times J) \subseteq I\cdot _IJ \)Definition of sumArbitraryIdeals:
\( \mathcal{J} \subseteq \mathcal{I} \Longrightarrow \oplus _I\mathcal{J} \equiv \langle \bigcup \mathcal{J} \rangle _I \)
lemma (in ring0) union_open_basic:
assumes \( \mathcal{J} \subseteq \mathcal{I} \)
shows \( \bigcup \{D(I).\ I\in \mathcal{J} \} = D(\oplus _I\mathcal{J} ) \) lemma (in ring0) intersection_open_basic:
assumes \( I\triangleleft R \), \( J\triangleleft R \)
shows \( D(I)\cap D(J) = D(I\cdot _IJ) \)Definition of IsATopology:
\( T \text{ is a topology } \equiv ( \forall M \in Pow(T).\ \bigcup M \in T ) \wedge \)
\( ( \forall U\in T.\ \forall V\in T.\ U\cap V \in T) \)
corollary (in ring0) zariski_top: shows \( \{D(J).\ J\in \mathcal{I} }\text{ is a topology \} \)
theorem (in ring0) intersection_ideals:
assumes \( \forall J\in \mathcal{J} .\ (J \triangleleft R) \), \( \mathcal{J} \neq 0 \)
shows \( (\bigcap \mathcal{J} ) \triangleleft R \) lemma (in topology0) Top_2_L5:
assumes \( U\subseteq A \) and \( U\in T \)
shows \( U \subseteq int(A) \) lemma (in ring0) D_operator_preserve_subset:
assumes \( S \subseteq T \), \( T\subseteq R \)
shows \( D(S) \subseteq D(T) \) lemma (in ring0) ring_self_ideal: shows \( R \triangleleft R \)
lemma (in ring0) openBasic_total: shows \( D(R) = Spec \)
lemma (in ring0) Ring_ZF_1_L2: shows \( 0 \in R \), \( 1 \in R \), \( ( - 0 ) = 0 \), \( 2 \in R \)
lemma (in ring0) ideal_dest_zero:
assumes \( I \triangleleft R \)
shows \( 0 \in I \)Definition of IsClosed:
\( D \text{ is closed in } T \equiv (D \subseteq \bigcup T \wedge (\bigcup T)\setminus D \in T) \)
corollary (in ring0) total_spec: shows \( \bigcup \{D(J).\ J\in \mathcal{I} \} = Spec \)
Definition of closeBasic:
\( S \subseteq R \Longrightarrow V(S) = \{K\in Spec.\ S\subseteq K\} \)
theorem (in ring0) product_in_intersection:
assumes \( I\triangleleft R \), \( J\triangleleft R \)
shows \( I\cdot _IJ \subseteq I\cap J \) and \( (I\cdot _IJ)\triangleleft R \) and \( M(I\times J) \subseteq I\cdot _IJ \) lemma (in ring0) V_is_closed:
assumes \( J\in \mathcal{I} \)
shows \( Spec-V(J) = D(J) \) and \( V(J)\{is closed in}\{D(J).\ J\in \mathcal{I} \\} \) lemma (in topology0) inter_neigh_cl:
assumes \( A \subseteq \bigcup T \) and \( x\in \bigcup T \) and \( \forall U\in T.\ x\in U \longrightarrow U\cap A \neq 0 \)
shows \( x \in cl(A) \) lemma (in ring0) V_is_closed:
assumes \( J\in \mathcal{I} \)
shows \( Spec-V(J) = D(J) \) and \( V(J)\{is closed in}\{D(J).\ J\in \mathcal{I} \\} \) lemma (in topology0) Top_3_L13:
assumes \( B \text{ is closed in } T \), \( A\subseteq B \)
shows \( cl(A) \subseteq B \)Definition of isT0:
\( T \text{ is }T_0 \equiv \forall x y.\ ((x \in \bigcup T \wedge y \in \bigcup T \wedge x\neq y) \longrightarrow \)
\( (\exists U\in T.\ (x\in U \wedge y\notin U) \vee (y\in U \wedge x\notin U))) \)
theorem (in ring0) sum_ideals_noetherian:
assumes \( \forall I\in \mathcal{I} .\ (I\text{ is finitely generated }) \), \( \mathcal{J} \subseteq \mathcal{I} \)
shows \( \exists \mathcal{T} \in \text{FinPow}(\mathcal{J} ).\ (\oplus _I\mathcal{J} ) = (\oplus _I\mathcal{T} ) \)Definition of FinPow:
\( \text{FinPow}(X) \equiv \{A \in Pow(X).\ Finite(A)\} \)
Definition of IsCompact:
\( K \text{ is compact in } T \equiv (K \subseteq \bigcup T \wedge \)
\( (\forall M\in Pow(T).\ K \subseteq \bigcup M \longrightarrow (\exists N \in \text{FinPow}(M).\ K \subseteq \bigcup N))) \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
