functor_skeletal — Mathlib

English

If C is thin and skeletal, then the functor category D ⥤ C is skeletal.

Русский

Если C тонкая и скелетальная, то категория функторов D ⥤ C скелетальна.

LaTeX

$$$\mathrm{Skeletal}(D \to C)$$$

Lean4

/-- If `C` is thin and skeletal, `D ⥤ C` is skeletal.
`CategoryTheory.functor_thin` shows it is thin also.
-/
theorem functor_skeletal [Quiver.IsThin C] (hC : Skeletal C) : Skeletal (D ⥤ C) := fun _ _ h =>
  h.elim (Functor.eq_of_iso hC)

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