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.

def AlgebraicGeometry.Proj.basicOpen {R : Type u_1} {A : Type u_2} [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.

Equations

• AlgebraicGeometry.Proj.basicOpen 𝒜 f = ProjectiveSpectrum.basicOpen 𝒜 f

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Proj.basicOpen_one {R : Type u_1} {A : Type u_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {ι : Type u_3} (f : ι → A) (hf : (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f)) : ⨆ (i : ι), basicOpen 𝒜 (f i) = ⊤

def AlgebraicGeometry.Proj.awayToSection {R : Type u_1} {A : Type u_2} [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.

Equations

• AlgebraicGeometry.Proj.awayToSection 𝒜 f = AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection 𝒜 f

noncomputable def AlgebraicGeometry.Proj.basicOpenToSpec {R : Type u_1} {A : Type u_2} [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.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Proj.basicOpenToSpec_app_top {R : Type u_1} {A : Type u_2} [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_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : Proj 𝒜 ⟶ Spec (CommRingCat.of ↥(𝒜 0))

The structure map Proj A ⟶ Spec A₀.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Proj.basicOpenIsoSpec {R : Type u_1} {A : Type u_2} [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.

Equations

• AlgebraicGeometry.Proj.basicOpenIsoSpec 𝒜 f f_deg hm = CategoryTheory.asIso (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f)

theorem AlgebraicGeometry.Proj.basicOpenIsoSpec_hom {R : Type u_1} {A : Type u_2} [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_2} [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.

Equations

• AlgebraicGeometry.Proj.basicOpenIsoAway 𝒜 f f_deg hm = CategoryTheory.asIso (AlgebraicGeometry.Proj.awayToSection 𝒜 f)

theorem AlgebraicGeometry.Proj.basicOpenIsoAway_hom {R : Type u_1} {A : Type u_2} [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_2} [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.

Equations

• AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenIsoSpec 𝒜 f f_deg hm).inv (AlgebraicGeometry.Proj.basicOpen 𝒜 f).ι

instance AlgebraicGeometry.Proj.instIsOpenImmersionAwayι {R : Type u_1} {A : Type u_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Proj.pullbackAwayιIso_hom_awayι {R : Type u_1} {A : Type u_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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

noncomputable def AlgebraicGeometry.Proj.openCoverOfISupEqTop {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] {ι : Type u_3} (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.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Proj.affineOpenCover {R : Type u_1} {A : Type u_2} [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.

Equations

• AlgebraicGeometry.Proj.affineOpenCover 𝒜 = AlgebraicGeometry.Proj.openCoverOfISupEqTop 𝒜 (fun (i : (i : ℕ+) × ↥(𝒜 ↑i)) => ↑i.snd) ⋯ ⋯ ⋯

noncomputable def AlgebraicGeometry.Proj.stalkIso {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] (x : ↑↑(Proj 𝒜).toPresheafedSpace) : (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.

Equations

• AlgebraicGeometry.Proj.stalkIso 𝒜 x = (AlgebraicGeometry.Proj.stalkIso' 𝒜 x).toCommRingCatIso