invFunIdAssoc_inv_app — Mathlib

English

Let e be an equivalence C ≌ D and F a functor D → E. The inv-component of invFunIdAssoc(e, F) at X is equal to F applied to the counitInv at X.

Русский

Пусть e — эквивалентность C ≌ D и F — функтор D → E. Компонента inv естественной трансформации invFunIdAssoc(e, F) в X равна F( counitInv_X ).

LaTeX

$$$((e\!\.invFunIdAssoc F)\!\mathrm{.inv}).\mathrm{app} X = F( e.counitInv .app X )$$$

Lean4

@[simp]
theorem invFunIdAssoc_inv_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
    (invFunIdAssoc e F).inv.app X = F.map (e.counitInv.app X) :=
  by
  dsimp [invFunIdAssoc]
  simp

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