pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app

English

The fac-app identity for the left Kan extension under preservation holds at a.

Русский

Выражение-фаска для левого кан-расширения сохраняющийся сохраняется в отношении a.

LaTeX

$$$\text{pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app}(a)$$$

Lean4

@[reassoc]
theorem pointwiseLeftKanExtensionCompIsoOfPreserves_fac_app (a : A) :
    (L.pointwiseLeftKanExtensionUnit <| F ⋙ G).app a ≫
        (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) =
      G.map (L.pointwiseLeftKanExtensionUnit F |>.app a) :=
  by
  simpa [-pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac] using
    NatTrans.congr_app (pointwiseLeftKanExtensionCompIsoOfPreserves_inv_fac G F L) a

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