Domain properties of homogeneous localizations

HomogeneousLocalization 𝒜 S is by construction a subring of the ordinary localization Localization S, through the injective map HomogeneousLocalization.val. Thus a homogeneous localization of a domain at nonzerodivisors is again a domain.

The Away specialization records nontriviality and the domain property away from a nonzero element, and reducedness for every element. These are statements about graded rings and localization only. Projective-spectrum geometry consumes them when proving that the standard affine charts of Proj 𝒜 are reduced or integral.

theorem HomogeneousLocalization.isDomain_of_le_nonZeroDivisors {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] [IsDomain A] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) : IsDomain (HomogeneousLocalization 𝒜 S)

A homogeneous localization at a multiplicative set of nonzerodivisors is a domain, provided it is nontrivial.

theorem HomogeneousLocalization.nontrivial_of_le_nonZeroDivisors {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] [IsDomain A] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) : Nontrivial (HomogeneousLocalization 𝒜 S)

A homogeneous localization at a multiplicative set of nonzerodivisors of a nontrivial ring is nontrivial: val is injective, so a trivial source would force 0 = 1 in the target.

theorem HomogeneousLocalization.Away.nontrivial {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] [IsDomain A] {f : A} (hf : f ≠ 0) : Nontrivial (Away 𝒜 f)

Away from a nonzero element of a graded domain the homogeneous localization is nontrivial.

Nonzero is needed and not cosmetic: away from 0 the localization is the zero ring, since 0 = 0 ^ 1 lies in the powers of 0.

theorem HomogeneousLocalization.Away.isDomain {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] [IsDomain A] {f : A} (hf : f ≠ 0) : IsDomain (Away 𝒜 f)

Away from a nonzero element of a graded domain, the degree-zero homogeneous localization is a domain.

Nonzero is what puts the powers of f among the nonzerodivisors; away from 0 the ring is trivial instead.

theorem HomogeneousLocalization.Away.isReduced {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [AddCommMonoid ι] [DecidableEq ι] [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] (𝒜 : ι → σ) [GradedRing 𝒜] [IsDomain A] (f : A) : IsReduced (Away 𝒜 f)

Every degree-zero homogeneous localization of a graded domain is reduced: away from a nonzero element it is a domain, and away from zero it is the zero ring.