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) : (AlgebraicGeometry.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 : ↑↑(AlgebraicGeometry.Proj 𝒜).toPresheafedSpace) : x ∈ AlgebraicGeometry.Proj.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 𝒜] : AlgebraicGeometry.Proj.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 𝒜] : AlgebraicGeometry.Proj.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) : AlgebraicGeometry.Proj.basicOpen 𝒜 (f ^ n) = AlgebraicGeometry.Proj.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) : AlgebraicGeometry.Proj.basicOpen 𝒜 (f * g) = AlgebraicGeometry.Proj.basicOpen 𝒜 f ⊓ AlgebraicGeometry.Proj.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) : AlgebraicGeometry.Proj.basicOpen 𝒜 g ≤ AlgebraicGeometry.Proj.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) : AlgebraicGeometry.Proj.basicOpen 𝒜 f = ⨆ (i : ℕ), AlgebraicGeometry.Proj.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 (AlgebraicGeometry.Proj.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 : ι), AlgebraicGeometry.Proj.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) ⟶ (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

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.

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)

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.

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)

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

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)

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

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).ι

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

• ⋯ = ⋯

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

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)

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

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

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.

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

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