isIso_iff_isIso_coyoneda_map — Mathlib

English

For a morphism f : X ⟶ Y, IsIso f is equivalent to the property that for each c ∈ C, (coyoneda.map f.op).app c is an isomorphism.

Русский

Для морфизма f: X ⟶ Y равенство IsIso f эквивалентно тому, что для каждого объекта c ∈ C отображение (coyoneda.map f.op).app c является изоморфизмом.

LaTeX

$$$$ \IsIso(f) \iff \forall c, \IsIso\big( (coyoneda.map f^{op}).app c\big) $$$$

Lean4

theorem isIso_iff_isIso_coyoneda_map {X Y : C} (f : X ⟶ Y) : IsIso f ↔ ∀ c : C, IsIso ((coyoneda.map f.op).app c) :=
  by
  rw [isIso_iff_coyoneda_map_bijective]
  exact forall_congr' fun _ ↦ (isIso_iff_bijective _).symm

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