Theory Ring_Zariski_ZF_2
section ‹Rings - Zariski Topology - Properties›
theory Ring_Zariski_ZF_2 imports Ring_Zariski_ZF Topology_ZF_1
begin
theorem (in ring0) zariski_t0:
shows "{D(I). I∈ℐ}{is T⇩0}" unfolding isT0_def
proof-
{
fix x y assume ass:"x:Spec" "y:Spec" "x≠y"
from ass(3) have "¬(x⊆y) ∨ ¬(y⊆x)" by auto
then have "y∈D(x) ∨ x∈D(y)" using ass(1,2)
unfolding Spec_def using ass(1,2) openBasic_def
by auto
then have "(x ∈ D(y) ∧ y ∉ D(y)) ∨ (y ∈ D(x) ∧ x ∉ D(x))"
using ass(1,2) unfolding Spec_def
using openBasic_def by auto
then have "∃U∈{D(I). I∈ℐ}. (x ∈ U ∧ y ∉ U) ∨ (y ∈ U ∧ x ∉ U)"
using ass(1,2) unfolding Spec_def by auto
}
then show "∀x y. x ∈ ⋃RepFun(ℐ, D) ∧ y ∈ ⋃RepFun(ℐ, D) ∧ x ≠ y ⟶
(∃U∈RepFun(ℐ, D). x ∈ U ∧ y ∉ U ∨ y ∈ U ∧ x ∉ U)"
using total_spec by auto
qed
text‹Noetherian rings have compact Zariski topology›
theorem (in ring0) zariski_compact:
assumes "∀I∈ℐ. (I{is finitely generated})"
shows "Spec {is compact in} {D(I). I∈ℐ}"
unfolding IsCompact_def
proof(safe)
show "⋀x. x ∈ Spec ⟹ x ∈ ⋃RepFun(ℐ, D)" using total_spec by auto
fix M assume M:"M ⊆ RepFun(ℐ, D)" "Spec ⊆ ⋃M"
let ?J ="{J∈ℐ. D(J)∈M}"
have m:"M = RepFun(?J,D)" using M(1) by auto
then have mm:"⋃M = D(⊕⇩I?J)" using union_open_basic[of ?J] by auto
obtain T where T:"T∈FinPow(?J)" "(⊕⇩I?J) = ⊕⇩IT" using
sum_ideals_noetherian[OF assms(1), of ?J] by blast
from T(2) have "D(⊕⇩I?J) = D(⊕⇩IT)" by auto
moreover have "T⊆ℐ" using T(1) unfolding FinPow_def by auto
ultimately have "D(⊕⇩I?J) = ⋃RepFun(T,D)" using union_open_basic[of T]
by auto
with mm have "⋃M = ⋃RepFun(T,D)" by auto
then have "Spec ⊆ ⋃RepFun(T,D)" using M(2) by auto moreover
from T(1) have "RepFun(T,D) ⊆ RepFun(?J,D)" unfolding FinPow_def by auto
with m have "RepFun(T,D) ⊆ M" by auto moreover
from T(1) have "Finite(RepFun(T,D))" unfolding FinPow_def
using Finite_RepFun by auto
ultimately show "∃N∈FinPow(M). Spec ⊆ ⋃N" unfolding FinPow_def
by auto
qed
end