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;
• PresheafOfModulesOfCommRing.symmetricPowerMul is the multiplication Symⁱ M ⊗ Symʲ M ⟶ Symⁱ⁺ʲ M, computed sectionwise by ModuleCat.symmetricPower.mul; with the unit R ⟶ Sym⁰ M given by symmetricPowerZeroIso it satisfies the graded associativity, commutativity and unit laws symmetricPowerMul_assoc, symmetricPowerMul_comm, symmetricPowerMul_one_mul and symmetricPowerMul_mul_one, and it is an epimorphism (PresheafOfModulesOfCommRing.epi_symmetricPowerMul).

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.

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.

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ᵢ.

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₀.

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

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

noncomputable def PresheafOfModulesOfCommRing.symmetricPowerMul {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (i j : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((symmetricPower i).obj M) ((symmetricPower j).obj M) ⟶ (symmetricPower (i + j)).obj M

The multiplication Symⁱ M ⊗ Symʲ M ⟶ Symⁱ⁺ʲ M of symmetric powers of a presheaf of modules, given on sections over X by the product in the symmetric algebra of M.obj X.

@[simp]

theorem PresheafOfModulesOfCommRing.symmetricPowerMul_app {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (i j : ℕ) (X : Cᵒᵖ) : (M.symmetricPowerMul i j).app X = ModuleCat.symmetricPower.mul (M.obj X) i j

The multiplication of symmetric powers is computed sectionwise.

instance PresheafOfModulesOfCommRing.epi_symmetricPowerMul {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (i j : ℕ) : CategoryTheory.Epi (M.symmetricPowerMul i j)

The multiplication of symmetric powers of a presheaf of modules is an epimorphism, since it is surjective on sections (ModuleCat.symmetricPower.mul_surjective).

theorem PresheafOfModulesOfCommRing.symmetricPowerMul_naturality {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M N : PresheafOfModulesOfCommRing R} (φ : M ⟶ N) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((symmetricPower i).map φ) ((symmetricPower j).map φ)) (N.symmetricPowerMul i j) = CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i j) ((symmetricPower (i + j)).map φ)

The multiplication of symmetric powers is natural in the presheaf of modules.

theorem PresheafOfModulesOfCommRing.symmetricPowerMul_naturality_assoc {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} {M N : PresheafOfModulesOfCommRing R} (φ : M ⟶ N) (i j : ℕ) {Z : PresheafOfModulesOfCommRing R} (h : (symmetricPower (i + j)).obj N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((symmetricPower i).map φ) ((symmetricPower j).map φ)) (CategoryTheory.CategoryStruct.comp (N.symmetricPowerMul i j) h) = CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i j) (CategoryTheory.CategoryStruct.comp ((symmetricPower (i + j)).map φ) h)

The multiplication of symmetric powers is natural in the presheaf of modules.

theorem PresheafOfModulesOfCommRing.symmetricPowerMul_assoc {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (i j k : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (M.symmetricPowerMul i j) ((symmetricPower k).obj M)) (M.symmetricPowerMul (i + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((symmetricPower i).obj M) ((symmetricPower j).obj M) ((symmetricPower k).obj M)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((symmetricPower i).obj M) (M.symmetricPowerMul j k)) (CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i (j + k)) (CategoryTheory.eqToHom ⋯)))

The multiplication of symmetric powers of a presheaf of modules is associative, up to the identification of the degrees i + (j + k) and i + j + k.

theorem PresheafOfModulesOfCommRing.symmetricPowerMul_assoc_assoc {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (i j k : ℕ) {Z : PresheafOfModulesOfCommRing R} (h : (symmetricPower (i + j + k)).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (M.symmetricPowerMul i j) ((symmetricPower k).obj M)) (CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul (i + j) k) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((symmetricPower i).obj M) ((symmetricPower j).obj M) ((symmetricPower k).obj M)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((symmetricPower i).obj M) (M.symmetricPowerMul j k)) (CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i (j + k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)))

The multiplication of symmetric powers of a presheaf of modules is associative, up to the identification of the degrees i + (j + k) and i + j + k.

theorem PresheafOfModulesOfCommRing.symmetricPowerMul_comm {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (β_ ((symmetricPower i).obj M) ((symmetricPower j).obj M)).hom (M.symmetricPowerMul j i) = CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i j) (CategoryTheory.eqToHom ⋯)

The multiplication of symmetric powers of a presheaf of modules is commutative, up to the identification of the degrees i + j and j + i.

theorem PresheafOfModulesOfCommRing.symmetricPowerMul_comm_assoc {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (i j : ℕ) {Z : PresheafOfModulesOfCommRing R} (h : (symmetricPower (j + i)).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (β_ ((symmetricPower i).obj M) ((symmetricPower j).obj M)).hom (CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul j i) h) = CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

The multiplication of symmetric powers of a presheaf of modules is commutative, up to the identification of the degrees i + j and j + i.

theorem PresheafOfModulesOfCommRing.symmetricPowerMul_one_mul {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((symmetricPowerZeroIso R).inv.app M) ((symmetricPower n).obj M)) (M.symmetricPowerMul 0 n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor ((symmetricPower n).obj M)).hom (CategoryTheory.eqToHom ⋯)

The unit R ⟶ Sym⁰ M is a left identity for the multiplication of symmetric powers, up to the identification of the degrees 0 + n and n.

theorem PresheafOfModulesOfCommRing.symmetricPowerMul_one_mul_assoc {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (n : ℕ) {Z : PresheafOfModulesOfCommRing R} (h : (symmetricPower (0 + n)).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((symmetricPowerZeroIso R).inv.app M) ((symmetricPower n).obj M)) (CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul 0 n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor ((symmetricPower n).obj M)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

The unit R ⟶ Sym⁰ M is a left identity for the multiplication of symmetric powers, up to the identification of the degrees 0 + n and n.

theorem PresheafOfModulesOfCommRing.symmetricPowerMul_mul_one {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((symmetricPower n).obj M) ((symmetricPowerZeroIso R).inv.app M)) (M.symmetricPowerMul n 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor ((symmetricPower n).obj M)).hom (CategoryTheory.eqToHom ⋯)

The unit R ⟶ Sym⁰ M is a right identity for the multiplication of symmetric powers, up to the identification of the degrees n + 0 and n.

theorem PresheafOfModulesOfCommRing.symmetricPowerMul_mul_one_assoc {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (M : PresheafOfModulesOfCommRing R) (n : ℕ) {Z : PresheafOfModulesOfCommRing R} (h : (symmetricPower (n + 0)).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((symmetricPower n).obj M) ((symmetricPowerZeroIso R).inv.app M)) (CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul n 0) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor ((symmetricPower n).obj M)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

The unit R ⟶ Sym⁰ M is a right identity for the multiplication of symmetric powers, up to the identification of the degrees n + 0 and n.