The universal property of the graded symmetric algebra

For a quasicoherent sheaf F on a scheme X and a graded quasicoherent algebra A = ⨁ₙ Aₙ, a morphism of quasicoherent sheaves φ : F ⟶ A₁ extends uniquely to a morphism of graded quasicoherent algebras Sym F ⟶ A. In other words, the graded symmetric algebra functor is left adjoint to the degree-one functor:

gradedSymmetricAlgebraAdjunction X : gradedSymmetricAlgebra X ⊣ degreeOne.

Its counit Sym A₁ ⟶ A extends the identity of A₁ (gradedSymmetricAlgebraAdjunction_counit_app). Its unit is the identification F ≅ Sym¹ F (gradedSymmetricAlgebraAdjunction_unit), an isomorphism, matching the fact that gradedSymmetricAlgebra X is fully faithful: it identifies quasicoherent sheaves with its essential image, the graded quasicoherent algebras freely generated in degree one. Under graded relative Spec these are the coordinate algebras of the linear schemes Spec_X Sym F over X.

The extension Symⁿ F ⟶ Aₙ is built over each open U from the universal property of the symmetric algebra of the Γ(X, U)-module Γ(F, U), with values in the graded ring ⨁ n, Γ(Aₙ, U) of sections of A, and then sheafified (TauCeti.SheafOfModules.symmetricPowerLift); its compatibility with the unit and the multiplication is checked on sections and transported along the monoidal sheafification adjunction. Uniqueness holds because Sym F is generated in degree one (gradedSymmetricAlgebra_hom_ext).

Main declarations

• TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraLift: the morphism Sym F ⟶ A of graded quasicoherent algebras extending φ : F ⟶ A₁, characterized by gradedSymmetricAlgebraDegreeOneIso_inv_app_comp_degreeOne_map_lift, and natural on both sides (gradedSymmetricAlgebraLift_comp, gradedSymmetricAlgebra_map_comp_lift);
• TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction: the adjunction gradedSymmetricAlgebra X ⊣ degreeOne, whose unit is the identification F ≅ Sym¹ F (gradedSymmetricAlgebraAdjunction_unit) and whose counit Sym A₁ ⟶ A extends the identity of A₁ (gradedSymmetricAlgebraAdjunction_counit_app).

References

• The Stacks Project, Tag 01M1.

The extension on sections

The universal property

noncomputable def TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraLift {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {A : GradedQuasicoherentAlgebra X} (φ : F ⟶ GradedQuasicoherentAlgebra.degreeOne.obj A) : (gradedSymmetricAlgebra X).obj F ⟶ A

The morphism of graded quasicoherent algebras Sym F ⟶ A extending a morphism φ : F ⟶ A₁ of quasicoherent sheaves into the degree-one component of A (gradedSymmetricAlgebraDegreeOneIso_inv_app_comp_degreeOne_map_lift).

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraDegreeOneIso_inv_app_comp_degreeOne_map_lift {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {A : GradedQuasicoherentAlgebra X} (φ : F ⟶ GradedQuasicoherentAlgebra.degreeOne.obj A) : CategoryTheory.CategoryStruct.comp ((gradedSymmetricAlgebraDegreeOneIso X).inv.app F) (GradedQuasicoherentAlgebra.degreeOne.map (gradedSymmetricAlgebraLift φ)) = φ

The degree-one component of gradedSymmetricAlgebraLift φ is φ, through the identification F ≅ Sym¹ F.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraDegreeOneIso_inv_app_comp_degreeOne_map_lift_assoc {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {A : GradedQuasicoherentAlgebra X} (φ : F ⟶ GradedQuasicoherentAlgebra.degreeOne.obj A) {Z : QuasicoherentSheaf X} (h : GradedQuasicoherentAlgebra.degreeOne.obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((gradedSymmetricAlgebraDegreeOneIso X).inv.app F) (CategoryTheory.CategoryStruct.comp (GradedQuasicoherentAlgebra.degreeOne.map (gradedSymmetricAlgebraLift φ)) h) = CategoryTheory.CategoryStruct.comp φ h

The degree-one component of gradedSymmetricAlgebraLift φ is φ, through the identification F ≅ Sym¹ F.

noncomputable def TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction (X : AlgebraicGeometry.Scheme) : gradedSymmetricAlgebra X ⊣ GradedQuasicoherentAlgebra.degreeOne

The graded symmetric algebra functor is left adjoint to the degree-one functor: morphisms of graded quasicoherent algebras Sym F ⟶ A correspond to morphisms of quasicoherent sheaves F ⟶ A₁, by restriction to degree one along F ≅ Sym¹ F and by gradedSymmetricAlgebraLift.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction_homEquiv_apply {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {A : GradedQuasicoherentAlgebra X} (f : (gradedSymmetricAlgebra X).obj F ⟶ A) : ((gradedSymmetricAlgebraAdjunction X).homEquiv F A) f = CategoryTheory.CategoryStruct.comp ((gradedSymmetricAlgebraDegreeOneIso X).inv.app F) (GradedQuasicoherentAlgebra.degreeOne.map f)

The bijection of gradedSymmetricAlgebraAdjunction restricts a morphism Sym F ⟶ A to degree one.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction_homEquiv_symm_apply {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {A : GradedQuasicoherentAlgebra X} (φ : F ⟶ GradedQuasicoherentAlgebra.degreeOne.obj A) : ((gradedSymmetricAlgebraAdjunction X).homEquiv F A).symm φ = gradedSymmetricAlgebraLift φ

The inverse bijection of gradedSymmetricAlgebraAdjunction is gradedSymmetricAlgebraLift.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraLift_comp {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {A B : GradedQuasicoherentAlgebra X} (φ : F ⟶ GradedQuasicoherentAlgebra.degreeOne.obj A) (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (gradedSymmetricAlgebraLift φ) f = gradedSymmetricAlgebraLift (CategoryTheory.CategoryStruct.comp φ (GradedQuasicoherentAlgebra.degreeOne.map f))

Postcomposing gradedSymmetricAlgebraLift φ with a morphism f of graded quasicoherent algebras extends φ followed by the degree-one component of f.

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraLift_comp_assoc {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {A B : GradedQuasicoherentAlgebra X} (φ : F ⟶ GradedQuasicoherentAlgebra.degreeOne.obj A) (f : A ⟶ B) {Z : GradedQuasicoherentAlgebra X} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (gradedSymmetricAlgebraLift φ) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (gradedSymmetricAlgebraLift (CategoryTheory.CategoryStruct.comp φ (GradedQuasicoherentAlgebra.degreeOne.map f))) h

Postcomposing gradedSymmetricAlgebraLift φ with a morphism f of graded quasicoherent algebras extends φ followed by the degree-one component of f.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra_map_comp_lift {X : AlgebraicGeometry.Scheme} {F' F : QuasicoherentSheaf X} {A : GradedQuasicoherentAlgebra X} (g : F' ⟶ F) (φ : F ⟶ GradedQuasicoherentAlgebra.degreeOne.obj A) : CategoryTheory.CategoryStruct.comp ((gradedSymmetricAlgebra X).map g) (gradedSymmetricAlgebraLift φ) = gradedSymmetricAlgebraLift (CategoryTheory.CategoryStruct.comp g φ)

Precomposing gradedSymmetricAlgebraLift φ with the map Sym F' ⟶ Sym F induced by a morphism g : F' ⟶ F extends g ≫ φ.

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra_map_comp_lift_assoc {X : AlgebraicGeometry.Scheme} {F' F : QuasicoherentSheaf X} {A : GradedQuasicoherentAlgebra X} (g : F' ⟶ F) (φ : F ⟶ GradedQuasicoherentAlgebra.degreeOne.obj A) {Z : GradedQuasicoherentAlgebra X} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((gradedSymmetricAlgebra X).map g) (CategoryTheory.CategoryStruct.comp (gradedSymmetricAlgebraLift φ) h) = CategoryTheory.CategoryStruct.comp (gradedSymmetricAlgebraLift (CategoryTheory.CategoryStruct.comp g φ)) h

Precomposing gradedSymmetricAlgebraLift φ with the map Sym F' ⟶ Sym F induced by a morphism g : F' ⟶ F extends g ≫ φ.

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction_unit (X : AlgebraicGeometry.Scheme) : (gradedSymmetricAlgebraAdjunction X).unit = (gradedSymmetricAlgebraDegreeOneIso X).inv

The unit of gradedSymmetricAlgebraAdjunction is the identification F ≅ Sym¹ F.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction_counit_app {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) : (gradedSymmetricAlgebraAdjunction X).counit.app A = gradedSymmetricAlgebraLift (CategoryTheory.CategoryStruct.id (GradedQuasicoherentAlgebra.degreeOne.obj A))

The counit of gradedSymmetricAlgebraAdjunction at A is the morphism Sym A₁ ⟶ A extending the identity of the degree-one component A₁.