hasColimit_of_domain_hasInitial — Mathlib

English

If J has an initial object and F maps every arrow to an isomorphism, then F has a colimit.

Русский

Если в J есть начальный объект и каждый отображаемый morphism является изоморфизмом, то диаграмма F: J → C имеет колимит.

LaTeX

$$$$[HasInitial\\ J]\\,[F:J\\to C]\\ ([\\forall i,j,f, IsIso(F.map f)])\\Rightarrow \\mathrm{HasColimit} F.$$$$

Lean4

instance hasColimit_of_domain_hasInitial [HasInitial J] {F : J ⥤ C} [∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)] :
    HasColimit F :=
  HasColimit.mk
    { cocone := _, isColimit := colimitOfDiagramInitial (initialIsInitial) F }
      -- This is reducible to allow usage of lemmas about `cocone_point_unique_up_to_iso`.

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