R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this :
  HomogeneousIdeal.toIdeal (vanishingIdeal (zeroLocus 𝒜 ↑(HomogeneousIdeal.toIdeal (vanishingIdeal t)))) =
    HomogeneousIdeal.toIdeal (vanishingIdeal t)
⊢ vanishingIdeal (closure t) = vanishingIdeal t
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
⊢ vanishingIdeal (closure t) = vanishingIdeal t
have := (gc_ideal 𝒜).u_l_u_eq_u t
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this :
  HomogeneousIdeal.toIdeal (vanishingIdeal (zeroLocus 𝒜 ↑(HomogeneousIdeal.toIdeal (vanishingIdeal t)))) =
    HomogeneousIdeal.toIdeal (vanishingIdeal t)
⊢ vanishingIdeal (closure t) = vanishingIdeal t
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this :
  HomogeneousIdeal.toIdeal (vanishingIdeal (zeroLocus 𝒜 ↑(HomogeneousIdeal.toIdeal (vanishingIdeal t)))) =
    HomogeneousIdeal.toIdeal (vanishingIdeal t)
⊢ vanishingIdeal (closure t) = vanishingIdeal t
dsimp only at this
case h
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this :
  HomogeneousIdeal.toIdeal (vanishingIdeal (zeroLocus 𝒜 ↑(HomogeneousIdeal.toIdeal (vanishingIdeal t)))) =
    HomogeneousIdeal.toIdeal (vanishingIdeal t)
⊢ HomogeneousIdeal.toIdeal (vanishingIdeal (closure t)) = HomogeneousIdeal.toIdeal (vanishingIdeal t)
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this :
  HomogeneousIdeal.toIdeal (vanishingIdeal (zeroLocus 𝒜 ↑(HomogeneousIdeal.toIdeal (vanishingIdeal t)))) =
    HomogeneousIdeal.toIdeal (vanishingIdeal t)
⊢ vanishingIdeal (closure t) = vanishingIdeal t
ext1
case h
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : HomogeneousIdeal.toIdeal (vanishingIdeal (closure t)) = HomogeneousIdeal.toIdeal (vanishingIdeal t)
⊢ HomogeneousIdeal.toIdeal (vanishingIdeal (closure t)) = HomogeneousIdeal.toIdeal (vanishingIdeal t)
case h
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this :
  HomogeneousIdeal.toIdeal (vanishingIdeal (zeroLocus 𝒜 ↑(HomogeneousIdeal.toIdeal (vanishingIdeal t)))) =
    HomogeneousIdeal.toIdeal (vanishingIdeal t)
⊢ HomogeneousIdeal.toIdeal (vanishingIdeal (closure t)) = HomogeneousIdeal.toIdeal (vanishingIdeal t)
erw [zeroLocus_vanishingIdeal_eq_closure 𝒜 t] at this
no goals
case h
R : Type u_2
A : Type u_1
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
t : Set (ProjectiveSpectrum 𝒜)
this : HomogeneousIdeal.toIdeal (vanishingIdeal (closure t)) = HomogeneousIdeal.toIdeal (vanishingIdeal t)
⊢ HomogeneousIdeal.toIdeal (vanishingIdeal (closure t)) = HomogeneousIdeal.toIdeal (vanishingIdeal t)
exact this