Reedy categories

In this file, we introduce the definition of a Reedy structure on a category C equipped with two classes of morphisms W₁ and W₂ (these are sometimes denoted C₋ and C₊ in the literature).

TODO

• Construct the Reedy model category structure on the category of functors C ⥤ D when C is a Reedy category and D a model category https://github.com/leanprover-community/project-intentions/issues/5

References

• Emily Riehl and Dominic Verity, Elements of ∞-Category Theory, C.4

structure HomotopicalAlgebra.ReedyStructure {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) [W₁.IsMultiplicative] [W₂.IsMultiplicative] (α : Type u_2) [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₂.

• deg : C → α

  the degree of an object

• lt₁ {X Y : C} (f : X ⟶ Y) (hf : W₁ f) (hf' : ¬CategoryTheory.MorphismProperty.identities C f) : self.deg Y < self.deg X
• lt₂ {X Y : C} (f : X ⟶ Y) (hf : W₂ f) (hf' : ¬CategoryTheory.MorphismProperty.identities C f) : self.deg X < self.deg Y
• nonempty_unique {X Y : C} (f : X ⟶ Y) : Nonempty (Unique (W₁.MapFactorizationData W₂ f))

def HomotopicalAlgebra.ReedyStructure.op {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) : ReedyStructure W₂.op W₁.op α

The opposite of a Reedy structure.

Equations

• r.op = { deg := r.deg ∘ Opposite.unop, lt₁ := ⋯, lt₂ := ⋯, nonempty_unique := ⋯ }

@[simp]

theorem HomotopicalAlgebra.ReedyStructure.op_deg {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) (a✝ : Cᵒᵖ) : r.op.deg a✝ = (r.deg ∘ Opposite.unop) a✝

theorem HomotopicalAlgebra.ReedyStructure.le₁ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y) (hf : W₁ f) : r.deg Y ≤ r.deg X

theorem HomotopicalAlgebra.ReedyStructure.le₂ {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y) (hf : W₂ f) : r.deg X ≤ r.deg Y

theorem HomotopicalAlgebra.ReedyStructure.identities_of_prop₁_of_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y} (hf : W₁ f) (h : r.deg X = r.deg Y) : CategoryTheory.MorphismProperty.identities C f

theorem HomotopicalAlgebra.ReedyStructure.identities_of_prop₂_of_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y} (hf : W₂ f) (h : r.deg X = r.deg Y) : CategoryTheory.MorphismProperty.identities C f

theorem HomotopicalAlgebra.ReedyStructure.subsingleton_mapFactorizationData {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) ⦃X Y : C⦄ (f : X ⟶ Y) : Subsingleton (W₁.MapFactorizationData W₂ f)

noncomputable def HomotopicalAlgebra.ReedyStructure.mapFactorizationData {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y) : W₁.MapFactorizationData W₂ f

The Reedy factorization of a morphism f : X ⟶ Y as a morphism in W₁ followed by a morphism in W₂.

Equations

• r.mapFactorizationData f = default

theorem HomotopicalAlgebra.ReedyStructure.unique_obj {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y} (fac fac' : W₁.MapFactorizationData W₂ f) : fac.Z = fac'.Z

theorem HomotopicalAlgebra.ReedyStructure.unique {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y} (fac fac' : W₁.MapFactorizationData W₂ f) : ∃ (h : fac.Z = fac'.Z), fac.i = CategoryTheory.CategoryStruct.comp fac'.i (CategoryTheory.eqToHom ⋯) ∧ fac.p = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) fac'.p

noncomputable def HomotopicalAlgebra.ReedyStructure.degHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y) : α

The degree of a morphisms 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.

Equations

• r.degHom f = r.deg (r.mapFactorizationData f).Z

theorem HomotopicalAlgebra.ReedyStructure.degHom_eq {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y} (h : W₁.MapFactorizationData W₂ f) : r.degHom f = r.deg h.Z

theorem HomotopicalAlgebra.ReedyStructure.exists_fac {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y) : ∃ (Z : C) (a : X ⟶ Z) (b : Z ⟶ Y), W₁ a ∧ W₂ b ∧ CategoryTheory.CategoryStruct.comp a b = f ∧ r.degHom f = r.deg Z

theorem HomotopicalAlgebra.ReedyStructure.degHom_le {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Z Y : C} (f : X ⟶ Z) (g : Z ⟶ Y) : r.degHom (CategoryTheory.CategoryStruct.comp f g) ≤ r.deg Z

theorem HomotopicalAlgebra.ReedyStructure.degHom_le_deg_left {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y) : r.degHom f ≤ r.deg X

theorem HomotopicalAlgebra.ReedyStructure.degHom_le_deg_right {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} (f : X ⟶ Y) : r.degHom f ≤ r.deg Y

theorem HomotopicalAlgebra.ReedyStructure.degHom_comp_le_left {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : r.degHom (CategoryTheory.CategoryStruct.comp f g) ≤ r.degHom f

theorem HomotopicalAlgebra.ReedyStructure.degHom_comp_le_right {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : r.degHom (CategoryTheory.CategoryStruct.comp f g) ≤ r.degHom g

theorem HomotopicalAlgebra.ReedyStructure.prop₂_of_degHom_eq_deg_left {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y} (hf : r.degHom f = r.deg X) : W₂ f

theorem HomotopicalAlgebra.ReedyStructure.prop₁_of_degHom_eq_deg_right {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y} (hf : r.degHom f = r.deg Y) : W₁ f

theorem HomotopicalAlgebra.ReedyStructure.degHom_lt_or_of_degHom_comp_lt {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Z Y : C} (f : X ⟶ Z) (g : Z ⟶ Y) (hfg : r.degHom (CategoryTheory.CategoryStruct.comp f g) < r.deg Z) : r.degHom f < r.deg Z ∨ r.degHom g < r.deg Z

@[simp]

theorem HomotopicalAlgebra.ReedyStructure.degHom_id {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) (X : C) : r.degHom (CategoryTheory.CategoryStruct.id X) = r.deg X

theorem HomotopicalAlgebra.ReedyStructure.deg_eq_of_iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} (e : X ≅ Y) : r.deg X = r.deg Y

theorem HomotopicalAlgebra.ReedyStructure.prop₁_of_iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} (e : X ≅ Y) : W₁ e.hom

theorem HomotopicalAlgebra.ReedyStructure.prop₂_of_iso {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) {X Y : C} (e : X ≅ Y) : W₂ e.hom

theorem HomotopicalAlgebra.ReedyStructure.skeletal {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} [W₁.IsMultiplicative] [W₂.IsMultiplicative] {α : Type u_2} [LinearOrder α] [OrderBot α] [SuccOrder α] [WellFoundedLT α] (r : ReedyStructure W₁ W₂ α) : CategoryTheory.Skeletal C