English
Given a filtered diagram D in a locally small category C, and a colimit cocone c, a morphism p: X → A that is finitely presentable yields a factorization through some object D.obj j via a map q: A → D.obj j compatible with the cocone.
Русский
Пусть D — фильтрованный диаграмма в локально малой категории C, c — колимит, и p: X → A finitely presentable; тогда существует объект j и q: A → D.obj j, удовлетворяющие совместимости с диагональю кокона.
LaTeX
$$$ \exists j: J \; (q: A \to D.obj j),\ p \;\circ\; q = s_j \wedge q \;\circ\; \iota_j = f $$$
Lean4
theorem exists_hom_of_isFinitelyPresentable {J : Type w} [SmallCategory J] [IsFiltered J] {D : J ⥤ C} {c : Cocone D}
(hc : IsColimit c) {X A : C} {p : X ⟶ A} (hp : isFinitelyPresentable.{w} C p) (s : (Functor.const J).obj X ⟶ D)
(f : A ⟶ c.pt) (h : ∀ (j : J), s.app j ≫ c.ι.app j = p ≫ f) :
∃ (j : J) (q : A ⟶ D.obj j), p ≫ q = s.app j ∧ q ≫ c.ι.app j = f :=
hp.exists_hom_of_isColimit_under hc _ s _ h
