hasInitial_of_equivalence — Mathlib

English

If e: D ⥤ C is an equivalence of categories and C has an initial object, then D has an initial object as well.

Русский

Если e: D ⥤ C является эквалентностью категорий и в C имеется начальный объект, то и в D он существует.

LaTeX

$$$ HasInitial D $$$

Lean4

theorem hasInitial_of_equivalence (e : D ⥤ C) [e.IsEquivalence] [HasInitial C] : HasInitial D :=
  Adjunction.hasColimitsOfShape_of_equivalence e

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