Points of Proj through standard charts, and compatibilities of Proj.map

For a graded ring A, a ring homomorphism φ : A →+* R and a homogeneous element f of positive degree with φ f a unit, the composite

Spec R ⟶ Spec A_{(f)} ⟶ Proj A

of Spec of HomogeneousLocalization.Away.lift φ with the standard chart Proj.awayι is the R-point of Proj A with "homogeneous coordinates" φ. This file proves that it does not depend on the chart: any other homogeneous g of positive degree with φ g a unit gives the same morphism. It also proves that Proj.map of a graded ring homomorphism lies over the induced map on Spec of the degree-zero parts, and packages Proj.map of a graded ring isomorphism as an isomorphism of schemes.

Main definitions

• AlgebraicGeometry.Proj.mapIso: the isomorphism Proj ℬ ≅ Proj 𝒜 induced by mutually inverse graded ring homomorphisms.

Main results

• AlgebraicGeometry.Proj.SpecMap_awayLift_awayι_eq: the point of Proj A defined by φ on the chart D₊(f) agrees with the one defined on the chart D₊(g).
• AlgebraicGeometry.Proj.map_toSpecZero: Proj.map f lies over Spec of the degree-zero part of f.
• ProjectiveSpectrum.ext_of_mem_pos: positive-degree homogeneous elements determine a projective point, allowing comparison through its positive-degree coordinate opens.

theorem AlgebraicGeometry.Proj.SpecMap_awayLift_awayι_eq {A σ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] {R : Type u} [CommRing R] (φ : A →+* R) {f g : A} {m m' : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') (hf : IsUnit (φ f)) (hg : IsUnit (φ g)) : CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.lift 𝒜 φ hf))) (awayι 𝒜 f f_deg hm) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.Away.lift 𝒜 φ hg))) (awayι 𝒜 g g_deg hm')

The R-point of Proj A with homogeneous coordinates φ : A →+* R, read on the standard chart D₊(f), does not depend on the homogeneous element f of positive degree with φ f a unit: both charts give the point read on D₊(fg).

@[simp]

theorem AlgebraicGeometry.Proj.map_toSpecZero {A B σ τ : Type u} [CommRing A] [CommRing B] [SetLike σ A] [AddSubgroupClass σ A] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) : CategoryTheory.CategoryStruct.comp (map f hf) (toSpecZero 𝒜) = CategoryTheory.CategoryStruct.comp (toSpecZero ℬ) (Spec.map (CommRingCat.ofHom f.gradedZeroRingHom))

Proj.map f lies over Spec of the ring homomorphism 𝒜 0 →+* ℬ 0 induced by f on the degree-zero parts.

@[simp]

theorem AlgebraicGeometry.Proj.map_toSpecZero_assoc {A B σ τ : Type u} [CommRing A] [CommRing B] [SetLike σ A] [AddSubgroupClass σ A] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) {Z : Scheme} (h : Spec ↧↥(𝒜 0) ⟶ Z) : CategoryTheory.CategoryStruct.comp (map f hf) (CategoryTheory.CategoryStruct.comp (toSpecZero 𝒜) h) = CategoryTheory.CategoryStruct.comp (toSpecZero ℬ) (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom f.gradedZeroRingHom)) h)

Proj.map f lies over Spec of the ring homomorphism 𝒜 0 →+* ℬ 0 induced by f on the degree-zero parts.

noncomputable def AlgebraicGeometry.Proj.mapIso {A B σ τ : Type u} [CommRing A] [CommRing B] [SetLike σ A] [AddSubgroupClass σ A] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒜) (hfg : Function.RightInverse ⇑g ⇑f) (hgf : Function.LeftInverse ⇑g ⇑f) : Proj ℬ ≅ Proj 𝒜

Mutually inverse graded ring homomorphisms f : 𝒜 →+*ᵍ ℬ and g : ℬ →+*ᵍ 𝒜 induce mutually inverse morphisms Proj.map f and Proj.map g.

Equations

• AlgebraicGeometry.Proj.mapIso f g hfg hgf = { hom := AlgebraicGeometry.Proj.map f ⋯, inv := AlgebraicGeometry.Proj.map g ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem AlgebraicGeometry.Proj.mapIso_hom {A B σ τ : Type u} [CommRing A] [CommRing B] [SetLike σ A] [AddSubgroupClass σ A] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒜) (hfg : Function.RightInverse ⇑g ⇑f) (hgf : Function.LeftInverse ⇑g ⇑f) : (mapIso f g hfg hgf).hom = map f ⋯

@[simp]

theorem AlgebraicGeometry.Proj.mapIso_inv {A B σ τ : Type u} [CommRing A] [CommRing B] [SetLike σ A] [AddSubgroupClass σ A] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒜) (hfg : Function.RightInverse ⇑g ⇑f) (hgf : Function.LeftInverse ⇑g ⇑f) : (mapIso f g hfg hgf).inv = map g ⋯

theorem ProjectiveSpectrum.ext_of_mem_pos {A : Type u_1} {σ : Type u_2} [CommRing A] [SetLike σ A] [AddSubmonoidClass σ A] {𝒜 : ℕ → σ} [GradedRing 𝒜] {x y : ProjectiveSpectrum 𝒜} (h : ∀ n > 0, ∀ s ∈ 𝒜 n, s ∈ x.asHomogeneousIdeal ↔ s ∈ y.asHomogeneousIdeal) : x = y

Relevant homogeneous prime ideals are determined by their positive-degree elements.