Theorems · Inductive type · category theory

CategoryTheory.JointlyReflectEpimorphisms

{C : Type u_1} →
  [inst : CategoryTheory.Category.{u_4, u_1} C] →
    {I : Type u_2} →
      {D : I → Type u_3} →
        [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] →
          ((i : I) → CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly

Cited by

5 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Category