exists_hom_of_isColimit — Mathlib

English

Let J be a small category and D : J ⥤ C, with c a cocone that is an IsColimit. Then any morphism f : X ⟶ D.obj i factors through some j via a morphism p : X ⟶ D.obj j and a compatible leg in the cocone.

Русский

Пусть J — малая категория и D : J ⥤ C, fункторный кокон c является IsColimit; тогда любой морфизм f: X ⟶ D.obj i факторизуется через некоторый j с морфизмом p: X ⟶ D.obj j и совместной ногой кокона.

LaTeX

$$$\exists j : J, \exists p : X \to D.obj j,\ p \circ c.ι.app j = f$$$

Lean4

theorem exists_hom_of_isColimit {J : Type w} [SmallCategory J] [IsFiltered J] {D : J ⥤ C} {c : Cocone D}
    (hc : IsColimit c) {X : C} [IsFinitelyPresentable.{w} X] (f : X ⟶ c.pt) :
    ∃ (j : J) (p : X ⟶ D.obj j), p ≫ c.ι.app j = f :=
  Types.jointly_surjective_of_isColimit (isColimitOfPreserves (coyoneda.obj (op X)) hc) f

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