-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
@[stacks 05JL]
lemma isClosed_image_of_stableUnderSpecialization
    (Z : Set (PrimeSpectrum S)) (hZ : IsClosed Z)
    (hf : StableUnderSpecialization (comap f '' Z)) :
    IsClosed (comap f '' Z)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
Z : Set (PrimeSpectrum S)
hZ : IsClosed Z
hf : StableUnderSpecialization (⇑(comap f) '' Z)
⊢ IsClosed (⇑(comap f) '' Z)

Tactic:
obtain ⟨I, rfl⟩ := (PrimeSpectrum.isClosed_iff_zeroLocus_ideal Z).mp hZ

Result:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (⇑(comap f) '' zeroLocus ↑I)
⊢ IsClosed (⇑(comap f) '' zeroLocus ↑I)

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (⇑(comap f) '' zeroLocus ↑I)
this : ⇑(comap f) '' zeroLocus ↑I = Set.range ⇑(comap ((Ideal.Quotient.mk I).comp f))
⊢ IsClosed (⇑(comap f) '' zeroLocus ↑I)

Tactic:
rw [this] at hf ⊢

Result:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (Set.range ⇑(comap ((Ideal.Quotient.mk I).comp f)))
this : ⇑(comap f) '' zeroLocus ↑I = Set.range ⇑(comap ((Ideal.Quotient.mk I).comp f))
⊢ IsClosed (Set.range ⇑(comap ((Ideal.Quotient.mk I).comp f)))

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (⇑(comap f) '' zeroLocus ↑I)
⊢ ⇑(comap f) '' zeroLocus ↑I = Set.range ⇑(comap ((Ideal.Quotient.mk I).comp f))

Tactic:
rw [comap_comp, ContinuousMap.coe_comp, Set.range_comp, range_comap_of_surjective, Ideal.mk_ker]

Result:
case hf
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (⇑(comap f) '' zeroLocus ↑I)
⊢ Function.Surjective ⇑(Ideal.Quotient.mk I)

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (⇑(comap f) '' zeroLocus ↑I)
⊢ IsClosed (⇑(comap f) '' zeroLocus ↑I)

Tactic:
have : (comap f '' zeroLocus I) = Set.range (comap ((Ideal.Quotient.mk I).comp f)) := by
  rw [comap_comp, ContinuousMap.coe_comp, Set.range_comp, range_comap_of_surjective, Ideal.mk_ker]
  exact Ideal.Quotient.mk_surjective

Result:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (⇑(comap f) '' zeroLocus ↑I)
this : ⇑(comap f) '' zeroLocus ↑I = Set.range ⇑(comap ((Ideal.Quotient.mk I).comp f))
⊢ IsClosed (⇑(comap f) '' zeroLocus ↑I)

Proof state:
case hf
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (⇑(comap f) '' zeroLocus ↑I)
⊢ Function.Surjective ⇑(Ideal.Quotient.mk I)

Tactic:
exact Ideal.Quotient.mk_surjective

Result:
no goals

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hZ : IsClosed (zeroLocus ↑I)
hf : StableUnderSpecialization (Set.range ⇑(comap ((Ideal.Quotient.mk I).comp f)))
this : ⇑(comap f) '' zeroLocus ↑I = Set.range ⇑(comap ((Ideal.Quotient.mk I).comp f))
⊢ IsClosed (Set.range ⇑(comap ((Ideal.Quotient.mk I).comp f)))

Tactic:
exact isClosed_range_of_stableUnderSpecialization _ hf

Result:
no goals