leftUnitor_hom_naturality — Mathlib

English

Let X, Y be objects in a category with binary products and a terminal object. For any morphism f: X → Y, the left unitor is compatible with prod.map on the second component: prod.map (id_X) f ∘ leftUnitor_Y = leftUnitor_X ∘ f.

Русский

Пусть X, Y — объекты в категории с бинарными произведениями и терминальным объектом. Для любого морфизма f: X → Y тождественный компонент левого юнитора совместим с отображением на произведении: prod.map (id_X) f ∘ leftUnitor_Y = leftUnitor_X ∘ f.

LaTeX

$$$ \\operatorname{prod.map}(\\mathrm{id}_X, f) \\circ (\\operatorname{prod.leftUnitor} Y) = (\\operatorname{prod.leftUnitor} X) \\circ f $$$

Lean4

@[reassoc]
theorem leftUnitor_hom_naturality [HasBinaryProducts C] (f : X ⟶ Y) :
    prod.map (𝟙 _) f ≫ (prod.leftUnitor Y).hom = (prod.leftUnitor X).hom ≫ f :=
  prod.map_snd _ _

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