Reducedness and integrality of Proj

For an ℕ-graded ring A, this file shows that Proj A is a reduced scheme when A is a reduced ring, and that it is an integral scheme when A is an integral domain whose irrelevant ideal is nonzero, that is, when A has a nonzero homogeneous element of positive degree.

Main results

• AlgebraicGeometry.Proj.isReduced: Proj A is reduced if A is reduced.
• AlgebraicGeometry.Proj.isIntegral_of_isDomain: Proj A is integral if A is a domain with nonzero irrelevant ideal.

References

• Stacks Project, Tag 01M3 (Proj of a graded ring).

Provenance

Adapted from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit c3415f32a313e19ace43e05479aeaa0d56ca287a, file projects/ModularCurves/ModularCurves/ForMathlib/ProjIntegral.lean, declaration AlgebraicGeometry.Proj.isIntegral_of_isDomain. Here reducedness is a separate instance for Proj of any reduced graded ring rather than of a domain, and the positivity hypothesis is phrased as the nonvanishing of the irrelevant ideal.

instance AlgebraicGeometry.Proj.isReduced {σ : Type u_1} {A : Type u_2} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] [_root_.IsReduced A] : IsReduced (Proj 𝒜)

Proj A of a reduced graded ring A is a reduced scheme.

theorem AlgebraicGeometry.Proj.isIntegral_of_isDomain {σ : Type u_1} {A : Type u_2} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] [IsDomain A] (h : HomogeneousIdeal.irrelevant 𝒜 ≠ ⊥) : IsIntegral (Proj 𝒜)

Proj A of a graded domain A with nonzero irrelevant ideal, that is, with a nonzero homogeneous element of positive degree, is an integral scheme.