Documentation

Mathlib.CategoryTheory.PEmpty

The empty category #

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

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

Equivalence between two empty categories.

Instances For
    source
    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.

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

      Any two functors out of the empty category are isomorphic.

      Instances For
        source
        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.

        Instances For
          source
          theorem CategoryTheory.Functor.empty_ext' {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1} ) C) (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.