hasInitial_iff — Mathlib

English

Let e be an equivalence between categories C and D. Then C has an initial object if and only if D has an initial object.

Русский

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

LaTeX

$$$\operatorname{HasInitial}(C) \iff \operatorname{HasInitial}(D)$$$

Lean4

theorem hasInitial_iff (e : C ≌ D) : HasInitial C ↔ HasInitial D :=
  ⟨fun (_ : HasInitial C) => hasInitial_of_equivalence e.inverse, fun (_ : HasInitial D) =>
    hasInitial_of_equivalence e.functor⟩

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