R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
hZ : (↑(basicOpen f) ∩ ⋂ (i : ι), Z i) = ∅
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
⊢ ∃ t, (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
hZ : (↑(basicOpen f) ∩ ⋂ (i : ι), Z i) = ∅
⊢ ∃ t, (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
let I : ι → Ideal R := fun i => vanishingIdeal (Z i)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
hZ : (↑(basicOpen f) ∩ ⋂ (i : ι), Z i) = ∅
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
⊢ ∃ t, (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
hZ : (↑(basicOpen f) ∩ ⋂ (i : ι), Z i) = ∅
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
⊢ ∃ t, (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
have hI : ∀ i, Z i = zeroLocus (I i) := fun i => by
  simpa only [zeroLocus_vanishingIdeal_eq_closure] using (hZc i).closure_eq.symm
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
⊢ ∃ t, (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
hZ : (↑(basicOpen f) ∩ ⋂ (i : ι), Z i) = ∅
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
⊢ ∃ t, (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
rw [basicOpen_eq_zeroLocus_compl f, Set.inter_comm, ← Set.diff_eq, Set.diff_eq_empty,
  funext hI, ← zeroLocus_iSup] at hZ
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
⊢ ∃ t, (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
⊢ ∃ t, (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
obtain ⟨n, hn⟩ : f ∈ (⨆ i : ι, I i).radical := by
  rw [← vanishingIdeal_zeroLocus_eq_radical]
  apply vanishingIdeal_anti_mono hZ
  exact subset_vanishingIdeal_zeroLocus {f} (Set.mem_singleton f)
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ ∃ t, (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
case intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
⊢ ∃ t, (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
rcases Submodule.exists_finset_of_mem_iSup I hn with ⟨s, hs⟩
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ s), Z i) = ∅
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ ∃ t, (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ t), Z i) = ∅
use s
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ (⋂ (i : ι) (_ : i ∈ s), Z i) ⊆ zeroLocus {f}
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ (↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ s), Z i) = ∅
simp_rw [basicOpen_eq_zeroLocus_compl f, Set.inter_comm (zeroLocus {f}ᶜ), ← Set.diff_eq,
  Set.diff_eq_empty]
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ (⋂ (i : ι) (_ : i ∈ s), zeroLocus ↑(I i)) ⊆ zeroLocus {f}
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ (⋂ (i : ι) (_ : i ∈ s), Z i) ⊆ zeroLocus {f}
rw [show (Set.iInter fun i => Set.iInter fun (_ : i ∈ s) => Z i) =
  Set.iInter fun i => Set.iInter fun (_ : i ∈ s) => zeroLocus (I i) from congr_arg _
    (funext fun i => congr_arg _ (funext fun _ => hI i))]
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ zeroLocus ↑(⨆ (i : ι) (_ : i ∈ s), vanishingIdeal (Z i)) ⊆ zeroLocus {f}
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ (⋂ (i : ι) (_ : i ∈ s), zeroLocus ↑(I i)) ⊆ zeroLocus {f}
simp_rw [← zeroLocus_iSup]
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ zeroLocus ↑(Ideal.radical (⨆ (i : ι) (_ : i ∈ s), vanishingIdeal (Z i))) ⊆ zeroLocus {f}
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ zeroLocus ↑(⨆ (i : ι) (_ : i ∈ s), vanishingIdeal (Z i)) ⊆ zeroLocus {f}
rw [← zeroLocus_radical]
case intro.intro.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ {f} ⊆ ↑(Ideal.radical (⨆ (i : ι) (_ : i ∈ s), vanishingIdeal (Z i)))
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ zeroLocus ↑(Ideal.radical (⨆ (i : ι) (_ : i ∈ s), vanishingIdeal (Z i))) ⊆ zeroLocus {f}
apply zeroLocus_anti_mono
case intro.intro.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ f ∈ ↑(Ideal.radical (⨆ (i : ι) (_ : i ∈ s), vanishingIdeal (Z i)))
case intro.intro.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ {f} ⊆ ↑(Ideal.radical (⨆ (i : ι) (_ : i ∈ s), vanishingIdeal (Z i)))
rw [Set.singleton_subset_iff]
no goals
case intro.intro.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
n : ℕ
hn : f ^ n ∈ ⨆ (i : ι), I i
s : Finset ι
hs : f ^ n ∈ ⨆ (i : ι) (_ : i ∈ s), I i
⊢ f ∈ ↑(Ideal.radical (⨆ (i : ι) (_ : i ∈ s), vanishingIdeal (Z i)))
exact ⟨n, hs⟩
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
hZ : (↑(basicOpen f) ∩ ⋂ (i : ι), Z i) = ∅
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
i : ι
⊢ Z i = zeroLocus ↑(I i)
simpa only [zeroLocus_vanishingIdeal_eq_closure] using (hZc i).closure_eq.symm
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
⊢ f ∈ vanishingIdeal (zeroLocus ↑(⨆ (i : ι), I i))
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
⊢ f ∈ Ideal.radical (⨆ (i : ι), I i)
rw [← vanishingIdeal_zeroLocus_eq_radical]
case a
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
⊢ f ∈ vanishingIdeal (zeroLocus {f})
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
⊢ f ∈ vanishingIdeal (zeroLocus ↑(⨆ (i : ι), I i))
apply vanishingIdeal_anti_mono hZ
no goals
case a
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
ι : Type u
Z : ι → Set (PrimeSpectrum R)
hZc : ∀ (i : ι), IsClosed (Z i)
I : ι → Ideal R := fun i => vanishingIdeal (Z i)
hZ : zeroLocus ↑(⨆ (i : ι), I i) ⊆ zeroLocus {f}
hI : ∀ (i : ι), Z i = zeroLocus ↑(I i)
⊢ f ∈ vanishingIdeal (zeroLocus {f})
exact subset_vanishingIdeal_zeroLocus {f} (Set.mem_singleton f)