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)
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)
rw [localization_comap_range S (Submonoid.powers r)]
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)
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)
ext x
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
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)
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]
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

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 ≤ ⊥
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
constructor
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
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
intro h₁ h₂
no goals
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
exact h₁ ⟨Submonoid.mem_powers r, h₂⟩
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 ∈ ⊥
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 ≤ ⊥
rintro h₁ _ ⟨⟨n, rfl⟩, h₃⟩
no goals
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 ∈ ⊥
exact h₁ (x.2.mem_of_pow_mem _ h₃)