case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
inst✝² : CommRing S'
f : R →+* S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
⊢ Inducing ↑(comap (algebraMap R S))
constructor
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
rw [topologicalSpace_eq_iff]
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
intro U
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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ᶜ)
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
rw [← isClosed_compl_iff, ← @isClosed_compl_iff (α := PrimeSpectrum S) (s := U)]
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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ᶜ)
generalize Uᶜ = Z
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
simp_rw [isClosed_induced_iff, isClosed_iff_zeroLocus]
case induced.mp
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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

case induced.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
case induced
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
constructor
case induced.mp.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
case induced.mp
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
rintro ⟨s, rfl⟩
case induced.mp.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
case induced.mp.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
refine ⟨_, ⟨algebraMap R S ⁻¹' Ideal.span s, rfl⟩, ?_⟩
case induced.mp.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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)
case induced.mp.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
rw [preimage_comap_zeroLocus, ← zeroLocus_span, ← zeroLocus_span s]
case induced.mp.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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)
case induced.mp.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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)
congr 2
no goals
case induced.mp.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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)
exact congr_arg (zeroLocus .) <| Submodule.carrier_inj.mpr
  (IsLocalization.map_comap M S (Ideal.span s))
case induced.mpr.intro.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
case induced.mpr
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
rintro ⟨_, ⟨t, rfl⟩, rfl⟩
case induced.mpr.intro.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
case induced.mpr.intro.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
rw [preimage_comap_zeroLocus]
no goals
case induced.mpr.intro.intro.intro
R : Type u
S : Type v
inst✝⁴ : CommRing R
inst✝³ : CommRing S
S' : Type ?u.199045
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
exact ⟨_, rfl⟩