leftUnitor_inv_naturality — Mathlib

English

Let X, Y be objects with binary products. For f: X → Y, the inverse of the left unitor satisfies (prod.leftUnitor X)^{-1} ∘ prod.map (id) f = f ∘ (prod.leftUnitor Y)^{-1}.

Русский

Пусть X, Y — объекты с бинарными произведениями. Для f: X → Y обратный левой единости удовлетворяет (prod.leftUnitor X)^{-1} ∘ prod.map (id) f = f ∘ (prod.leftUnitor Y)^{-1}.

LaTeX

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

Lean4

@[reassoc]
theorem leftUnitor_inv_naturality [HasBinaryProducts C] (f : X ⟶ Y) :
    (prod.leftUnitor X).inv ≫ prod.map (𝟙 _) f = f ≫ (prod.leftUnitor Y).inv := by
  rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.leftUnitor_hom_naturality]

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