English
For objects X,Y in C^op and a morphism f: X→Y, there is a canonical map from M1(X)⊗M2(X) to M1(Y)⊗M2(Y) compatible with the R-map along f.
Русский
Для X,Y в C^op и гомоморфизма f: X→Y существует каноническое отображение из M1(X)⊗M2(X) в M1(Y)⊗M2(Y), совместимое с отображением R вдоль f.
LaTeX
$$$\\mathrm{tensorObjMap}_{X,Y,f}: M_1(X) \\otimes M_2(X) \\to (M_1(Y) \\otimes M_2(Y))$ is defined by $m_1\\otimes m_2 \\mapsto M_1(f)(m_1) \\otimes M_2(f)(m_2)$.$$
Lean4
/-- Auxiliary definition for `tensorObj`. -/
noncomputable def tensorObjMap {X Y : Cᵒᵖ} (f : X ⟶ Y) :
M₁.obj X ⊗ M₂.obj X ⟶ (ModuleCat.restrictScalars (R.map f).hom).obj (M₁.obj Y ⊗ M₂.obj Y) :=
ModuleCat.MonoidalCategory.tensorLift (fun m₁ m₂ ↦ M₁.map f m₁ ⊗ₜ M₂.map f m₂)
(by intro m₁ m₁' m₂; dsimp; rw [map_add, TensorProduct.add_tmul]) (by intro a m₁ m₂; dsimp; erw [M₁.map_smul]; rfl)
(by intro m₁ m₂ m₂'; dsimp; rw [map_add, TensorProduct.tmul_add])
(by intro a m₁ m₂; dsimp; erw [M₂.map_smul, TensorProduct.tmul_smul (r := R.map f a)]; rfl)
