Symmetric powers of presheaves of modules

Let R be a presheaf of commutative rings on a category C. For a presheaf of R-modules M and n : ℕ, the n-th symmetric power of M is the presheaf of modules whose sections over X are the symmetric power (M.obj X).symmetricPower n (ModuleCat.symmetricPower, the degree-n part of the symmetric algebra of M.obj X), and whose restriction along f : X ⟶ Y sends a product m₁ ⋯ mₙ to M.map f m₁ ⋯ M.map f mₙ. The restriction maps are induced by the semilinear restriction maps of M through SymmetricAlgebra.mapₛₗ. This is the presheaf-level input to symmetric powers of sheaves of modules, which are obtained by sheafification. As for Mathlib's monoidal structure on these presheaves of modules (PresheafOfModulesOfCommRing.monoidalCategoryStruct), modules are taken in the universe of the rings.

Main declarations

• PresheafOfModulesOfCommRing.symmetricPower n is the n-th symmetric power, as an endofunctor of presheaves of R-modules; symmetricPower_obj_obj, coe_symmetricPower_obj_map_apply and symmetricPower_map_app compute its sections, restriction maps and action on morphisms;
• PresheafOfModulesOfCommRing.symmetricPowerZeroIso identifies the zeroth symmetric power with the constant functor at the unit presheaf of modules R;
• PresheafOfModulesOfCommRing.symmetricPowerOneIso identifies the first symmetric power with the identity functor.

noncomputable def PresheafOfModulesOfCommRing.symmetricPowerObjMap {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (n : ℕ) {X Y : Cᵒᵖ} (f : X ⟶ Y) : (M.obj X).symmetricPower n ⟶ (ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).obj ((M.obj Y).symmetricPower n)

Auxiliary definition for symmetricPower: the restriction maps of the symmetric power of a presheaf of modules, induced on degree-n parts of symmetric algebras by the semilinear restriction map of the presheaf.

Equations

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

theorem PresheafOfModulesOfCommRing.coe_symmetricPowerObjMap_apply {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (n : ℕ) {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : ↑((M.obj X).symmetricPower n)) : ↑((CategoryTheory.ConcreteCategory.hom (M.symmetricPowerObjMap n f)) x) = (SymmetricAlgebra.mapₛₗ ((ModuleCat.semilinearMapAddEquiv (CommRingCat.Hom.hom (R.map f)) (M.obj X) (M.obj Y)).symm (M.map f))) ↑x

The restriction maps of the symmetric power are computed in the symmetric algebra by the ring homomorphism induced by the restriction map of the presheaf.

noncomputable def PresheafOfModulesOfCommRing.symmetricPowerObj {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (n : ℕ) : PresheafOfModulesOfCommRing R

Auxiliary definition for symmetricPower: the symmetric power of a presheaf of modules.

Equations

• M.symmetricPowerObj n = PresheafOfModulesOfCommRing.mk (fun (X : Cᵒᵖ) => (M.obj X).symmetricPower n) (fun {X Y : Cᵒᵖ} (f : X ⟶ Y) => M.symmetricPowerObjMap n f) ⋯ ⋯

theorem PresheafOfModulesOfCommRing.symmetricPowerObjMap_naturality {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M N : PresheafOfModulesOfCommRing R} (φ : M ⟶ N) (n : ℕ) {X Y : Cᵒᵖ} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (M.symmetricPowerObjMap n f) ((ModuleCat.restrictScalars (CommRingCat.Hom.hom (R.map f))).map (ModuleCat.symmetricPower.map (PresheafOfModules.Hom.app' φ Y) n)) = CategoryTheory.CategoryStruct.comp (ModuleCat.symmetricPower.map (PresheafOfModules.Hom.app' φ X) n) (N.symmetricPowerObjMap n f)

The restriction maps of the symmetric power are natural in the presheaf of modules.

noncomputable def PresheafOfModulesOfCommRing.symmetricPower {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (n : ℕ) : CategoryTheory.Functor (PresheafOfModulesOfCommRing R) (PresheafOfModulesOfCommRing R)

The n-th symmetric power of presheaves of modules over a presheaf of commutative rings, computed sectionwise: its sections over X are (M.obj X).symmetricPower n, and its restriction maps send a product m₁ ⋯ mₙ to the product of the restrictions of the mᵢ.

Equations

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

theorem PresheafOfModulesOfCommRing.symmetricPower_obj_obj {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (n : ℕ) (M : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : ((symmetricPower n).obj M).obj X = (M.obj X).symmetricPower n

The sections of the symmetric power over X are the symmetric power of the sections.

@[simp]

theorem PresheafOfModulesOfCommRing.coe_symmetricPower_obj_map_apply {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (n : ℕ) (M : PresheafOfModulesOfCommRing R) {X Y : Cᵒᵖ} (f : X ⟶ Y) (x : ↑((M.obj X).symmetricPower n)) : ↑((CategoryTheory.ConcreteCategory.hom (((symmetricPower n).obj M).map f)) x) = (SymmetricAlgebra.mapₛₗ ((ModuleCat.semilinearMapAddEquiv (CommRingCat.Hom.hom (R.map f)) (M.obj X) (M.obj Y)).symm (M.map f))) ↑x

The restriction maps of the symmetric power are computed in the symmetric algebra by the ring homomorphism induced by the restriction map of the presheaf, which sends the generator of m to the generator of its restriction (SymmetricAlgebra.mapₛₗ_ι).

@[simp]

theorem PresheafOfModulesOfCommRing.symmetricPower_map_app {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (n : ℕ) {M N : PresheafOfModulesOfCommRing R} (φ : M ⟶ N) (X : Cᵒᵖ) : ((symmetricPower n).map φ).app X = ModuleCat.symmetricPower.map (PresheafOfModules.Hom.app' φ X) n

The symmetric power of a morphism is computed sectionwise.

noncomputable def PresheafOfModulesOfCommRing.symmetricPowerZeroIso {C : Type v} [CategoryTheory.Category.{w, v} C] (R : CategoryTheory.Functor Cᵒᵖ CommRingCat) : symmetricPower 0 ≅ (CategoryTheory.Functor.const (PresheafOfModulesOfCommRing R)).obj (unit R)

The zeroth symmetric power of a presheaf of R-modules is the unit presheaf of modules R, naturally; on sections it is ModuleCat.symmetricPower.iso₀.

Equations

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

@[simp]

theorem PresheafOfModulesOfCommRing.symmetricPowerZeroIso_hom_app_app {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : ((symmetricPowerZeroIso R).hom.app M).app X = (ModuleCat.symmetricPower.iso₀ (M.obj X)).hom

@[simp]

theorem PresheafOfModulesOfCommRing.symmetricPowerZeroIso_inv_app_app {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : ((symmetricPowerZeroIso R).inv.app M).app X = (ModuleCat.symmetricPower.iso₀ (M.obj X)).inv

noncomputable def PresheafOfModulesOfCommRing.symmetricPowerOneIso {C : Type v} [CategoryTheory.Category.{w, v} C] (R : CategoryTheory.Functor Cᵒᵖ CommRingCat) : symmetricPower 1 ≅ CategoryTheory.Functor.id (PresheafOfModulesOfCommRing R)

The first symmetric power of a presheaf of R-modules is the presheaf of modules itself, naturally; on sections it is ModuleCat.symmetricPower.iso₁.

Equations

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

@[simp]

theorem PresheafOfModulesOfCommRing.symmetricPowerOneIso_hom_app_app {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : ((symmetricPowerOneIso R).hom.app M).app X = (ModuleCat.symmetricPower.iso₁ (M.obj X)).hom

@[simp]

theorem PresheafOfModulesOfCommRing.symmetricPowerOneIso_inv_app_app {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (X : Cᵒᵖ) : ((symmetricPowerOneIso R).inv.app M).app X = (ModuleCat.symmetricPower.iso₁ (M.obj X)).inv