The symmetric algebra of a quasicoherent sheaf is free

For a quasicoherent sheaf F on a scheme X, the symmetric algebra Sym F = ⨁ₙ Symⁿ F is the direct-sum algebra of the graded symmetric algebra of F:

symmetricAlgebra X : QuasicoherentSheaf X ⥤ QuasicoherentAlgebra X.

Forgetting the grading, Sym F is the free commutative 𝒪_X-algebra on F: a morphism of 𝒪_X-modules φ : F ⟶ B into any commutative 𝒪_X-algebra B extends uniquely to a morphism of commutative 𝒪_X-algebras Sym F ⟶ B (symmetricAlgebraHomEquiv). The algebra B need not be quasicoherent; this is what makes the statement applicable to the algebras of regular functions q_* 𝒪_T of arbitrary schemes q : T ⟶ X, and so to the universal property of the relative spectrum Spec_X (Sym F) (Stacks Project, Tag 01M1).

The extension is built in each degree as for the graded universal property (TauCeti.AlgebraicGeometry.gradedSymmetricAlgebraAdjunction), with the ring of sections Γ(B, U) in place of the graded ring of sections of a graded algebra: over each open U the universal property of the symmetric algebra of the Γ(X, U)-module Γ(F, U) gives an algebra map Sym Γ(F, U) → Γ(B, U), whose degree-n parts are sheafified (TauCeti.SheafOfModules.symmetricPowerLift) and assembled over the summands of ⨁ₙ Symⁿ F. Uniqueness holds because Sym F is generated by its unit and by F in degree one.

Main declarations

• TauCeti.AlgebraicGeometry.symmetricAlgebra: the symmetric algebra of a quasicoherent sheaf, as a quasicoherent algebra;
• TauCeti.AlgebraicGeometry.symmetricAlgebraι: the inclusion F ⟶ Sym F of the summand of degree one, natural in F (symmetricAlgebraι_naturality);
• TauCeti.AlgebraicGeometry.symmetricAlgebra_hom_ext: algebra morphisms out of Sym F are determined on F, and TauCeti.AlgebraicGeometry.ιTotal_one_comp_eq_iff: morphisms out of Sym F agree on the summand Sym¹ F exactly when they agree on F;
• TauCeti.AlgebraicGeometry.symmetricAlgebraLift: the algebra morphism Sym F ⟶ B extending a module morphism F ⟶ B (symmetricAlgebraι_comp_lift), natural on both sides (symmetricAlgebraLift_comp, symmetricAlgebra_map_comp_lift);
• TauCeti.AlgebraicGeometry.symmetricAlgebraHomEquiv: the universal property (Sym F ⟶ B) ≃ (F ⟶ B);
• TauCeti.AlgebraicGeometry.symmetricAlgebraAdjunction: restricted to quasicoherent B, the universal property makes Sym left adjoint to the forgetful functor QuasicoherentAlgebra.forget X to quasicoherent sheaves, so Sym preserves colimits.

References

• The Stacks Project, Tag 01M1.

The universal property

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.symmetricAlgebra (X : AlgebraicGeometry.Scheme) : CategoryTheory.Functor (QuasicoherentSheaf X) (QuasicoherentAlgebra X)

The symmetric algebra Sym F = ⨁ₙ Symⁿ F of a quasicoherent sheaf F, as a quasicoherent commutative 𝒪_X-algebra: the direct-sum algebra of the graded symmetric algebra.

noncomputable def TauCeti.AlgebraicGeometry.symmetricAlgebraι {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) : F.obj ⟶ ((symmetricAlgebra X).obj F).obj.X

The inclusion F ≅ Sym¹ F ⟶ Sym F of a quasicoherent sheaf into its symmetric algebra, as the summand of degree one.

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraι_def {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) : symmetricAlgebraι F = CategoryTheory.CategoryStruct.comp ((gradedSymmetricAlgebraDegreeOneIso X).inv.app F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (((gradedSymmetricAlgebra X).obj F).ιTotal 1))

The inclusion F ⟶ Sym F is the identification F ≅ Sym¹ F of gradedSymmetricAlgebraDegreeOneIso followed by the inclusion of the summand of degree one.

theorem TauCeti.AlgebraicGeometry.ιTotal_one_comp_eq_iff {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {Z : X.Modules} {f g : ((symmetricAlgebra X).obj F).obj.X ⟶ Z} : CategoryTheory.CategoryStruct.comp (((gradedSymmetricAlgebra X).obj F).ιTotal 1) f = CategoryTheory.CategoryStruct.comp (((gradedSymmetricAlgebra X).obj F).ιTotal 1) g ↔ CategoryTheory.CategoryStruct.comp (symmetricAlgebraι F) f = CategoryTheory.CategoryStruct.comp (symmetricAlgebraι F) g

Morphisms out of the direct sum Sym F agree on its summand Sym¹ F exactly when they agree on F, through the identification of F with Sym¹ F.

theorem TauCeti.AlgebraicGeometry.symmetricAlgebra_hom_ext {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {B : CategoryTheory.CommMon X.Modules} {f g : ((symmetricAlgebra X).obj F).obj ⟶ B} (h : CategoryTheory.CategoryStruct.comp (symmetricAlgebraι F) f.hom.hom = CategoryTheory.CategoryStruct.comp (symmetricAlgebraι F) g.hom.hom) : f = g

The direct-sum algebra Sym F is generated by F: morphisms of commutative 𝒪_X-algebras out of it agree as soon as they agree on F.

noncomputable def TauCeti.AlgebraicGeometry.symmetricAlgebraLift {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {B : CategoryTheory.CommMon X.Modules} (φ : F.obj ⟶ B.X) : ((symmetricAlgebra X).obj F).obj ⟶ B

The morphism of commutative 𝒪_X-algebras Sym F ⟶ B extending a morphism of 𝒪_X-modules φ : F ⟶ B (symmetricAlgebraι_comp_lift). The target B need not be quasicoherent.

@[simp]

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraι_comp_lift {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {B : CategoryTheory.CommMon X.Modules} (φ : F.obj ⟶ B.X) : CategoryTheory.CategoryStruct.comp (symmetricAlgebraι F) (symmetricAlgebraLift φ).hom.hom = φ

The extension symmetricAlgebraLift φ restricts to φ on F.

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraι_comp_lift_assoc {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {B : CategoryTheory.CommMon X.Modules} (φ : F.obj ⟶ B.X) {Z : SheafOfModules X.ringCatSheaf} (h : B.toMon.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (symmetricAlgebraι F) (symmetricAlgebraLift φ).hom.hom) h = CategoryTheory.CategoryStruct.comp φ h

The extension symmetricAlgebraLift φ restricts to φ on F.

noncomputable def TauCeti.AlgebraicGeometry.symmetricAlgebraHomEquiv {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) (B : CategoryTheory.CommMon X.Modules) : (((symmetricAlgebra X).obj F).obj ⟶ B) ≃ (F.obj ⟶ B.X)

The universal property of the symmetric algebra: morphisms of commutative 𝒪_X-algebras Sym F ⟶ B correspond to morphisms of 𝒪_X-modules F ⟶ B, by restriction along symmetricAlgebraι and by symmetricAlgebraLift.

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraHomEquiv_apply {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {B : CategoryTheory.CommMon X.Modules} (f : ((symmetricAlgebra X).obj F).obj ⟶ B) : (symmetricAlgebraHomEquiv F B) f = CategoryTheory.CategoryStruct.comp (symmetricAlgebraι F) f.hom.hom

The bijection symmetricAlgebraHomEquiv restricts a morphism Sym F ⟶ B to F.

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraHomEquiv_symm_apply {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {B : CategoryTheory.CommMon X.Modules} (φ : F.obj ⟶ B.X) : (symmetricAlgebraHomEquiv F B).symm φ = symmetricAlgebraLift φ

The inverse bijection of symmetricAlgebraHomEquiv is symmetricAlgebraLift.

@[simp]

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraLift_comp {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {B B' : CategoryTheory.CommMon X.Modules} (φ : F.obj ⟶ B.X) (f : B ⟶ B') : CategoryTheory.CategoryStruct.comp (symmetricAlgebraLift φ) f = symmetricAlgebraLift (CategoryTheory.CategoryStruct.comp φ f.hom.hom)

Postcomposing symmetricAlgebraLift φ with a morphism of commutative 𝒪_X-algebras f extends φ followed by f.

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraLift_comp_assoc {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {B B' : CategoryTheory.CommMon X.Modules} (φ : F.obj ⟶ B.X) (f : B ⟶ B') {Z : CategoryTheory.CommMon X.Modules} (h : B' ⟶ Z) : CategoryTheory.CategoryStruct.comp (symmetricAlgebraLift φ) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (symmetricAlgebraLift (CategoryTheory.CategoryStruct.comp φ f.hom.hom)) h

Postcomposing symmetricAlgebraLift φ with a morphism of commutative 𝒪_X-algebras f extends φ followed by f.

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraι_naturality {X : AlgebraicGeometry.Scheme} {F F' : QuasicoherentSheaf X} (g : F' ⟶ F) : CategoryTheory.CategoryStruct.comp g.hom (symmetricAlgebraι F) = CategoryTheory.CategoryStruct.comp (symmetricAlgebraι F') ((symmetricAlgebra X).map g).hom.hom.hom

The inclusion F ⟶ Sym F is natural in F.

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraι_naturality_assoc {X : AlgebraicGeometry.Scheme} {F F' : QuasicoherentSheaf X} (g : F' ⟶ F) {Z : SheafOfModules X.ringCatSheaf} (h : (GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.obj ((gradedSymmetricAlgebra X).obj F)).obj.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g.hom (symmetricAlgebraι F)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (symmetricAlgebraι F') (GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.map ((gradedSymmetricAlgebra X).map g)).hom.hom.hom) h

The inclusion F ⟶ Sym F is natural in F.

@[simp]

theorem TauCeti.AlgebraicGeometry.symmetricAlgebra_map_comp_lift {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {B : CategoryTheory.CommMon X.Modules} {F' : QuasicoherentSheaf X} (g : F' ⟶ F) (φ : F.obj ⟶ B.X) : CategoryTheory.CategoryStruct.comp (GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.map ((gradedSymmetricAlgebra X).map g)).hom (symmetricAlgebraLift φ) = symmetricAlgebraLift (CategoryTheory.CategoryStruct.comp g.hom φ)

Precomposing symmetricAlgebraLift φ with the map Sym F' ⟶ Sym F induced by a morphism g : F' ⟶ F extends g ≫ φ. The left-hand side is stated with symmetricAlgebra X unfolded to the direct-sum algebra of the graded symmetric algebra, its simp-normal form.

theorem TauCeti.AlgebraicGeometry.symmetricAlgebra_map_comp_lift_assoc {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {B : CategoryTheory.CommMon X.Modules} {F' : QuasicoherentSheaf X} (g : F' ⟶ F) (φ : F.obj ⟶ B.X) {Z : CategoryTheory.CommMon X.Modules} (h : B ⟶ Z) : CategoryTheory.CategoryStruct.comp (GradedQuasicoherentAlgebra.toQuasicoherentAlgebra.map ((gradedSymmetricAlgebra X).map g)).hom (CategoryTheory.CategoryStruct.comp (symmetricAlgebraLift φ) h) = CategoryTheory.CategoryStruct.comp (symmetricAlgebraLift (CategoryTheory.CategoryStruct.comp g.hom φ)) h

Precomposing symmetricAlgebraLift φ with the map Sym F' ⟶ Sym F induced by a morphism g : F' ⟶ F extends g ≫ φ. The left-hand side is stated with symmetricAlgebra X unfolded to the direct-sum algebra of the graded symmetric algebra, its simp-normal form.

The free-forgetful adjunction

noncomputable def TauCeti.AlgebraicGeometry.symmetricAlgebraAdjunction (X : AlgebraicGeometry.Scheme) : symmetricAlgebra X ⊣ QuasicoherentAlgebra.forget X

The symmetric algebra is the free quasicoherent algebra: Sym is left adjoint to the forgetful functor from quasicoherent commutative 𝒪_X-algebras to quasicoherent sheaves. This packages the universal property symmetricAlgebraHomEquiv, restricted to quasicoherent algebras, and its naturality on both sides. In particular Sym preserves colimits: it sends coproducts of quasicoherent sheaves to coproducts, that is to tensor products, of quasicoherent algebras.

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraAdjunction_homEquiv_apply_hom {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {A : QuasicoherentAlgebra X} (f : (symmetricAlgebra X).obj F ⟶ A) : (((symmetricAlgebraAdjunction X).homEquiv F A) f).hom = CategoryTheory.CategoryStruct.comp (symmetricAlgebraι F) (CategoryTheory.CategoryStruct.comp f.hom.hom.hom A.forgetObjIso.inv)

The bijection of symmetricAlgebraAdjunction restricts an algebra morphism Sym F ⟶ A to F, followed by the identification QuasicoherentAlgebra.forgetObjIso of the underlying module of A.

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraAdjunction_homEquiv_symm_apply_hom {X : AlgebraicGeometry.Scheme} {F : QuasicoherentSheaf X} {A : QuasicoherentAlgebra X} (φ : F ⟶ (QuasicoherentAlgebra.forget X).obj A) : (((symmetricAlgebraAdjunction X).homEquiv F A).symm φ).hom = symmetricAlgebraLift (CategoryTheory.CategoryStruct.comp φ.hom A.forgetObjIso.hom)

The inverse bijection of symmetricAlgebraAdjunction extends a module morphism F ⟶ A, read through the identification QuasicoherentAlgebra.forgetObjIso, to the algebra morphism symmetricAlgebraLift.

@[simp]

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraAdjunction_unit_app_hom {X : AlgebraicGeometry.Scheme} (F : QuasicoherentSheaf X) : ((symmetricAlgebraAdjunction X).unit.app F).hom = CategoryTheory.CategoryStruct.comp (symmetricAlgebraι F) ((symmetricAlgebra X).obj F).forgetObjIso.inv

The unit of symmetricAlgebraAdjunction is the inclusion F ⟶ Sym F of the summand of degree one.

@[simp]

theorem TauCeti.AlgebraicGeometry.symmetricAlgebraAdjunction_counit_app_hom {X : AlgebraicGeometry.Scheme} (A : QuasicoherentAlgebra X) : ((symmetricAlgebraAdjunction X).counit.app A).hom = symmetricAlgebraLift A.forgetObjIso.hom

The counit of symmetricAlgebraAdjunction at a quasicoherent algebra A is the algebra morphism Sym A ⟶ A extending the identity of the underlying module of A.

instance TauCeti.AlgebraicGeometry.instIsLeftAdjointQuasicoherentSheafQuasicoherentAlgebraSymmetricAlgebra {X : AlgebraicGeometry.Scheme} : (symmetricAlgebra X).IsLeftAdjoint