Theorems · Definition · category theory

HomotopicalAlgebra.ReedyStructure.degHom

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      [inst_1 : W₁.IsMultiplicative] →
        [inst_2 : W₂.IsMultiplicative] →
          {α : Type u_2} →
            [inst_3 : LinearOrder α] →
              [inst_4 : OrderBot α] →
                [inst_5 : SuccOrder α] →
                  [inst_6 : WellFoundedLT α] → HomotopicalAlgebra.ReedyStructure W₁ W₂ α → {X Y : C} → (X ⟶ Y) → α

The degree of a morphism for a Reedy structure. It is defined as the degree of the intermediate object in the Reedy factorization, but it is also the smallest degree of an intermediate object in a factorization, see the lemma degHom_le.

Defined in

Mathlib.AlgebraicTopology.Reedy.Basic

Cited by

13 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Classical.choice

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicativeCategoryTheory.MorphismProperty.IsMultiplicativeLinearOrderOrderBotSuccOrderWellFoundedLT