Basic properties of the scheme Proj A

The scheme Proj 𝒜 for a graded algebra 𝒜 is constructed in AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean. In this file we provide basic properties of the scheme.

Main results

• AlgebraicGeometry.Proj.toSpecZero: The structure map Proj A ⟶ Spec (A 0).
• AlgebraicGeometry.Proj.basicOpenIsoSpec: The canonical isomorphism Proj A |_ D₊(f) ≅ Spec (A_f)₀ when f is homogeneous of positive degree.
• AlgebraicGeometry.Proj.awayι: The open immersion Spec (A_f)₀ ⟶ Proj A.
• AlgebraicGeometry.Proj.affineOpenCover: The open cover of Proj A by Spec (A_f)₀ for all homogeneous f of positive degree.
• AlgebraicGeometry.Proj.stalkIso: The stalk of Proj A at x is the degree 0 part of the localization of A at x.
• AlgebraicGeometry.Proj.fromOfGlobalSections: Given a map f : A →+* Γ(X, ⊤) such that the image of the irrelevant ideal under f generates the whole ring, we can construct a map X ⟶ Proj 𝒜.

def AlgebraicGeometry.Proj.basicOpen {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) : (Proj 𝒜).Opens

The basic open set D₊(f) associated to f : A.

@[simp]

theorem AlgebraicGeometry.Proj.mem_basicOpen {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) (x : ↥(Proj 𝒜)) : x ∈ basicOpen 𝒜 f ↔ f ∉ x.asHomogeneousIdeal

@[simp]

theorem AlgebraicGeometry.Proj.basicOpen_one {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : basicOpen 𝒜 1 = ⊤

@[simp]

theorem AlgebraicGeometry.Proj.basicOpen_zero {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : basicOpen 𝒜 0 = ⊥

@[simp]

theorem AlgebraicGeometry.Proj.basicOpen_pow {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) (n : ℕ) (hn : 0 < n) : basicOpen 𝒜 (f ^ n) = basicOpen 𝒜 f

theorem AlgebraicGeometry.Proj.basicOpen_mul {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f g : A) : basicOpen 𝒜 (f * g) = basicOpen 𝒜 f ⊓ basicOpen 𝒜 g

theorem AlgebraicGeometry.Proj.basicOpen_mono {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f g : A) (hfg : f ∣ g) : basicOpen 𝒜 g ≤ basicOpen 𝒜 f

theorem AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) : basicOpen 𝒜 f = ⨆ (i : ℕ), basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f)

theorem AlgebraicGeometry.Proj.isBasis_basicOpen {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : TopologicalSpace.Opens.IsBasis (Set.range (basicOpen 𝒜))

theorem AlgebraicGeometry.Proj.iSup_basicOpen_eq_top {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {ι : Type u_2} (f : ι → A) (hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)) : ⨆ (i : ι), basicOpen 𝒜 (f i) = ⊤

If { xᵢ } spans the irrelevant ideal of A, then D₊(xᵢ) covers Proj A.

theorem AlgebraicGeometry.Proj.iSup_basicOpen_eq_top' {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {ι : Type u_2} (f : ι → A) (hfn : ∀ (i : ι), ∃ (n : ℕ), f i ∈ 𝒜 n) (hf : Algebra.adjoin (↥(𝒜 0)) (Set.range f) = ⊤) : ⨆ (i : ι), basicOpen 𝒜 (f i) = ⊤

If { xᵢ } are homogeneous and span A as an A₀ algebra, then D₊(xᵢ) covers Proj A.

def AlgebraicGeometry.Proj.awayToSection {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) : CommRingCat.of (HomogeneousLocalization.Away 𝒜 f) ⟶ (Proj 𝒜).presheaf.obj (Opposite.op (basicOpen 𝒜 f))

The canonical map (A_f)₀ ⟶ Γ(Proj A, D₊(f)). This is an isomorphism when f is homogeneous of positive degree. See basicOpenIsoAway below.

noncomputable def AlgebraicGeometry.Proj.basicOpenToSpec {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) : ↑(basicOpen 𝒜 f) ⟶ Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))

The canonical map Proj A |_ D₊(f) ⟶ Spec (A_f)₀. This is an isomorphism when f is homogeneous of positive degree. See basicOpenIsoSpec below.

theorem AlgebraicGeometry.Proj.basicOpenToSpec_app_top {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) : Scheme.Hom.app (basicOpenToSpec 𝒜 f) ⊤ = CategoryTheory.CategoryStruct.comp (Scheme.ΓSpecIso (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).hom (CategoryTheory.CategoryStruct.comp (awayToSection 𝒜 f) (basicOpen 𝒜 f).topIso.inv)

noncomputable def AlgebraicGeometry.Proj.toSpecZero {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : Proj 𝒜 ⟶ Spec (CommRingCat.of ↥(𝒜 0))

The structure map Proj A ⟶ Spec A₀.

noncomputable def AlgebraicGeometry.Proj.basicOpenIsoSpec {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : ↑(basicOpen 𝒜 f) ≅ Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))

The canonical isomorphism Proj A |_ D₊(f) ≅ Spec (A_f)₀ when f is homogeneous of positive degree.

theorem AlgebraicGeometry.Proj.basicOpenIsoSpec_hom {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : (basicOpenIsoSpec 𝒜 f f_deg hm).hom = basicOpenToSpec 𝒜 f

noncomputable def AlgebraicGeometry.Proj.basicOpenIsoAway {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : CommRingCat.of (HomogeneousLocalization.Away 𝒜 f) ≅ (Proj 𝒜).presheaf.obj (Opposite.op (basicOpen 𝒜 f))

The canonical isomorphism (A_f)₀ ≅ Γ(Proj A, D₊(f)) when f is homogeneous of positive degree.

theorem AlgebraicGeometry.Proj.basicOpenIsoAway_hom {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : (basicOpenIsoAway 𝒜 f f_deg hm).hom = awayToSection 𝒜 f

noncomputable def AlgebraicGeometry.Proj.awayι {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Proj 𝒜

The open immersion Spec (A_f)₀ ⟶ Proj A.

theorem AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : CategoryTheory.CategoryStruct.comp (basicOpenIsoSpec 𝒜 f f_deg hm).inv (basicOpen 𝒜 f).ι = awayι 𝒜 f f_deg hm

theorem AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι_assoc {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {Z : Scheme} (h : Proj 𝒜 ⟶ Z) : CategoryTheory.CategoryStruct.comp (basicOpenIsoSpec 𝒜 f f_deg hm).inv (CategoryTheory.CategoryStruct.comp (basicOpen 𝒜 f).ι h) = CategoryTheory.CategoryStruct.comp (awayι 𝒜 f f_deg hm) h

instance AlgebraicGeometry.Proj.instIsOpenImmersionAwayι {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : IsOpenImmersion (awayι 𝒜 f f_deg hm)

theorem AlgebraicGeometry.Proj.opensRange_awayι {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : Scheme.Hom.opensRange (awayι 𝒜 f f_deg hm) = basicOpen 𝒜 f

theorem AlgebraicGeometry.Proj.isAffineOpen_basicOpen {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : IsAffineOpen (basicOpen 𝒜 f)

theorem AlgebraicGeometry.Proj.awayι_toSpecZero {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : CategoryTheory.CategoryStruct.comp (awayι 𝒜 f f_deg hm) (toSpecZero 𝒜) = Spec.map (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers f)))

theorem AlgebraicGeometry.Proj.awayι_toSpecZero_assoc {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {Z : Scheme} (h : Spec (CommRingCat.of ↥(𝒜 0)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (awayι 𝒜 f f_deg hm) (CategoryTheory.CategoryStruct.comp (toSpecZero 𝒜) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers f)))) h

theorem AlgebraicGeometry.Proj.awayMap_awayToSection {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx)) (awayToSection 𝒜 x) = CategoryTheory.CategoryStruct.comp (awayToSection 𝒜 f) ((Proj 𝒜).presheaf.map (CategoryTheory.homOfLE ⋯).op)

theorem AlgebraicGeometry.Proj.awayMap_awayToSection_assoc {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g) {Z : CommRingCat} (h : (Proj 𝒜).presheaf.obj (Opposite.op (basicOpen 𝒜 x)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx)) (CategoryTheory.CategoryStruct.comp (awayToSection 𝒜 x) h) = CategoryTheory.CategoryStruct.comp (awayToSection 𝒜 f) (CategoryTheory.CategoryStruct.comp ((Proj 𝒜).presheaf.map (CategoryTheory.homOfLE ⋯).op) h)

theorem AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (basicOpenToSpec 𝒜 x) (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) = CategoryTheory.CategoryStruct.comp ((Proj 𝒜).homOfLE ⋯) (basicOpenToSpec 𝒜 f)

theorem AlgebraicGeometry.Proj.basicOpenToSpec_SpecMap_awayMap_assoc {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g) {Z : Scheme} (h : Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (basicOpenToSpec 𝒜 x) (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) h) = CategoryTheory.CategoryStruct.comp ((Proj 𝒜).homOfLE ⋯) (CategoryTheory.CategoryStruct.comp (basicOpenToSpec 𝒜 f) h)

theorem AlgebraicGeometry.Proj.SpecMap_awayMap_awayι {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) (awayι 𝒜 f f_deg hm) = awayι 𝒜 x ⋯ ⋯

theorem AlgebraicGeometry.Proj.SpecMap_awayMap_awayι_assoc {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') {x : A} (hx : x = f * g) {Z : Scheme} (h : Proj 𝒜 ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) (CategoryTheory.CategoryStruct.comp (awayι 𝒜 f f_deg hm) h) = CategoryTheory.CategoryStruct.comp (awayι 𝒜 x ⋯ ⋯) h

noncomputable def AlgebraicGeometry.Proj.pullbackAwayιIso {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) : CategoryTheory.Limits.pullback (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm') ≅ Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 x))

The isomorphism D₊(f) ×[Proj 𝒜] D₊(g) ≅ D₊(fg).

@[simp]

theorem AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (awayι 𝒜 x ⋯ ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')) (awayι 𝒜 f f_deg hm)

@[simp]

theorem AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι_assoc {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : Scheme} (h : Proj 𝒜 ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (CategoryTheory.CategoryStruct.comp (awayι 𝒜 x ⋯ ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')) (CategoryTheory.CategoryStruct.comp (awayι 𝒜 f f_deg hm) h)

@[simp]

theorem AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) = CategoryTheory.Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')

@[simp]

theorem AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : Scheme} (h : Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')) h

@[simp]

theorem AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))) = CategoryTheory.Limits.pullback.snd (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')

@[simp]

theorem AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_right_assoc {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : Scheme} (h : Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 g)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')) h

@[simp]

theorem AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv (CategoryTheory.Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')) = Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))

@[simp]

theorem AlgebraicGeometry.Proj.pullbackAwayιIso_inv_fst_assoc {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : Scheme} (h : Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) h

@[simp]

theorem AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) : CategoryTheory.CategoryStruct.comp (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv (CategoryTheory.Limits.pullback.snd (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')) = Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))

@[simp]

theorem AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd_assoc {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : Scheme} (h : Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 g)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (awayι 𝒜 f f_deg hm) (awayι 𝒜 g g_deg hm')) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))) h

theorem AlgebraicGeometry.Proj.awayι_preimage_basicOpen {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m') (hm' : 0 < m') : (TopologicalSpace.Opens.map (awayι 𝒜 f f_deg hm).base).obj (basicOpen 𝒜 g) = PrimeSpectrum.basicOpen (HomogeneousLocalization.Away.isLocalizationElem f_deg g_deg)

noncomputable def AlgebraicGeometry.Proj.openCoverOfISupEqTop {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {ι : Type u_2} (f : ι → A) {m : ι → ℕ} (f_deg : ∀ (i : ι), f i ∈ 𝒜 (m i)) (hm : ∀ (i : ι), 0 < m i) (hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)) : (Proj 𝒜).AffineOpenCover

Given a family of homogeneous elements f of positive degree that spans the irrelevant ideal, Spec (A_f)₀ ⟶ Proj A forms an affine open cover of Proj A.

noncomputable def AlgebraicGeometry.Proj.affineOpenCover {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : (Proj 𝒜).AffineOpenCover

Proj A is covered by Spec (A_f)₀ for all homogeneous elements of positive degree.

noncomputable def AlgebraicGeometry.Proj.stalkIso {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (x : ↥(Proj 𝒜)) : (Proj 𝒜).presheaf.stalk x ≅ CommRingCat.of (HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)

The stalk of Proj A at x is the degree 0 part of the localization of A at x.

def AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {X : Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) {x : ↑(X.presheaf.obj (Opposite.op ⊤))} {t : A} {d : ℕ} (H : f t = x) (h0d : 0 < d) (hd : t ∈ 𝒜 d) : ↑(X.basicOpen x) ⟶ ↑(basicOpen 𝒜 t)

Given a graded ring A and a map f : A →+* Γ(X, ⊤), for each homogeneous t of positive degree, it induces a map from D(f(t)) ⟶ D₊(t).

theorem AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {X : Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) {x x' : ↑(X.presheaf.obj (Opposite.op ⊤))} {t t' : A} {d d' : ℕ} {H : f t = x} {h0d : 0 < d} {hd : t ∈ 𝒜 d} {H' : f t' = x'} {h0d' : 0 < d'} {hd' : t' ∈ 𝒜 d'} {s : A} (hts : t * s = t') {n : ℕ} (hn : d + n = d') (hs : s ∈ 𝒜 n) : CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) (CategoryTheory.CategoryStruct.comp (toBasicOpenOfGlobalSections 𝒜 f H h0d hd) (basicOpen 𝒜 t).ι) = CategoryTheory.CategoryStruct.comp (toBasicOpenOfGlobalSections 𝒜 f H' h0d' hd') (basicOpen 𝒜 t').ι

theorem AlgebraicGeometry.Proj.homOfLE_toBasicOpenOfGlobalSections_ι_assoc {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {X : Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) {x x' : ↑(X.presheaf.obj (Opposite.op ⊤))} {t t' : A} {d d' : ℕ} {H : f t = x} {h0d : 0 < d} {hd : t ∈ 𝒜 d} {H' : f t' = x'} {h0d' : 0 < d'} {hd' : t' ∈ 𝒜 d'} {s : A} (hts : t * s = t') {n : ℕ} (hn : d + n = d') (hs : s ∈ 𝒜 n) {Z : Scheme} (h : Proj 𝒜 ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) (CategoryTheory.CategoryStruct.comp (toBasicOpenOfGlobalSections 𝒜 f H h0d hd) (CategoryTheory.CategoryStruct.comp (basicOpen 𝒜 t).ι h)) = CategoryTheory.CategoryStruct.comp (toBasicOpenOfGlobalSections 𝒜 f H' h0d' hd') (CategoryTheory.CategoryStruct.comp (basicOpen 𝒜 t').ι h)

def AlgebraicGeometry.Proj.openCoverOfMapIrreleventEqTop {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {X : Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) : X.OpenCover

Given a graded ring A and a map f : A →+* Γ(X, ⊤) such that the image of the irrelevant ideal under f generates the whole ring, the set of D(f(r)) for homogeneous r of positive degree forms an open cover on X.

def AlgebraicGeometry.Proj.fromOfGlobalSections {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {X : Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) : X ⟶ Proj 𝒜

Given a graded ring A and a map f : A →+* Γ(X, ⊤) such that the image of the irrelevant ideal under f generates the whole ring, we can construct a map X ⟶ Proj 𝒜.

theorem AlgebraicGeometry.Proj.fromOfGlobalSections_preimage_basicOpen {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {X : Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) {r : A} {n : ℕ} (hn : 0 < n) (hr : r ∈ 𝒜 n) : (TopologicalSpace.Opens.map (fromOfGlobalSections 𝒜 f hf).base).obj (basicOpen 𝒜 r) = X.basicOpen (f r)

theorem AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {X : Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) {r : A} {n : ℕ} (hn : 0 < n) (hr : r ∈ 𝒜 n) : fromOfGlobalSections 𝒜 f hf ∣_ basicOpen 𝒜 r = CategoryTheory.CategoryStruct.comp (X.isoOfEq ⋯).hom (toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr)

theorem AlgebraicGeometry.Proj.fromOfGlobalSections_resLE {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {X : Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) {r : A} {n : ℕ} (hn : 0 < n) (hr : r ∈ 𝒜 n) : Scheme.Hom.resLE (fromOfGlobalSections 𝒜 f hf) (basicOpen 𝒜 r) (X.basicOpen (f r)) ⋯ = toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr

theorem AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {X : Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) : CategoryTheory.CategoryStruct.comp (fromOfGlobalSections 𝒜 f hf) (toSpecZero 𝒜) = CategoryTheory.CategoryStruct.comp X.toSpecΓ (Spec.map (CommRingCat.ofHom (f.comp (algebraMap (↥(𝒜 0)) A))))

theorem AlgebraicGeometry.Proj.fromOfGlobalSections_toSpecZero_assoc {R : Type u_1} {A : Type u} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {X : Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤))) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) {Z : Scheme} (h : Spec (CommRingCat.of ↥(𝒜 0)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (fromOfGlobalSections 𝒜 f hf) (CategoryTheory.CategoryStruct.comp (toSpecZero 𝒜) h) = CategoryTheory.CategoryStruct.comp X.toSpecΓ (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (f.comp (algebraMap (↥(𝒜 0)) A)))) h)