Epi-mono factorization in the simplex category presented by generators and relations

This file aims to establish that there is a nice epi-mono factorization in SimplexCategoryGenRel. More precisely, we introduce two morphism properties P_δ and P_σ that single out morphisms that are compositions of δ i (resp. σ i).

The main result of this file is exists_P_σ_P_δ_factorization, which asserts that every morphism as a decomposition of a P_σ followed by a P_δ.

def SimplexCategoryGenRel.splitMonoδ {n : ℕ} (i : Fin (n + 2)) : CategoryTheory.SplitMono (δ i)

δ i is a split monomorphism thanks to the simplicial identities.

instance SimplexCategoryGenRel.instIsSplitMonoδ {n : ℕ} {i : Fin (n + 2)} : CategoryTheory.IsSplitMono (δ i)

def SimplexCategoryGenRel.splitEpiσ {n : ℕ} (i : Fin (n + 1)) : CategoryTheory.SplitEpi (σ i)

δ i is a split epimorphism thanks to the simplicial identities.

instance SimplexCategoryGenRel.instIsSplitEpiσ {n : ℕ} {i : Fin (n + 1)} : CategoryTheory.IsSplitEpi (σ i)

@[reducible, inline]

abbrev SimplexCategoryGenRel.P_σ : CategoryTheory.MorphismProperty SimplexCategoryGenRel

Auxiliary predicate to express that a morphism is purely a composition of σ is.

@[reducible, inline]

abbrev SimplexCategoryGenRel.P_δ : CategoryTheory.MorphismProperty SimplexCategoryGenRel

Auxiliary predicate to express that a morphism is purely a composition of δ is.

theorem SimplexCategoryGenRel.P_σ.σ {n : ℕ} (i : Fin (n + 1)) : P_σ (SimplexCategoryGenRel.σ i)

theorem SimplexCategoryGenRel.P_δ.δ {n : ℕ} (i : Fin (n + 2)) : P_δ (SimplexCategoryGenRel.δ i)

theorem SimplexCategoryGenRel.isSplitEpi_P_σ {x y : SimplexCategoryGenRel} {e : x ⟶ y} (he : P_σ e) : CategoryTheory.IsSplitEpi e

All P_σ are split epis as composition of such.

theorem SimplexCategoryGenRel.isSplitMono_P_δ {x y : SimplexCategoryGenRel} {m : x ⟶ y} (hm : P_δ m) : CategoryTheory.IsSplitMono m

All P_δ are split monos as composition of such.

theorem SimplexCategoryGenRel.isSplitEpi_toSimplexCategory_map_of_P_σ {x y : SimplexCategoryGenRel} {e : x ⟶ y} (he : P_σ e) : CategoryTheory.IsSplitEpi (toSimplexCategory.map e)

theorem SimplexCategoryGenRel.isSplitMono_toSimplexCategory_map_of_P_δ {x y : SimplexCategoryGenRel} {m : x ⟶ y} (hm : P_δ m) : CategoryTheory.IsSplitMono (toSimplexCategory.map m)

theorem SimplexCategoryGenRel.eq_or_len_le_of_P_δ {x y : SimplexCategoryGenRel} {f : x ⟶ y} (h_δ : P_δ f) : (∃ (h : x = y), f = CategoryTheory.eqToHom h) ∨ x.len < y.len

theorem SimplexCategoryGenRel.exists_P_σ_P_δ_factorization {x y : SimplexCategoryGenRel} (f : x ⟶ y) : ∃ (z : SimplexCategoryGenRel) (e : x ⟶ z) (m : z ⟶ y) (_ : P_σ e) (_ : P_δ m), f = CategoryTheory.CategoryStruct.comp e m

Any morphism in SimplexCategoryGenRel can be decomposed as a P_σ followed by a P_δ.

instance SimplexCategoryGenRel.instHasFactorizationP_σP_δ : P_σ.HasFactorization P_δ