hasLimit_of_domain_hasInitial — Mathlib

English

If J has an initial object, then any functor F: J → C with all F.map f isomorphisms has a limit.

Русский

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

LaTeX

$$$$[HasInitial\\ J]\\,[F:J\\to C]\\ ([\\forall f,\\; F.map f\\text{ is iso}])\\Rightarrow \\mathrm{HasLimit}\;F.$$$$

Lean4

instance hasLimit_of_domain_hasInitial [HasInitial J] {F : J ⥤ C} : HasLimit F :=
  HasLimit.mk
    { cone := _, isLimit := limitOfDiagramInitial (initialIsInitial) F }
      -- This is reducible to allow usage of lemmas about `cone_point_unique_up_to_iso`.

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