tensor_ε — Mathlib

English

The μ morphism for the tensor functor factorizes through the product of components, aligning with the tensor structure on the product category.

Русский

Морфизм μ для тензорной функции факторизуется через произведение компонент и согласуется с тензорной структурой произведения.

LaTeX

$$$\; tensorμ (X_1,X_2) (Y_1,Y_2) = tensorμ X_1 X_2 Y_1 Y_2.$$$

Lean4

@[simp]
theorem tensor_ε : ε (tensor C) = (λ_ (𝟙_ C)).inv :=
  rfl

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