Scheme-theoretically dense standard opens of Proj

For an ℕ-graded ring A and a homogeneous element g of positive degree that is a nonzerodivisor of A, the standard open D₊(g) is scheme-theoretically dense in Proj A: the open immersion Proj.awayι 𝒜 g : Spec A_{(g)} ⟶ Proj A is scheme-theoretically dominant.

On the standard chart Spec A_{(f)} of Proj A, the open D₊(g) is the spectrum of A_{(fg)}, and the restriction A_{(f)} → A_{(fg)} is injective because g is a nonzerodivisor.

Main results

• AlgebraicGeometry.Proj.isSchemeTheoreticallyDominant_awayι: for a homogeneous nonzerodivisor g of positive degree, the open immersion Proj.awayι 𝒜 g is scheme-theoretically dominant.

References

• The Stacks Project, Tag 01RA (scheme theoretic closure and density), especially Lemma 29.7.5 (Tag 01RE).

Provenance

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/EllipticCurve/PoleFiltration.lean, declarations spec_hom_ext_of_nonZeroDivisor and projModel_hom_ext_of_affine. The first is the affine case: by an equalizer argument, two morphisms from an affine scheme to a separated scheme that agree after inverting a nonzerodivisor of its coordinate ring are equal. The second treats the projective Weierstrass model only: on each standard chart D₊(Xⱼ) it presents A_{(XⱼZ)} as the localization of A_{(Xⱼ)} at a nonzerodivisor and applies the first, so that two morphisms to a separated scheme that agree on D₊(Z) are equal. Here the conclusion is Mathlib's AlgebraicGeometry.IsSchemeTheoreticallyDominant, from which that extension statement follows by TauCeti.ext_of_isSchemeTheoreticallyDominant. The statement for Proj of an arbitrary graded ring, with the hypothesis that g is a nonzerodivisor of A rather than of each chart, is not in the source.

theorem AlgebraicGeometry.Proj.isSchemeTheoreticallyDominant_awayι {σ : Type u_1} {A : Type u_2} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] {g : A} {m : ℕ} (g_deg : g ∈ 𝒜 m) (hm : 0 < m) (hg : g ∈ nonZeroDivisors A) : IsSchemeTheoreticallyDominant (awayι 𝒜 g g_deg hm)

For a homogeneous element g of positive degree that is a nonzerodivisor of the graded ring A, the standard open D₊(g) is scheme-theoretically dense in Proj A: the open immersion Proj.awayι 𝒜 g : Spec A_{(g)} ⟶ Proj A is scheme-theoretically dominant.