Transporting existence of specific limits across equivalences #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
For now, we only treat the case of initial and terminal objects, but other special shapes can be added in the future.
theorem
category_theory.has_initial_of_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(e : D ⥤ C)
[category_theory.is_equivalence e]
[category_theory.limits.has_initial C] :
theorem
category_theory.equivalence.has_initial_iff
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :
theorem
category_theory.has_terminal_of_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(e : D ⥤ C)
[category_theory.is_equivalence e]
[category_theory.limits.has_terminal C] :
theorem
category_theory.equivalence.has_terminal_iff
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(e : C ≌ D) :