funInvIdAssoc_hom_app — Mathlib

English

Describes the explicit hom-component of the isomorphism in the functor-inverse-id construction.

Русский

Уточняет гом-компоненту изоморфности в конструкции funInvIdAssoc.

LaTeX

$$(\\mathrm{funInvIdAssoc}\\; e\\; F)^{\\mathrm{hom}}_{X} = F.map (e.unitInv.app X)$$

Lean4

@[simp]
theorem funInvIdAssoc_hom_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
    (funInvIdAssoc e F).hom.app X = F.map (e.unitInv.app X) :=
  by
  dsimp [funInvIdAssoc]
  simp

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