Theorems · Definition · category theory

CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.transfiniteCompositionOfShapeMapFromBot

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : C} →
      [inst_1 : CategoryTheory.Abelian C] →
        (hG : CategoryTheory.IsSeparator G) →
          {X : C} →
            [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] →
              (A₀ : CategoryTheory.Subobject X) →
                {J : Type w} →
                  [inst_3 : LinearOrder J] →
                    [inst_4 : OrderBot J] →
                      [inst_5 : SuccOrder J] →
                        [inst_6 : WellFoundedLT J] →
                          (j : J) →
                            (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms
                                    G).pushouts.TransfiniteCompositionOfShape
                              (↑(Set.Iic j))
                              ((CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functor hG A₀ J).map
                                (CategoryTheory.homOfLE ⋯))

For any j, the map (functor hG A₀ J).map (homOfLE bot_le : ⊥ ⟶ j) is a transfinite composition of pushouts of monomorphisms in the family generatingMonomorphisms G.

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.IsGrothendieckAbelianLinearOrderOrderBotSuccOrderWellFoundedLT