Theorems · Theorem · category theory

CategoryTheory.Functor.ReflectsIsomorphisms.reflects

∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} (F : CategoryTheory.Functor C D) [self : F.ReflectsIsomorphisms]
  {A B : C} (f : A ⟶ B) [CategoryTheory.IsIso (F.map f)], CategoryTheory.IsIso f

For any f, if F.map f is an iso, then so was f.

Defined in

Mathlib.CategoryTheory.Functor.ReflectsIso.Basic

Cited by

3 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.Functor.ReflectsIsomorphismsCategoryTheory.IsIso