Mathlib.CategoryTheory.PEmpty

CategoryTheory.instIsEmptyDiscrete instance

(α : Type*) [IsEmpty α] : IsEmpty (Discrete α)

Full source

instance (α : Type*) [IsEmpty α] : IsEmpty (Discrete α) := Function.isEmpty Discrete.as

Discrete Category of Empty Type is Empty

Informal description

For any empty type $\alpha$, the discrete category on $\alpha$ is also empty.

CategoryTheory.functorOfIsEmpty definition

[IsEmpty C] : C ⥤ D

Full source

/-- The (unique) functor from an empty category. -/
def functorOfIsEmpty [IsEmpty C] : C ⥤ D where
  obj := isEmptyElim
  map := fun {X} ↦ isEmptyElim X
  map_id := fun {X} ↦ isEmptyElim X
  map_comp := fun {X} ↦ isEmptyElim X

Unique functor from empty category

Informal description

The unique functor from an empty category $C$ to any category $D$. Since $C$ has no objects, the functor is uniquely determined by the empty mapping.

CategoryTheory.Functor.isEmptyExt definition

[IsEmpty C] (F G : C ⥤ D) : F ≅ G

Full source

/-- Any two functors out of an empty category are isomorphic. -/
def Functor.isEmptyExt [IsEmpty C] (F G : C ⥤ D) : F ≅ G :=
  NatIso.ofComponents isEmptyElim (fun {X} ↦ isEmptyElim X)

Isomorphism of functors from empty category

Informal description

For any empty category $C$ and any two functors $F, G : C \to D$ to a category $D$, there exists a natural isomorphism between $F$ and $G$. This is because there are no objects in $C$ to compare the functors on, making them trivially isomorphic.

CategoryTheory.equivalenceOfIsEmpty definition

[IsEmpty C] [IsEmpty D] : C ≌ D

Full source

/-- The equivalence between two empty categories. -/
def equivalenceOfIsEmpty [IsEmpty C] [IsEmpty D] : C ≌ D where
  functor := functorOfIsEmpty C D
  inverse := functorOfIsEmpty D C
  unitIso := Functor.isEmptyExt _ _
  counitIso := Functor.isEmptyExt _ _
  functor_unitIso_comp := isEmptyElim

Equivalence between empty categories

Informal description

Given two empty categories $C$ and $D$, there exists an equivalence of categories between them. This equivalence is constructed using: - The unique functor from $C$ to $D$ (since $C$ is empty) - The unique functor from $D$ to $C$ (since $D$ is empty) - The trivial natural isomorphisms between identity functors and compositions (since there are no objects to compare) - The triangle identities hold vacuously (since all compositions are between empty functors)

CategoryTheory.emptyEquivalence definition

: Discrete.{w} PEmpty ≌ Discrete.{v} PEmpty

Full source

/-- Equivalence between two empty categories. -/
def emptyEquivalence : DiscreteDiscrete.{w} PEmpty ≌ Discrete.{v} PEmpty := equivalenceOfIsEmpty _ _

Equivalence between empty discrete categories

Informal description

An equivalence between two empty categories, specifically between the discrete categories on the empty type in universes $w$ and $v$. This equivalence is constructed using the unique functors between these categories (since they are empty) and the trivial natural isomorphisms (since there are no objects to compare).

CategoryTheory.Functor.empty definition

: Discrete.{w} PEmpty ⥤ C

Full source

/-- The canonical functor out of the empty category. -/
def empty : DiscreteDiscrete.{w} PEmpty ⥤ C :=
  Discrete.functor PEmpty.elim

Empty functor

Informal description

The unique functor from the empty category (discrete category on the empty type) to any category $C$, defined by elimination on the empty type.

CategoryTheory.Functor.emptyExt definition

(F G : Discrete.{w} PEmpty ⥤ C) : F ≅ G

Full source

/-- Any two functors out of the empty category are isomorphic. -/
def emptyExt (F G : DiscreteDiscrete.{w} PEmpty ⥤ C) : F ≅ G :=
  Discrete.natIso fun x => x.as.elim

Isomorphism between functors from the empty category

Informal description

For any two functors $F$ and $G$ from the empty category (discrete category on the empty type) to a category $C$, there exists a natural isomorphism between $F$ and $G$. This is constructed by elimination on the empty type.

CategoryTheory.Functor.uniqueFromEmpty definition

(F : Discrete.{w} PEmpty ⥤ C) : F ≅ empty C

Full source

/-- Any functor out of the empty category is isomorphic to the canonical functor from the empty
category.
-/
def uniqueFromEmpty (F : DiscreteDiscrete.{w} PEmpty ⥤ C) : F ≅ empty C :=
  emptyExt _ _

Isomorphism between any functor from the empty category and the canonical empty functor

Informal description

For any functor $F$ from the empty category (discrete category on the empty type) to a category $C$, there exists a natural isomorphism between $F$ and the canonical empty functor $\text{empty}\ C$.

CategoryTheory.Functor.empty_ext' theorem

(F G : Discrete.{w} PEmpty ⥤ C) : F = G

Full source

/-- Any two functors out of the empty category are *equal*. You probably want to use
`emptyExt` instead of this.
-/
theorem empty_ext' (F G : DiscreteDiscrete.{w} PEmpty ⥤ C) : F = G :=
  Functor.ext (fun x => x.as.elim) fun x _ _ => x.as.elim

Uniqueness of Functors from the Empty Category

Informal description

For any two functors $F$ and $G$ from the empty category (discrete category on the empty type) to a category $\mathcal{C}$, the functors are equal, i.e., $F = G$.