Quasicoherence of symmetric powers

The symmetric powers of a quasicoherent module sheaf are quasicoherent, with no finiteness, flatness, or characteristic assumptions. Thus symmetric powers define endofunctors of the category of quasicoherent sheaves. These are the components of its graded symmetric algebra.

instance AlgebraicGeometry.Scheme.Modules.isQuasicoherent_symmetricPower {X : Scheme} (n : ℕ) (M : X.Modules) [SheafOfModules.IsQuasicoherent M] : ((SheafOfModules.symmetricPower X.sheaf n).obj M).IsQuasicoherent

Every symmetric power of a quasicoherent module sheaf on an arbitrary scheme is quasicoherent. No finite-generation, flatness, or characteristic assumption is needed.

instance TauCeti.AlgebraicGeometry.QuasicoherentSheaf.isQuasicoherent_symmetricPower_obj {X : AlgebraicGeometry.Scheme} (n : ℕ) (M : QuasicoherentSheaf X) : ((SheafOfModules.symmetricPower X.sheaf n).obj M.obj).IsQuasicoherent

The symmetric powers of the underlying module sheaf of a quasicoherent sheaf are quasicoherent. This restates Scheme.Modules.isQuasicoherent_symmetricPower for the underlying object of a quasicoherent sheaf, whose type SheafOfModules X.ringCatSheaf instance search does not identify with X.Modules.

noncomputable def TauCeti.AlgebraicGeometry.QuasicoherentSheaf.symmetricPower (X : AlgebraicGeometry.Scheme) (n : ℕ) : CategoryTheory.Functor (QuasicoherentSheaf X) (QuasicoherentSheaf X)

The symmetric-power endofunctor of quasicoherent sheaves on a scheme, inherited from the symmetric-power endofunctor of all module sheaves.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.symmetricPower_obj_obj (X : AlgebraicGeometry.Scheme) (n : ℕ) (M : QuasicoherentSheaf X) : ((symmetricPower X n).obj M).obj = (SheafOfModules.symmetricPower X.sheaf n).obj M.obj

The underlying module sheaf of a quasicoherent symmetric power.

@[simp]

theorem TauCeti.AlgebraicGeometry.QuasicoherentSheaf.symmetricPower_map_hom (X : AlgebraicGeometry.Scheme) (n : ℕ) {M N : QuasicoherentSheaf X} (φ : M ⟶ N) : ((symmetricPower X n).map φ).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPower X.sheaf n).map φ.hom) (CategoryTheory.eqToHom ⋯))

Symmetric power acts on morphisms by the underlying symmetric-power map. The equality transports identify the underlying objects of the lifted functor.