eq_of_iso — Mathlib

English

If C is thin and skeletal, then any two functors F1, F2 : D ⥤ C that are isomorphic are equal.

Русский

Если C тонкая и скелетальная, то любые изоморфные функторы F1, F2 : D ⥤ C равны.

LaTeX

$$$F_1 \cong F_2 \Rightarrow F_1 = F_2$$$

Lean4

/-- If `C` is thin and skeletal, then any naturally isomorphic functors to `C` are equal. -/
theorem eq_of_iso {F₁ F₂ : D ⥤ C} [Quiver.IsThin C] (hC : Skeletal C) (hF : F₁ ≅ F₂) : F₁ = F₂ :=
  Functor.ext (fun X => hC ⟨hF.app X⟩) fun _ _ _ => Subsingleton.elim _ _

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