toPresheaf_map_sheafificationHomEquiv_def

English

The left and right unitor and associator comply with tensorObj/tensorHom structure of presheaf modules.

Русский

Левый и правый унитор и ассоциатор удовлетворяют тензорной структуре прешефов модулей.

LaTeX

$$$\\lambda,\\rho,\\alpha$ satisfy coherence with tensorObj and tensorHom$$

Lean4

theorem toPresheaf_map_sheafificationHomEquiv_def {P : PresheafOfModules.{v} R₀} {F : SheafOfModules.{v} R}
    (f : (sheafification α).obj P ⟶ F) :
    (toPresheaf R₀).map (sheafificationHomEquiv α f) =
      CategoryTheory.toSheafify J P.presheaf ≫ (toPresheaf R.val).map f.val :=
  rfl

Похожие утверждения