rightKanExtensionCompIsoOfPreserves_inv_fac_app

English

For each a in A, the inverse-fac of the preserving iso, applied at a, composed with G.map of the counit, yields the counit at a for the composite F ⋙ G.

Русский

Для каждого элемента a из A обратная часть сохраняющего изоморфизма, применённая в a, компонуется с отображением counit через G, давая counit для композиции F ⋙ G.

LaTeX

$$$\\forall a,\\ (G.rightKanExtensionCompIsoOfPreserves F L)^{\\mathrm{inv}}_{\\mathrm{app}(L a)} \\circ G.map((L.rightKanExtensionCounit F)_{a}) = (L.rightKanExtensionCounit (F \\cdot G))_{a}.$$$

Lean4

@[reassoc (attr := simp)]
theorem rightKanExtensionCompIsoOfPreserves_inv_fac_app (a : A) :
    (G.rightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) ≫ G.map (L.rightKanExtensionCounit F |>.app a) =
      (L.rightKanExtensionCounit (F ⋙ G)).app a :=
  by
  simpa [-rightKanExtensionCompIsoOfPreserves_inv_fac] using
    NatTrans.congr_app (rightKanExtensionCompIsoOfPreserves_inv_fac G F L) a

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