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;
• TauCeti.SheafOfModules.symmetricPower_hom_ext checks equality of maps out of a symmetric power on the sheafifications of sectionwise symmetric tensors;
• TauCeti.SheafOfModules.symmetricPowerLift sheafifies a sectionwise map out of a symmetric power, compatibly with symmetricPowerZeroIso and symmetricPowerOneIso;
• SheafOfModules.symmetricPowerZeroIso identifies Sym⁰ M with the structure sheaf, with components computed by symmetricPowerZeroIso_hom_app and symmetricPowerZeroIso_inv_app;
• SheafOfModules.symmetricPowerOneIso identifies Sym¹ M with M;
• SheafOfModules.overSymmetricPowerIso identifies the restriction of Symⁿ M to a slice site with the symmetric power of the restriction of 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.

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.

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.

@[simp]

theorem SheafOfModules.symmetricPower_map_val_app_unit {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) (X : Cᵒᵖ) (x : ↑((PresheafOfModulesOfCommRing.obj M.val X).symmetricPower n)) : (CategoryTheory.ConcreteCategory.hom (((symmetricPower R n).map φ).val.app X)) ((CategoryTheory.ConcreteCategory.hom ((symmetricPowerIso n M).inv.val.app X)) ((CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).unit.app ((PresheafOfModulesOfCommRing.symmetricPower n).obj M.val)).app X)) x)) = (CategoryTheory.ConcreteCategory.hom ((symmetricPowerIso n N).inv.val.app X)) ((CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).unit.app ((PresheafOfModulesOfCommRing.symmetricPower n).obj N.val)).app X)) ((CategoryTheory.ConcreteCategory.hom (ModuleCat.symmetricPower.map (PresheafOfModules.Hom.app' φ.val X) n)) x))

On sections over X, the symmetric power of a morphism φ sends the sheafification of a sectionwise symmetric tensor x to the sheafification of its image under Symⁿ (φ_X).

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.

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.

@[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.symmetricPowerZeroIso_inv_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).inv.app M = CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) (unit (TauCeti.SheafOfModules.ringCatSheaf R))).inv (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map ((PresheafOfModulesOfCommRing.symmetricPowerZeroIso R.obj).inv.app M.val)) (symmetricPowerIso 0 M).inv)

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

theorem SheafOfModules.symmetricPowerZeroIso_inv_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 : (symmetricPower R 0).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp ((symmetricPowerZeroIso R).inv.app M) h = CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) (unit (TauCeti.SheafOfModules.ringCatSheaf R))).inv (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map ((PresheafOfModulesOfCommRing.symmetricPowerZeroIso R.obj).inv.app M.val)) (CategoryTheory.CategoryStruct.comp (symmetricPowerIso 0 M).inv h))

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

@[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.

noncomputable def SheafOfModules.presheafPushforwardSymmetricPowerIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} [K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] (F : CategoryTheory.Functor D C) [F.IsContinuous K J] (n : ℕ) : (PresheafOfModulesOfCommRing.symmetricPower n).comp (PresheafOfModules.pushforward (TauCeti.SheafOfModules.pushforwardRingIso F (TauCeti.SheafOfModules.ringCatSheaf R)).inv) ≅ (PresheafOfModules.pushforward (TauCeti.SheafOfModules.pushforwardRingIso F (TauCeti.SheafOfModules.ringCatSheaf R)).inv).comp (PresheafOfModulesOfCommRing.symmetricPower n)

Symmetric powers of presheaves of modules commute with pushforward of the underlying presheaves.

@[simp]

theorem SheafOfModules.presheafPushforwardSymmetricPowerIso_hom_app_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} [K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] (F : CategoryTheory.Functor D C) [F.IsContinuous K J] (n : ℕ) (M : PresheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R).obj) (X : Dᵒᵖ) : ((presheafPushforwardSymmetricPowerIso F n).hom.app M).app X = CategoryTheory.CategoryStruct.id ((((PresheafOfModulesOfCommRing.symmetricPower n).comp (PresheafOfModules.pushforward (TauCeti.SheafOfModules.pushforwardRingIso F (TauCeti.SheafOfModules.ringCatSheaf R)).inv)).obj M).obj X)

On sections, presheafPushforwardSymmetricPowerIso is the identity.

@[simp]

theorem SheafOfModules.presheafPushforwardSymmetricPowerIso_inv_app_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {R : CategoryTheory.Sheaf J CommRingCat} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} [K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] (F : CategoryTheory.Functor D C) [F.IsContinuous K J] (n : ℕ) (M : PresheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R).obj) (X : Dᵒᵖ) : ((presheafPushforwardSymmetricPowerIso F n).inv.app M).app X = CategoryTheory.CategoryStruct.id ((((PresheafOfModules.pushforward (TauCeti.SheafOfModules.pushforwardRingIso F (TauCeti.SheafOfModules.ringCatSheaf R)).inv).comp (PresheafOfModulesOfCommRing.symmetricPower n)).obj M).obj X)

On sections, the inverse of presheafPushforwardSymmetricPowerIso is the identity.

noncomputable def SheafOfModules.pushforwardSymmetricPowerIso {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} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} [K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor D C) [F.IsContinuous K J] [F.IsCocontinuous K J] (n : ℕ) (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) : (TauCeti.SheafOfModules.pushforwardModule F R).obj ((symmetricPower R n).obj M) ≅ (symmetricPower (TauCeti.SheafOfModules.pushforwardCommRing F R) n).obj ((TauCeti.SheafOfModules.pushforwardModule F R).obj M)

Pushforward along a continuous and cocontinuous functor commutes with symmetric powers of sheaves of modules.

@[simp]

theorem SheafOfModules.pushforwardSymmetricPowerIso_hom {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} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} [K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor D C) [F.IsContinuous K J] [F.IsCocontinuous K J] (n : ℕ) (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) : (pushforwardSymmetricPowerIso F n M).hom = CategoryTheory.CategoryStruct.comp ((TauCeti.SheafOfModules.pushforwardModule F R).map (symmetricPowerIso n M).hom) (CategoryTheory.CategoryStruct.comp (TauCeti.SheafOfModules.pushforwardSheafificationIso F (TauCeti.SheafOfModules.ringCatSheaf R) ((PresheafOfModulesOfCommRing.symmetricPower n).obj M.val)).hom (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf (TauCeti.SheafOfModules.pushforwardCommRing F R)).obj)).map ((presheafPushforwardSymmetricPowerIso F n).hom.app M.val)) (symmetricPowerIso n ((TauCeti.SheafOfModules.pushforwardModule F R).obj M)).inv))

The forward map of pushforwardSymmetricPowerIso is the sheafification--pushforward comparison followed by the sheafified sectionwise comparison.

theorem SheafOfModules.pushforwardSymmetricPowerIso_hom_naturality {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} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} [K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor D C) [F.IsContinuous K J] [F.IsCocontinuous K J] (n : ℕ) {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp ((TauCeti.SheafOfModules.pushforwardModule F R).map ((symmetricPower R n).map φ)) (pushforwardSymmetricPowerIso F n N).hom = CategoryTheory.CategoryStruct.comp (pushforwardSymmetricPowerIso F n M).hom ((symmetricPower (TauCeti.SheafOfModules.pushforwardCommRing F R) n).map ((TauCeti.SheafOfModules.pushforwardModule F R).map φ))

pushforwardSymmetricPowerIso is natural in the sheaf of modules.

theorem SheafOfModules.pushforwardSymmetricPowerIso_hom_naturality_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} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} [K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] (F : CategoryTheory.Functor D C) [F.IsContinuous K J] [F.IsCocontinuous K J] (n : ℕ) {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (φ : M ⟶ N) {Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf (TauCeti.SheafOfModules.pushforwardCommRing F R))} (h : (symmetricPower (TauCeti.SheafOfModules.pushforwardCommRing F R) n).obj ((TauCeti.SheafOfModules.pushforwardModule F R).obj N) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((TauCeti.SheafOfModules.pushforwardModule F R).map ((symmetricPower R n).map φ)) (CategoryTheory.CategoryStruct.comp (pushforwardSymmetricPowerIso F n N).hom h) = CategoryTheory.CategoryStruct.comp (pushforwardSymmetricPowerIso F n M).hom (CategoryTheory.CategoryStruct.comp ((symmetricPower (TauCeti.SheafOfModules.pushforwardCommRing F R) n).map ((TauCeti.SheafOfModules.pushforwardModule F R).map φ)) h)

pushforwardSymmetricPowerIso is natural in the sheaf of modules.

noncomputable def SheafOfModules.overSymmetricPowerIso {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)) (X : C) [(J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [(J.over X).WEqualsLocallyBijective AddCommGrpCat] : ((symmetricPower R n).obj M).over X ≅ (symmetricPower (R.over X) n).obj (M.over X)

The restriction of a symmetric power to a slice site is the symmetric power of the restriction.

@[simp]

theorem SheafOfModules.overSymmetricPowerIso_hom {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)) (X : C) [(J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [(J.over X).WEqualsLocallyBijective AddCommGrpCat] : (overSymmetricPowerIso n M X).hom = (pushforwardSymmetricPowerIso (CategoryTheory.Over.forget X) n M).hom

The forward map of overSymmetricPowerIso is the slice-site pushforward comparison.

theorem SheafOfModules.overSymmetricPowerIso_hom_naturality {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) (X : C) [(J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [(J.over X).WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.CategoryStruct.comp (Hom.over ((symmetricPower R n).map φ) X) (overSymmetricPowerIso n N X).hom = CategoryTheory.CategoryStruct.comp (overSymmetricPowerIso n M X).hom ((symmetricPower (R.over X) n).map (Hom.over φ X))

overSymmetricPowerIso is natural in the sheaf of modules.

theorem SheafOfModules.overSymmetricPowerIso_hom_naturality_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} (n : ℕ) {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (φ : M ⟶ N) (X : C) [(J.over X).HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [(J.over X).WEqualsLocallyBijective AddCommGrpCat] {Z : SheafOfModules ((TauCeti.SheafOfModules.ringCatSheaf R).over X)} (h : (symmetricPower (R.over X) n).obj (N.over X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (Hom.over ((symmetricPower R n).map φ) X) (overSymmetricPowerIso n N X).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (overSymmetricPowerIso n M X).hom ((symmetricPower (R.over X) n).map (Hom.over φ X))) h

overSymmetricPowerIso is natural in the sheaf of modules.

theorem TauCeti.SheafOfModules.symmetricPower_hom_ext {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 (ringCatSheaf R)) {N : SheafOfModules (ringCatSheaf R)} {f g : (SheafOfModules.symmetricPower R n).obj M ⟶ N} (h : ∀ (U : Cᵒᵖ) (x : ↑((PresheafOfModulesOfCommRing.obj M.val U).symmetricPower n)), (CategoryTheory.ConcreteCategory.hom (f.val.app U)) ((CategoryTheory.ConcreteCategory.hom ((SheafOfModules.symmetricPowerIso n M).inv.val.app U)) ((CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app ((PresheafOfModulesOfCommRing.symmetricPower n).obj M.val)).app U)) x)) = (CategoryTheory.ConcreteCategory.hom (g.val.app U)) ((CategoryTheory.ConcreteCategory.hom ((SheafOfModules.symmetricPowerIso n M).inv.val.app U)) ((CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app ((PresheafOfModulesOfCommRing.symmetricPower n).obj M.val)).app U)) x))) : f = g

Maps from a sheaf symmetric power are determined by their values on the sheafifications of sectionwise symmetric tensors.

noncomputable def TauCeti.SheafOfModules.symmetricPowerLift {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 B : SheafOfModules (ringCatSheaf R)} (ψ : (PresheafOfModulesOfCommRing.symmetricPower n).obj M.val ⟶ B.val) : (SheafOfModules.symmetricPower R n).obj M ⟶ B

The transpose along sheafification of a sectionwise map ψ : Symⁿ M.val ⟶ B.val out of the presheaf symmetric power of M: a morphism Symⁿ M ⟶ B of sheaves of modules, as CategoryTheory.sheafifyLift does for presheaves.

theorem TauCeti.SheafOfModules.symmetricPowerLift_def {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 B : SheafOfModules (ringCatSheaf R)} (ψ : (PresheafOfModulesOfCommRing.symmetricPower n).obj M.val ⟶ B.val) : symmetricPowerLift ψ = CategoryTheory.CategoryStruct.comp (SheafOfModules.symmetricPowerIso n M).hom (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).map ψ) (sheafificationIso (ringCatSheaf R) B).hom)

The defining equation of symmetricPowerLift.

theorem TauCeti.SheafOfModules.symmetricPowerZeroIso_inv_app_comp_symmetricPowerLift {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 B : SheafOfModules (ringCatSheaf R)} {ψ : (PresheafOfModulesOfCommRing.symmetricPower 0).obj M.val ⟶ B.val} {one : SheafOfModules.unit (ringCatSheaf R) ⟶ B} (h : CategoryTheory.CategoryStruct.comp ((PresheafOfModulesOfCommRing.symmetricPowerZeroIso R.obj).inv.app M.val) ψ = one.val) : CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPowerZeroIso R).inv.app M) (symmetricPowerLift ψ) = one

A sectionwise map out of Sym⁰ M.val restricting to one along R ≅ Sym⁰ M.val lifts to a map out of Sym⁰ M restricting to one along R ≅ Sym⁰ M.

theorem TauCeti.SheafOfModules.symmetricPowerOneIso_inv_app_comp_symmetricPowerLift {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 B : SheafOfModules (ringCatSheaf R)} {ψ : (PresheafOfModulesOfCommRing.symmetricPower 1).obj M.val ⟶ B.val} {φ : M ⟶ B} (h : CategoryTheory.CategoryStruct.comp ((PresheafOfModulesOfCommRing.symmetricPowerOneIso R.obj).inv.app M.val) ψ = φ.val) : CategoryTheory.CategoryStruct.comp ((SheafOfModules.symmetricPowerOneIso R).inv.app M) (symmetricPowerLift ψ) = φ

A sectionwise map out of Sym¹ M.val restricting to φ.val along M.val ≅ Sym¹ M.val lifts to a map out of Sym¹ M restricting to φ along M ≅ Sym¹ M.