Theorems · Definition · category theory

HomotopicalAlgebra.RelativeCellComplex.transfiniteCompositionOfShape

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          [inst_3 : SuccOrder J] →
            [inst_4 : WellFoundedLT J] →
              {X Y : C} →
                {f : X ⟶ Y} →
                  {α : Type u_1} →
                    {A B : α → C} →
                      (g : (i : α) → A i ⟶ B i) →
                        HomotopicalAlgebra.RelativeCellComplex (fun x => g) f →
                          (CategoryTheory.MorphismProperty.coproducts.{w, v, u}
                                  (CategoryTheory.MorphismProperty.ofHoms g)).pushouts.TransfiniteCompositionOfShape
                            J f

If f is a relative cell complex with respect to a constant family of morphisms g, then f is a transfinite composition of pushouts of coproducts of morphisms in the family g.

Defined in

Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryLinearOrderOrderBotSuccOrderWellFoundedLT