English
For a groupoid C, C is thin if and only if every endomorphism Hom(c,c) is a subsingleton (has at most one element).
Русский
Для группыодного C выполняется: C тонко тогда и только тогда, когда для каждого объекта c множество End(c) содержит не более одного элемента.
LaTeX
$$$\\mathrm{Quiver.IsThin}\\; C \\iff \\forall c:\\, C,\\; \\#\\{f:\\, c \\to c\\} \\le 1$$$
Lean4
theorem isThin_iff : Quiver.IsThin C ↔ ∀ c : C, Subsingleton (c ⟶ c) :=
by
refine ⟨fun h c => h c c, fun h c d => Subsingleton.intro fun f g => ?_⟩
haveI := h d
calc
f = f ≫ inv g ≫ g := by simp only [inv_eq_inv, IsIso.inv_hom_id, Category.comp_id]
_ = f ≫ inv f ≫ g := by
congr 1
simp only [inv_eq_inv, IsIso.inv_hom_id, eq_iff_true_of_subsingleton]
_ = g := by simp only [inv_eq_inv, IsIso.hom_inv_id_assoc]
