instHasTensorTensorUnit_1 — Mathlib

English

Naturality of the right unitor with respect to φ: X → X' and the tensor unit on the right.

Русский

Естественность правого унитора по отношению к φ: X → X' и тензорная единица справа.

LaTeX

$$$\text{tensorHom } φ (𝟙 (tensorUnit)) ≫ (rightUnitor X').hom = (rightUnitor X).hom ≫ φ.$$$

Lean4

instance : HasTensor X tensorUnit :=
  mapBifunctorRightUnitor_hasMap (curriedTensor C) _ (rightUnitorNatIso C) _ add_zero _

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