case h₁
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ zeroLocus ↑(vanishingIdeal t) ⊆ closure t

case h₂
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ closure t ⊆ zeroLocus ↑(vanishingIdeal t)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ zeroLocus ↑(vanishingIdeal t) = closure t
apply Set.Subset.antisymm
case h₁.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
x : PrimeSpectrum R
hx : x ∈ zeroLocus ↑(vanishingIdeal t)
t' : Set (PrimeSpectrum R)
ht' : IsClosed t'
ht : t ⊆ t'
⊢ x ∈ t'
case h₁
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ zeroLocus ↑(vanishingIdeal t) ⊆ closure t
rintro x hx t' ⟨ht', ht⟩
case h₁.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
x : PrimeSpectrum R
hx : x ∈ zeroLocus ↑(vanishingIdeal t)
fs : Set R
ht' : IsClosed (zeroLocus fs)
ht : t ⊆ zeroLocus fs
⊢ x ∈ zeroLocus fs
case h₁.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
x : PrimeSpectrum R
hx : x ∈ zeroLocus ↑(vanishingIdeal t)
t' : Set (PrimeSpectrum R)
ht' : IsClosed t'
ht : t ⊆ t'
⊢ x ∈ t'
obtain ⟨fs, rfl⟩ : ∃ s, t' = zeroLocus s := by rwa [isClosed_iff_zeroLocus] at ht'
case h₁.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
x : PrimeSpectrum R
hx : x ∈ zeroLocus ↑(vanishingIdeal t)
fs : Set R
ht' : IsClosed (zeroLocus fs)
ht : fs ⊆ ↑(vanishingIdeal t)
⊢ x ∈ zeroLocus fs
case h₁.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
x : PrimeSpectrum R
hx : x ∈ zeroLocus ↑(vanishingIdeal t)
fs : Set R
ht' : IsClosed (zeroLocus fs)
ht : t ⊆ zeroLocus fs
⊢ x ∈ zeroLocus fs
rw [subset_zeroLocus_iff_subset_vanishingIdeal] at ht
no goals
case h₁.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
x : PrimeSpectrum R
hx : x ∈ zeroLocus ↑(vanishingIdeal t)
fs : Set R
ht' : IsClosed (zeroLocus fs)
ht : fs ⊆ ↑(vanishingIdeal t)
⊢ x ∈ zeroLocus fs
exact Set.Subset.trans ht hx
no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
x : PrimeSpectrum R
hx : x ∈ zeroLocus ↑(vanishingIdeal t)
t' : Set (PrimeSpectrum R)
ht' : IsClosed t'
ht : t ⊆ t'
⊢ ∃ s, t' = zeroLocus s
rwa [isClosed_iff_zeroLocus] at ht'
case h₂
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ t ⊆ zeroLocus ↑(vanishingIdeal t)
case h₂
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ closure t ⊆ zeroLocus ↑(vanishingIdeal t)
rw [(isClosed_zeroLocus _).closure_subset_iff]
no goals
case h₂
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ t ⊆ zeroLocus ↑(vanishingIdeal t)
exact subset_zeroLocus_vanishingIdeal t