isIso_iff_isIso_yoneda_map — Mathlib

English

IsIso f iff for all c ∈ C, IsIso ((yoneda.map f).app ⟨c⟩).

Русский

Изоморфизм f эквивалентен тому, что для каждого объекта c в C отображение IsIso ((yoneda.map f).app ⟨c⟩) верно.

LaTeX

$$IsIso f ↔ ∀ c : C, IsIso ((yoneda.map f).app ⟨c⟩)$$

Lean4

theorem isIso_iff_isIso_yoneda_map {X Y : C} (f : X ⟶ Y) : IsIso f ↔ ∀ c : C, IsIso ((yoneda.map f).app ⟨c⟩) :=
  by
  rw [isIso_iff_yoneda_map_bijective]
  exact forall_congr' fun _ ↦ (isIso_iff_bijective _).symm

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