Theorems · Inductive type · category theory

HomotopicalAlgebra.RelativeCellComplex

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w'} →
      [inst_1 : LinearOrder J] →
        [OrderBot J] →
          [SuccOrder J] →
            [WellFoundedLT J] →
              {α : J → Type t} →
                {A B : (j : J) → α j → C} →
                  ((j : J) → (i : α j) → A j i ⟶ B j i) →
                    {X Y : C} → (X ⟶ Y) → Type (max (max (max (max t u) v) (w + 1)) w')

Let J be a well-ordered type. Assume that for each j : J, we have a family basicCell j of morphisms. A relative cell complex is a morphism f : X ⟶ Y which is a transfinite composition of morphisms in such a way that at the step j : J, we attach cells in the family basicCell j.

Defined in

Mathlib.AlgebraicTopology.RelativeCellComplex.Basic

Cited by

12 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

CategoryTheory.CategoryLinearOrderOrderBotSuccOrderWellFoundedLT