English
If f,g: M1 ⊗ M2 ⟶ M3 satisfy f(m ⊗ n) = g(m ⊗ n) for all pure tensors m ⊗ n, then f = g.
Русский
Если две отображения f,g: M1 ⊗ M2 ⟶ M3 совпадают на всех чистых тензорах m ⊗ n, то f = g.
LaTeX
$$$\\forall m \\in M_1, \\forall n \\in M_2:\\; f(m \\otimes n) = g(m \\otimes n) \\Rightarrow f = g$$$
Lean4
instance : MonoidalPreadditive (ModuleCat.{u} R) :=
by
refine ⟨?_, ?_, ?_, ?_⟩
· intros
ext : 1
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply, hom_zero, LinearMap.zero_apply]
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
erw [MonoidalCategory.whiskerLeft_apply]
simp
· intros
ext : 1
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply, hom_zero, LinearMap.zero_apply, ]
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
erw [MonoidalCategory.whiskerRight_apply]
simp
· intros
ext : 1
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply, hom_add, LinearMap.add_apply]
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
erw [MonoidalCategory.whiskerLeft_apply, MonoidalCategory.whiskerLeft_apply]
erw [MonoidalCategory.whiskerLeft_apply]
simp [TensorProduct.tmul_add]
· intros
ext : 1
refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply, hom_add, LinearMap.add_apply]
-- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
erw [MonoidalCategory.whiskerRight_apply, MonoidalCategory.whiskerRight_apply]
erw [MonoidalCategory.whiskerRight_apply]
simp [TensorProduct.add_tmul]
