Theorems · Inductive type · category theory

HomotopicalAlgebra.ReedyStructure

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W₁ W₂ : CategoryTheory.MorphismProperty C) →
      [W₁.IsMultiplicative] →
        [W₂.IsMultiplicative] →
          (α : Type u_2) →
            [inst : LinearOrder α] → [OrderBot α] → [SuccOrder α] → [WellFoundedLT α] → Type (max u_1 u_2)

A Reedy structure on a category C equipped with two multiplicative classes of morphisms W₁ and W₂ consists of the data of a degree map for objects deg : C → α, where α is a well ordered type. The first two axioms lt₁ and lt₂ express the behaviour of the degree with respect to morphisms in W₁ (resp. W₂) that are not identities, and the last axiom says that any morphism can be factored in a unique way as a morphism in W₁ followed by a morphism in W₂.

Defined in

Mathlib.AlgebraicTopology.Reedy.Basic

Cited by

30 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicativeCategoryTheory.MorphismProperty.IsMultiplicativeLinearOrderOrderBotSuccOrderWellFoundedLT