empty_ext' — Mathlib

English

A category is equivalent to the discrete one on PUnit if and only if it is nonempty and between any two objects there is a unique morphism.

Русский

Категория эквивалентна дискретной над PUnit тогда и только тогда, когда она непустая и между любыми двумя объектами существует единственный морфизм.

LaTeX

$$$\text{Nonempty } C \text{ and } \forall x,y\in C, \text{Unique}(x\to y) \iff \exists \mathcal{E}: C \simeq \mathrm{Discrete}\, PUnit$$$

Lean4

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

Похожие утверждения