unit_naturality — Mathlib

English

The unit is natural with respect to morphisms in the source category.

Русский

Единица естественна по отношению к морфизмам в исходной категории.

LaTeX

$$$e.unit.app X \\;\\circ \\;e.inverse.map (e.functor.map f) = f \\;\\circ \\;e.unit.app Y$$$

Lean4

@[reassoc]
theorem unit_naturality (e : C ≌ D) {X Y : C} (f : X ⟶ Y) :
    e.unit.app X ≫ e.inverse.map (e.functor.map f) = f ≫ e.unit.app Y :=
  (e.unit.naturality f).symm

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