English
If f: X → Y and g: Z → W are monoid homomorphisms, then their tensor f ⊗ g is also a monoid homomorphism.
Русский
Если f: X → Y и g: Z → W — моноидные гомоморфизмы, то их тензор f ⊗ g также является моноидным гомоморфизмом.
LaTeX
$$$\\text{If } f:\\,X\\to Y,\\ g:\\,Z\\to W \\text{ with } f,g \\text{ IsMonHom},\\; f\\otimes g:\\, X\\otimes Z \\to Y\\otimes W \\text{ isMonHom}$$$
Lean4
instance {f : X ⟶ Y} {g : Z ⟶ W} [IsMonHom f] [IsMonHom g] : IsMonHom (f ⊗ₘ g)
where
one_hom := by
dsimp [tensorObj.one_def]
slice_lhs 2 3 => rw [tensorHom_comp_tensorHom, one_hom, one_hom]
mul_hom := by
dsimp [tensorObj.mul_def]
slice_rhs 1 2 => rw [tensorμ_natural]
slice_lhs 2 3 => rw [tensorHom_comp_tensorHom, mul_hom, mul_hom, ← tensorHom_comp_tensorHom]
simp only [Category.assoc]
