fun_inv_map — Mathlib

English

A standard expression of the inverse-functor naturality relating F, its inverse, and the counit.

Русский

Стандартное выражение естественности обратного функторa через F, его обратный и counit.

LaTeX

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

Lean4

@[reassoc, simp]
theorem fun_inv_map (e : C ≌ D) (X Y : D) (f : X ⟶ Y) :
    e.functor.map (e.inverse.map f) = e.counit.app X ≫ f ≫ e.counitInv.app Y :=
  (NatIso.naturality_2 e.counitIso f).symm

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