leftKanExtensionCompIsoOfPreserves_inv_fac_app

English

The inverse factor in the preserved iso is compatible with whiskering and associativity.

Русский

Обратный фактор сохраняемого изоморфизма совместим с whisker и ассоциативностью.

LaTeX

$$$\text{Preserves_inv_fac}$$$

Lean4

@[reassoc (attr := simp)]
theorem leftKanExtensionCompIsoOfPreserves_inv_fac_app (a : A) :
    (L.leftKanExtensionUnit (F ⋙ G)).app a ≫ (G.leftKanExtensionCompIsoOfPreserves F L).inv.app (L.obj a) =
      G.map ((L.leftKanExtensionUnit F).app a) :=
  by
  simpa [-leftKanExtensionCompIsoOfPreserves_inv_fac] using
    NatTrans.congr_app (leftKanExtensionCompIsoOfPreserves_inv_fac G F L) a

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