Evaluation of presheaves of modules is monoidal

Let R be a presheaf of commutative rings on a category C and X an object of Cᵒᵖ. The tensor product of presheaves of R-modules is computed sectionwise, so evaluation at X, valued in modules over the commutative ring R.obj X, is a strong monoidal functor whose unit and tensor comparisons are identities. The braiding is computed sectionwise as well, so evaluation is braided.

Composed with the lax monoidal inclusion of sheaves of modules into presheaves of modules, this makes taking sections over an object lax monoidal; over a terminal object this is the global sections functor.

Main declarations

• TauCeti.PresheafOfModulesOfCommRing.evaluation: evaluation at X, as a functor to ModuleCat (R.obj X);
• TauCeti.PresheafOfModulesOfCommRing.evaluationMonoidal: its monoidal structure;
• TauCeti.PresheafOfModulesOfCommRing.evaluationBraided: evaluation preserves the braiding.

@[reducible, inline]

abbrev TauCeti.PresheafOfModulesOfCommRing.evaluation {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (X : Cᵒᵖ) : CategoryTheory.Functor (PresheafOfModulesOfCommRing R) (ModuleCat ↑(R.obj X))

Evaluation at X of presheaves of modules over a presheaf of commutative rings, valued in modules over the commutative ring R.obj X. This is PresheafOfModules.evaluation, with its target written as ModuleCat (R.obj X) so that the monoidal structure of that category applies.

Equations

• TauCeti.PresheafOfModulesOfCommRing.evaluation X = PresheafOfModules.evaluation (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)) X

@[instance_reducible]

noncomputable instance TauCeti.PresheafOfModulesOfCommRing.evaluationMonoidal {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (X : Cᵒᵖ) : (evaluation X).Monoidal

Evaluation of presheaves of modules is monoidal: the tensor product of presheaves of modules is computed sectionwise, so the unit and tensor comparisons are identities.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.PresheafOfModulesOfCommRing.evaluationBraided {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (X : Cᵒᵖ) : (evaluation X).Braided

Evaluation of presheaves of modules is braided: the braiding of presheaves of modules is computed sectionwise.

Equations

• TauCeti.PresheafOfModulesOfCommRing.evaluationBraided X = { toMonoidal := TauCeti.PresheafOfModulesOfCommRing.evaluationMonoidal X, braided := ⋯ }

@[simp]

theorem TauCeti.PresheafOfModulesOfCommRing.evaluation_ε {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (X : Cᵒᵖ) : CategoryTheory.Functor.LaxMonoidal.ε (evaluation X) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat ↑(R.obj X)))

The unit comparison of evaluation is the identity.

@[simp]

theorem TauCeti.PresheafOfModulesOfCommRing.evaluation_η {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (X : Cᵒᵖ) : CategoryTheory.Functor.OplaxMonoidal.η (evaluation X) = CategoryTheory.CategoryStruct.id ((evaluation X).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (PresheafOfModulesOfCommRing R)))

The inverse unit comparison of evaluation is the identity.

@[simp]

theorem TauCeti.PresheafOfModulesOfCommRing.evaluation_μ {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (X : Cᵒᵖ) (M N : PresheafOfModulesOfCommRing R) : CategoryTheory.Functor.LaxMonoidal.μ (evaluation X) M N = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj ((evaluation X).obj M) ((evaluation X).obj N))

The tensor comparison of evaluation is the identity.

@[simp]

theorem TauCeti.PresheafOfModulesOfCommRing.evaluation_δ {C : Type v} [CategoryTheory.Category.{w, v} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (X : Cᵒᵖ) (M N : PresheafOfModulesOfCommRing R) : CategoryTheory.Functor.OplaxMonoidal.δ (evaluation X) M N = CategoryTheory.CategoryStruct.id ((evaluation X).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj M N))

The inverse tensor comparison of evaluation is the identity.