isIso_of_fully_faithful — Mathlib

English

For a fully faithful F, if F.map f is an isomorphism, then f is an isomorphism.

Русский

Для полностью верного F, если F.map f является изоморфизмом, то и f является изоморфизмом.

LaTeX

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

Lean4

/-- If the image of a morphism under a fully faithful functor in an isomorphism,
then the original morphisms is also an isomorphism.
-/
theorem isIso_of_fully_faithful (f : X ⟶ Y) [IsIso (F.map f)] : IsIso f :=
  ⟨⟨F.preimage (inv (F.map f)), ⟨F.map_injective (by simp), F.map_injective (by simp)⟩⟩⟩

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