isIso_of_reflects_iso — Mathlib

English

If F reflects isomorphisms and F.map f is an isomorphism, then f is an isomorphism.

Русский

Если F отражает изоморфизмы и F.map f является изоморфизмом, то и f является изоморфизмом.

LaTeX

$$$\\big( F.ReflectsIsomorphisms \\big) \\wedge IsIso(F.map f) \\Rightarrow IsIso f,$ for arbitrary morphism f.$$

Lean4

/-- If `F` reflects isos and `F.map f` is an iso, then `f` is an iso. -/
theorem isIso_of_reflects_iso {A B : C} (f : A ⟶ B) (F : C ⥤ D) [IsIso (F.map f)] [F.ReflectsIsomorphisms] : IsIso f :=
  ReflectsIsomorphisms.reflects F f

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