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
  • One or more equations did not get rendered due to their size.
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
    • One or more equations did not get rendered due to their size.
    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))