Properness of Proj A

We show that Proj 𝒜 is a separated scheme.

TODO

• Show that Proj 𝒜 satisfies the valuative criterion.

Notes

This contribution was created as part of the Durham Computational Algebraic Geometry Workshop

theorem AlgebraicGeometry.Proj.lift_awayMapₐ_awayMapₐ_surjective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {d e : ℕ} {f : A} (hf : f ∈ 𝒜 d) {g : A} (hg : g ∈ 𝒜 e) {x : A} (hx : x = f * g) (hd : 0 < d) : Function.Surjective ⇑(Algebra.TensorProduct.lift (HomogeneousLocalization.awayMapₐ 𝒜 hg hx) (HomogeneousLocalization.awayMapₐ 𝒜 hf ⋯) ⋯)

instance AlgebraicGeometry.Proj.isSeparated {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : AlgebraicGeometry.IsSeparated (AlgebraicGeometry.Proj.toSpecZero 𝒜)

instance AlgebraicGeometry.Proj.instIsSeparated {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : (AlgebraicGeometry.Proj 𝒜).IsSeparated

Stacks Tag 01MC