ι_leftKanExtensionObjIsoColimit_hom

English

Inverse of the isomorphism given by the left Kan extension object iso colimit relates the injections appropriately.

Русский

Обратное к изоморфизму левого канонического расширения через объект-изол колимита корректно восстанавливает инъекции.

LaTeX

$$$\iota_\text{L}(X)^{f} \circ (L.leftKanExtensionObjIsoColimit F X)^{ -1} = \text{...}$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_leftKanExtensionObjIsoColimit_hom (X : D) (f : CostructuredArrow L X) :
    (L.leftKanExtensionUnit F).app f.left ≫
        (L.leftKanExtension F).map f.hom ≫ (L.leftKanExtensionObjIsoColimit F X).hom =
      colimit.ι (proj L X ⋙ F) f :=
  LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom (F := F)
    (isPointwiseLeftKanExtensionLeftKanExtensionUnit L F X) f

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