unitInv_naturality — Mathlib

English

UnitInv is natural with respect to arrows in the source category.

Русский

UnitInv естественна по отношению к стрелам в исходной категории.

LaTeX

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

Lean4

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

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