tensorHom — Mathlib

English

Auxiliary definition giving the tensor product of morphisms via tmul of isometries.

Русский

Вспомогательное определение, задающее тензорное произведение морфизмов через tmul изометрий.

LaTeX

$$$ \\text{tensorHom}(f,g) := \\langle f^\\otimes g^\\rangle. $$$

Lean4

/-- Auxiliary definition used to build `QuadraticModuleCat.instMonoidalCategory`.

We want this up front so that we can re-use it to define `whiskerLeft` and `whiskerRight`. -/
abbrev tensorHom {W X Y Z : QuadraticModuleCat.{u} R} (f : W ⟶ X) (g : Y ⟶ Z) : tensorObj W Y ⟶ tensorObj X Z :=
  ⟨f.toIsometry.tmul g.toIsometry⟩

Похожие утверждения