Theorems · Definition · category theory

CategoryTheory.SmallObject.functorMapSrc

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S T X Y : C} →
            {πX : X ⟶ S} →
              {πY : Y ⟶ T} →
                (CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY) →
                  [inst_1 :
                      CategoryTheory.Limits.HasColimitsOfShape
                        (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                    [inst_2 :
                        CategoryTheory.Limits.HasColimitsOfShape
                          (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY)) C] →
                      ∐ CategoryTheory.SmallObject.functorObjSrcFamily f πX ⟶
                        ∐ CategoryTheory.SmallObject.functorObjSrcFamily f πY

The canonical morphism ∐ (functorObjSrcFamily f πX) ⟶ ∐ (functorObjSrcFamily f πY) induced by a morphism Arrow.mk πX ⟶ Arrow.mk πY.

Defined in

Mathlib.CategoryTheory.SmallObject.Construction

Cited by

8 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasColimitsOfShapeCategoryTheory.Limits.HasColimitsOfShape