The graded symmetric algebra of a quasicoherent sheaf

For a quasicoherent sheaf F on a scheme X, the symmetric powers Symⁿ F are quasicoherent, and the multiplications Symⁱ F ⊗ Symʲ F ⟶ Symⁱ⁺ʲ F together with the unit 𝒪_X ≅ Sym⁰ F make Sym F = ⨁ₙ Symⁿ F a commutative nonnegatively graded quasicoherent 𝒪_X-algebra. This file packages that construction as a functor

gradedSymmetricAlgebra X : QuasicoherentSheaf X ⥤ GradedQuasicoherentAlgebra X,

whose value on a morphism φ : F ⟶ G is the family of symmetric powers Symⁿ φ. Its degree-n component is naturally the symmetric power functor QuasicoherentSheaf.symmetricPower X n (gradedSymmetricAlgebraDegreeIso), and its degree-one component recovers F (gradedSymmetricAlgebraDegreeOneIso), so the functor is faithful. Its unit and multiplications are epimorphisms, so Sym F is generated in degree one and a graded algebra morphism out of it is determined in degree one; hence the functor is also full. The graded algebras isomorphic to some Sym F are the coordinate algebras of linear schemes Spec_X Sym F over X (Stacks Project, tag 01M1).

Main declarations

• TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra: the graded symmetric algebra functor;
• TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra_obj_obj_X, TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra_map_hom_hom_hom, TauCeti.AlgebraicGeometry.mul_gradedSymmetricAlgebra and TauCeti.AlgebraicGeometry.one_gradedSymmetricAlgebra: its homogeneous components, its action on morphisms, its homogeneous multiplication and its unit;
• TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraDegreeIso: the natural isomorphism between the degree-n component of Sym F and the quasicoherent symmetric power Symⁿ F;
• TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraDegreeOneIso: the natural isomorphism between the degree-one component of Sym F and F;
• TauCeti.AlgebraicGeometry.epi_one_gradedSymmetricAlgebra and TauCeti.AlgebraicGeometry.epi_mul_gradedSymmetricAlgebra: the unit and the multiplications of Sym F are epimorphisms;
• TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra_hom_ext: a graded algebra morphism out of Sym F is determined by its degree-one component;
• TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra_map_degreeOne: a graded algebra morphism Sym F ⟶ Sym G is the graded symmetric algebra of its degree-one component, and TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra_preimage computes its preimage accordingly;
• the instances (gradedSymmetricAlgebra X).Faithful and (gradedSymmetricAlgebra X).Full.

noncomputable def TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (QuasicoherentSheaf X) (GradedQuasicoherentAlgebra X)

The graded symmetric algebra Sym F = ⨁ₙ Symⁿ F of a quasicoherent sheaf F, as a graded quasicoherent algebra, functorially in F: its homogeneous components are the symmetric powers Symⁿ F, its unit is 𝒪_X ≅ Sym⁰ F, its homogeneous multiplication is the multiplication of symmetric powers Symⁱ F ⊗ Symʲ F ⟶ Symⁱ⁺ʲ F, and a morphism φ : F ⟶ G acts by Symⁿ φ in degree n.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra_obj_obj_X {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) (n : ℕ) : ((gradedSymmetricAlgebra X).obj F).obj.X n = (SheafOfModules.symmetricPower X.sheaf n).obj F.obj

The degree-n component of the graded symmetric algebra of F is the symmetric power Symⁿ F.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra_map_hom_hom_hom {X : AlgebraicGeometry.Scheme} {F G : QuasicoherentSheaf X} (φ : F ⟶ G) (n : ℕ) : ((gradedSymmetricAlgebra X).map φ).hom.hom.hom n = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower X.sheaf n).map φ.hom) (CategoryTheory.eqToHom ⋯))

In degree n, the graded symmetric algebra acts on a morphism φ by Symⁿ φ, up to the identifications gradedSymmetricAlgebra_obj_obj_X of the homogeneous components with the symmetric powers.

@[simp]

theorem TauCeti.AlgebraicGeometry.mul_gradedSymmetricAlgebra {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) (i j : ℕ) : ((gradedSymmetricAlgebra X).obj F).obj.toMon.mul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (F.obj.symmetricPowerMul i j) (CategoryTheory.eqToHom ⋯))

The homogeneous multiplication of the graded symmetric algebra of F is the multiplication of symmetric powers Symⁱ F ⊗ Symʲ F ⟶ Symⁱ⁺ʲ F, up to the identifications gradedSymmetricAlgebra_obj_obj_X.

@[simp]

theorem TauCeti.AlgebraicGeometry.one_gradedSymmetricAlgebra {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) : ((gradedSymmetricAlgebra X).obj F).obj.toMon.one = CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPowerZeroIso X.sheaf).inv.app F.obj) (CategoryTheory.eqToHom ⋯)

The unit of the graded symmetric algebra of F is the identification 𝒪_X ≅ Sym⁰ F, up to the identification gradedSymmetricAlgebra_obj_obj_X.

theorem TauCeti.AlgebraicGeometry.degree_obj_gradedSymmetricAlgebra_obj {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) (n : ℕ) : ((GradedQuasicoherentAlgebra.degree n).obj ((gradedSymmetricAlgebra X).obj F)).obj = (SheafOfModules.symmetricPower X.sheaf n).obj F.obj

The degree-n component of the graded symmetric algebra of F, as a quasicoherent sheaf, has underlying module sheaf the symmetric power Symⁿ F.

theorem TauCeti.AlgebraicGeometry.degree_map_gradedSymmetricAlgebra_map_hom {X : AlgebraicGeometry.Scheme} {F G : QuasicoherentSheaf X} (φ : F ⟶ G) (n : ℕ) : ((GradedQuasicoherentAlgebra.degree n).map ((gradedSymmetricAlgebra X).map φ)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower X.sheaf n).map φ.hom) (CategoryTheory.eqToHom ⋯))

The degree-n component functor acts on the graded symmetric algebra of a morphism φ by Symⁿ φ, up to the identifications degree_obj_gradedSymmetricAlgebra_obj.

This is not a simp lemma: degree_map_hom and gradedSymmetricAlgebra_map_hom_hom_hom already rewrite its left-hand side, so pass it to simp explicitly in place of degree_map_hom.

noncomputable def TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraDegreeIso (X : AlgebraicGeometry.Scheme) (n : ℕ) : (gradedSymmetricAlgebra X).comp (GradedQuasicoherentAlgebra.degree n) ≅ QuasicoherentSheaf.symmetricPower X n

The degree-n component of the graded symmetric algebra of a quasicoherent sheaf F is naturally isomorphic to the symmetric power Symⁿ F of quasicoherent sheaves.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraDegreeIso_hom_app_hom {X : AlgebraicGeometry.Scheme} (n : ℕ) (F : QuasicoherentSheaf X) : ((gradedSymmetricAlgebraDegreeIso X n).hom.app F).hom = CategoryTheory.eqToHom ⋯

The component of gradedSymmetricAlgebraDegreeIso at F is the identification of the degree-n component of the graded symmetric algebra of F with Symⁿ F.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraDegreeIso_inv_app_hom {X : AlgebraicGeometry.Scheme} (n : ℕ) (F : QuasicoherentSheaf X) : ((gradedSymmetricAlgebraDegreeIso X n).inv.app F).hom = CategoryTheory.eqToHom ⋯

The inverse component of gradedSymmetricAlgebraDegreeIso at F is the identification of Symⁿ F with the degree-n component of the graded symmetric algebra of F.

noncomputable def TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraDegreeOneIso (X : AlgebraicGeometry.Scheme) : (gradedSymmetricAlgebra X).comp GradedQuasicoherentAlgebra.degreeOne ≅ CategoryTheory.Functor.id (QuasicoherentSheaf X)

The degree-one component of the graded symmetric algebra of a quasicoherent sheaf F is naturally isomorphic to F, through the identification Sym¹ F ≅ F.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraDegreeOneIso_hom_app_hom {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) : ((gradedSymmetricAlgebraDegreeOneIso X).hom.app F).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((SheafOfModules.symmetricPowerOneIso X.sheaf).hom.app F.obj)

The component of gradedSymmetricAlgebraDegreeOneIso at F is the identification Sym¹ F ≅ F, after identifying the degree-one component with Sym¹ F.

@[simp]

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraDegreeOneIso_inv_app_hom {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) : ((gradedSymmetricAlgebraDegreeOneIso X).inv.app F).hom = CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPowerOneIso X.sheaf).inv.app F.obj) (CategoryTheory.eqToHom ⋯)

The inverse component of gradedSymmetricAlgebraDegreeOneIso at F is the identification F ≅ Sym¹ F, followed by the identification of Sym¹ F with the degree-one component.

instance TauCeti.AlgebraicGeometry.instFaithfulQuasicoherentSheafGradedQuasicoherentAlgebraGradedSymmetricAlgebra {X : AlgebraicGeometry.Scheme} : (gradedSymmetricAlgebra X).Faithful

The graded symmetric algebra functor is faithful: a morphism of quasicoherent sheaves is recovered from its action in degree one.

instance TauCeti.AlgebraicGeometry.epi_one_gradedSymmetricAlgebra {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) : CategoryTheory.Epi ((gradedSymmetricAlgebra X).obj F).obj.toMon.one

The unit 𝒪_X ⟶ Sym⁰ F of the graded symmetric algebra is an epimorphism, being an isomorphism.

instance TauCeti.AlgebraicGeometry.epi_mul_gradedSymmetricAlgebra {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) (i j : ℕ) : CategoryTheory.Epi (((gradedSymmetricAlgebra X).obj F).obj.toMon.mul i j)

The multiplications Symⁱ F ⊗ Symʲ F ⟶ Symⁱ⁺ʲ F of the graded symmetric algebra are epimorphisms; in particular the graded symmetric algebra is generated in degree one.

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra_hom_ext {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {A : GradedQuasicoherentAlgebra X} {f g : (gradedSymmetricAlgebra X).obj F ⟶ A} (h : GradedQuasicoherentAlgebra.degreeOne.map f = GradedQuasicoherentAlgebra.degreeOne.map g) : f = g

Morphisms of graded quasicoherent algebras out of the graded symmetric algebra Sym F are determined by their degree-one components.

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra_map_degreeOne {X : AlgebraicGeometry.Scheme} {F G : QuasicoherentSheaf X} (φ : (gradedSymmetricAlgebra X).obj F ⟶ (gradedSymmetricAlgebra X).obj G) : (gradedSymmetricAlgebra X).map (CategoryTheory.CategoryStruct.comp ((gradedSymmetricAlgebraDegreeOneIso X).inv.app F) (CategoryTheory.CategoryStruct.comp (GradedQuasicoherentAlgebra.degreeOne.map φ) ((gradedSymmetricAlgebraDegreeOneIso X).hom.app G))) = φ

Since Sym F is generated in degree one, a morphism of graded algebras φ : Sym F ⟶ Sym G is the graded symmetric algebra of its degree-one component F ⟶ G.

instance TauCeti.AlgebraicGeometry.instFullQuasicoherentSheafGradedQuasicoherentAlgebraGradedSymmetricAlgebra {X : AlgebraicGeometry.Scheme} : (gradedSymmetricAlgebra X).Full

The graded symmetric algebra functor is full: a morphism of graded algebras Sym F ⟶ Sym G is the graded symmetric algebra of its degree-one component (gradedSymmetricAlgebra_map_degreeOne).

theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebra_preimage {X : AlgebraicGeometry.Scheme} {F G : QuasicoherentSheaf X} (φ : (gradedSymmetricAlgebra X).obj F ⟶ (gradedSymmetricAlgebra X).obj G) : (gradedSymmetricAlgebra X).preimage φ = CategoryTheory.CategoryStruct.comp ((gradedSymmetricAlgebraDegreeOneIso X).inv.app F) (CategoryTheory.CategoryStruct.comp (GradedQuasicoherentAlgebra.degreeOne.map φ) ((gradedSymmetricAlgebraDegreeOneIso X).hom.app G))

The preimage of a morphism of graded algebras φ : Sym F ⟶ Sym G under the graded symmetric algebra functor is its degree-one component F ⟶ G.