Theorems · Theorem · category theory

HomotopicalAlgebra.ReedyStructure.exists_fac

∀ {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 α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y),
  ∃ Z a b, W₁ a ∧ W₂ b ∧ CategoryTheory.CategoryStruct.comp a b = f ∧ r.degHom f = r.deg Z

Defined in

Mathlib.AlgebraicTopology.Reedy.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsMultiplicativeCategoryTheory.MorphismProperty.IsMultiplicativeLinearOrderOrderBotSuccOrderWellFoundedLT