Documentation

TauCeti.AlgebraicGeometry.Modules.Quasicoherent.GradedAlgebra.Free

Graded quasicoherent algebras freely generated in degree one #

A graded quasicoherent algebra A on a scheme X is freely generated in degree one when it is isomorphic, as a graded algebra, to the graded symmetric algebra Sym F of some quasicoherent sheaf F; equivalently, when Sym A₁ ≅ A (essImage_gradedSymmetricAlgebra_iff). These algebras form the full subcategory FreeGradedQuasicoherentAlgebra X of GradedQuasicoherentAlgebra X, the essential image of gradedSymmetricAlgebra X. Their relative spectra are the linear schemes Spec_X Sym F over X (Stacks Project, tag 01M1), whose morphisms preserve the grading.

Since the graded symmetric algebra functor is fully faithful and its degree-one component recovers F, it is an equivalence gradedSymmetricAlgebraEquiv X : QuasicoherentSheaf X ≌ FreeGradedQuasicoherentAlgebra X, whose inverse is the degree-one functor and whose unit is the identification F ≅ Sym¹ F, the inverse of gradedSymmetricAlgebraDegreeOneIso. A morphism of free graded algebras is therefore the same as a morphism of their degree-one components.

Main declarations #

source
@[reducible, inline]
abbrev TauCeti.AlgebraicGeometry.FreeGradedQuasicoherentAlgebra (X : AlgebraicGeometry.Scheme) :
Type (u + 1)

The category of graded quasicoherent algebras freely generated in degree one: the full subcategory of GradedQuasicoherentAlgebra X on the algebras isomorphic to the graded symmetric algebra Sym F of a quasicoherent sheaf F.

Instances For
    source
    noncomputable def TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraEquiv (X : AlgebraicGeometry.Scheme) :
    QuasicoherentSheaf X ≌ FreeGradedQuasicoherentAlgebra X

    The graded symmetric algebra functor is an equivalence between quasicoherent sheaves and graded quasicoherent algebras freely generated in degree one. Its inverse takes the degree-one component, and its unit is the identification F ≅ Sym¹ F.

    Instances For
      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraEquiv_functor (X : AlgebraicGeometry.Scheme) :
      (gradedSymmetricAlgebraEquiv X).functor = (gradedSymmetricAlgebra X).toEssImage

      The forward functor of gradedSymmetricAlgebraEquiv is the graded symmetric algebra, corestricted to its essential image.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraEquiv_inverse (X : AlgebraicGeometry.Scheme) :
      (gradedSymmetricAlgebraEquiv X).inverse = (gradedSymmetricAlgebra X).essImage.ι.comp GradedQuasicoherentAlgebra.degreeOne

      The inverse functor of gradedSymmetricAlgebraEquiv is the degree-one functor.

      source
      @[simp]
      theorem TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraEquiv_unitIso (X : AlgebraicGeometry.Scheme) :
      (gradedSymmetricAlgebraEquiv X).unitIso = (gradedSymmetricAlgebraDegreeOneIso X).symm

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

      source
      theorem TauCeti.AlgebraicGeometry.essImage_gradedSymmetricAlgebra_iff {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) :
      (gradedSymmetricAlgebra X).essImage A ↔ Nonempty ((gradedSymmetricAlgebra X).obj (GradedQuasicoherentAlgebra.degreeOne.obj A) ≅ A)

      A graded quasicoherent algebra is freely generated in degree one exactly when it is isomorphic, as a graded algebra, to the graded symmetric algebra of its degree-one component.