tensor_apply — Mathlib

English

In a cartesian monoidal setting, the action of the tensor product on a pair of arrows is componentwise: (f ⊗ g)(p) = (f p.1, g p.2) for p ∈ W ⊗ Y.

Русский

Действие тензорирования на пару морфизмов осуществляется по компонентам: (f ⊗ g)(p) = (f p.1, g p.2) при p ∈ W ⊗ Y.

LaTeX

$$$(f \\otimes_{\\mathsf{m}} g) p = (f(p.1),\\; g(p.2)).$$$

Lean4

@[simp]
theorem tensor_apply {W X Y Z : Type u} (f : W ⟶ X) (g : Y ⟶ Z) (p : W ⊗ Y) : (f ⊗ₘ g) p = (f p.1, g p.2) :=
  rfl

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