The pushforward functor is monoidal #
If F : C ⥤ D is a functor and R : Dᵒᵖ ⥤ CommRingCat is a presheaf
of commutative rings, then the pushforward functor from the category
of presheaves of modules on R to the category of presheaves of
modules on F.op ⋙ R is monoidal.
@[implicit_reducible]
noncomputable instance
PresheafOfModules.instMonoidalCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierOpPushforward₀OfCommRingCat
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{v_1, u_1} C]
[CategoryTheory.Category.{v_2, u_2} D]
(F : CategoryTheory.Functor C D)
(R : CategoryTheory.Functor Dᵒᵖ CommRingCat)
:
Equations
- One or more equations did not get rendered due to their size.