English
Natural coherence for tensorObj with respect to composition of morphisms.
Русский
Единообразная когеренция для tensorObj относительно композиции гомоморфизмов.
LaTeX
$$$\\text{tensorObj}_{M_1,M_2}$ is compatible with composition: $\\mathrm{tensorObj}(M_1,M_2)_{X} \\circ (\\mathrm{tensorObj}(M_1,M_3)_{Y} \\otimes \\mathrm{tensorObj}(M_2,M_4)_{Z}) = \\cdots$$$
Lean4
noncomputable instance monoidalCategoryStruct : MonoidalCategoryStruct (PresheafOfModules.{u} (R ⋙ forget₂ _ _))
where
tensorObj := tensorObj
whiskerLeft _ _ _ g := tensorHom (𝟙 _) g
whiskerRight f _ := tensorHom f (𝟙 _)
tensorHom := tensorHom
tensorUnit := unit _
associator M₁ M₂ M₃ := isoMk (fun _ ↦ α_ _ _ _) (fun _ _ _ ↦ ModuleCat.MonoidalCategory.tensor_ext₃' (by intros; rfl))
leftUnitor
M :=
Iso.symm
(isoMk (fun _ ↦ (λ_ _).symm)
(fun X Y f ↦ by
ext m
dsimp [CommRingCat.forgetToRingCat_obj]
erw [leftUnitor_inv_apply, leftUnitor_inv_apply, tensorObj_map_tmul, (R.map f).hom.map_one]
rfl))
rightUnitor
M :=
Iso.symm
(isoMk (fun _ ↦ (ρ_ _).symm)
(fun X Y f ↦ by
ext m
dsimp [CommRingCat.forgetToRingCat_obj]
erw [rightUnitor_inv_apply, rightUnitor_inv_apply, tensorObj_map_tmul, (R.map f).hom.map_one]
rfl))
