mathlib3 documentation

category_theory.pempty

The empty category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Defines a category structure on pempty, and the unique functor pempty ⥤ C for any category C.

source
def category_theory.functor.empty_equivalence  :
category_theory.discrete pempty ≌ category_theory.discrete pempty

Equivalence between two empty categories.

Equations
source
def category_theory.functor.empty (C : Type u) [category_theory.category C] :
category_theory.discrete pempty ⥤ C

The canonical functor out of the empty category.

Equations
source
def category_theory.functor.empty_ext {C : Type u} [category_theory.category C] (F G : category_theory.discrete pempty ⥤ C) :
F ≅ G

Any two functors out of the empty category are isomorphic.

Equations
source
def category_theory.functor.unique_from_empty {C : Type u} [category_theory.category C] (F : category_theory.discrete pempty ⥤ C) :
F ≅ category_theory.functor.empty C

Any functor out of the empty category is isomorphic to the canonical functor from the empty category.

Equations
source
theorem category_theory.functor.empty_ext' {C : Type u} [category_theory.category C] (F G : category_theory.discrete pempty ⥤ C) :
F = G

Any two functors out of the empty category are equal. You probably want to use empty_ext instead of this.