isIso_iff_of_reflects_iso — Mathlib

English

IsIso (F.map f) if and only if IsIso f, given that F reflects isomorphisms.

Русский

IsIso (F.map f) эквивалентно IsIso f, при условии, что F отражает изоморфизмы.

LaTeX

$$$IsIso (F.map f) \\iff IsIso f \\quad(\\text{under } F.ReflectsIsomorphisms).$$$

Lean4

theorem isIso_iff_of_reflects_iso {A B : C} (f : A ⟶ B) (F : C ⥤ D) [F.ReflectsIsomorphisms] :
    IsIso (F.map f) ↔ IsIso f :=
  ⟨fun _ => isIso_of_reflects_iso f F, fun _ => inferInstance⟩

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