functor_thin — Mathlib

English

In a thin category, there is at most one isomorphism between any two objects.

Русский

В тонкой (thin) категории между любыми двумя объектами существует не более одного изоморфизма.

LaTeX

$$Subsingleton (X ≅ Y) for all X,Y in C$$

Lean4

/-- If `C` is a thin category, then `D ⥤ C` is a thin category. -/
instance functor_thin : Quiver.IsThin (D ⥤ C) := fun _ _ => ⟨fun α β => NatTrans.ext (by subsingleton)⟩

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