Theorems · Theorem · category theory

CategoryTheory.isIso_of_fully_faithful

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso (F.map f)],
  CategoryTheory.IsIso f

If the image of a morphism under a fully faithful functor in an isomorphism, then the original morphisms is also an isomorphism.

Defined in

Mathlib.CategoryTheory.Functor.FullyFaithful

Cited by

7 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext, Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.FullCategoryTheory.Functor.FaithfulCategoryTheory.IsIso