hasColimit_iff_small_colimitType — Mathlib

English

For a diagram F: J → Type u, the statement hasColimit F is equivalent to Small F.ColimitType, i.e., the colimit type lives in a small universe.

Русский

Для диаграммы F: J → Type u утверждение hasColimit F эквивалентно тому, что F.ColimitType принадлежит малому множеству, т.е. колимитный тип расположен в малой вселенной.

LaTeX

$$$$ HasColimit F \iff Small\ F.ColimitType. $$$$

Lean4

theorem hasColimit_iff_small_colimitType (F : J ⥤ Type u) : HasColimit F ↔ Small.{u} F.ColimitType :=
  ⟨fun _ ↦ small_of_injective ((isColimit_iff_coconeTypesIsColimit _).1 ⟨colimit.isColimit F⟩).bijective.1, fun _ ↦
    ⟨_, colimitCoconeIsColimit F⟩⟩

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