The empty category

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

instance CategoryTheory.instIsEmptyDiscrete (α : Type u_1) [IsEmpty α] : IsEmpty (CategoryTheory.Discrete α)

def CategoryTheory.functorOfIsEmpty (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u') [CategoryTheory.Category.{v', u'} D] [IsEmpty C] : CategoryTheory.Functor C D

The (unique) functor from an empty category.

Equations

• CategoryTheory.functorOfIsEmpty C D = { obj := fun (a : C) => isEmptyElim a, map := fun {X Y : C} => isEmptyElim X, map_id := ⋯, map_comp := ⋯ }

def CategoryTheory.Functor.isEmptyExt {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [IsEmpty C] (F G : CategoryTheory.Functor C D) : F ≅ G

Any two functors out of an empty category are isomorphic.

Equations

• F.isEmptyExt G = CategoryTheory.NatIso.ofComponents (fun (a : C) => isEmptyElim a) ⋯

def CategoryTheory.equivalenceOfIsEmpty (C : Type u) [CategoryTheory.Category.{v, u} C] (D : Type u') [CategoryTheory.Category.{v', u'} D] [IsEmpty C] [IsEmpty D] : C ≌ D

The equivalence between two empty categories.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.emptyEquivalence : CategoryTheory.Discrete PEmpty.{w + 1} ≌ CategoryTheory.Discrete PEmpty.{v + 1}

Equivalence between two empty categories.

Equations

• CategoryTheory.emptyEquivalence = CategoryTheory.equivalenceOfIsEmpty (CategoryTheory.Discrete PEmpty.{?u.10 + 1}) (CategoryTheory.Discrete PEmpty.{?u.9 + 1})

def CategoryTheory.Functor.empty (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C

The canonical functor out of the empty category.

Equations

• CategoryTheory.Functor.empty C = CategoryTheory.Discrete.functor PEmpty.elim

def CategoryTheory.Functor.emptyExt {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C) : F ≅ G

Any two functors out of the empty category are isomorphic.

Equations

• F.emptyExt G = CategoryTheory.Discrete.natIso fun (x : CategoryTheory.Discrete PEmpty.{?u.37 + 1}) => x.as.elim

def CategoryTheory.Functor.uniqueFromEmpty {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C) : F ≅ CategoryTheory.Functor.empty C

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

Equations

• F.uniqueFromEmpty = F.emptyExt (CategoryTheory.Functor.empty C)

theorem CategoryTheory.Functor.empty_ext' {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C) : F = G

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