Properties of morphisms in the simplex category

In this file, we show that morphisms in the simplex category are generated by faces and degeneracies. This is stated by saying that if W : MorphismProperty SimplexCategory is multiplicative, and contains faces and degeneracies, then W = ⊤. We first prove the stamentes in SimplexCategory.Truncated d, and then in SimplexCategory

theorem SimplexCategory.Truncated.mono_induction {d : ℕ} {motive : CategoryTheory.MorphismProperty (Truncated d)} (id : ∀ (x : Truncated d), motive (CategoryTheory.CategoryStruct.id x)) (comp_δ : ∀ {x y : Truncated d} (f : x ⟶ y) (hy : y.obj.len < d) (i : Fin (y.obj.len + 2)), motive f → motive (CategoryTheory.CategoryStruct.comp f (δ d i ⋯ hy))) {x y : Truncated d} (f : x ⟶ y) [hf : CategoryTheory.Mono f] : motive f

In the truncated simplex category, a property of morphisms which holds for identities and is stable under postcomposition with faces holds for all monomorphisms.

theorem SimplexCategory.Truncated.epi_induction {d : ℕ} {motive : CategoryTheory.MorphismProperty (Truncated d)} (id : ∀ (x : Truncated d), motive (CategoryTheory.CategoryStruct.id x)) (σ_comp : ∀ {x y : Truncated d} (f : x ⟶ y) (hx : x.obj.len < d) (i : Fin (x.obj.len + 1)), motive f → motive (CategoryTheory.CategoryStruct.comp (σ d i hx ⋯) f)) {x y : Truncated d} (f : x ⟶ y) [hf : CategoryTheory.Epi f] : motive f

In the truncated simplex category, a property of morphisms which holds for identities and is stable under precomposition with degeneracies holds for all epimorphisms.

theorem SimplexCategory.Truncated.morphismProperty_eq_top {d : ℕ} (W : CategoryTheory.MorphismProperty (Truncated d)) [W.IsMultiplicative] (δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)) (σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)) : W = ⊤

Morphisms in Truncated d are generated by faces and degeneracies.

theorem SimplexCategory.mono_induction {motive : CategoryTheory.MorphismProperty SimplexCategory} (id : ∀ (x : SimplexCategory), motive (CategoryTheory.CategoryStruct.id x)) (comp_δ : ∀ {x y : SimplexCategory} (f : x ⟶ y) (i : Fin (y.len + 2)), motive f → motive (CategoryTheory.CategoryStruct.comp f (δ i))) {x y : SimplexCategory} (f : x ⟶ y) [hf : CategoryTheory.Mono f] : motive f

A property of morphisms which holds for identities and is stable under postcomposition with faces holds for all monomorphisms.

theorem SimplexCategory.epi_induction {motive : CategoryTheory.MorphismProperty SimplexCategory} (id : ∀ (x : SimplexCategory), motive (CategoryTheory.CategoryStruct.id x)) (σ_comp : ∀ {x y : SimplexCategory} (f : x ⟶ y) (i : Fin (x.len + 1)), motive f → motive (CategoryTheory.CategoryStruct.comp (σ i) f)) {x y : SimplexCategory} (f : x ⟶ y) [hf : CategoryTheory.Epi f] : motive f

A property of morphisms which holds for identities and is stable under precomposition with degeneracies holds for all epimorphisms.

theorem SimplexCategory.morphismProperty_eq_top (W : CategoryTheory.MorphismProperty SimplexCategory) [W.IsMultiplicative] (δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)) (σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)) : W = ⊤

Morphisms in SimplexCategory are generated by faces and degeneracies.