Documentation

TauCeti.RingTheory.GradedAlgebra.HomogeneousLocalization.Equality

Equality of degree-zero localization maps #

For a degree-one denominator, equality of degree-zero localization maps is equivalent to unit rescaling of homogeneous coordinates. This is the algebraic criterion for comparing scheme-valued points in a standard projective chart, including over rings with nilpotents.

theorem HomogeneousLocalization.Away.lift_eq_iff_exists_unit {A : Type u_1} {B : Type u_2} {σ : Type u_3} [CommRing A] [CommRing B] [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] (f g : A →+* B) {t : A} (ht : t ∈ 𝒜 1) (hf : IsUnit (f t)) (hg : IsUnit (g t)) :
lift 𝒜 f hf = lift 𝒜 g hg ↔ ∃ (c : Bˣ), ∀ (n : ℕ), ∀ a ∈ 𝒜 n, g a = ↑c ^ n * f a

On a degree-one chart, equal degree-zero localization maps are precisely unit rescalings of the homogeneous coordinates.