Families of functors which jointly reflect isomorphisms

Let Fᵢ : C ⥤ Dᵢ be a family of functors. The family is said to jointly reflect isomorphisms (resp. monomorphisms, resp. epimorphisms) if every f : X ⟶ Y in C for which Fᵢ.map f is an isomorphism (resp. monomorphism, resp. epimorphism) for all i is an isomorphism.

structure CategoryTheory.JointlyReflectIsomorphisms {C : Type u_1} [Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{u_5, u_3} (D i)] (F : (i : I) → Functor C (D i)) : Prop

A family of functors jointly reflects isomorphisms if for every morphism f : X ⟶ Y such that the image of f under all F i is an isomorphism, then f is an isomorphism.

• isIso {X Y : C} (f : X ⟶ Y) [∀ (i : I), IsIso ((F i).map f)] : IsIso f

structure CategoryTheory.JointlyReflectMonomorphisms {C : Type u_1} [Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{u_5, u_3} (D i)] (F : (i : I) → Functor C (D i)) : Prop

A family of functors jointly reflects monomorphisms if for every morphism f : X ⟶ Y such that the image of f under all F i is an monomorphism, then f is an monomorphism.

• mono {X Y : C} (f : X ⟶ Y) [∀ (i : I), Mono ((F i).map f)] : Mono f

structure CategoryTheory.JointlyReflectEpimorphisms {C : Type u_1} [Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{u_5, u_3} (D i)] (F : (i : I) → Functor C (D i)) : Prop

A family of functors jointly reflects epimorphisms if for every morphism f : X ⟶ Y such that the image of f under all F i is an epimorphism, then f is an epimorphism.

• epi {X Y : C} (f : X ⟶ Y) [∀ (i : I), Epi ((F i).map f)] : Epi f

theorem CategoryTheory.JointlyReflectIsomorphisms.isIso_iff {C : Type u_1} [Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{u_5, u_3} (D i)] {F : (i : I) → Functor C (D i)} (h : JointlyReflectIsomorphisms F) {X Y : C} (f : X ⟶ Y) : IsIso f ↔ ∀ (i : I), IsIso ((F i).map f)

theorem CategoryTheory.JointlyReflectIsomorphisms.mono {C : Type u_1} [Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{u_5, u_3} (D i)] {F : (i : I) → Functor C (D i)} (h : JointlyReflectIsomorphisms F) {X Y : C} (f : X ⟶ Y) [hf : ∀ (i : I), Mono ((F i).map f)] [∀ (i : I), Limits.PreservesLimit (Limits.cospan f f) (F i)] [Limits.HasPullback f f] : Mono f

theorem CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectMonomorphisms {C : Type u_1} [Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{u_5, u_3} (D i)] {F : (i : I) → Functor C (D i)} (h : JointlyReflectIsomorphisms F) [∀ (i : I), Limits.PreservesLimitsOfShape Limits.WalkingCospan (F i)] [Limits.HasPullbacks C] : JointlyReflectMonomorphisms F

theorem CategoryTheory.JointlyReflectIsomorphisms.epi {C : Type u_1} [Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{u_5, u_3} (D i)] {F : (i : I) → Functor C (D i)} (h : JointlyReflectIsomorphisms F) {X Y : C} (f : X ⟶ Y) [hf : ∀ (i : I), Epi ((F i).map f)] [∀ (i : I), Limits.PreservesColimit (Limits.span f f) (F i)] [Limits.HasPushout f f] : Epi f

theorem CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectEpimorphisms {C : Type u_1} [Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{u_5, u_3} (D i)] {F : (i : I) → Functor C (D i)} (h : JointlyReflectIsomorphisms F) [∀ (i : I), Limits.PreservesColimitsOfShape Limits.WalkingSpan (F i)] [Limits.HasPushouts C] : JointlyReflectEpimorphisms F

theorem CategoryTheory.JointlyReflectMonomorphisms.mono_iff {C : Type u_1} [Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{u_5, u_3} (D i)] {F : (i : I) → Functor C (D i)} (h : JointlyReflectMonomorphisms F) [∀ (i : I), (F i).PreservesMonomorphisms] {X Y : C} (f : X ⟶ Y) : Mono f ↔ ∀ (i : I), Mono ((F i).map f)

theorem CategoryTheory.JointlyReflectEpimorphisms.epi_iff {C : Type u_1} [Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → Category.{u_5, u_3} (D i)] {F : (i : I) → Functor C (D i)} (h : JointlyReflectEpimorphisms F) [∀ (i : I), (F i).PreservesEpimorphisms] {X Y : C} (f : X ⟶ Y) : Epi f ↔ ∀ (i : I), Epi ((F i).map f)