English
Compatibility relations hold for tmul and map under pullback scalars, ensuring coherence of tensorObjMap with morphisms.
Русский
Согласованность операций tmul и отображений сохраняется при переводе скаляров по гомоморфизмам.
LaTeX
$$$\\mathrm{tmul}$ and $\\mathrm{map}$ commute under pullback of scalars, i.e. tensorObjMap respects composition of morphisms.$$
Lean4
/-- The tensor product of two morphisms of presheaves of modules. -/
@[simps]
noncomputable def tensorHom (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄) : tensorObj M₁ M₃ ⟶ tensorObj M₂ M₄
where
app X := f.app X ⊗ₘ g.app X
naturality {X Y}
φ :=
ModuleCat.MonoidalCategory.tensor_ext
(fun m₁ m₃ ↦ by
dsimp
rw [tensorObj_map_tmul]
-- Need `erw` because of the type mismatch in `map` and the tensor product.
erw [ModuleCat.MonoidalCategory.tensorHom_tmul, tensorObj_map_tmul]
rw [naturality_apply, naturality_apply]
simp)
