Properness of Proj A

We show that Proj 𝒜 is proper over Spec 𝒜₀.

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 𝒜] : IsSeparated (toSpecZero 𝒜)

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

Stacks Tag 01MC

instance AlgebraicGeometry.Proj.instLocallyOfFiniteTypeToSpecZeroOfFiniteTypeSubtypeMemSubmoduleOfNatNat {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A] : LocallyOfFiniteType (toSpecZero 𝒜)

instance AlgebraicGeometry.Proj.instQuasiCompactToSpecZeroOfFiniteTypeSubtypeMemSubmoduleOfNatNat {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A] : QuasiCompact (toSpecZero 𝒜)

theorem AlgebraicGeometry.Proj.valuativeCriterion_existence_aux {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {O : Type u_3} [CommRing O] [IsDomain O] [ValuationRing O] {K : Type u_4} [Field K] [Algebra O K] [IsFractionRing O K] (φ₀ : ↥(𝒜 0) →+* O) (ι : Type u_5) [Finite ι] (x : ι → A) (h2 : Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤) (j : ι) (φ : HomogeneousLocalization.Away 𝒜 (x j) →+* K) (hcomm : (algebraMap O K).comp φ₀ = φ.comp (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers (x j)))) (d : ι → ℕ) (hdi : ∀ (i : ι), 0 < d i) (hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)) : ∃ (j₀ : ι) (φ' : HomogeneousLocalization.Away 𝒜 (x j * x j₀) →+* K), φ'.comp (HomogeneousLocalization.awayMap 𝒜 ⋯ ⋯) = φ ∧ (φ'.comp (HomogeneousLocalization.awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range

Let 𝒜 be a graded ring generated over 𝒜₀ by finitely many homogeneous elements. Suppose we have the following diagram for some homogeneous x with O a valuation ring and K = Frac(O).

    φ
K ←--- 𝒜_{(x)}
↑       ↑
|       |
|       |
O ←---- 𝒜₀
    φ₀

Then there exists a lift φₗ : 𝒜_{(x₀)} →+* O for some x₀ such that these two diagrams exist and commute.

    φ'                      φ'
K ←--- 𝒜_{(x x₀)}       K ←--- 𝒜_{(x x₀)}
↑       ↑                 ↖       ↑
|       |                 φ ⟍     |
|       |                     ⟍   |
O ←---- 𝒜_{(x₀)}                𝒜_{(x)}
    φₗ

This is the underlying algebraic statement of the valuative criterion for Proj 𝒜.

Stacks Tag 01MF (algebraic part)

theorem AlgebraicGeometry.Proj.valuativeCriterion_existence {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A] : ValuativeCriterion.Existence (toSpecZero 𝒜)

Stacks Tag 01MF

instance AlgebraicGeometry.Proj.instUniversallyClosedToSpecZeroOfFiniteTypeSubtypeMemSubmoduleOfNatNat {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A] : UniversallyClosed (toSpecZero 𝒜)

instance AlgebraicGeometry.Proj.instIsProperToSpecZeroOfFiniteTypeSubtypeMemSubmoduleOfNatNat {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A] : IsProper (toSpecZero 𝒜)