Exactness of families of functors which jointly reflect isomorphisms

Let Fᵢ : C ⥤ Dᵢ be a conservative family of functors (i.e. they jointly reflect isomorphisms). Let G : J ⥤ C be a functor that has a limit that is preserved by the functors Fᵢ. In this file, we show that a cone for G is a limit if it is so after applying the functors Fᵢ.

noncomputable def CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectsLimit {C : Type u_1} [Category.{u_5, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{u_6, u_3} (D i)] {F : (i : I) → Functor C (D i)} (hF : JointlyReflectIsomorphisms F) {J : Type u_4} [Category.{v_1, u_4} J] {G : Functor J C} {c : Limits.Cone G} (hc : (i : I) → Limits.IsLimit ((F i).mapCone c)) [Limits.HasLimit G] [∀ (i : I), Limits.PreservesLimit G (F i)] : Limits.IsLimit c

If Fᵢ : C ⥤ Dᵢ is a conservative family of functors which also preserve the (existing) limit of a functor G : J ⥤ C, then a cone for G is a limit if it is so after applying the functors Fᵢ (see also reflectsLimit_of_reflectsIsomorphisms in the file Mathlib/CategoryTheory/Limits/Preserves/Basic.lean for the corresponding result for a single functor).

Equations

• hF.jointlyReflectsLimit hc = (CategoryTheory.Limits.limit.isLimit G).ofIsoLimit (CategoryTheory.Limits.Cone.ext (CategoryTheory.asIso (CategoryTheory.Limits.limit.lift G c)) ⋯).symm

noncomputable def CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectsColimit {C : Type u_1} [Category.{u_5, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{u_6, u_3} (D i)] {F : (i : I) → Functor C (D i)} (hF : JointlyReflectIsomorphisms F) {J : Type u_4} [Category.{v_1, u_4} J] {G : Functor J C} {c : Limits.Cocone G} (hc : (i : I) → Limits.IsColimit ((F i).mapCocone c)) [Limits.HasColimit G] [∀ (i : I), Limits.PreservesColimit G (F i)] : Limits.IsColimit c

If Fᵢ : C ⥤ Dᵢ is a conservative family of functors which also preserve the (existing) colimit of a functor G : J ⥤ C, then a cocone for G is a colimit if it is so after applying the functors Fᵢ (see also reflectsColimit_of_reflectsIsomorphisms in the file Mathlib/CategoryTheory/Limits/Preserves/Basic.lean for the corresponding result for a single functor)

Equations

• hF.jointlyReflectsColimit hc = (CategoryTheory.Limits.colimit.isColimit G).ofIsoColimit (CategoryTheory.Limits.Cocone.ext (CategoryTheory.asIso (CategoryTheory.Limits.colimit.desc G c)) ⋯)