English
Duplicate entry of the equivalence between punit and unique morphisms condition; see 78251.
Русский
Дубликат эквивалентности между punit и условием уникальности морфизмов; см. 78251.
LaTeX
$$$\text{Nonempty } C \text{ and } \forall x y,\; Nonempty (\mathrm{Unique}(x \to y)) \iff \exists \mathcal{E}: C \simeq \mathrm{Discrete}\, PUnit$$$
Lean4
/-- A category being equivalent to `PUnit` is equivalent to it having a unique morphism between
any two objects. (In fact, such a category is also a groupoid;
see `CategoryTheory.Groupoid.ofHomUnique`) -/
theorem equiv_punit_iff_unique :
Nonempty (C ≌ Discrete PUnit.{w + 1}) ↔ Nonempty C ∧ ∀ x y : C, Nonempty <| Unique (x ⟶ y) :=
by
constructor
· rintro ⟨h⟩
refine ⟨⟨h.inverse.obj ⟨⟨⟩⟩⟩, fun x y => Nonempty.intro ?_⟩
let f : x ⟶ y := by
have hx : x ⟶ h.inverse.obj ⟨⟨⟩⟩ := by convert h.unit.app x
have hy : h.inverse.obj ⟨⟨⟩⟩ ⟶ y := by convert h.unitInv.app y
exact hx ≫ hy
suffices sub : Subsingleton (x ⟶ y) from uniqueOfSubsingleton f
have : ∀ z, z = h.unit.app x ≫ (h.functor ⋙ h.inverse).map z ≫ h.unitInv.app y :=
by
intro z
simp
apply Subsingleton.intro
intro a b
rw [this a, this b]
simp only [Functor.comp_map]
congr 3
apply ULift.ext
simp [eq_iff_true_of_subsingleton]
· rintro ⟨⟨p⟩, h⟩
haveI := fun x y => (h x y).some
refine
Nonempty.intro
(CategoryTheory.Equivalence.mk ((Functor.const _).obj ⟨⟨⟩⟩) ((@Functor.const <| Discrete PUnit).obj p) ?_
(by apply Functor.punitExt))
exact
NatIso.ofComponents fun _ =>
{ hom := default
inv := default }
