Theorems · Definition · category theory

CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.transfiniteCompositionOfShapeOfEqTop

{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 : C} →
                {f : A ⟶ X} →
                  [inst_3 : CategoryTheory.Mono f] →
                    {J : Type w} →
                      [inst_4 : LinearOrder J] →
                        [inst_5 : OrderBot J] →
                          [inst_6 : SuccOrder J] →
                            [inst_7 : WellFoundedLT J] →
                              {j : J} →
                                transfiniteIterate
                                      (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject hG)
                                      j (CategoryTheory.Subobject.mk f) =
                                    ⊤ →
                                  (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms
                                          G).pushouts.TransfiniteCompositionOfShape
                                    (↑(Set.Iic j)) f

If transfiniteIterate (largerSubobject hG) j (Subobject.mk f) = ⊤, then the monomorphism f is a transfinite composition of pushouts of monomorphisms in the family generatingMonomorphisms G.

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.AbelianCategoryTheory.IsGrothendieckAbelianCategoryTheory.MonoLinearOrderOrderBotSuccOrderWellFoundedLT