Theorems · Definition · category theory

CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.map

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {J : Type w} →
          [inst_2 : LinearOrder J] →
            [inst_3 : SuccOrder J] →
              [inst_4 : OrderBot J] →
                [inst_5 : WellFoundedLT J] →
                  {X Y : C} →
                    {f : X ⟶ Y} →
                      {W : CategoryTheory.MorphismProperty D} →
                        {F : CategoryTheory.Functor C D} →
                          [CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J F] →
                            [CategoryTheory.Limits.PreservesColimitsOfShape J F] →
                              (W.inverseImage F).TransfiniteCompositionOfShape J f →
                                W.TransfiniteCompositionOfShape J (F.map f)

If f is a transfinite composition of shape J of morphisms in W.inverseImage F, then F is a transfinite composition of shape J of morphisms in W provided F preserves suitable colimits.

Defined in

Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryLinearOrderSuccOrderOrderBotWellFoundedLTCategoryTheory.Limits.PreservesWellOrderContinuousOfShapeCategoryTheory.Limits.PreservesColimitsOfShape