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 = ⊤.
This statement is deduced from a similar statement for
the category SimplexCategory.Truncated d.
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 = ⊤
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 = ⊤