tensorHom_app_apply — Mathlib

English

In a monoidal functor setting for SSet, the tensor product of morphisms f and g acts on a tensor object by applying f and g componentwise on the respective factors.

Русский

В условиях моноидальной функториальности для SSet тензорное произведение отображений f и g действует на тензорный объект по компонентам на соответствующих компонентах.

LaTeX

$$$(f \\otimes g).\\mathrm{app}\\ \\Delta x = \\langle f.\\mathrm{app}\\ \\Delta x.1,\\ g.\\mathrm{app}\\ \\Delta x.2\\rangle$$$

Lean4

@[simp]
theorem tensorHom_app_apply {K K' L L' : SSet.{u}} (f : K ⟶ K') (g : L ⟶ L') {Δ : SimplexCategoryᵒᵖ}
    (x : (K ⊗ L).obj Δ) : (f ⊗ₘ g).app Δ x = ⟨f.app Δ x.1, g.app Δ x.2⟩ :=
  rfl

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