R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.259728
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ᶜ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.259728
inst✝ : CommRing S'
f : R →+* S
hf : Surjective ↑f
⊢ zariskiTopology = TopologicalSpace.induced (↑(comap f)) zariskiTopology
simp_rw [topologicalSpace_eq_iff, ← isClosed_compl_iff,
  ← @isClosed_compl_iff (PrimeSpectrum S)
    ((TopologicalSpace.induced (comap f) zariskiTopology)), isClosed_induced_iff,
  isClosed_iff_zeroLocus]
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.259728
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
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.259728
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ᶜ
refine' fun s =>
  ⟨fun ⟨F, hF⟩ =>
    ⟨zeroLocus (f ⁻¹' F), ⟨f ⁻¹' F, rfl⟩, by
      rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]⟩,
    _⟩
case intro.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.259728
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
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.259728
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
rintro ⟨-, ⟨F, rfl⟩, hF⟩
no goals
case intro.intro.intro
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.259728
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
exact ⟨f '' F, hF.symm.trans (preimage_comap_zeroLocus f F)⟩
no goals
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
S' : Type ?u.259728
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ᶜ
rw [preimage_comap_zeroLocus, Function.Surjective.image_preimage hf, hF]