Theorems · Definition · category theory

CategoryTheory.MonoOver.coconeOfHasStrongEpiMonoFactorisation

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y : C} →
      [CategoryTheory.Limits.HasCoproducts C] →
        [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] →
          {J : Type u₂} →
            [inst_3 : CategoryTheory.Category.{v₂, u₂} J] →
              (F : CategoryTheory.Functor J (CategoryTheory.MonoOver Y)) → CategoryTheory.Limits.Cocone F

If a category C has strong epi-mono factorization, for any Y : C and functor F : J ⥤ MonoOver Y, there is a cocone under F.

Defined in

Mathlib.CategoryTheory.Subobject.MonoOver

Cited by

1 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasCoproductsCategoryTheory.Limits.HasStrongEpiMonoFactorisationsCategoryTheory.Category