[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ Function.Bijective (primeSpectrumProdOfSum R S)
[PROOFSTEP]
constructor
[GOAL]
case left
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ Function.Injective (primeSpectrumProdOfSum R S)
[PROOFSTEP]
rintro (⟨I, hI⟩ | ⟨J, hJ⟩) (⟨I', hI'⟩ | ⟨J', hJ'⟩) h
[GOAL]
case left.inl.mk.inl.mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsPrime I
I' : Ideal R
hI' : Ideal.IsPrime I'
h :
  primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, IsPrime := hI }) =
    primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I', IsPrime := hI' })
⊢ Sum.inl { asIdeal := I, IsPrime := hI } = Sum.inl { asIdeal := I', IsPrime := hI' }
[PROOFSTEP]
simp only [mk.injEq, Ideal.prod.ext_iff, primeSpectrumProdOfSum] at h 
[GOAL]
case left.inl.mk.inr.mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsPrime I
J' : Ideal S
hJ' : Ideal.IsPrime J'
h :
  primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I, IsPrime := hI }) =
    primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J', IsPrime := hJ' })
⊢ Sum.inl { asIdeal := I, IsPrime := hI } = Sum.inr { asIdeal := J', IsPrime := hJ' }
[PROOFSTEP]
simp only [mk.injEq, Ideal.prod.ext_iff, primeSpectrumProdOfSum] at h 
[GOAL]
case left.inr.mk.inl.mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
J : Ideal S
hJ : Ideal.IsPrime J
I' : Ideal R
hI' : Ideal.IsPrime I'
h :
  primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, IsPrime := hJ }) =
    primeSpectrumProdOfSum R S (Sum.inl { asIdeal := I', IsPrime := hI' })
⊢ Sum.inr { asIdeal := J, IsPrime := hJ } = Sum.inl { asIdeal := I', IsPrime := hI' }
[PROOFSTEP]
simp only [mk.injEq, Ideal.prod.ext_iff, primeSpectrumProdOfSum] at h 
[GOAL]
case left.inr.mk.inr.mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
J : Ideal S
hJ : Ideal.IsPrime J
J' : Ideal S
hJ' : Ideal.IsPrime J'
h :
  primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J, IsPrime := hJ }) =
    primeSpectrumProdOfSum R S (Sum.inr { asIdeal := J', IsPrime := hJ' })
⊢ Sum.inr { asIdeal := J, IsPrime := hJ } = Sum.inr { asIdeal := J', IsPrime := hJ' }
[PROOFSTEP]
simp only [mk.injEq, Ideal.prod.ext_iff, primeSpectrumProdOfSum] at h 
[GOAL]
case left.inl.mk.inl.mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsPrime I
I' : Ideal R
hI' : Ideal.IsPrime I'
h : I = I' ∧ True
⊢ Sum.inl { asIdeal := I, IsPrime := hI } = Sum.inl { asIdeal := I', IsPrime := hI' }
[PROOFSTEP]
simp only [h]
[GOAL]
case left.inl.mk.inr.mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsPrime I
J' : Ideal S
hJ' : Ideal.IsPrime J'
h : I = ⊤ ∧ ⊤ = J'
⊢ Sum.inl { asIdeal := I, IsPrime := hI } = Sum.inr { asIdeal := J', IsPrime := hJ' }
[PROOFSTEP]
exact False.elim (hI.ne_top h.left)
[GOAL]
case left.inr.mk.inl.mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
J : Ideal S
hJ : Ideal.IsPrime J
I' : Ideal R
hI' : Ideal.IsPrime I'
h : ⊤ = I' ∧ J = ⊤
⊢ Sum.inr { asIdeal := J, IsPrime := hJ } = Sum.inl { asIdeal := I', IsPrime := hI' }
[PROOFSTEP]
exact False.elim (hJ.ne_top h.right)
[GOAL]
case left.inr.mk.inr.mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
J : Ideal S
hJ : Ideal.IsPrime J
J' : Ideal S
hJ' : Ideal.IsPrime J'
h : True ∧ J = J'
⊢ Sum.inr { asIdeal := J, IsPrime := hJ } = Sum.inr { asIdeal := J', IsPrime := hJ' }
[PROOFSTEP]
simp only [h]
[GOAL]
case right
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ Function.Surjective (primeSpectrumProdOfSum R S)
[PROOFSTEP]
rintro ⟨I, hI⟩
[GOAL]
case right.mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal (R × S)
hI : Ideal.IsPrime I
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := I, IsPrime := hI }
[PROOFSTEP]
rcases(Ideal.ideal_prod_prime I).mp hI with (⟨p, ⟨hp, rfl⟩⟩ | ⟨p, ⟨hp, rfl⟩⟩)
[GOAL]
case right.mk.inl.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : Ideal R
hp : Ideal.IsPrime p
hI : Ideal.IsPrime (Ideal.prod p ⊤)
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := Ideal.prod p ⊤, IsPrime := hI }
[PROOFSTEP]
exact ⟨Sum.inl ⟨p, hp⟩, rfl⟩
[GOAL]
case right.mk.inr.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : Ideal S
hp : Ideal.IsPrime p
hI : Ideal.IsPrime (Ideal.prod ⊤ p)
⊢ ∃ a, primeSpectrumProdOfSum R S a = { asIdeal := Ideal.prod ⊤ p, IsPrime := hI }
[PROOFSTEP]
exact ⟨Sum.inr ⟨p, hp⟩, rfl⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
⊢ (↑(primeSpectrumProd R S).symm (Sum.inl x)).asIdeal = Ideal.prod x.asIdeal ⊤
[PROOFSTEP]
cases x
[GOAL]
case mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
asIdeal✝ : Ideal R
IsPrime✝ : Ideal.IsPrime asIdeal✝
⊢ (↑(primeSpectrumProd R S).symm (Sum.inl { asIdeal := asIdeal✝, IsPrime := IsPrime✝ })).asIdeal =
    Ideal.prod { asIdeal := asIdeal✝, IsPrime := IsPrime✝ }.asIdeal ⊤
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum S
⊢ (↑(primeSpectrumProd R S).symm (Sum.inr x)).asIdeal = Ideal.prod ⊤ x.asIdeal
[PROOFSTEP]
cases x
[GOAL]
case mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
asIdeal✝ : Ideal S
IsPrime✝ : Ideal.IsPrime asIdeal✝
⊢ (↑(primeSpectrumProd R S).symm (Sum.inr { asIdeal := asIdeal✝, IsPrime := IsPrime✝ })).asIdeal =
    Ideal.prod ⊤ { asIdeal := asIdeal✝, IsPrime := IsPrime✝ }.asIdeal
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
⊢ zeroLocus ↑(Ideal.span s) = zeroLocus s
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
x : PrimeSpectrum R
⊢ x ∈ zeroLocus ↑(Ideal.span s) ↔ x ∈ zeroLocus s
[PROOFSTEP]
exact (Submodule.gi R R).gc s x.asIdeal
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ ↑(vanishingIdeal t) = {f | ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal}
[PROOFSTEP]
ext f
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
⊢ f ∈ ↑(vanishingIdeal t) ↔ f ∈ {f | ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal}
[PROOFSTEP]
rw [vanishingIdeal, SetLike.mem_coe, Submodule.mem_iInf]
[GOAL]
case h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
⊢ (∀ (i : PrimeSpectrum R), f ∈ ⨅ (_ : i ∈ t), i.asIdeal) ↔ f ∈ {f | ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal}
[PROOFSTEP]
apply forall_congr'
[GOAL]
case h.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
⊢ ∀ (a : PrimeSpectrum R), f ∈ ⨅ (_ : a ∈ t), a.asIdeal ↔ a ∈ t → f ∈ a.asIdeal
[PROOFSTEP]
intro x
[GOAL]
case h.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
x : PrimeSpectrum R
⊢ f ∈ ⨅ (_ : x ∈ t), x.asIdeal ↔ x ∈ t → f ∈ x.asIdeal
[PROOFSTEP]
rw [Submodule.mem_iInf]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
f : R
⊢ f ∈ vanishingIdeal t ↔ ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal
[PROOFSTEP]
rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
⊢ vanishingIdeal {x} = x.asIdeal
[PROOFSTEP]
simp [vanishingIdeal]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ GaloisConnection (fun s => zeroLocus s) fun t => ↑(vanishingIdeal t)
[PROOFSTEP]
have ideal_gc : GaloisConnection Ideal.span _ := (Submodule.gi R R).gc
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
ideal_gc : GaloisConnection Ideal.span SetLike.coe
⊢ GaloisConnection (fun s => zeroLocus s) fun t => ↑(vanishingIdeal t)
[PROOFSTEP]
simpa [zeroLocus_span, Function.comp] using ideal_gc.compose (gc R)
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
f : R
⊢ f ∈ vanishingIdeal (zeroLocus ↑I) ↔ f ∈ Ideal.radical I
[PROOFSTEP]
rw [mem_vanishingIdeal, Ideal.radical_eq_sInf, Submodule.mem_sInf]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
f : R
⊢ (∀ (x : PrimeSpectrum R), x ∈ zeroLocus ↑I → f ∈ x.asIdeal) ↔
    ∀ (p : Submodule R R), p ∈ {J | I ≤ J ∧ Ideal.IsPrime J} → f ∈ p
[PROOFSTEP]
exact ⟨fun h x hx => h ⟨x, hx.2⟩ hx.1, fun h x hx => h x.1 ⟨hx, x.2⟩⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f g : R
⊢ zeroLocus {f} ⊆ zeroLocus {g} ↔ g ∈ Ideal.radical (Ideal.span {f})
[PROOFSTEP]
rw [← zeroLocus_span { f }, ← zeroLocus_span { g }, zeroLocus_subset_zeroLocus_iff, Ideal.span_le,
  Set.singleton_subset_iff, SetLike.mem_coe]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ vanishingIdeal ∅ = ⊤
[PROOFSTEP]
simpa using (gc R).u_top
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
⊢ zeroLocus s = ∅
[PROOFSTEP]
rw [Set.eq_empty_iff_forall_not_mem]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
⊢ ∀ (x : PrimeSpectrum R), ¬x ∈ zeroLocus s
[PROOFSTEP]
intro x hx
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : x ∈ zeroLocus s
⊢ False
[PROOFSTEP]
rw [mem_zeroLocus] at hx 
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ False
[PROOFSTEP]
have x_prime : x.asIdeal.IsPrime := by infer_instance
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
⊢ Ideal.IsPrime x.asIdeal
[PROOFSTEP]
infer_instance
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : Ideal.IsPrime x.asIdeal
⊢ False
[PROOFSTEP]
have eq_top : x.asIdeal = ⊤ := by
  rw [Ideal.eq_top_iff_one]
  exact hx h
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : Ideal.IsPrime x.asIdeal
⊢ x.asIdeal = ⊤
[PROOFSTEP]
rw [Ideal.eq_top_iff_one]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : Ideal.IsPrime x.asIdeal
⊢ 1 ∈ x.asIdeal
[PROOFSTEP]
exact hx h
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
h : 1 ∈ s
x : PrimeSpectrum R
hx : s ⊆ ↑x.asIdeal
x_prime : Ideal.IsPrime x.asIdeal
eq_top : x.asIdeal = ⊤
⊢ False
[PROOFSTEP]
apply x_prime.ne_top eq_top
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ zeroLocus ↑I = ∅ ↔ I = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ zeroLocus ↑I = ∅ → I = ⊤
[PROOFSTEP]
contrapose!
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ I ≠ ⊤ → zeroLocus ↑I ≠ ∅
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
h : I ≠ ⊤
⊢ zeroLocus ↑I ≠ ∅
[PROOFSTEP]
rcases Ideal.exists_le_maximal I h with ⟨M, hM, hIM⟩
[GOAL]
case mp.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
h : I ≠ ⊤
M : Ideal R
hM : Ideal.IsMaximal M
hIM : I ≤ M
⊢ zeroLocus ↑I ≠ ∅
[PROOFSTEP]
exact Set.Nonempty.ne_empty ⟨⟨M, hM.isPrime⟩, hIM⟩
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
⊢ I = ⊤ → zeroLocus ↑I = ∅
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ zeroLocus ↑⊤ = ∅
[PROOFSTEP]
apply zeroLocus_empty_of_one_mem
[GOAL]
case mpr.h
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ 1 ∈ ↑⊤
[PROOFSTEP]
trivial
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s = ⊤ ↔ s = ∅
[PROOFSTEP]
rw [← top_le_iff, ← subset_zeroLocus_iff_le_vanishingIdeal, Submodule.top_coe, zeroLocus_univ, Set.subset_empty_iff]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set (Set R)
⊢ zeroLocus (⋃ (s' : Set R) (_ : s' ∈ s), s') = ⋂ (s' : Set R) (_ : s' ∈ s), zeroLocus s'
[PROOFSTEP]
simp only [zeroLocus_iUnion]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s s' : Set R
⊢ zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s ⊓ Ideal.span s')
[PROOFSTEP]
rw [zeroLocus_inf]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s s' : Set R
⊢ zeroLocus s ∪ zeroLocus s' = zeroLocus ↑(Ideal.span s) ∪ zeroLocus ↑(Ideal.span s')
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f g : R
x : PrimeSpectrum R
⊢ x ∈ zeroLocus {f * g} ↔ x ∈ zeroLocus {f} ∪ zeroLocus {g}
[PROOFSTEP]
simpa using x.2.mul_mem_iff_mem_or_mem
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
n : ℕ
hn : 0 < n
x : PrimeSpectrum R
⊢ x ∈ zeroLocus {f ^ n} ↔ x ∈ zeroLocus {f}
[PROOFSTEP]
simpa using x.2.pow_mem_iff_mem n hn
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
⊢ vanishingIdeal t ⊔ vanishingIdeal t' ≤ vanishingIdeal (t ∩ t')
[PROOFSTEP]
intro r
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
r : R
⊢ r ∈ vanishingIdeal t ⊔ vanishingIdeal t' → r ∈ vanishingIdeal (t ∩ t')
[PROOFSTEP]
rw [Submodule.mem_sup, mem_vanishingIdeal]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
r : R
⊢ (∃ y, y ∈ vanishingIdeal t ∧ ∃ z, z ∈ vanishingIdeal t' ∧ y + z = r) →
    ∀ (x : PrimeSpectrum R), x ∈ t ∩ t' → r ∈ x.asIdeal
[PROOFSTEP]
rintro ⟨f, hf, g, hg, rfl⟩ x ⟨hxt, hxt'⟩
[GOAL]
case intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
f : R
hf : f ∈ vanishingIdeal t
g : R
hg : g ∈ vanishingIdeal t'
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal
[PROOFSTEP]
rw [mem_vanishingIdeal] at hf hg 
[GOAL]
case intro.intro.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal
g : R
hg : ∀ (x : PrimeSpectrum R), x ∈ t' → g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f + g ∈ x.asIdeal
[PROOFSTEP]
apply Submodule.add_mem
[GOAL]
case intro.intro.intro.intro.intro.h₁
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal
g : R
hg : ∀ (x : PrimeSpectrum R), x ∈ t' → g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ f ∈ x.asIdeal
[PROOFSTEP]
solve_by_elim
[GOAL]
case intro.intro.intro.intro.intro.h₂
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t t' : Set (PrimeSpectrum R)
f : R
hf : ∀ (x : PrimeSpectrum R), x ∈ t → f ∈ x.asIdeal
g : R
hg : ∀ (x : PrimeSpectrum R), x ∈ t' → g ∈ x.asIdeal
x : PrimeSpectrum R
hxt : x ∈ t
hxt' : x ∈ t'
⊢ g ∈ x.asIdeal
[PROOFSTEP]
solve_by_elim
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
I : PrimeSpectrum R
⊢ I ∈ (zeroLocus {f})ᶜ ↔ ¬f ∈ I.asIdeal
[PROOFSTEP]
rw [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
I : PrimeSpectrum R
⊢ ¬f ∈ ↑I.asIdeal ↔ ¬f ∈ I.asIdeal
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ zeroLocus Set.univ = ∅
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (A : Set (Set (PrimeSpectrum R))), A ⊆ Set.range zeroLocus → ⋂₀ A ∈ Set.range zeroLocus
[PROOFSTEP]
intro Zs h
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
⊢ ⋂₀ Zs ∈ Set.range zeroLocus
[PROOFSTEP]
rw [Set.sInter_eq_iInter]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
⊢ ⋂ (i : ↑Zs), ↑i ∈ Set.range zeroLocus
[PROOFSTEP]
choose f hf using fun i : Zs => h i.prop
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
f : ↑Zs → Set R
hf : ∀ (i : ↑Zs), zeroLocus (f i) = ↑i
⊢ ⋂ (i : ↑Zs), ↑i ∈ Set.range zeroLocus
[PROOFSTEP]
simp only [← hf]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
Zs : Set (Set (PrimeSpectrum R))
h : Zs ⊆ Set.range zeroLocus
f : ↑Zs → Set R
hf : ∀ (i : ↑Zs), zeroLocus (f i) = ↑i
⊢ ⋂ (i : ↑Zs), zeroLocus (f i) ∈ Set.range zeroLocus
[PROOFSTEP]
exact ⟨_, zeroLocus_iUnion _⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (A : Set (PrimeSpectrum R)),
    A ∈ Set.range zeroLocus → ∀ (B : Set (PrimeSpectrum R)), B ∈ Set.range zeroLocus → A ∪ B ∈ Set.range zeroLocus
[PROOFSTEP]
rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩
[GOAL]
case intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s t : Set R
⊢ zeroLocus s ∪ zeroLocus t ∈ Set.range zeroLocus
[PROOFSTEP]
exact ⟨_, (union_zeroLocus s t).symm⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
U : Set (PrimeSpectrum R)
⊢ IsOpen U ↔ ∃ s, Uᶜ = zeroLocus s
[PROOFSTEP]
simp only [@eq_comm _ Uᶜ]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
U : Set (PrimeSpectrum R)
⊢ IsOpen U ↔ ∃ s, zeroLocus s = Uᶜ
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
Z : Set (PrimeSpectrum R)
⊢ IsClosed Z ↔ ∃ s, Z = zeroLocus s
[PROOFSTEP]
rw [← isOpen_compl_iff, isOpen_iff, compl_compl]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
⊢ IsClosed (zeroLocus s)
[PROOFSTEP]
rw [isClosed_iff_zeroLocus]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set R
⊢ ∃ s_1, zeroLocus s = zeroLocus s_1
[PROOFSTEP]
exact ⟨s, rfl⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
⊢ IsClosed {x} ↔ Ideal.IsMaximal x.asIdeal
[PROOFSTEP]
refine' (isClosed_iff_zeroLocus _).trans ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
h : ∃ s, {x} = zeroLocus s
⊢ Ideal.IsMaximal x.asIdeal
[PROOFSTEP]
obtain ⟨s, hs⟩ := h
[GOAL]
case refine'_1.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
s : Set R
hs : {x} = zeroLocus s
⊢ Ideal.IsMaximal x.asIdeal
[PROOFSTEP]
rw [eq_comm, Set.eq_singleton_iff_unique_mem] at hs 
[GOAL]
case refine'_1.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
s : Set R
hs : x ∈ zeroLocus s ∧ ∀ (x_1 : PrimeSpectrum R), x_1 ∈ zeroLocus s → x_1 = x
⊢ Ideal.IsMaximal x.asIdeal
[PROOFSTEP]
refine'
  ⟨⟨x.2.1, fun I hI =>
      Classical.not_not.1 (mt (Ideal.exists_le_maximal I) <| not_exists.2 fun J => not_and.2 fun hJ hIJ => _)⟩⟩
[GOAL]
case refine'_1.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
s : Set R
hs : x ∈ zeroLocus s ∧ ∀ (x_1 : PrimeSpectrum R), x_1 ∈ zeroLocus s → x_1 = x
I : Ideal R
hI : x.asIdeal < I
J : Ideal R
hJ : Ideal.IsMaximal J
hIJ : I ≤ J
⊢ False
[PROOFSTEP]
exact
  ne_of_lt (lt_of_lt_of_le hI hIJ)
    (symm <| congr_arg PrimeSpectrum.asIdeal (hs.2 ⟨J, hJ.isPrime⟩ fun r hr => hIJ (le_of_lt hI <| hs.1 hr)))
[GOAL]
case refine'_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
h : Ideal.IsMaximal x.asIdeal
⊢ ∃ s, {x} = zeroLocus s
[PROOFSTEP]
refine' ⟨x.asIdeal.1, _⟩
[GOAL]
case refine'_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
h : Ideal.IsMaximal x.asIdeal
⊢ {x} = zeroLocus ↑x.asIdeal.toAddSubmonoid
[PROOFSTEP]
rw [eq_comm, Set.eq_singleton_iff_unique_mem]
[GOAL]
case refine'_2
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
h : Ideal.IsMaximal x.asIdeal
⊢ x ∈ zeroLocus ↑x.asIdeal.toAddSubmonoid ∧
    ∀ (x_1 : PrimeSpectrum R), x_1 ∈ zeroLocus ↑x.asIdeal.toAddSubmonoid → x_1 = x
[PROOFSTEP]
refine' ⟨fun _ h => h, fun y hy => PrimeSpectrum.ext _ _ (h.eq_of_le y.2.ne_top hy).symm⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ zeroLocus ↑(vanishingIdeal t) = closure t
[PROOFSTEP]
apply Set.Subset.antisymm
[GOAL]
case h₁
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ zeroLocus ↑(vanishingIdeal t) ⊆ closure t
[PROOFSTEP]
rintro x hx t' ⟨ht', ht⟩
[GOAL]
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'
[PROOFSTEP]
obtain ⟨fs, rfl⟩ : ∃ s, t' = zeroLocus s := by rwa [isClosed_iff_zeroLocus] at ht' 
[GOAL]
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
[PROOFSTEP]
rwa [isClosed_iff_zeroLocus] at ht' 
[GOAL]
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
[PROOFSTEP]
rw [subset_zeroLocus_iff_subset_vanishingIdeal] at ht 
[GOAL]
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
[PROOFSTEP]
exact Set.Subset.trans ht hx
[GOAL]
case h₂
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ closure t ⊆ zeroLocus ↑(vanishingIdeal t)
[PROOFSTEP]
rw [(isClosed_zeroLocus _).closure_subset_iff]
[GOAL]
case h₂
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
t : Set (PrimeSpectrum R)
⊢ t ⊆ zeroLocus ↑(vanishingIdeal t)
[PROOFSTEP]
exact subset_zeroLocus_vanishingIdeal t
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x : PrimeSpectrum R
⊢ closure {x} = zeroLocus ↑x.asIdeal
[PROOFSTEP]
rw [← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_singleton]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set (PrimeSpectrum R)
⊢ Ideal.IsRadical (vanishingIdeal s)
[PROOFSTEP]
rw [← vanishingIdeal_closure, ← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_zeroLocus_eq_radical]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set (PrimeSpectrum R)
⊢ Ideal.IsRadical (Ideal.radical (vanishingIdeal s))
[PROOFSTEP]
apply Ideal.radical_isRadical
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ s ⊆ t
[PROOFSTEP]
rw [← ht.closure_subset_iff, ← ht.closure_eq]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ closure s ⊆ closure t
[PROOFSTEP]
convert ← zeroLocus_anti_mono_ideal h
[GOAL]
case h.e'_3
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ zeroLocus ↑(vanishingIdeal s) = closure s
[PROOFSTEP]
apply zeroLocus_vanishingIdeal_eq_closure
[GOAL]
case h.e'_4
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s t : Set (PrimeSpectrum R)
ht : IsClosed t
h : vanishingIdeal t ≤ vanishingIdeal s
⊢ zeroLocus ↑(vanishingIdeal t) = closure t
[PROOFSTEP]
apply zeroLocus_vanishingIdeal_eq_closure
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s t : Set (PrimeSpectrum R)
hs : IsClosed s
ht : IsClosed t
⊢ s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s
[PROOFSTEP]
rw [Set.ssubset_def, vanishingIdeal_anti_mono_iff hs, vanishingIdeal_anti_mono_iff ht, lt_iff_le_not_le]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
⊢ T1Space (PrimeSpectrum R) ↔ IsField R
[PROOFSTEP]
refine' ⟨_, fun h => _⟩
[GOAL]
case refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
⊢ T1Space (PrimeSpectrum R) → IsField R
[PROOFSTEP]
intro h
[GOAL]
case refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
⊢ IsField R
[PROOFSTEP]
have hbot : Ideal.IsPrime (⊥ : Ideal R) := Ideal.bot_prime
[GOAL]
case refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
hbot : Ideal.IsPrime ⊥
⊢ IsField R
[PROOFSTEP]
exact
  Classical.not_not.1
    (mt (Ring.ne_bot_of_isMaximal_of_not_isField <| (isClosed_singleton_iff_isMaximal _).1 (T1Space.t1 ⟨⊥, hbot⟩))
      (by aesop))
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : T1Space (PrimeSpectrum R)
hbot : Ideal.IsPrime ⊥
⊢ ¬{ asIdeal := ⊥, IsPrime := hbot }.asIdeal ≠ ⊥
[PROOFSTEP]
aesop
[GOAL]
case refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
⊢ T1Space (PrimeSpectrum R)
[PROOFSTEP]
refine' ⟨fun x => (isClosed_singleton_iff_isMaximal x).2 _⟩
[GOAL]
case refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
⊢ Ideal.IsMaximal x.asIdeal
[PROOFSTEP]
by_cases hx : x.asIdeal = ⊥
[GOAL]
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
⊢ Ideal.IsMaximal x.asIdeal
[PROOFSTEP]
letI := h.toField
[GOAL]
case pos
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : x.asIdeal = ⊥
this : Field R := IsField.toField h
⊢ Ideal.IsMaximal x.asIdeal
[PROOFSTEP]
exact hx.symm ▸ Ideal.bot_isMaximal
[GOAL]
case neg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
h : IsField R
x : PrimeSpectrum R
hx : ¬x.asIdeal = ⊥
⊢ Ideal.IsMaximal x.asIdeal
[PROOFSTEP]
exact absurd h (Ring.not_isField_iff_exists_prime.2 ⟨x.asIdeal, ⟨hx, x.2⟩⟩)
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ IsIrreducible (zeroLocus ↑I) ↔ Ideal.IsPrime I
[PROOFSTEP]
rw [Ideal.isPrime_iff, IsIrreducible]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ Set.Nonempty (zeroLocus ↑I) ∧ IsPreirreducible (zeroLocus ↑I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
apply and_congr
[GOAL]
case h₁
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ Set.Nonempty (zeroLocus ↑I) ↔ I ≠ ⊤
[PROOFSTEP]
rw [Set.nonempty_iff_ne_empty, Ne.def, zeroLocus_empty_iff_eq_top]
[GOAL]
case h₂
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ IsPreirreducible (zeroLocus ↑I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
trans ∀ x y : Ideal R, Z(I) ⊆ Z(x) ∪ Z(y) → Z(I) ⊆ Z(x) ∨ Z(I) ⊆ Z(y)
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ IsPreirreducible (zeroLocus ↑I) ↔
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
[PROOFSTEP]
simp_rw [isPreirreducible_iff_closed_union_closed, isClosed_iff_zeroLocus_ideal]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂) ↔
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂) →
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
[PROOFSTEP]
rintro h x y
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h :
  ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
    (∃ I, z₁ = zeroLocus ↑I) → (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂
x y : Ideal R
⊢ zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
[PROOFSTEP]
exact h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) →
    ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂
[PROOFSTEP]
rintro h _ _ ⟨x, rfl⟩ ⟨y, rfl⟩
[GOAL]
case mpr.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h :
  ∀ (x y : Ideal R),
    zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
x y : Ideal R
⊢ zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
[PROOFSTEP]
exact h x y
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
simp_rw [← zeroLocus_inf, subset_zeroLocus_iff_le_vanishingIdeal, vanishingIdeal_zeroLocus_eq_radical, hI.radical]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) ↔ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) → ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
[PROOFSTEP]
simp_rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Ideal.span_le, ← Ideal.span_singleton_mul_span_singleton]
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) →
    ∀ {x y : R}, Ideal.span {x} * Ideal.span {y} ≤ I → Ideal.span {x} ≤ I ∨ Ideal.span {y} ≤ I
[PROOFSTEP]
refine' fun h x y h' => h _ _ _
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : Ideal.span {x} * Ideal.span {y} ≤ I
⊢ Ideal.span {x} ⊓ Ideal.span {y} ≤ I
[PROOFSTEP]
rw [← hI.radical_le_iff] at h' ⊢
[GOAL]
case mp
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h : ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
x y : R
h' : Ideal.radical (Ideal.span {x} * Ideal.span {y}) ≤ I
⊢ Ideal.radical (Ideal.span {x} ⊓ Ideal.span {y}) ≤ I
[PROOFSTEP]
simpa only [Ideal.radical_inf, Ideal.radical_mul] using h'
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
[PROOFSTEP]
simp_rw [or_iff_not_imp_left, SetLike.not_le_iff_exists]
[GOAL]
case mpr
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
⊢ (∀ {x y : R}, x * y ∈ I → ¬x ∈ I → y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → (∃ x_1, x_1 ∈ x ∧ ¬x_1 ∈ I) → y ≤ I
[PROOFSTEP]
rintro h s t h' ⟨x, hx, hx'⟩ y hy
[GOAL]
case mpr.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
I : Ideal R
hI : Ideal.IsRadical I
h : ∀ {x y : R}, x * y ∈ I → ¬x ∈ I → y ∈ I
s t : Ideal R
h' : s ⊓ t ≤ I
x : R
hx : x ∈ s
hx' : ¬x ∈ I
y : R
hy : y ∈ t
⊢ y ∈ I
[PROOFSTEP]
exact h (h' ⟨Ideal.mul_mem_right _ _ hx, Ideal.mul_mem_left _ _ hy⟩) hx'
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set (PrimeSpectrum R)
⊢ IsIrreducible s ↔ Ideal.IsPrime (vanishingIdeal s)
[PROOFSTEP]
rw [← isIrreducible_iff_closure, ← zeroLocus_vanishingIdeal_eq_closure,
  isIrreducible_zeroLocus_iff_of_radical _ (isRadical_vanishingIdeal s)]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
⊢ IrreducibleSpace (PrimeSpectrum R)
[PROOFSTEP]
rw [irreducibleSpace_def, Set.top_eq_univ, ← zeroLocus_bot, isIrreducible_zeroLocus_iff]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : IsDomain R
⊢ Ideal.IsPrime (Ideal.radical ⊥)
[PROOFSTEP]
simpa using Ideal.bot_prime
[GOAL]
R : Type u
S✝ : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S✝
S : Set (PrimeSpectrum R)
h₁ : IsIrreducible S
h₂ : IsClosed S
⊢ IsGenericPoint { asIdeal := vanishingIdeal S, IsPrime := (_ : Ideal.IsPrime (vanishingIdeal S)) } S
[PROOFSTEP]
rw [IsGenericPoint, closure_singleton, zeroLocus_vanishingIdeal_eq_closure, h₂.closure_eq]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
s : Set R
⊢ (fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }) ⁻¹'
      zeroLocus s =
    zeroLocus (↑f '' s)
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
s : Set R
x : PrimeSpectrum S
⊢ x ∈
      (fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }) ⁻¹'
        zeroLocus s ↔
    x ∈ zeroLocus (↑f '' s)
[PROOFSTEP]
simp only [mem_zeroLocus, Set.image_subset_iff]
[GOAL]
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
s : Set R
x : PrimeSpectrum S
⊢ x ∈
      (fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }) ⁻¹'
        zeroLocus s ↔
    s ⊆ (fun a => ↑f a) ⁻¹' ↑x.asIdeal
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
⊢ Continuous fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }
[PROOFSTEP]
simp only [continuous_iff_isClosed, isClosed_iff_zeroLocus]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
⊢ ∀ (s : Set (PrimeSpectrum R)),
    (∃ s_1, s = zeroLocus s_1) →
      ∃ s_1,
        (fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }) ⁻¹'
            s =
          zeroLocus s_1
[PROOFSTEP]
rintro _ ⟨s, rfl⟩
[GOAL]
case intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
s : Set R
⊢ ∃ s_1,
    (fun y => { asIdeal := Ideal.comap f y.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.comap f y.asIdeal)) }) ⁻¹'
        zeroLocus s =
      zeroLocus s_1
[PROOFSTEP]
exact ⟨_, preimage_comap_zeroLocus_aux f s⟩
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
⊢ comap (RingHom.id R) = ContinuousMap.id (PrimeSpectrum R)
[PROOFSTEP]
ext
[GOAL]
case h.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
a✝ : PrimeSpectrum R
x✝ : R
⊢ x✝ ∈ (↑(comap (RingHom.id R)) a✝).asIdeal ↔ x✝ ∈ (↑(ContinuousMap.id (PrimeSpectrum R)) a✝).asIdeal
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Inducing ↑(comap (algebraMap R S))
[PROOFSTEP]
constructor
[GOAL]
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ zariskiTopology = TopologicalSpace.induced (↑(comap (algebraMap R S))) zariskiTopology
[PROOFSTEP]
rw [topologicalSpace_eq_iff]
[GOAL]
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ ∀ (s : Set (PrimeSpectrum S)), IsOpen s ↔ IsOpen s
[PROOFSTEP]
intro U
[GOAL]
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
U : Set (PrimeSpectrum S)
⊢ IsOpen U ↔ IsOpen U
[PROOFSTEP]
rw [← isClosed_compl_iff, ← @isClosed_compl_iff (α := PrimeSpectrum S) (s := U)]
[GOAL]
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
U : Set (PrimeSpectrum S)
⊢ IsClosed Uᶜ ↔ IsClosed Uᶜ
[PROOFSTEP]
generalize Uᶜ = Z
[GOAL]
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
U Z : Set (PrimeSpectrum S)
⊢ IsClosed Z ↔ IsClosed Z
[PROOFSTEP]
simp_rw [isClosed_induced_iff, isClosed_iff_zeroLocus]
[GOAL]
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
U Z : Set (PrimeSpectrum S)
⊢ (∃ s, Z = zeroLocus s) ↔ ∃ t, (∃ s, t = zeroLocus s) ∧ ↑(comap (algebraMap R S)) ⁻¹' t = Z
[PROOFSTEP]
constructor
[GOAL]
case induced.mp
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
U Z : Set (PrimeSpectrum S)
⊢ (∃ s, Z = zeroLocus s) → ∃ t, (∃ s, t = zeroLocus s) ∧ ↑(comap (algebraMap R S)) ⁻¹' t = Z
[PROOFSTEP]
rintro ⟨s, rfl⟩
[GOAL]
case induced.mp.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
U : Set (PrimeSpectrum S)
s : Set S
⊢ ∃ t, (∃ s, t = zeroLocus s) ∧ ↑(comap (algebraMap R S)) ⁻¹' t = zeroLocus s
[PROOFSTEP]
refine ⟨_, ⟨algebraMap R S ⁻¹' Ideal.span s, rfl⟩, ?_⟩
[GOAL]
case induced.mp.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
U : Set (PrimeSpectrum S)
s : Set S
⊢ ↑(comap (algebraMap R S)) ⁻¹' zeroLocus (↑(algebraMap R S) ⁻¹' ↑(Ideal.span s)) = zeroLocus s
[PROOFSTEP]
rw [preimage_comap_zeroLocus, ← zeroLocus_span, ← zeroLocus_span s]
[GOAL]
case induced.mp.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
U : Set (PrimeSpectrum S)
s : Set S
⊢ zeroLocus ↑(Ideal.span (↑(algebraMap R S) '' (↑(algebraMap R S) ⁻¹' ↑(Ideal.span s)))) = zeroLocus ↑(Ideal.span s)
[PROOFSTEP]
congr 2
[GOAL]
case induced.mp.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
U : Set (PrimeSpectrum S)
s : Set S
⊢ zeroLocus ↑(Ideal.span (↑(algebraMap R S) '' (↑(algebraMap R S) ⁻¹' ↑(Ideal.span s)))) = zeroLocus ↑(Ideal.span s)
[PROOFSTEP]
exact congr_arg (zeroLocus ·) <| Submodule.carrier_inj.mpr (IsLocalization.map_comap M S (Ideal.span s))
[GOAL]
case induced.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
U Z : Set (PrimeSpectrum S)
⊢ (∃ t, (∃ s, t = zeroLocus s) ∧ ↑(comap (algebraMap R S)) ⁻¹' t = Z) → ∃ s, Z = zeroLocus s
[PROOFSTEP]
rintro ⟨_, ⟨t, rfl⟩, rfl⟩
[GOAL]
case induced.mpr.intro.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
U : Set (PrimeSpectrum S)
t : Set R
⊢ ∃ s, ↑(comap (algebraMap R S)) ⁻¹' zeroLocus t = zeroLocus s
[PROOFSTEP]
rw [preimage_comap_zeroLocus]
[GOAL]
case induced.mpr.intro.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
U : Set (PrimeSpectrum S)
t : Set R
⊢ ∃ s, zeroLocus (↑(algebraMap R S) '' t) = zeroLocus s
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Function.Injective ↑(comap (algebraMap R S))
[PROOFSTEP]
intro p q h
[GOAL]
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h : ↑(comap (algebraMap R S)) p = ↑(comap (algebraMap R S)) q
⊢ p = q
[PROOFSTEP]
replace h := congr_arg (fun x : PrimeSpectrum R => Ideal.map (algebraMap R S) x.asIdeal) h
[GOAL]
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h :
  (fun x => Ideal.map (algebraMap R S) x.asIdeal) (↑(comap (algebraMap R S)) p) =
    (fun x => Ideal.map (algebraMap R S) x.asIdeal) (↑(comap (algebraMap R S)) q)
⊢ p = q
[PROOFSTEP]
dsimp only [comap, ContinuousMap.coe_mk] at h 
[GOAL]
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h :
  Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) p.asIdeal) =
    Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) q.asIdeal)
⊢ p = q
[PROOFSTEP]
rw [IsLocalization.map_comap M S, IsLocalization.map_comap M S] at h 
[GOAL]
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h : p.asIdeal = q.asIdeal
⊢ p = q
[PROOFSTEP]
ext1
[GOAL]
case asIdeal
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p q : PrimeSpectrum S
h : p.asIdeal = q.asIdeal
⊢ p.asIdeal = q.asIdeal
[PROOFSTEP]
exact h
[GOAL]
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Set.range ↑(comap (algebraMap R S)) = {p | Disjoint ↑M ↑p.asIdeal}
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range ↑(comap (algebraMap R S)) ↔ x ∈ {p | Disjoint ↑M ↑p.asIdeal}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range ↑(comap (algebraMap R S)) → x ∈ {p | Disjoint ↑M ↑p.asIdeal}
[PROOFSTEP]
simp_rw [disjoint_iff_inf_le]
[GOAL]
case h.mp
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ Set.range ↑(comap (algebraMap R S)) → x ∈ {p | ↑M ⊓ ↑p.asIdeal ≤ ⊥}
[PROOFSTEP]
rintro ⟨p, rfl⟩ x ⟨hx₁, hx₂⟩
[GOAL]
case h.mp.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
p : PrimeSpectrum S
x : R
hx₁ : x ∈ ↑M
hx₂ : x ∈ ↑(↑(comap (algebraMap R S)) p).asIdeal
⊢ x ∈ ⊥
[PROOFSTEP]
exact (p.2.1 : ¬_) (p.asIdeal.eq_top_of_isUnit_mem hx₂ (IsLocalization.map_units S ⟨x, hx₁⟩))
[GOAL]
case h.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
⊢ x ∈ {p | Disjoint ↑M ↑p.asIdeal} → x ∈ Set.range ↑(comap (algebraMap R S))
[PROOFSTEP]
intro h
[GOAL]
case h.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ x ∈ Set.range ↑(comap (algebraMap R S))
[PROOFSTEP]
use⟨x.asIdeal.map (algebraMap R S), IsLocalization.isPrime_of_isPrime_disjoint M S _ x.2 h⟩
[GOAL]
case h
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ ↑(comap (algebraMap R S))
      { asIdeal := Ideal.map (algebraMap R S) x.asIdeal,
        IsPrime := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) x.asIdeal)) } =
    x
[PROOFSTEP]
ext1
[GOAL]
case h.asIdeal
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type u_1
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ (↑(comap (algebraMap R S))
        { asIdeal := Ideal.map (algebraMap R S) x.asIdeal,
          IsPrime := (_ : Ideal.IsPrime (Ideal.map (algebraMap R S) x.asIdeal)) }).asIdeal =
    x.asIdeal
[PROOFSTEP]
exact IsLocalization.comap_map_of_isPrime_disjoint M S _ x.2 h
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ zariskiTopology = TopologicalSpace.induced (↑(comap f)) zariskiTopology
[PROOFSTEP]
simp_rw [topologicalSpace_eq_iff, ← isClosed_compl_iff, ←
  @isClosed_compl_iff (PrimeSpectrum S) ((TopologicalSpace.induced (comap f) zariskiTopology)), isClosed_induced_iff,
  isClosed_iff_zeroLocus]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ ∀ (s : Set (PrimeSpectrum S)), (∃ s_1, sᶜ = zeroLocus s_1) ↔ ∃ t, (∃ s, t = zeroLocus s) ∧ ↑(comap f) ⁻¹' t = sᶜ
[PROOFSTEP]
refine' fun s =>
  ⟨fun ⟨F, hF⟩ =>
    ⟨zeroLocus (f ⁻¹' F), ⟨f ⁻¹' F, rfl⟩, by rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]⟩,
    _⟩
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
s : Set (PrimeSpectrum S)
x✝ : ∃ s_1, sᶜ = zeroLocus s_1
F : Set S
hF : sᶜ = zeroLocus F
⊢ ↑(comap f) ⁻¹' zeroLocus (↑f ⁻¹' F) = sᶜ
[PROOFSTEP]
rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
s : Set (PrimeSpectrum S)
⊢ (∃ t, (∃ s, t = zeroLocus s) ∧ ↑(comap f) ⁻¹' t = sᶜ) → ∃ s_1, sᶜ = zeroLocus s_1
[PROOFSTEP]
rintro ⟨-, ⟨F, rfl⟩, hF⟩
[GOAL]
case intro.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
s : Set (PrimeSpectrum S)
F : Set R
hF : ↑(comap f) ⁻¹' zeroLocus F = sᶜ
⊢ ∃ s_1, sᶜ = zeroLocus s_1
[PROOFSTEP]
exact ⟨f '' F, hF.symm.trans (preimage_comap_zeroLocus f F)⟩
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
⊢ ↑(comap f) '' zeroLocus ↑I = zeroLocus ↑(Ideal.comap f I)
[PROOFSTEP]
simp only [Set.ext_iff, Set.mem_image, mem_zeroLocus, SetLike.coe_subset_coe]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
⊢ ∀ (x : PrimeSpectrum R), (∃ x_1, I ≤ x_1.asIdeal ∧ ↑(comap f) x_1 = x) ↔ Ideal.comap f I ≤ x.asIdeal
[PROOFSTEP]
refine' fun p => ⟨_, fun h_I_p => _⟩
[GOAL]
case refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
⊢ (∃ x, I ≤ x.asIdeal ∧ ↑(comap f) x = p) → Ideal.comap f I ≤ p.asIdeal
[PROOFSTEP]
rintro ⟨p, hp, rfl⟩ a ha
[GOAL]
case refine'_1.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum S
hp : I ≤ p.asIdeal
a : R
ha : a ∈ Ideal.comap f I
⊢ a ∈ (↑(comap f) p).asIdeal
[PROOFSTEP]
exact hp ha
[GOAL]
case refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ ↑(comap f) x = p
[PROOFSTEP]
have hp : ker f ≤ p.asIdeal := (Ideal.comap_mono bot_le).trans h_I_p
[GOAL]
case refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ ∃ x, I ≤ x.asIdeal ∧ ↑(comap f) x = p
[PROOFSTEP]
refine' ⟨⟨p.asIdeal.map f, Ideal.map_isPrime_of_surjective hf hp⟩, fun x hx => _, _⟩
[GOAL]
case refine'_2.refine'_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : S
hx : x ∈ I
⊢ x ∈ { asIdeal := Ideal.map f p.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map f p.asIdeal)) }.asIdeal
[PROOFSTEP]
obtain ⟨x', rfl⟩ := hf x
[GOAL]
case refine'_2.refine'_1.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x' : R
hx : ↑f x' ∈ I
⊢ ↑f x' ∈ { asIdeal := Ideal.map f p.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map f p.asIdeal)) }.asIdeal
[PROOFSTEP]
exact Ideal.mem_map_of_mem f (h_I_p hx)
[GOAL]
case refine'_2.refine'_2
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
⊢ ↑(comap f) { asIdeal := Ideal.map f p.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map f p.asIdeal)) } = p
[PROOFSTEP]
ext x
[GOAL]
case refine'_2.refine'_2.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ x ∈
      (↑(comap f)
          { asIdeal := Ideal.map f p.asIdeal, IsPrime := (_ : Ideal.IsPrime (Ideal.map f p.asIdeal)) }).asIdeal ↔
    x ∈ p.asIdeal
[PROOFSTEP]
change f x ∈ p.asIdeal.map f ↔ _
[GOAL]
case refine'_2.refine'_2.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ ↑f x ∈ Ideal.map f p.asIdeal ↔ x ∈ p.asIdeal
[PROOFSTEP]
rw [Ideal.mem_map_iff_of_surjective f hf]
[GOAL]
case refine'_2.refine'_2.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ (∃ x_1, x_1 ∈ p.asIdeal ∧ ↑f x_1 = ↑f x) ↔ x ∈ p.asIdeal
[PROOFSTEP]
refine' ⟨_, fun hx => ⟨x, hx, rfl⟩⟩
[GOAL]
case refine'_2.refine'_2.asIdeal.h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x : R
⊢ (∃ x_1, x_1 ∈ p.asIdeal ∧ ↑f x_1 = ↑f x) → x ∈ p.asIdeal
[PROOFSTEP]
rintro ⟨x', hx', heq⟩
[GOAL]
case refine'_2.refine'_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : ↑f x' = ↑f x
⊢ x ∈ p.asIdeal
[PROOFSTEP]
rw [← sub_sub_cancel x' x]
[GOAL]
case refine'_2.refine'_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : ↑f x' = ↑f x
⊢ x' - (x' - x) ∈ p.asIdeal
[PROOFSTEP]
refine' p.asIdeal.sub_mem hx' (hp _)
[GOAL]
case refine'_2.refine'_2.asIdeal.h.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
I : Ideal S
p : PrimeSpectrum R
h_I_p : Ideal.comap f I ≤ p.asIdeal
hp : ker f ≤ p.asIdeal
x x' : R
hx' : x' ∈ p.asIdeal
heq : ↑f x' = ↑f x
⊢ x' - x ∈ ker f
[PROOFSTEP]
rwa [mem_ker, map_sub, sub_eq_zero]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ Set.range ↑(comap f) = zeroLocus ↑(ker f)
[PROOFSTEP]
rw [← Set.image_univ]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ ↑(comap f) '' Set.univ = zeroLocus ↑(ker f)
[PROOFSTEP]
convert image_comap_zeroLocus_eq_zeroLocus_comap _ _ hf _
[GOAL]
case h.e'_2.h.e'_4
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ Set.univ = zeroLocus ↑⊥
[PROOFSTEP]
rw [zeroLocus_bot]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ IsClosed (Set.range ↑(comap f))
[PROOFSTEP]
rw [range_comap_of_surjective _ f hf]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type u_1
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ IsClosed (zeroLocus ↑(ker f))
[PROOFSTEP]
exact isClosed_zeroLocus _
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
x : PrimeSpectrum R
⊢ x ∈ ↑(basicOpen r) ↔ x ∈ (zeroLocus {r})ᶜ
[PROOFSTEP]
simp only [SetLike.mem_coe, mem_basicOpen, Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ↑(basicOpen 1) = ↑⊤
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ↑(basicOpen 0) = ↑⊥
[PROOFSTEP]
simp
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f g : R
⊢ basicOpen f ≤ basicOpen g ↔ f ∈ Ideal.radical (Ideal.span {g})
[PROOFSTEP]
rw [← SetLike.coe_subset_coe, basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_compl, Set.compl_subset_compl,
  zeroLocus_subset_zeroLocus_singleton_iff]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f g : R
⊢ ↑(basicOpen (f * g)) = ↑(basicOpen f ⊓ basicOpen g)
[PROOFSTEP]
simp [zeroLocus_singleton_mul]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f g : R
⊢ basicOpen (f * g) ≤ basicOpen f
[PROOFSTEP]
rw [basicOpen_mul f g]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f g : R
⊢ basicOpen f ⊓ basicOpen g ≤ basicOpen f
[PROOFSTEP]
exact inf_le_left
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f g : R
⊢ basicOpen (f * g) ≤ basicOpen g
[PROOFSTEP]
rw [basicOpen_mul f g]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f g : R
⊢ basicOpen f ⊓ basicOpen g ≤ basicOpen g
[PROOFSTEP]
exact inf_le_right
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
n : ℕ
hn : 0 < n
⊢ ↑(basicOpen (f ^ n)) = ↑(basicOpen f)
[PROOFSTEP]
simpa using zeroLocus_singleton_pow f n hn
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ TopologicalSpace.IsTopologicalBasis (Set.range fun r => ↑(basicOpen r))
[PROOFSTEP]
apply TopologicalSpace.isTopologicalBasis_of_open_of_nhds
[GOAL]
case h_open
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (u : Set (PrimeSpectrum R)), (u ∈ Set.range fun r => ↑(basicOpen r)) → IsOpen u
[PROOFSTEP]
rintro _ ⟨r, rfl⟩
[GOAL]
case h_open.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
r : R
⊢ IsOpen ((fun r => ↑(basicOpen r)) r)
[PROOFSTEP]
exact isOpen_basicOpen
[GOAL]
case h_nhds
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u → IsOpen u → ∃ v, (v ∈ Set.range fun r => ↑(basicOpen r)) ∧ a ∈ v ∧ v ⊆ u
[PROOFSTEP]
rintro p U hp ⟨s, hs⟩
[GOAL]
case h_nhds.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
hp : p ∈ U
s : Set R
hs : zeroLocus s = Uᶜ
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen r)) ∧ p ∈ v ∧ v ⊆ U
[PROOFSTEP]
rw [← compl_compl U, Set.mem_compl_iff, ← hs, mem_zeroLocus, Set.not_subset] at hp 
[GOAL]
case h_nhds.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hp : ∃ a, a ∈ s ∧ ¬a ∈ ↑p.asIdeal
hs : zeroLocus s = Uᶜ
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen r)) ∧ p ∈ v ∧ v ⊆ U
[PROOFSTEP]
obtain ⟨f, hfs, hfp⟩ := hp
[GOAL]
case h_nhds.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asIdeal
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen r)) ∧ p ∈ v ∧ v ⊆ U
[PROOFSTEP]
refine' ⟨basicOpen f, ⟨f, rfl⟩, hfp, _⟩
[GOAL]
case h_nhds.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asIdeal
⊢ ↑(basicOpen f) ⊆ U
[PROOFSTEP]
rw [← Set.compl_subset_compl, ← hs, basicOpen_eq_zeroLocus_compl, compl_compl]
[GOAL]
case h_nhds.intro.intro.intro
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
p : PrimeSpectrum R
U : Set (PrimeSpectrum R)
s : Set R
hs : zeroLocus s = Uᶜ
f : R
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asIdeal
⊢ zeroLocus s ⊆ zeroLocus {f}
[PROOFSTEP]
exact zeroLocus_anti_mono (Set.singleton_subset_iff.mpr hfs)
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ TopologicalSpace.Opens.IsBasis (Set.range basicOpen)
[PROOFSTEP]
unfold TopologicalSpace.Opens.IsBasis
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ TopologicalSpace.IsTopologicalBasis (SetLike.coe '' Set.range basicOpen)
[PROOFSTEP]
convert isTopologicalBasis_basic_opens (R := R)
[GOAL]
case h.e'_3
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ SetLike.coe '' Set.range basicOpen = Set.range fun r => ↑(basicOpen r)
[PROOFSTEP]
rw [← Set.range_comp]
[GOAL]
case h.e'_3
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ Set.range (SetLike.coe ∘ basicOpen) = Set.range fun r => ↑(basicOpen r)
[PROOFSTEP]
rfl
[GOAL]
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 = ∅
[PROOFSTEP]
let I : ι → Ideal R := fun i => vanishingIdeal (Z i)
[GOAL]
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 = ∅
[PROOFSTEP]
have hI : ∀ i, Z i = zeroLocus (I i) := fun i => by
  simpa only [zeroLocus_vanishingIdeal_eq_closure] using (hZc i).closure_eq.symm
[GOAL]
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)
[PROOFSTEP]
simpa only [zeroLocus_vanishingIdeal_eq_closure] using (hZc i).closure_eq.symm
[GOAL]
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 = ∅
[PROOFSTEP]
rw [basicOpen_eq_zeroLocus_compl f, Set.inter_comm, ← Set.diff_eq, Set.diff_eq_empty, funext hI, ← zeroLocus_iSup] at hZ 
[GOAL]
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 = ∅
[PROOFSTEP]
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)
[GOAL]
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)
[PROOFSTEP]
rw [← vanishingIdeal_zeroLocus_eq_radical]
[GOAL]
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))
[PROOFSTEP]
apply vanishingIdeal_anti_mono hZ
[GOAL]
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})
[PROOFSTEP]
exact subset_vanishingIdeal_zeroLocus { f } (Set.mem_singleton f)
[GOAL]
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 = ∅
[PROOFSTEP]
rcases Submodule.exists_finset_of_mem_iSup I hn with ⟨s, hs⟩
[GOAL]
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 = ∅
[PROOFSTEP]
use s
[GOAL]
case 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
⊢ ↑(basicOpen f) ∩ ⋂ (i : ι) (_ : i ∈ s), Z i = ∅
[PROOFSTEP]
simp_rw [basicOpen_eq_zeroLocus_compl f, Set.inter_comm (zeroLocus { f })ᶜ, ← Set.diff_eq, Set.diff_eq_empty]
[GOAL]
case 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
⊢ ⋂ (i : ι) (_ : i ∈ s), Z i ⊆ zeroLocus {f}
[PROOFSTEP]
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))]
[GOAL]
case 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
⊢ ⋂ (i : ι) (_ : i ∈ s), zeroLocus ↑(I i) ⊆ zeroLocus {f}
[PROOFSTEP]
simp_rw [← zeroLocus_iSup]
[GOAL]
case 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
⊢ zeroLocus ↑(⨆ (i : ι) (_ : i ∈ s), vanishingIdeal (Z i)) ⊆ zeroLocus {f}
[PROOFSTEP]
rw [← zeroLocus_radical]
  -- this one can't be in `simp_rw` because it would loop
[GOAL]
case 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
⊢ zeroLocus ↑(Ideal.radical (⨆ (i : ι) (_ : i ∈ s), vanishingIdeal (Z i))) ⊆ zeroLocus {f}
[PROOFSTEP]
apply zeroLocus_anti_mono
[GOAL]
case h.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)))
[PROOFSTEP]
rw [Set.singleton_subset_iff]
[GOAL]
case h.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)))
[PROOFSTEP]
exact ⟨n, hs⟩
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
⊢ basicOpen f = ⊥ ↔ IsNilpotent f
[PROOFSTEP]
rw [← TopologicalSpace.Opens.coe_inj, basicOpen_eq_zeroLocus_compl]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
⊢ (zeroLocus {f})ᶜ = ↑⊥ ↔ IsNilpotent f
[PROOFSTEP]
simp only [Set.eq_univ_iff_forall, Set.singleton_subset_iff, TopologicalSpace.Opens.coe_bot, nilpotent_iff_mem_prime,
  Set.compl_empty_iff, mem_zeroLocus, SetLike.mem_coe]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R
⊢ (∀ (x : PrimeSpectrum R), f ∈ x.asIdeal) ↔ ∀ (J : Ideal R), Ideal.IsPrime J → f ∈ J
[PROOFSTEP]
exact ⟨fun h I hI => h ⟨I, hI⟩, fun h ⟨I, hI⟩ => h I hI⟩
[GOAL]
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ Set.range ↑(comap (algebraMap R S)) = ↑(basicOpen r)
[PROOFSTEP]
rw [localization_comap_range S (Submonoid.powers r)]
[GOAL]
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ {p | Disjoint ↑(Submonoid.powers r) ↑p.asIdeal} = ↑(basicOpen r)
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ x ∈ {p | Disjoint ↑(Submonoid.powers r) ↑p.asIdeal} ↔ x ∈ ↑(basicOpen r)
[PROOFSTEP]
simp only [mem_zeroLocus, basicOpen_eq_zeroLocus_compl, SetLike.mem_coe, Set.mem_setOf_eq, Set.singleton_subset_iff,
  Set.mem_compl_iff, disjoint_iff_inf_le]
[GOAL]
case h
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ≤ ⊥ ↔ ¬r ∈ x.asIdeal
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ≤ ⊥ → ¬r ∈ x.asIdeal
[PROOFSTEP]
intro h₁ h₂
[GOAL]
case h.mp
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
h₁ : ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ≤ ⊥
h₂ : r ∈ x.asIdeal
⊢ False
[PROOFSTEP]
exact h₁ ⟨Submonoid.mem_powers r, h₂⟩
[GOAL]
case h.mpr
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ ¬r ∈ x.asIdeal → ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ≤ ⊥
[PROOFSTEP]
rintro h₁ _ ⟨⟨n, rfl⟩, h₃⟩
[GOAL]
case h.mpr.intro.intro
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
h₁ : ¬r ∈ x.asIdeal
n : ℕ
h₃ : (fun x x_1 => x ^ x_1) r n ∈ ↑x.asIdeal
⊢ (fun x x_1 => x ^ x_1) r n ∈ ⊥
[PROOFSTEP]
exact h₁ (x.2.mem_of_pow_mem _ h₃)
[GOAL]
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ IsOpen (Set.range ↑(comap (algebraMap R S)))
[PROOFSTEP]
rw [localization_away_comap_range S r]
[GOAL]
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
⊢ IsOpen ↑(basicOpen r)
[PROOFSTEP]
exact isOpen_basicOpen
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ IsCompact Set.univ
[PROOFSTEP]
convert isCompact_basicOpen (1 : R)
[GOAL]
case h.e'_3
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ Set.univ = ↑(basicOpen 1)
[PROOFSTEP]
rw [basicOpen_one]
[GOAL]
case h.e'_3
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
⊢ Set.univ = ↑⊤
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : PrimeSpectrum R
⊢ x ≤ y ↔ y ∈ closure {x}
[PROOFSTEP]
rw [← asIdeal_le_asIdeal, ← zeroLocus_vanishingIdeal_eq_closure, mem_zeroLocus, vanishingIdeal_singleton,
  SetLike.coe_subset_coe]
[GOAL]
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : PrimeSpectrum R
h : x ⤳ y
⊢ ∀ (y_1 : { x // x ∈ Ideal.primeCompl y.asIdeal }), IsUnit (↑(algebraMap R (Localization.AtPrime x.asIdeal)) ↑y_1)
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : PrimeSpectrum R
h : x ⤳ y
a : R
ha : a ∈ Ideal.primeCompl y.asIdeal
⊢ IsUnit (↑(algebraMap R (Localization.AtPrime x.asIdeal)) ↑{ val := a, property := ha })
[PROOFSTEP]
rw [← PrimeSpectrum.le_iff_specializes, ← asIdeal_le_asIdeal, ← SetLike.coe_subset_coe, ← Set.compl_subset_compl] at h 
[GOAL]
case mk
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : PrimeSpectrum R
h : (↑y.asIdeal)ᶜ ⊆ (↑x.asIdeal)ᶜ
a : R
ha : a ∈ Ideal.primeCompl y.asIdeal
⊢ IsUnit (↑(algebraMap R (Localization.AtPrime x.asIdeal)) ↑{ val := a, property := ha })
[PROOFSTEP]
exact (IsLocalization.map_units (Localization.AtPrime x.asIdeal) ⟨a, show a ∈ x.asIdeal.primeCompl from h ha⟩ : _)
[GOAL]
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
inst✝² : LocalRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : LocalRing S
f : R →+* S
⊢ IsLocalRingHom f ↔ ↑(PrimeSpectrum.comap f) (closedPoint S) = closedPoint R
[PROOFSTEP]
have := (local_hom_TFAE f).out 0 4
[GOAL]
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
inst✝² : LocalRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : LocalRing S
f : R →+* S
this : IsLocalRingHom f ↔ Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ IsLocalRingHom f ↔ ↑(PrimeSpectrum.comap f) (closedPoint S) = closedPoint R
[PROOFSTEP]
rw [this, PrimeSpectrum.ext_iff]
[GOAL]
R : Type u
S✝ : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S✝
inst✝² : LocalRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : LocalRing S
f : R →+* S
this : IsLocalRingHom f ↔ Ideal.comap f (maximalIdeal S) = maximalIdeal R
⊢ Ideal.comap f (maximalIdeal S) = maximalIdeal R ↔
    (↑(PrimeSpectrum.comap f) (closedPoint S)).asIdeal = (closedPoint R).asIdeal
[PROOFSTEP]
rfl
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U ↔ U = ⊤
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → U = ⊤
[PROOFSTEP]
rw [eq_top_iff]
[GOAL]
case mp
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ closedPoint R ∈ U → ⊤ ≤ U
[PROOFSTEP]
exact fun h x _ => (specializes_closedPoint x).mem_open U.2 h
[GOAL]
case mpr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
U : TopologicalSpace.Opens (PrimeSpectrum R)
⊢ U = ⊤ → closedPoint R ∈ U
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
⊢ closedPoint R ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
x : PrimeSpectrum (ResidueField R)
⊢ ↑(PrimeSpectrum.comap (residue R)) x = closedPoint R
[PROOFSTEP]
rw [Subsingleton.elim x ⊥]
[GOAL]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
x : PrimeSpectrum (ResidueField R)
⊢ ↑(PrimeSpectrum.comap (residue R)) ⊥ = closedPoint R
[PROOFSTEP]
ext1
[GOAL]
case asIdeal
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : LocalRing R
x : PrimeSpectrum (ResidueField R)
⊢ (↑(PrimeSpectrum.comap (residue R)) ⊥).asIdeal = (closedPoint R).asIdeal
[PROOFSTEP]
exact Ideal.mk_ker
