case h_open
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ (u : Set (ProjectiveSpectrum 𝒜)), (u ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) → IsOpen u

case h_nhds
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ (a : ProjectiveSpectrum 𝒜) (u : Set (ProjectiveSpectrum 𝒜)),
    a ∈ u → IsOpen u → ∃ v, (v ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) ∧ a ∈ v ∧ v ⊆ u
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ IsTopologicalBasis (Set.range fun r => ↑(basicOpen 𝒜 r))
apply TopologicalSpace.isTopologicalBasis_of_open_of_nhds
case h_open.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
r : A
⊢ IsOpen ((fun r => ↑(basicOpen 𝒜 r)) r)
case h_open
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ (u : Set (ProjectiveSpectrum 𝒜)), (u ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) → IsOpen u
rintro _ ⟨r, rfl⟩
no goals
case h_open.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
r : A
⊢ IsOpen ((fun r => ↑(basicOpen 𝒜 r)) r)
exact isOpen_basicOpen 𝒜
case h_nhds.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
hp : p ∈ U
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) ∧ p ∈ v ∧ v ⊆ U
case h_nhds
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
⊢ ∀ (a : ProjectiveSpectrum 𝒜) (u : Set (ProjectiveSpectrum 𝒜)),
    a ∈ u → IsOpen u → ∃ v, (v ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) ∧ a ∈ v ∧ v ⊆ u
rintro p U hp ⟨s, hs⟩
case h_nhds.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hp : ∃ a, a ∈ s ∧ ¬a ∈ ↑p.asHomogeneousIdeal
hs : zeroLocus 𝒜 s = Uᶜ
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) ∧ p ∈ v ∧ v ⊆ U
case h_nhds.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
hp : p ∈ U
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) ∧ p ∈ v ∧ v ⊆ U
rw [← compl_compl U, Set.mem_compl_iff, ← hs, mem_zeroLocus, Set.not_subset] at hp
case h_nhds.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asHomogeneousIdeal
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) ∧ p ∈ v ∧ v ⊆ U
case h_nhds.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hp : ∃ a, a ∈ s ∧ ¬a ∈ ↑p.asHomogeneousIdeal
hs : zeroLocus 𝒜 s = Uᶜ
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) ∧ p ∈ v ∧ v ⊆ U
obtain ⟨f, hfs, hfp⟩ := hp
case h_nhds.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asHomogeneousIdeal
⊢ ↑(basicOpen 𝒜 f) ⊆ U
case h_nhds.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asHomogeneousIdeal
⊢ ∃ v, (v ∈ Set.range fun r => ↑(basicOpen 𝒜 r)) ∧ p ∈ v ∧ v ⊆ U
refine' ⟨basicOpen 𝒜 f, ⟨f, rfl⟩, hfp, _⟩
case h_nhds.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asHomogeneousIdeal
⊢ zeroLocus 𝒜 s ⊆ zeroLocus 𝒜 {f}
case h_nhds.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asHomogeneousIdeal
⊢ ↑(basicOpen 𝒜 f) ⊆ U
rw [← Set.compl_subset_compl, ← hs, basicOpen_eq_zeroLocus_compl, compl_compl]
no goals
case h_nhds.intro.intro.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
p : ProjectiveSpectrum 𝒜
U : Set (ProjectiveSpectrum 𝒜)
s : Set A
hs : zeroLocus 𝒜 s = Uᶜ
f : A
hfs : f ∈ s
hfp : ¬f ∈ ↑p.asHomogeneousIdeal
⊢ zeroLocus 𝒜 s ⊆ zeroLocus 𝒜 {f}
exact zeroLocus_anti_mono 𝒜 (Set.singleton_subset_iff.mpr hfs)