counit_naturality — Mathlib

English

The counit is natural with respect to morphisms in the target category.

Русский

Коути́н естествен по отношению к морфизмам в целевой категории.

LaTeX

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

Lean4

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

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