pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app

English

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

Русский

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

LaTeX

$$$(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]
theorem pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac_app (a : A) :
    (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) ≫
        G.map (L.pointwiseRightKanExtensionCounit F |>.app a) =
      (L.pointwiseRightKanExtensionCounit <| F ⋙ G).app a :=
  by
  simpa [-pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac] using
    NatTrans.congr_app (pointwiseRightKanExtensionCompIsoOfPreserves_inv_fac G F L) a

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