The Reedy structure on the simplex category

In this file, we show that for the simplex category equipped with the classes of epimorphisms and monomorphisms, the length map SimplexCategory → ℕ is the degree map of a Reedy structure.

References

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

instance SimplexCategory.instSubsingletonMapFactorizationDataEpimorphismsMonomorphisms {x y : SimplexCategory} (f : x ⟶ y) : Subsingleton ((CategoryTheory.MorphismProperty.epimorphisms SimplexCategory).MapFactorizationData (CategoryTheory.MorphismProperty.monomorphisms SimplexCategory) f)

@[implicit_reducible]

def SimplexCategory.reedyStructure : HomotopicalAlgebra.ReedyStructure (CategoryTheory.MorphismProperty.epimorphisms SimplexCategory) (CategoryTheory.MorphismProperty.monomorphisms SimplexCategory) ℕ

The Reedy structure on the simplex category.

Equations

• SimplexCategory.reedyStructure = { deg := SimplexCategory.len, lt₁ := @SimplexCategory.reedyStructure._proof_4, lt₂ := @SimplexCategory.reedyStructure._proof_5, nonempty_unique := ⋯ }

@[simp]

theorem SimplexCategory.reedyStructure_deg (self : SimplexCategory) : reedyStructure.deg self = self.len