Graded relative Spec

A grading of an affine scheme p : V ⟶ X over X is a nonnegatively graded quasicoherent algebra A = (Aₙ)ₙ on X together with an isomorphism of quasicoherent algebras p_* 𝒪_V ≅ ⨁ₙ Aₙ. Affine schemes over X equipped with a grading form the category GradedAffineSchemeOver X: the categorical pullback of the coordinate-algebra functor affineFunctions X along the direct-sum functor A ↦ ⨁ₙ Aₙ. A morphism consists of a morphism of schemes over X and a graded algebra morphism between the gradings, in the opposite direction, which induces the pullback of regular functions along the morphism of schemes.

Since relative Spec is an anti-equivalence between quasicoherent algebras and affine schemes over X, relative Spec with the grading retained, A ↦ (Spec_X (⨁ₙ Aₙ), A, p_* 𝒪 ≅ ⨁ₙ Aₙ), is an anti-equivalence gradedRelativeSpecEquiv X : (GradedQuasicoherentAlgebra X)ᵒᵖ ≌ GradedAffineSchemeOver X. Its inverse reads off the grading, and forgetting the grading recovers relative Spec of the direct-sum algebra. This is the setting for linear schemes such as Spec_X (Sym F), graded by the symmetric powers of a quasicoherent sheaf F.

Main declarations

• TauCeti.AlgebraicGeometry.GradedAffineSchemeOver: affine schemes over X with a grading of their function algebra;
• TauCeti.AlgebraicGeometry.gradedRelativeSpec: relative Spec of the direct-sum algebra, with its grading;
• TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv: graded relative Spec is an anti-equivalence, with identity unit and with counit given on underlying schemes by relative Spec of the grading isomorphism followed by the relative-Spec counit;
• TauCeti.AlgebraicGeometry.gradedRelativeSpecForgetIso: forgetting the grading of gradedRelativeSpec X gives relative Spec of the direct-sum algebra.

References

• The Stacks Project, Tag 01LQ (relative spectrum as a functor).
• A. Grothendieck and J. Dieudonné, Éléments de géométrie algébrique II, §1.3.

@[reducible, inline]

abbrev TauCeti.AlgebraicGeometry.GradedAffineSchemeOver (X : AlgebraicGeometry.Scheme) : Type (u + 1)

Affine schemes over X with a nonnegative grading of their function algebra: triples of an affine scheme p : V ⟶ X over X, a graded quasicoherent algebra A = (Aₙ)ₙ, and an isomorphism p_* 𝒪_V ≅ ⨁ₙ Aₙ of quasicoherent algebras. A morphism is a morphism of schemes over X together with a graded algebra morphism of the gradings, in the opposite direction, such that the two agree as morphisms of function algebras.

noncomputable def TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv (X : AlgebraicGeometry.Scheme) : (GradedQuasicoherentAlgebra X)ᵒᵖ ≌ GradedAffineSchemeOver X

Graded relative Spec is an anti-equivalence between graded quasicoherent algebras and graded affine schemes over X. The functor sends A to the relative spectrum of ⨁ₙ Aₙ, graded through the relative-Spec unit p_* 𝒪 ≅ ⨁ₙ Aₙ, and the inverse reads off the grading. The unit is the identity, and the counit is, on underlying schemes, relative Spec of the grading isomorphism followed by the relative-Spec counit.

noncomputable def TauCeti.AlgebraicGeometry.gradedRelativeSpec (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (GradedQuasicoherentAlgebra X)ᵒᵖ (GradedAffineSchemeOver X)

Relative Spec of the direct-sum algebra of a graded quasicoherent algebra, with its grading retained.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv_functor {X : AlgebraicGeometry.Scheme} : (gradedRelativeSpecEquiv X).functor = gradedRelativeSpec X

The functor of the graded relative-Spec anti-equivalence is graded relative Spec.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv_inverse {X : AlgebraicGeometry.Scheme} : (gradedRelativeSpecEquiv X).inverse = CategoryTheory.Limits.CategoricalPullback.π₂ (affineFunctions X) GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.op

The inverse of the graded relative-Spec anti-equivalence reads off the grading.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpec_obj_fst {X : AlgebraicGeometry.Scheme} (A : (GradedQuasicoherentAlgebra X)ᵒᵖ) : ((gradedRelativeSpec X).obj A).fst = (relativeSpec X).obj (Opposite.op (GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.obj (Opposite.unop A)))

The scheme underlying the graded relative spectrum of A is the relative spectrum of the direct-sum algebra ⨁ₙ Aₙ.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpec_obj_snd {X : AlgebraicGeometry.Scheme} (A : (GradedQuasicoherentAlgebra X)ᵒᵖ) : ((gradedRelativeSpec X).obj A).snd = A

The grading of the graded relative spectrum of A is A.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpec_obj_iso {X : AlgebraicGeometry.Scheme} (A : (GradedQuasicoherentAlgebra X)ᵒᵖ) : ((gradedRelativeSpec X).obj A).iso = ((relativeSpecUnit X).app (Opposite.op (GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.obj (Opposite.unop A)))).symm

The grading of the graded relative spectrum of A identifies its function algebra with ⨁ₙ Aₙ through the relative-Spec unit.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpec_map_fst {X : AlgebraicGeometry.Scheme} {A B : (GradedQuasicoherentAlgebra X)ᵒᵖ} (f : A ⟶ B) : ((gradedRelativeSpec X).map f).fst = (relativeSpec X).map (GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.map f.unop).op

On underlying schemes, graded relative Spec acts on a graded algebra morphism through relative Spec of the induced morphism of direct-sum algebras.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpec_map_snd {X : AlgebraicGeometry.Scheme} {A B : (GradedQuasicoherentAlgebra X)ᵒᵖ} (f : A ⟶ B) : ((gradedRelativeSpec X).map f).snd = f

On gradings, graded relative Spec acts on a graded algebra morphism by that morphism.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv_unitIso_hom_app {X : AlgebraicGeometry.Scheme} (A : (GradedQuasicoherentAlgebra X)ᵒᵖ) : (gradedRelativeSpecEquiv X).unitIso.hom.app A = CategoryTheory.CategoryStruct.id A

The unit of the graded relative-Spec anti-equivalence is the identity.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv_unitIso_inv_app {X : AlgebraicGeometry.Scheme} (A : (GradedQuasicoherentAlgebra X)ᵒᵖ) : (gradedRelativeSpecEquiv X).unitIso.inv.app A = CategoryTheory.CategoryStruct.id A

The inverse unit of the graded relative-Spec anti-equivalence is the identity.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv_counitIso_hom_app_fst {X : AlgebraicGeometry.Scheme} (V : GradedAffineSchemeOver X) : ((gradedRelativeSpecEquiv X).counitIso.hom.app V).fst = CategoryTheory.CategoryStruct.comp ((relativeSpec X).map V.iso.inv) ((relativeSpecCounit X).hom.app V.fst)

On underlying schemes, the counit at a graded affine scheme (V, A, φ) is relative Spec of φ, followed by the relative-Spec counit Spec_X (p_* 𝒪_V) ⟶ V.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv_counitIso_hom_app_snd {X : AlgebraicGeometry.Scheme} (V : GradedAffineSchemeOver X) : ((gradedRelativeSpecEquiv X).counitIso.hom.app V).snd = CategoryTheory.CategoryStruct.id V.snd

On gradings, the counit of the graded relative-Spec anti-equivalence is the identity.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv_counitIso_inv_app_fst {X : AlgebraicGeometry.Scheme} (V : GradedAffineSchemeOver X) : ((gradedRelativeSpecEquiv X).counitIso.inv.app V).fst = CategoryTheory.CategoryStruct.comp ((relativeSpecCounit X).inv.app V.fst) ((relativeSpec X).map V.iso.hom)

On underlying schemes, the inverse counit at a graded affine scheme (V, A, φ) is the inverse relative-Spec counit V ⟶ Spec_X (p_* 𝒪_V), followed by relative Spec of φ⁻¹.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpecEquiv_counitIso_inv_app_snd {X : AlgebraicGeometry.Scheme} (V : GradedAffineSchemeOver X) : ((gradedRelativeSpecEquiv X).counitIso.inv.app V).snd = CategoryTheory.CategoryStruct.id V.snd

On gradings, the inverse counit of the graded relative-Spec anti-equivalence is the identity.

instance TauCeti.AlgebraicGeometry.gradedRelativeSpec_isEquivalence (X : AlgebraicGeometry.Scheme) : (gradedRelativeSpec X).IsEquivalence

Graded relative Spec is an equivalence, in particular fully faithful and essentially surjective.

noncomputable def TauCeti.AlgebraicGeometry.gradedRelativeSpecForgetIso (X : AlgebraicGeometry.Scheme) : (gradedRelativeSpec X).comp (CategoryTheory.Limits.CategoricalPullback.π₁ (affineFunctions X) GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.op) ≅ GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.op.comp (relativeSpec X)

Forgetting the grading of the graded relative spectrum gives relative Spec of the direct-sum algebra.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpecForgetIso_hom_app {X : AlgebraicGeometry.Scheme} (A : (GradedQuasicoherentAlgebra X)ᵒᵖ) : (gradedRelativeSpecForgetIso X).hom.app A = CategoryTheory.CategoryStruct.id (((gradedRelativeSpec X).comp (CategoryTheory.Limits.CategoricalPullback.π₁ (affineFunctions X) GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.op)).obj A)

The comparison gradedRelativeSpecForgetIso is the identity on each object.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedRelativeSpecForgetIso_inv_app {X : AlgebraicGeometry.Scheme} (A : (GradedQuasicoherentAlgebra X)ᵒᵖ) : (gradedRelativeSpecForgetIso X).inv.app A = CategoryTheory.CategoryStruct.id ((GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.op.comp (relativeSpec X)).obj A)

The inverse comparison gradedRelativeSpecForgetIso is the identity on each object.