R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ ¬f ∈ z.asHomogeneousIdeal ↔ ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ z ∈ ↑(basicOpen 𝒜 f) ↔ z ∈ ↑(⨆ (i : ℕ), basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f))
erw [mem_coe_basicOpen, TopologicalSpace.Opens.mem_sSup]
case mp
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ¬f ∈ z.asHomogeneousIdeal
⊢ ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u

case mpr
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u
⊢ ¬f ∈ z.asHomogeneousIdeal
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
⊢ ¬f ∈ z.asHomogeneousIdeal ↔ ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u
constructor <;> intro hz
case mp.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ¬f ∈ z.asHomogeneousIdeal
i : ℕ
hi : ¬↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u
case mp
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ¬f ∈ z.asHomogeneousIdeal
⊢ ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u
rcases show ∃ i, GradedAlgebra.proj 𝒜 i f ∉ z.asHomogeneousIdeal by
  contrapose! hz with H
  classical
  rw [← DirectSum.sum_support_decompose 𝒜 f]
  apply Ideal.sum_mem _ fun i _ => H i with ⟨i, hi⟩
no goals
case mp.intro
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ¬f ∈ z.asHomogeneousIdeal
i : ℕ
hi : ¬↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u
exact ⟨basicOpen 𝒜 (GradedAlgebra.proj 𝒜 i f), ⟨i, rfl⟩, by rwa [mem_basicOpen]⟩
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), ↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ f ∈ z.asHomogeneousIdeal
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ¬f ∈ z.asHomogeneousIdeal
⊢ ∃ i, ¬↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
contrapose! hz with H
no goals
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), ↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ f ∈ z.asHomogeneousIdeal
classical
rw [← DirectSum.sum_support_decompose 𝒜 f]
apply Ideal.sum_mem _ fun i _ => H i
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), ↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ ∑ i in Dfinsupp.support (↑(decompose 𝒜) f), ↑(↑(↑(decompose 𝒜) f) i) ∈ z.asHomogeneousIdeal
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), ↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ f ∈ z.asHomogeneousIdeal
rw [← DirectSum.sum_support_decompose 𝒜 f]
no goals
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
H : ∀ (i : ℕ), ↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ ∑ i in Dfinsupp.support (↑(decompose 𝒜) f), ↑(↑(↑(decompose 𝒜) f) i) ∈ z.asHomogeneousIdeal
apply Ideal.sum_mem _ fun i _ => H i
no goals
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ¬f ∈ z.asHomogeneousIdeal
i : ℕ
hi : ¬↑(GradedAlgebra.proj 𝒜 i) f ∈ z.asHomogeneousIdeal
⊢ z ∈ basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)
rwa [mem_basicOpen]
case mpr.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 𝒜
f : A
z : ProjectiveSpectrum 𝒜
i : ℕ
hz : z ∈ (fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) i
⊢ ¬f ∈ z.asHomogeneousIdeal
case mpr
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
z : ProjectiveSpectrum 𝒜
hz : ∃ u, (u ∈ Set.range fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) ∧ z ∈ u
⊢ ¬f ∈ z.asHomogeneousIdeal
obtain ⟨_, ⟨i, rfl⟩, hz⟩ := hz
no goals
case mpr.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 𝒜
f : A
z : ProjectiveSpectrum 𝒜
i : ℕ
hz : z ∈ (fun i => basicOpen 𝒜 (↑(GradedAlgebra.proj 𝒜 i) f)) i
⊢ ¬f ∈ z.asHomogeneousIdeal
exact fun rid => hz (z.1.2 i rid)