Theorems · Definition · category theory

HomotopicalAlgebra.RelativeCellComplex.attachCells

{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] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  {basicCell : (j : J) → (i : α j) → A j i ⟶ B j i} →
                    {X Y : C} →
                      {f : X ⟶ Y} →
                        (self : HomotopicalAlgebra.RelativeCellComplex basicCell f) →
                          (j : J) →
                            ¬IsMax j →
                              HomotopicalAlgebra.AttachCells (basicCell j) (self.F.map (CategoryTheory.homOfLE ⋯))

If j is not the maximum element, F.obj (Order.succ j) is obtained from F.obj j by attaching cells in the family of morphisms basicCell j.

Defined in

Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Cited by

15 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext

Assumes

CategoryTheory.CategoryLinearOrderOrderBotSuccOrderWellFoundedLT