isIso_of_isIso_map — Mathlib

English

If F is fully faithful and f: X → Y has F.map f an isomorphism, then f is an isomorphism.

Русский

Если F полностью верен и морфизм f: X → Y имеет изоморфизм образа F.map f, то сам f является изоморфизмом.

LaTeX

$$$\forall X,Y:\; \forall f:\; X \to Y, [\operatorname{IsIso}(F.map(f))] \Rightarrow \operatorname{IsIso}(f)$$$

Lean4

theorem isIso_of_isIso_map {X Y : C} (f : X ⟶ Y) [IsIso (F.map f)] : IsIso f := by
  simpa using (hF.preimageIso (asIso (F.map f))).isIso_hom

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