unit_app_map_app — Mathlib

English

Compatibility of unit with map apps: the transformation of unit after mapping equals mapped units composed with unit of the target functors.

Русский

Совместимость единицы с отображениями приложений: преобразование единицы после отображения равно отображённой единице на целевых функторов.

LaTeX

$$$ (\\text{unit } F G)_{(x,y)} \\; \\circ \\; (\\text{map } f g)_{(x \\otimes y)} = (f_{x} \\otimes g_{y}) \\circ (\\text{unit } F' G')_{(x,y)} $$$

Lean4

@[reassoc (attr := simp)]
theorem unit_app_map_app :
    (unit F G).app (x, y) ≫ (map f g).app (x ⊗ y : C) = (f.app x ⊗ₘ g.app y) ≫ (unit F' G').app (x, y) := by
  simpa [tensorHom_def] using
    (Functor.descOfIsLeftKanExtension_fac_app (F ⊛ G) (unit F G) (F' ⊛ G') <|
        (externalProductBifunctor C C V).map (f ×ₘ g) ≫ unit F' G')
      (x, y)

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