Documentation

Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images

The category of type-valued functors has images #

source
def CategoryTheory.FunctorToTypes.monoFactorisation {C : Type u_1} [Category.{v_1, u_1} C] {F G : Functor C (Type u)} (f : F ⟶ G) :
Limits.MonoFactorisation f

The image of a natural transformation between type-valued functors is a MonoFactorisation

Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.FunctorToTypes.monoFactorisation_m {C : Type u_1} [Category.{v_1, u_1} C] {F G : Functor C (Type u)} (f : F ⟶ G) :
      (monoFactorisation f).m = (Subfunctor.range f).ι
      source
      @[simp]
      theorem CategoryTheory.FunctorToTypes.monoFactorisation_I {C : Type u_1} [Category.{v_1, u_1} C] {F G : Functor C (Type u)} (f : F ⟶ G) :
      (monoFactorisation f).I = (Subfunctor.range f).toFunctor
      source
      @[simp]
      theorem CategoryTheory.FunctorToTypes.monoFactorisation_e {C : Type u_1} [Category.{v_1, u_1} C] {F G : Functor C (Type u)} (f : F ⟶ G) :
      (monoFactorisation f).e = Subfunctor.toRange f
      source
      noncomputable def CategoryTheory.FunctorToTypes.monoFactorisationIsImage {C : Type u_1} [Category.{v_1, u_1} C] {F G : Functor C (Type u)} (f : F ⟶ G) :
      Limits.IsImage (monoFactorisation f)

      The image of a natural transformation between type-valued functors satisfies the universal property of images

      Equations
        Instances For
          source
          instance CategoryTheory.FunctorToTypes.instHasImagesFunctorType {C : Type u_1} [Category.{v_1, u_1} C] :
          Limits.HasImages (Functor C (Type u_2))
          source
          instance CategoryTheory.FunctorToTypes.instHasStrongEpiMonoFactorisationsFunctorType {C : Type u_1} [Category.{v_1, u_1} C] :
          Limits.HasStrongEpiMonoFactorisations (Functor C (Type u_2))