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.

source

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) :

(AlgebraicGeometry.Proj 𝒜).Opens

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

Equations

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

Instances For

source

@[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 : ↑↑(AlgebraicGeometry.Proj 𝒜).toPresheafedSpace) :

x ∈ AlgebraicGeometry.Proj.basicOpen 𝒜 f ↔ f ∉ x.asHomogeneousIdeal

source

@[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 𝒜] :

AlgebraicGeometry.Proj.basicOpen 𝒜 1 = ⊤

source

@[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 𝒜] :

AlgebraicGeometry.Proj.basicOpen 𝒜 0 = ⊥

source

@[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) :

AlgebraicGeometry.Proj.basicOpen 𝒜 (f ^ n) = AlgebraicGeometry.Proj.basicOpen 𝒜 f

source

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) :

AlgebraicGeometry.Proj.basicOpen 𝒜 (f * g) = AlgebraicGeometry.Proj.basicOpen 𝒜 f ⊓ AlgebraicGeometry.Proj.basicOpen 𝒜 g

source

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) :

AlgebraicGeometry.Proj.basicOpen 𝒜 g ≤ AlgebraicGeometry.Proj.basicOpen 𝒜 f

source

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) :

AlgebraicGeometry.Proj.basicOpen 𝒜 f = ⨆ (i : ℕ), AlgebraicGeometry.Proj.basicOpen 𝒜 ((GradedAlgebra.proj 𝒜 i) f)

source

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 (AlgebraicGeometry.Proj.basicOpen 𝒜))

source

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 : ι), AlgebraicGeometry.Proj.basicOpen 𝒜 (f i) = ⊤

source

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) ⟶ (AlgebraicGeometry.Proj 𝒜).presheaf.obj (Opposite.op (AlgebraicGeometry.Proj.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

Instances For

source

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) :

↑(AlgebraicGeometry.Proj.basicOpen 𝒜 f) ⟶ AlgebraicGeometry.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.

Instances For

source

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) :

AlgebraicGeometry.Scheme.Hom.app (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f) ⊤ = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayToSection 𝒜 f) (AlgebraicGeometry.Proj.basicOpen 𝒜 f).topIso.inv)

source

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

AlgebraicGeometry.Proj 𝒜 ⟶ AlgebraicGeometry.Spec (CommRingCat.of ↥(𝒜 0))

The structure map Proj A ⟶ Spec A₀.

Equations

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

Instances For

source

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) :

↑(AlgebraicGeometry.Proj.basicOpen 𝒜 f) ≅ AlgebraicGeometry.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)

Instances For

source

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) :

(AlgebraicGeometry.Proj.basicOpenIsoSpec 𝒜 f f_deg hm).hom = AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f

source

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) ≅ (AlgebraicGeometry.Proj 𝒜).presheaf.obj (Opposite.op (AlgebraicGeometry.Proj.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)

Instances For

source

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) :

(AlgebraicGeometry.Proj.basicOpenIsoAway 𝒜 f f_deg hm).hom = AlgebraicGeometry.Proj.awayToSection 𝒜 f

source

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) :

AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ AlgebraicGeometry.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).ι

Instances For

source

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) :

AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)

Equations

⋯ = ⋯

source

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) :

AlgebraicGeometry.Scheme.Hom.opensRange (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) = AlgebraicGeometry.Proj.basicOpen 𝒜 f

source

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) :

AlgebraicGeometry.IsAffineOpen (AlgebraicGeometry.Proj.basicOpen 𝒜 f)

source

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 (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.toSpecZero 𝒜) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers f)))

source

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 : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of ↥(𝒜 0)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.toSpecZero 𝒜) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers f)))) h

source

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)) (AlgebraicGeometry.Proj.awayToSection 𝒜 x) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayToSection 𝒜 f) ((AlgebraicGeometry.Proj 𝒜).presheaf.map (CategoryTheory.homOfLE ⋯).op)

source

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 : (AlgebraicGeometry.Proj 𝒜).presheaf.obj (Opposite.op (AlgebraicGeometry.Proj.basicOpen 𝒜 x)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx)) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayToSection 𝒜 x) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayToSection 𝒜 f) (CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Proj 𝒜).presheaf.map (CategoryTheory.homOfLE ⋯).op) h)

source

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 (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 x) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Proj 𝒜).homOfLE ⋯) (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f)

source

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 : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 x) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) h) = CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Proj 𝒜).homOfLE ⋯) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenToSpec 𝒜 f) h)

source

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 (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) = AlgebraicGeometry.Proj.awayι 𝒜 x ⋯ ⋯

source

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 : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj 𝒜 ⟶ Z) :

CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 x ⋯ ⋯) h

source

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 (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm') ≅ AlgebraicGeometry.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.

Instances For

source

@[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 (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (AlgebraicGeometry.Proj.awayι 𝒜 x ⋯ ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)

source

@[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 : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Proj 𝒜 ⟶ Z) :

CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 x ⋯ ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) h)

source

@[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 (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) = CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')

source

@[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 : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) h

source

@[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 (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))) = CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')

source

@[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 : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 g)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) h

source

@[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 (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))

source

@[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 : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) h

source

@[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 (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))

source

@[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 : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 g)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) h) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))) h

source

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)) :

(AlgebraicGeometry.Proj 𝒜).AffineOpenCover

Given a family of homogeneous elements f of positive degree that spans the irrelavent 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.

Instances For

source

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

(AlgebraicGeometry.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) ⋯ ⋯ ⋯

Instances For

source

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 : ↑↑(AlgebraicGeometry.Proj 𝒜).toPresheafedSpace) :

(AlgebraicGeometry.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

Instances For

Documentation

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic

Basic properties of the scheme `Proj A` #

Main results #

Basic properties of the scheme Proj A #

Main results #

Basic properties of the scheme `Proj A` #