Exactness properties of functors which jointly reflect isomorphisms

Let Fᵢ : C ⥤ Dᵢ be a family of exact functors between abelian categories. Assume that they jointly reflect isomorphisms. We show that a short complex in C is exact (resp. short exact) iff it is so after applying the functor Fᵢ. Similar results are obtained for the detection of quasi-isomorphisms between short complexes or homological complexes in C. (Corresponding results for a single functor are HomologicalComplex.quasiIsoAt_map_iff_of_preservesHomology and HomologicalComplex.quasiIso_map_iff_of_preservesHomology in the files Mathlib/Algebra/Homology/QuasiIso.lean and ShortComplex.quasiIso_map_iff_of_preservesLeftHomology Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean.)

theorem CategoryTheory.JointlyReflectIsomorphisms.isZero_iff {C : Type u_1} [Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{v_2, u_3} (D i)] {F : (i : I) → Functor C (D i)} (hP : JointlyReflectIsomorphisms F) [Limits.HasZeroMorphisms C] [(i : I) → Limits.HasZeroMorphisms (D i)] [∀ (i : I), (F i).PreservesZeroMorphisms] [Limits.HasZeroObject C] {X : C} : Limits.IsZero X ↔ ∀ (i : I), Limits.IsZero ((F i).obj X)

theorem CategoryTheory.JointlyReflectIsomorphisms.exact_iff {C : Type u_1} [Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{v_2, u_3} (D i)] {F : (i : I) → Functor C (D i)} (hP : JointlyReflectIsomorphisms F) [Limits.HasZeroMorphisms C] [(i : I) → Limits.HasZeroMorphisms (D i)] [∀ (i : I), (F i).PreservesZeroMorphisms] [CategoryWithHomology C] [∀ (i : I), (F i).PreservesHomology] [Limits.HasZeroObject C] (S : ShortComplex C) : S.Exact ↔ ∀ (i : I), (S.map (F i)).Exact

theorem CategoryTheory.JointlyReflectIsomorphisms.exactAt_iff {C : Type u_1} [Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{v_2, u_3} (D i)] {F : (i : I) → Functor C (D i)} (hP : JointlyReflectIsomorphisms F) [Limits.HasZeroMorphisms C] [(i : I) → Limits.HasZeroMorphisms (D i)] [∀ (i : I), (F i).PreservesZeroMorphisms] [CategoryWithHomology C] [∀ (i : I), (F i).PreservesHomology] [Limits.HasZeroObject C] {α : Type u_4} {c : ComplexShape α} (K : HomologicalComplex C c) (a : α) : K.ExactAt a ↔ ∀ (i : I), (((F i).mapHomologicalComplex c).obj K).ExactAt a

theorem CategoryTheory.JointlyReflectIsomorphisms.shortExact_iff {C : Type u_1} [Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{v_2, u_3} (D i)] {F : (i : I) → Functor C (D i)} (hP : JointlyReflectIsomorphisms F) [Abelian C] [(i : I) → Abelian (D i)] [CategoryWithHomology C] [∀ (i : I), Limits.PreservesFiniteLimits (F i)] [∀ (i : I), Limits.PreservesFiniteColimits (F i)] (S : ShortComplex C) : S.ShortExact ↔ ∀ (i : I), (S.map (F i)).ShortExact

theorem CategoryTheory.JointlyReflectIsomorphisms.shortComplexQuasiIso_iff {C : Type u_1} [Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{v_2, u_3} (D i)] {F : (i : I) → Functor C (D i)} (hP : JointlyReflectIsomorphisms F) [Abelian C] [(i : I) → Abelian (D i)] [CategoryWithHomology C] [∀ (i : I), Limits.PreservesFiniteLimits (F i)] [∀ (i : I), Limits.PreservesFiniteColimits (F i)] {S₁ S₂ : ShortComplex C} (f : S₁ ⟶ S₂) : ShortComplex.QuasiIso f ↔ ∀ (i : I), ShortComplex.QuasiIso ((F i).mapShortComplex.map f)

theorem CategoryTheory.JointlyReflectIsomorphisms.quasiIsoAt_iff {C : Type u_1} [Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{v_2, u_3} (D i)] {F : (i : I) → Functor C (D i)} (hP : JointlyReflectIsomorphisms F) [Abelian C] [(i : I) → Abelian (D i)] [CategoryWithHomology C] [∀ (i : I), Limits.PreservesFiniteLimits (F i)] [∀ (i : I), Limits.PreservesFiniteColimits (F i)] {α : Type u_4} {c : ComplexShape α} {K L : HomologicalComplex C c} (f : K ⟶ L) (a : α) : QuasiIsoAt f a ↔ ∀ (i : I), QuasiIsoAt (((F i).mapHomologicalComplex c).map f) a

theorem CategoryTheory.JointlyReflectIsomorphisms.quasiIso_iff {C : Type u_1} [Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{v_2, u_3} (D i)] {F : (i : I) → Functor C (D i)} (hP : JointlyReflectIsomorphisms F) [Abelian C] [(i : I) → Abelian (D i)] [CategoryWithHomology C] [∀ (i : I), Limits.PreservesFiniteLimits (F i)] [∀ (i : I), Limits.PreservesFiniteColimits (F i)] {α : Type u_4} {c : ComplexShape α} {K L : HomologicalComplex C c} (f : K ⟶ L) : QuasiIso f ↔ ∀ (i : I), QuasiIso (((F i).mapHomologicalComplex c).map f)