exists_hom_of_hom — Mathlib

English

Given i, u: j → j', and IsFiltered(I j'), with ((P j).diag.obj i) finitely presentable, there exists i' in I j' and a morphism f: Total.mk P j i → Total.mk P j' i' such that its base is u.

Русский

Пусть дано i, u: j → j', а также IsFiltered(I j') и ((P j).diag.obj i) является конечно презентируемым; существует i'∈I j' и морфизм f: Total.mk P j i → Total.mk P j' i', такой что f.base = u.

LaTeX

$$$\exists i' : I(j'), \exists f : Total.mk P j i \to Total.mk P j' i',\ f.base = u$$$

Lean4

theorem exists_hom_of_hom {j j' : J} (i : I j) (u : j ⟶ j') [IsFiltered (I j')]
    [IsFinitelyPresentable.{w} ((P j).diag.obj i)] :
    ∃ (i' : I j') (f : Total.mk P j i ⟶ Total.mk P j' i'), f.base = u :=
  by
  obtain ⟨i', q, hq⟩ := IsFinitelyPresentable.exists_hom_of_isColimit (P j').isColimit ((P j).ι.app i ≫ D.map u)
  use i', { base := u, hom := q, w := by simp [← hq] }

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