Theory Ring_Zariski_ZF

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2022  Daniel de la Concepcion

    This program is free software; Redistribution and use in source and binary forms, 
    with or without modification, are permitted provided that the following conditions are met:

   1. Redistributions of source code must retain the above copyright notice, 
   this list of conditions and the following disclaimer.
   2. Redistributions in binary form must reproduce the above copyright notice, 
   this list of conditions and the following disclaimer in the documentation and/or 
   other materials provided with the distribution.
   3. The name of the author may not be used to endorse or promote products 
   derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES,
INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT,
INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES LOSS OF USE, DATA, OR PROFITS OR
BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE
USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

section ‹Rings - Zariski Topology›

text‹This file deals with the definition of the topology on the set of prime ideals›

text‹It defines the topology, computes the closed sets and the closure and interior operators›

theory Ring_Zariski_ZF imports Ring_ZF_2 Topology_ZF

begin

text‹The set where the topology is defined is in the spectrum
of a ring; i.e. the set of all prime ideals.›

definition (in ring0) Spec where
"Spec ≡ {I∈ℐ. I◃⇩pR}"

text‹The basic set that defines the topoogy is given
by the D operator›

definition (in ring0) openBasic ("D") where
"S⊆R ⟹ D(S) ≡ {I∈Spec. ¬(S⊆I)}"

text‹The D operator preserves subsets›

lemma (in ring0) D_operator_preserve_subset:
  assumes "S ⊆ T" "T⊆R"
  shows "D(S) ⊆ D(T)"
proof
  from assms have S:"S⊆R" by auto
  fix x assume "x∈D(S)"
  then have x:"x∈Spec" "¬(S⊆x)" using openBasic_def S by auto
  with assms(1) have "x∈Spec" "¬(T⊆x)" by auto
  then show "x:D(T)" using openBasic_def assms(2) by auto
qed

text‹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⊆R"
  shows "D(T) = D(⟨T⟩⇩I)"
proof
  have T:"T⊆⟨T⟩⇩I" "⟨T⟩⇩I ⊆R" using generated_ideal_contains_set assms
    generated_ideal_is_ideal[OF assms] ideal_dest_subset by auto
  with D_operator_preserve_subset show "D(T) ⊆ D(⟨T⟩⇩I)"
    by auto
  {
    fix t assume "t∈D(⟨T⟩⇩I)"
    with T(2) have t:"t∈Spec" "¬(⟨T⟩⇩I ⊆t)" using openBasic_def by auto
    {
      assume as:"T ⊆ t"
      from t(1) have "t◃R" unfolding Spec_def primeIdeal_def by auto
      with as have "⟨T⟩⇩I ⊆t" using generated_ideal_small by auto
      with t(2) have False by auto
    }
    then have "¬(T ⊆ t)" by auto
    with t(1) have "t∈D(T)" using openBasic_def assms by auto
  }
  then show "D(⟨T⟩⇩I) ⊆ D(T)" by auto
qed

text‹The intersection of to D-sets is the D-set on the 
product of ideals›

lemma (in ring0) intersection_open_basic:
  assumes "I◃R" "J◃R"
  shows "D(I)∩D(J) = D(I⋅⇩IJ)"
proof
  have S:"I⋅⇩IJ ⊆ R" using product_in_intersection(2) ideal_dest_subset assms by auto
  {
    fix K assume K:"K∈D(I)∩D(J)"
    then have "K◃⇩pR" "¬(I⊆K)" "¬(J⊆K)"
      using assms ideal_dest_subset openBasic_def 
      unfolding Spec_def by auto
    then have "¬(I⊆K)" "¬(J⊆K)" "∀I∈ℐ. ∀J∈ℐ. I⋅⇩IJ⊆K ⟶ I ⊆ K ∨ J ⊆ K"
      unfolding primeIdeal_def by auto
    then have "¬(I⋅⇩IJ⊆K)" using assms
      using ideal_dest_subset[of I] ideal_dest_subset[of J] by auto
    moreover note K
    ultimately have "K∈D(I⋅⇩IJ)" using openBasic_def[of "I"]
      ideal_dest_subset[OF assms(1)]
      unfolding Spec_def openBasic_def[OF S] by auto
  }
  then show "D(I)∩D(J) ⊆ D(I⋅⇩IJ)" by auto
  {
    fix K assume Kass:"K∈D(I⋅⇩IJ)"
    then have K:"K◃⇩pR" "¬(I⋅⇩IJ⊆K)" using openBasic_def[OF S] unfolding Spec_def by auto
    {
      assume "I ⊆ K ∨ J ⊆K"
      then have "I∩J ⊆ K" by auto
      then have "I⋅⇩IJ⊆K" using product_in_intersection assms by auto
      with K(2) have False by auto
    }
    then have "¬(I⊆K)" "¬(J⊆K)" by auto
    with Kass have "K∈D(I)∩D(J)" using assms ideal_dest_subset
      openBasic_def[of I] openBasic_def[of J]
      unfolding openBasic_def[OF S] Spec_def by auto
  }
  then show "D(I ⋅⇩I J) ⊆ D(I) ∩ D(J)" by auto
qed

text‹The union of D-sets is the D-set of the sum of the ideals›

lemma (in ring0) union_open_basic:
  assumes "𝒥 ⊆ ℐ"
  shows "⋃{D(I). I∈𝒥} = D(⊕⇩I𝒥)"
proof
  have S:"(⊕⇩I𝒥) ⊆ R" using generated_ideal_is_ideal[of "⋃𝒥"] assms
      unfolding sumArbitraryIdeals_def[OF assms]
      using ideal_dest_subset by auto
  {
    fix t assume "t∈⋃{D(I). I∈𝒥}"
    then obtain K where K:"K∈𝒥" "t∈D(K)" by auto
    then have t:"t◃⇩pR" "¬(K⊆t)" using assms openBasic_def unfolding Spec_def by auto
    {
      assume "(⊕⇩I𝒥) ⊆ t"
      then have "⋃𝒥 ⊆ t" using generated_ideal_contains_set[of "⋃𝒥"]
        assms unfolding sumArbitraryIdeals_def[OF assms] by auto
      with K(1) have "K ⊆ t" by auto
      with t(2) have False by auto
    }
    then have "¬((⊕⇩I𝒥) ⊆ t)" by auto moreover
    note K S ultimately have "t∈D(⊕⇩I𝒥)" using openBasic_def[of K] openBasic_def[of "⊕⇩I𝒥"]
      assms by auto
  }
  then show "⋃{D(I). I∈𝒥} ⊆ D(⊕⇩I𝒥)" by auto
  {
    fix t assume as:"t∈D(⊕⇩I𝒥)"
    then have t:"t∈Spec" "¬((⊕⇩I𝒥)⊆t)" unfolding openBasic_def[OF S]
      by auto
    {
      assume "⋃𝒥 ⊆ t"
      with t(1) have "⟨⋃𝒥⟩⇩I ⊆ t" using generated_ideal_small
        unfolding Spec_def primeIdeal_def
        by auto
      with t(2) have False unfolding sumArbitraryIdeals_def[OF assms]
        by auto
    }
    then obtain J where J:"¬(J ⊆ t)" "J∈𝒥" by auto
    note J(1) moreover have "J⊆R" using `J∈𝒥` assms by auto
    moreover note t(1) ultimately have "t∈D(J)" using openBasic_def[of J]
      by auto
    then have "t:⋃{D(I). I∈𝒥}" using J(2) by auto
  }
  then show "D(⊕⇩I𝒥) ⊆ ⋃{D(I). I∈𝒥}" by auto
qed

text‹From the previous results on intesertion and union,
we conclude that the D-sets we computed form a topology›

corollary (in ring0) zariski_top:
  shows "{D(J). J∈ℐ}{is a topology}" unfolding IsATopology_def
proof(safe)
  fix M assume "M ⊆ {D(J). J∈ℐ}"
  then have "M = {D(J). J∈{K∈ℐ. D(K)∈M}}" by auto
  then have "⋃M = ⋃{D(J). J∈{K∈ℐ. D(K)∈M}}" by auto
  then have "⋃M = D(⊕⇩I{K∈ℐ. D(K)∈M})" using union_open_basic[of "{K ∈ ℐ . D(K) ∈ M}"] by auto
  moreover have "(⊕⇩I{K∈ℐ. D(K)∈M})◃R" using
    generated_ideal_is_ideal[of "⋃{K∈ℐ. D(K)∈M}"]
    sumArbitraryIdeals_def [of "{K∈ℐ. D(K)∈M}"]
    by force
  then have "(⊕⇩I{K∈ℐ. D(K)∈M})∈ℐ" using ideal_dest_subset
    by auto
  ultimately show "⋃M:{D(J). J∈ℐ}" by auto
next
  fix x xa assume as:"x◃R" "xa◃R"
  then have "D(x) ∩ D(xa) = D(x⋅⇩Ixa)" using intersection_open_basic
    by auto
  moreover have "(x⋅⇩Ixa) ◃R" using product_in_intersection(2)
    as by auto
  then have "(x⋅⇩Ixa):ℐ" using ideal_dest_subset by auto
  ultimately show "D(x) ∩ D(xa)∈{D(J). J∈ℐ}" by auto
qed

text‹We include all the results of topology0
  into ring0 under the namespace "zariski"›

definition(in ring0) ZarInt ("int") where
  "int(U) ≡ Interior(U,{D(J). J∈ℐ})"

definition (in ring0) ZarCl ("cl") where
  "cl(U) ≡ Closure(U,{D(J). J∈ℐ})"

definition (in ring0) ZarBound ("∂_") where
  "∂U ≡ Boundary(U,{D(J). J∈ℐ})"

sublocale ring0 < zariski:topology0 "{D(J). J∈ℐ}"
  ZarInt ZarCl ZarBound unfolding topology0_def
  ZarBound_def ZarInt_def ZarCl_def
  using zariski_top by auto

text‹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 ⊆ Spec" "U≠Spec"
  shows "int(U) = D(⋂(Spec-U))"
proof
  {
    fix t assume t:"t∈⋂(Spec-U)"
    then have "∀V∈Spec-U. t:V" by auto
    moreover from t have "(Spec-U) ≠0" by auto
    ultimately obtain V where "V∈Spec-U" "t∈V" by auto
    then have "t∈⋃Spec" by auto
    then have "t∈R" unfolding Spec_def by auto
  }
  then have S:"⋂(Spec-U) ⊆ R" by auto
  {
    fix t assume "t∈D(⋂(Spec-U))"
    then have t:"t:Spec" "¬(⋂(Spec-U) ⊆ t)" using openBasic_def[OF S]
      by auto
    {
      assume "t∉U"
      with t(1) have "t∈Spec-U" by auto
      then have "⋂(Spec-U) ⊆ t" by auto
      then have False using t(2) by auto
    }
    then have "t∈U" by auto
  }
  then have "D(⋂(Spec-U)) ⊆ U" by auto moreover
  {
    assume "Spec-U = 0"
    with assms(1) have "U=Spec" by auto
    with assms(2) have False by auto
  }
  then have P:"Spec-U ⊆ ℐ" "Spec-U ≠0" unfolding Spec_def by auto
  then have "(⋂(Spec-U))◃R" using intersection_ideals by auto
  then have "(⋂(Spec-U))∈ℐ" using ideal_dest_subset by auto
  then have "D(⋂(Spec-U)) ∈{D(J). J∈ℐ}" by auto
  ultimately
  show "D(⋂(Spec-U)) ⊆int(U)" using zariski.Top_2_L5 by auto
  {
    fix V assume V:"V∈{D(J). J∈ℐ}" "V ⊆ U"
    from V(1) obtain J where J:"J:ℐ" "V=D(J)" by auto
    from V(2) have SS:"Spec-U ⊆ Spec-V" by auto
    {
      fix K assume K:"K∈Spec-U"
      {
        assume "¬(J⊆K)"
        with K have "K∈D(J)" using J(1) using openBasic_def
          by auto
        with SS K J(2) have False by auto
      }
      then have "J⊆K" by auto
    }
    then have "J⊆ ⋂(Spec-U)" using P(2) by auto
    then have "D(J) ⊆ D(⋂(Spec-U))" using D_operator_preserve_subset
      S by auto
    with J(2) have "V ⊆D(⋂(Spec-U))" by auto
  }
  then show "int(U) ⊆ D(⋂(Spec-U))" using
    zariski.Top_2_L1 zariski.Top_2_L2 by auto
qed

text‹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) ⊆ Spec" using openBasic_def by auto
  {
    fix t assume t:"t∈Spec"
    {
      assume "R ⊆ t"
      then have False using t unfolding Spec_def primeIdeal_def
        using ideal_dest_subset[of t] by auto
    }
    with t have "t∈D(R)" using openBasic_def by auto
  }
  then show "Spec ⊆ D(R)" by auto
qed

corollary (in ring0) total_spec:
  shows "⋃{D(J). J∈ℐ} = Spec"
proof
  show "⋃{D(J). J∈ℐ} ⊆ Spec" using openBasic_def by auto
  have "D(R)∈{D(J). J∈ℐ}" using ring_self_ideal by auto
  then have "D(R) ⊆ ⋃{D(J). J∈ℐ}" by auto
  then show "Spec ⊆ ⋃{D(J). J∈ℐ}" using openBasic_total by auto
qed

text‹The empty set is the D-set of the zero ideal›

lemma (in ring0) openBasic_empty:
  shows "D({𝟬}) = 0"
proof-
  {
    fix t assume t:"t∈D({𝟬})"
    then have "t◃⇩pR" "¬({𝟬} ⊆ t)" using openBasic_def
      Ring_ZF_1_L2(1) unfolding Spec_def by auto
    then have False using ideal_dest_zero unfolding primeIdeal_def by auto
  }
  then show "D({𝟬}) =0" by auto
qed

text‹A closed set is a set of primes containing a given
ideal›

lemma (in ring0) closeBasic:
  assumes "U{is closed in}{D(J). J∈ℐ}"
  obtains J where "J∈ℐ" and "U={K∈Spec. J⊆K}"
proof-
  assume rule:"⋀J. J ∈ ℐ ⟹ U = {K ∈ Spec . J ⊆ K} ⟹ thesis"
  from assms have U:"U⊆Spec" "Spec-U ∈ {D(J). J∈ℐ}" unfolding IsClosed_def
    using total_spec by auto
  then obtain J where J:"J∈ℐ" "Spec-U = D(J)" by auto
  moreover from U(1) have "Spec-(Spec-U) = U" by auto
  ultimately have "U = Spec-{K∈Spec. ¬(J⊆K)}" using openBasic_def
    by auto
  then have "U = {K∈Spec. J⊆K}" by auto
  with J show ?thesis using rule by auto
qed

text‹We define the closed sets as V-sets›

definition (in ring0) closeBasic ("V") where
"S ⊆ R ⟹ V(S) = {K∈Spec. S⊆K}"

text‹V-sets and D-sets are complementary›

lemma (in ring0) V_is_closed:
  assumes "J∈ℐ"
  shows "Spec-V(J) = D(J)" and "V(J){is closed in}{D(J). J∈ℐ}"
  unfolding IsClosed_def
proof(safe)
  from assms have "V(J) ⊆ Spec" using closeBasic_def by auto
  then show "⋀x. x ∈ V(J) ⟹ x ∈ ⋃RepFun(ℐ, D)" using total_spec by auto
  show "Spec-V(J) = D(J)" using assms
    closeBasic_def openBasic_def by auto
  with assms show "⋃RepFun(ℐ, D) - V(J) ∈ RepFun(ℐ, D)"
    using total_spec by auto
qed

text‹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∈ℐ" "K∈ℐ"
  shows "V(J)∪V(K) = V(J⋅⇩IK)"
proof-
  {
    fix t assume "t∈V(J)"
    then have "t∈Spec" "J⊆t" using closeBasic_def
      assms(1) by auto
    moreover have "J⋅⇩IK ⊆ J" using product_in_intersection(1)[of J K]
      assms by auto
    ultimately have "t∈Spec" "J⋅⇩IK ⊆t" by auto
    then have "t: V(J⋅⇩IK)" using closeBasic_def
      product_in_intersection(2)[of J K] assms ideal_dest_subset
      by auto
  }
  moreover
  {
    fix t assume "t∈V(K)"
    then have "t∈Spec" "K⊆t" using closeBasic_def
      assms(2) by auto
    moreover have "J⋅⇩IK ⊆ K" using product_in_intersection(1)[of J K]
      assms by auto
    ultimately have "t∈Spec" "J⋅⇩IK ⊆t" by auto
    then have "t: V(J⋅⇩IK)" using closeBasic_def
      product_in_intersection(2)[of J K] assms ideal_dest_subset
      by auto
  }
  moreover
  {
    fix t assume "t∈ V(J⋅⇩IK)"
    then have t:"t∈Spec" "J⋅⇩IK⊆t" using closeBasic_def
      assms product_in_intersection(2)[of J K]
      ideal_dest_subset by auto
    from this(1) have "∀Ia∈ℐ. ∀J∈ℐ. Ia ⋅⇩I J ⊆ t ⟶ Ia ⊆ t ∨ J ⊆ t"
      unfolding Spec_def primeIdeal_def by blast
    with assms have "J⋅⇩IK⊆t ⟶ J⊆t ∨ K⊆t" by auto
    with t have "t∈Spec"  "J ⊆ t ∨ K ⊆ t" by auto
    then have "t∈V(J)∪V(K)" using closeBasic_def
      assms by auto
  }
  ultimately show ?thesis by auto
qed

lemma (in ring0) V_intersect:
  assumes "𝒥 ⊆ ℐ" "𝒥 ≠0"
  shows "⋂{V(I). I∈𝒥} = V(⊕⇩I𝒥)"
proof-
  have "Spec - (⋂{V(I). I∈𝒥}) = ⋃{D(I). I∈𝒥}"
  proof
    {
      fix t assume "t:Spec - (⋂{V(I). I∈𝒥})"
      then have t:"t:Spec" "t∉⋂{V(I). I∈𝒥}" by auto
      from t(2) obtain K where "(t∉V(K) ∧ K∈𝒥) ∨ 𝒥=0" by auto
      with assms(2) have "t∉V(K)" "K∈𝒥" by auto
      with t(1) have "t∈Spec-V(K)" "K:𝒥" by auto moreover
      from `K:𝒥` have "Spec-V(K) = D(K)" using assms(1) V_is_closed(1) by auto
      ultimately have "t:D(K)" "K:𝒥" by auto
      then have "t∈⋃{D(I). I∈𝒥}" by auto
    }
    then show "Spec - (⋂{V(I). I∈𝒥}) ⊆ ⋃{D(I). I∈𝒥}" by auto
    {
      fix t assume "t∈⋃{D(I). I∈𝒥}"
      then obtain K where K:"K:𝒥" "t:D(K)" using assms(2)
        by auto
      from `K:𝒥` have "Spec-V(K) = D(K)" using assms(1) V_is_closed(1) by auto     
      with K(2) have "t:Spec-V(K)" by auto
      with K(1) have "t∈Spec-⋂{V(I). I:𝒥}" by auto
    }
    then show "⋃{D(I). I∈𝒥} ⊆ Spec - (⋂{V(I). I∈𝒥})" by auto
  qed
  then have "Spec - (⋂{V(I). I∈𝒥}) = D(⊕⇩I𝒥)" using union_open_basic
    assms by auto
  then have "Spec-(Spec - (⋂{V(I). I∈𝒥})) = Spec- D(⊕⇩I𝒥)" by auto
  moreover
  have JI:"(⊕⇩I𝒥) ∈ ℐ" using generated_ideal_is_ideal[of "⋃𝒥"] assms
    unfolding sumArbitraryIdeals_def[OF assms(1)]
    using ideal_dest_subset by auto
  then have "Spec- V(⊕⇩I𝒥) = D(⊕⇩I𝒥)" using V_is_closed(1)[of "⊕⇩I𝒥"]
    by auto
  then have "Spec-(Spec-V(⊕⇩I𝒥) ) = Spec-D(⊕⇩I𝒥)" by auto
  ultimately have R:"Spec-(Spec - (⋂{V(I). I∈𝒥})) = Spec-(Spec-V(⊕⇩I𝒥) )"
    by auto
  {
    fix t assume t:"t∈⋂{V(I). I∈𝒥}"
    with assms(2) obtain I where "I:𝒥" "t:V(I)" by auto
    then have "t∈Spec" using closeBasic_def assms(1)
      by auto
    with t have "t∈Spec-(Spec - (⋂{V(I). I∈𝒥}))" by auto
    with R have "t∈Spec-(Spec-V(⊕⇩I𝒥) )" by auto
    then have "t∈V(⊕⇩I𝒥)" by auto
  } moreover
  {
    fix t assume t:"t∈V(⊕⇩I𝒥)"
    with JI have "t:Spec" using closeBasic_def by auto
    with t have "t∈Spec-(Spec-V(⊕⇩I𝒥) )" by auto
    then have "t∈Spec-(Spec - (⋂{V(I). I∈𝒥}))" using R by auto
    then have "t∈⋂{V(I). I∈𝒥}" by auto
  }
  ultimately show ?thesis by force
qed

text‹The closure of a set is the V-set of the intersection
of all its points.›

lemma (in ring0) closure_zariski:
  assumes "U ⊆ Spec" "U≠0"
  shows "cl(U) = V(⋂U)"
proof
  have "U ⊆ ℐ" using assms(1) unfolding Spec_def by auto
  then have ideal:"(⋂U)◃R" using intersection_ideals[of U] assms(2) by auto
  {
    fix t assume t:"t∈V(⋂U)"
    {
      fix q assume q:"q∈⋂U"
      with q obtain M where "M:U" "q:M" using assms(2) by blast
      with assms have "q∈⋃Spec" by auto
      then have "q:R" unfolding Spec_def by auto
    }
    then have sub:"⋂U ⊆ R" by auto
    with t have tt:"t∈Spec" "⋂U ⊆ t" using closeBasic_def by auto
    {
      fix VV assume VV:"VV∈{D(J). J∈ℐ}" "t∈VV"
      then obtain J where J:"VV= D(J)" "J∈ℐ" by auto
      from VV(2) J have jt:"¬(J ⊆ t)" using openBasic_def by auto
      {
        assume "U∩D(J) = 0"
        then have "∀x∈U. x∉D(J)" by auto
        with J(2) have "∀x∈U. J⊆x" using openBasic_def[of J]
          assms(1) by auto
        then have "J⊆ ⋂U ∨ U=0" by auto 
        with tt(2) jt have False using assms(2) by auto
      }
      then have "U∩VV ≠ 0" using J(1) by auto
    }
    then have R:"∀VV∈{D(J). J∈ℐ}. t∈VV ⟶ VV∩U ≠ 0" by auto
    from tt(1) assms(1) have RR:"t∈⋃{D(J). J∈ℐ}" "U ⊆ ⋃{D(J). J∈ℐ}"
      using total_spec by auto
    have "t∈cl(U)" using zariski.inter_neigh_cl[OF RR(2,1) R].
  }
  then show "V(⋂U) ⊆ cl(U)"
    apply (rule subsetI) by auto
  {
    fix p assume p:"p∈U"
    then have "⋂U ⊆p" by auto
    moreover
    from p assms(1) have "p∈Spec" "⋂U⊆⋃Spec" by auto
    then have "p∈Spec" "⋂U⊆R" unfolding Spec_def by auto
    ultimately have "p∈V(⋂U)" using closeBasic_def[of "⋂U"]
      by auto
  }
  then have A:"U⊆V(⋂U)" by auto
  have B:"V(⋂U){is closed in}{D(J). J∈ℐ}"
    using V_is_closed(2) ideal ideal_dest_subset by auto
  show "cl(U) ⊆ V(⋂U)"
    apply (rule zariski.Top_3_L13[of "V(⋂U)" U])
    using A B by auto
qed

end