Transporting existence of specific limits across equivalences #
For now, we only treat the case of initial and terminal objects, but other special shapes can be added in the future.
theorem
CategoryTheory.hasInitial_of_equivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(e : CategoryTheory.Functor D C)
[e.IsEquivalence]
[CategoryTheory.Limits.HasInitial C]
:
theorem
CategoryTheory.Equivalence.hasInitial_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(e : C ≌ D)
:
theorem
CategoryTheory.hasTerminal_of_equivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(e : CategoryTheory.Functor D C)
[e.IsEquivalence]
[CategoryTheory.Limits.HasTerminal C]
:
theorem
CategoryTheory.Equivalence.hasTerminal_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(e : C ≌ D)
: