@[reducible, inline]

abbrev Functor.IsConservative {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Prop

Definition 27 (Lec 13): a functor is conservative if it reflects isomorphisms.

noncomputable def adjunction_equivalence_of_fullyFaithful_conservative {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (adj : L ⊣ R) [L.Full] [L.Faithful] [R.ReflectsIsomorphisms] : C ≌ D

A fully faithful left adjoint with a conservative right adjoint gives an equivalence of categories.

theorem jointlyReflectIsomorphisms_of_conservative {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (R : CategoryTheory.Functor C D) [R.ReflectsIsomorphisms] : CategoryTheory.JointlyReflectIsomorphisms fun (x : PUnit.{1}) => R

A single conservative functor (indexed by a singleton) jointly reflects isomorphisms.

theorem conservative_exact_functor_reflects_exact_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (R : CategoryTheory.Functor C D) [R.PreservesZeroMorphisms] [R.PreservesHomology] [R.ReflectsIsomorphisms] (S : CategoryTheory.ShortComplex C) : S.Exact ↔ (S.map R).Exact

A conservative exact functor between abelian categories reflects exactness of short complexes: S.Exact ↔ (S.map R).Exact.