CategoryTheory.equiv_punit_iff_unique
theorem CategoryTheory.equiv_punit_iff_unique :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
Nonempty (C ≌ CategoryTheory.Discrete PUnit.{w + 1}) ↔ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
The theorem `CategoryTheory.equiv_punit_iff_unique` states that in category theory, a category 'C' is equivalent to the category of a single point (`PUnit`) if and only if the category 'C' is nonempty and there exists a unique morphism (arrow) between any two objects in the category. In other words, every pair of objects in 'C' can be connected by exactly one arrow. This theorem also notes that such a category is a groupoid, as indicated by `CategoryTheory.Groupoid.ofHomUnique`.
More concisely: A category is equivalent to the category of a single point if and only if it is nonempty and has unique morphisms between any two objects, making it a groupoid.
|
CategoryTheory.Functor.punit_ext'
theorem CategoryTheory.Functor.punit_ext' :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
(F G : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1})), F = G
This theorem states that for any given category `C` and any two functors `F` and `G` from `C` to the discrete category of a single point (`PUnit`), these two functors `F` and `G` are equal. In other words, there is only one functor from any category to the category with a single object and a single morphism (the identity). While this theorem might be useful, it's generally recommended to use `punitExt` function instead for these purposes.
More concisely: For any category `C` and functors `F` and `G` from `C` to the discrete category `PUnit`, `F` equals `G`.
|
Mathlib.CategoryTheory.PUnit._auxLemma.1
theorem Mathlib.CategoryTheory.PUnit._auxLemma.1 : ∀ {α : Sort u_1} [inst : Subsingleton α] (x y : α), (x = y) = True
This theorem, from the Mathlib library in Category Theory, states that for any type `α` that is a subsingleton (i.e., a type that has at most one inhabitant), any two elements `x` and `y` of `α` are necessarily equal. This is expressed by the equality `(x = y) = True`. In other words, in a subsingleton type, all elements are identical.
More concisely: In a subsingleton type, all elements are equal.
|