Proj of a graded domain is integral

A scheme is integral when it is irreducible and reduced, and both halves of that for Proj 𝒜 come from the standard affine charts D₊(f) ≅ Spec (A_f)₀:

• every (A_f)₀ is reduced -- a domain away from a nonzero f, and the zero ring away from 0 -- so Proj 𝒜 is reduced on an affine cover;
• away from a nonzero f the chart is the spectrum of a domain, hence irreducible, and two charts meet because D₊(f) ⊓ D₊(g) = D₊(fg) with fg ≠ 0.

Mathlib proves Spec of a domain is integral and provides the affine charts of Proj, but does not record integrality of Proj itself.

instance AlgebraicGeometry.Proj.isReduced_spec_away {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsDomain A] (f : A) : IsReduced (Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)))

Every standard affine chart of Proj of a graded domain is reduced.

instance AlgebraicGeometry.Proj.isReduced {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsDomain A] : IsReduced (Proj 𝒜)

Proj of a graded domain is reduced.

theorem AlgebraicGeometry.Proj.isDomain_away {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsDomain A] {f : A} (hf : f ≠ 0) : IsDomain ↑(CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))

The chart at a nonzero homogeneous element of positive degree is the spectrum of a domain.

theorem AlgebraicGeometry.Proj.isPreirreducible_basicOpen {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsDomain A] {m : ℕ} {f : A} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (hf : f ≠ 0) : IsPreirreducible ↑(basicOpen 𝒜 f)

A basic open of Proj at a nonzero homogeneous element of positive degree is the range of the corresponding chart, hence preirreducible.

theorem AlgebraicGeometry.Proj.basicOpen_nonempty {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsDomain A] {m : ℕ} {f : A} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (hf : f ≠ 0) : (↑(basicOpen 𝒜 f)).Nonempty

A basic open of Proj at a nonzero homogeneous element of positive degree is nonempty.

This is what makes two charts meet, and it is where the domain hypothesis is used a second time: the chart ring is nontrivial exactly because the element is not nilpotent.

theorem AlgebraicGeometry.Proj.irreducibleSpace {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsDomain A] [Nonempty ↥(Proj 𝒜)] : IrreducibleSpace ↥(Proj 𝒜)

Proj of a graded domain is irreducible, as soon as it is nonempty.

The charts at nonzero homogeneous elements of positive degree are irreducible, they still cover -- a chart at zero is empty, so it can be discarded -- and any two of them meet, because D₊(f) ⊓ D₊(g) = D₊(fg) and a product of nonzero elements of a domain is nonzero.

theorem AlgebraicGeometry.Proj.isIntegral {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] [IsDomain A] [Nonempty ↥(Proj 𝒜)] : IsIntegral (Proj 𝒜)

Proj of a graded domain is an integral scheme, as soon as it is nonempty.