Symmetric powers of sheaves of modules

Given a site (C, J) carrying a sheaf of commutative rings R and n : ℕ, the n-th symmetric power of a sheaf of R-modules M is obtained by taking sectionwise symmetric powers Sym^n_{R(U)} M(U) (PresheafOfModulesOfCommRing.symmetricPower, the degree-n parts of the sectionwise symmetric algebras) and sheafifying, exactly as the tensor product TauCeti.SheafOfModules.tensorProduct sheafifies sectionwise tensor products and SheafOfModules.exteriorPower sheafifies sectionwise exterior powers. On a scheme X this gives SheafOfModules.symmetricPower X.sheaf n : X.Modules ⥤ X.Modules, the symmetric powers of 𝒪ₓ-modules. They are the graded pieces of the symmetric algebra Sym(F) = ⨁ₙ Symⁿ(F) of an 𝒪ₓ-module F, whose relative spectrum is the linear scheme of a quasi-coherent F.

Main declarations

• SheafOfModules.symmetricPower R n is the n-th symmetric power, as an endofunctor of sheaves of R-modules;
• SheafOfModules.symmetricPowerIso and SheafOfModules.symmetricPower_map are its defining identification with the sheafification of the sectionwise symmetric power;
• SheafOfModules.symmetricPowerZeroIso identifies Sym⁰ M with the structure sheaf;
• SheafOfModules.symmetricPowerOneIso identifies Sym¹ M with M.

noncomputable def SheafOfModules.symmetricPower {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) (n : ℕ) : CategoryTheory.Functor (SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))

The n-th symmetric power of sheaves of R-modules: the sectionwise symmetric power of the underlying presheaf of modules, sheafified.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SheafOfModules.symmetricPowerIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (n : ℕ) (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) : (symmetricPower R n).obj M ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).obj ((PresheafOfModulesOfCommRing.symmetricPower n).obj M.val)

The defining identification of the symmetric power of a sheaf of modules with the sheafification of the sectionwise symmetric power of its underlying presheaf of modules.

Equations

• SheafOfModules.symmetricPowerIso n M = CategoryTheory.Iso.refl ((SheafOfModules.symmetricPower R n).obj M)

theorem SheafOfModules.symmetricPower_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (n : ℕ) {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (φ : M ⟶ N) : (symmetricPower R n).map φ = CategoryTheory.CategoryStruct.comp (symmetricPowerIso n M).hom (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map ((PresheafOfModulesOfCommRing.symmetricPower n).map φ.val)) (symmetricPowerIso n N).inv)

The symmetric power of a morphism of sheaves of modules is the sheafification of the sectionwise symmetric power of the underlying morphism of presheaves of modules.

noncomputable def SheafOfModules.symmetricPowerZeroIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) : symmetricPower R 0 ≅ (CategoryTheory.Functor.const (SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))).obj (unit (TauCeti.SheafOfModules.ringCatSheaf R))

The zeroth symmetric power of a sheaf of modules is the structure sheaf, naturally: the sheafification of the presheaf-level identification PresheafOfModulesOfCommRing.symmetricPowerZeroIso, followed by the identification of the sheafified unit with the structure sheaf.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SheafOfModules.symmetricPowerOneIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) : symmetricPower R 1 ≅ CategoryTheory.Functor.id (SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))

The first symmetric power of a sheaf of modules is the sheaf itself, naturally: the sheafification of the presheaf-level identification PresheafOfModulesOfCommRing.symmetricPowerOneIso, followed by the counit TauCeti.SheafOfModules.sheafificationIso.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SheafOfModules.symmetricPowerZeroIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) : (symmetricPowerZeroIso R).hom.app M = CategoryTheory.CategoryStruct.comp (symmetricPowerIso 0 M).hom (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map ((PresheafOfModulesOfCommRing.symmetricPowerZeroIso R.obj).hom.app M.val)) (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) (unit (TauCeti.SheafOfModules.ringCatSheaf R))).hom)

On components, symmetricPowerZeroIso is the sheafification of the presheaf-level identification PresheafOfModulesOfCommRing.symmetricPowerZeroIso, followed by the identification of the sheafified unit with the structure sheaf.

theorem SheafOfModules.symmetricPowerZeroIso_hom_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) {Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (h : ((CategoryTheory.Functor.const (SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R))).obj (unit (TauCeti.SheafOfModules.ringCatSheaf R))).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp ((symmetricPowerZeroIso R).hom.app M) h = CategoryTheory.CategoryStruct.comp (symmetricPowerIso 0 M).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map ((PresheafOfModulesOfCommRing.symmetricPowerZeroIso R.obj).hom.app M.val)) (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) (unit (TauCeti.SheafOfModules.ringCatSheaf R))).hom) h)

On components, symmetricPowerZeroIso is the sheafification of the presheaf-level identification PresheafOfModulesOfCommRing.symmetricPowerZeroIso, followed by the identification of the sheafified unit with the structure sheaf.

@[simp]

theorem SheafOfModules.symmetricPowerOneIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) : (symmetricPowerOneIso R).hom.app M = CategoryTheory.CategoryStruct.comp (symmetricPowerIso 1 M).hom (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map ((PresheafOfModulesOfCommRing.symmetricPowerOneIso R.obj).hom.app M.val)) (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) M).hom)

On components, symmetricPowerOneIso is the sheafification of the presheaf-level identification PresheafOfModulesOfCommRing.symmetricPowerOneIso, followed by the counit TauCeti.SheafOfModules.sheafificationIso.

theorem SheafOfModules.symmetricPowerOneIso_hom_app_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) {Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp ((symmetricPowerOneIso R).hom.app M) h = CategoryTheory.CategoryStruct.comp (symmetricPowerIso 1 M).hom (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map ((PresheafOfModulesOfCommRing.symmetricPowerOneIso R.obj).hom.app M.val)) (CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) M).hom h))

On components, symmetricPowerOneIso is the sheafification of the presheaf-level identification PresheafOfModulesOfCommRing.symmetricPowerOneIso, followed by the counit TauCeti.SheafOfModules.sheafificationIso.