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