Mathlib.CategoryTheory.Limits.Shapes.Equivalence

Module docstring

{"# 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. "}

CategoryTheory.hasInitial_of_equivalence theorem

(e : D ⥤ C) [e.IsEquivalence] [HasInitial C] : HasInitial D

Full source

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

Equivalence Preserves Initial Objects

Informal description

Let $e \colon D \to C$ be an equivalence of categories. If $C$ has an initial object, then $D$ also has an initial object.

CategoryTheory.Equivalence.hasInitial_iff theorem

(e : C ≌ D) : HasInitial C ↔ HasInitial D

Full source

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

Equivalence of Categories Preserves Initial Objects (Bidirectional)

Informal description

Given an equivalence of categories $e \colon C \simeq D$, the category $C$ has an initial object if and only if the category $D$ has an initial object.

CategoryTheory.hasTerminal_of_equivalence theorem

(e : D ⥤ C) [e.IsEquivalence] [HasTerminal C] : HasTerminal D

Full source

theorem hasTerminal_of_equivalence (e : D ⥤ C) [e.IsEquivalence] [HasTerminal C] : HasTerminal D :=
  Adjunction.hasLimitsOfShape_of_equivalence e

Preservation of Terminal Objects under Equivalence of Categories

Informal description

Let $e \colon D \to C$ be an equivalence of categories. If $C$ has a terminal object, then $D$ also has a terminal object.

CategoryTheory.Equivalence.hasTerminal_iff theorem

(e : C ≌ D) : HasTerminal C ↔ HasTerminal D

Full source

theorem Equivalence.hasTerminal_iff (e : C ≌ D) : HasTerminalHasTerminal C ↔ HasTerminal D :=
  ⟨fun (_ : HasTerminal C) => hasTerminal_of_equivalence e.inverse,
    fun (_ : HasTerminal D) => hasTerminal_of_equivalence e.functor⟩

Equivalence Preserves Terminal Objects: $C \simeq D$ implies $C$ has terminal object iff $D$ has terminal object

Informal description

Given an equivalence of categories $e \colon C \simeq D$, the category $C$ has a terminal object if and only if the category $D$ has a terminal object.