Documentation

Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

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 moprhism as a decomposition of a P_σ followed by a P_δ.

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

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

Equations
    Instances For
      source
      instance SimplexCategoryGenRel.instIsSplitMonoδ {n : ℕ} {i : Fin (n + 2)} :
      CategoryTheory.IsSplitMono (δ i)
      source
      def SimplexCategoryGenRel.splitEpiσ {n : ℕ} (i : Fin (n + 1)) :
      CategoryTheory.SplitEpi (σ i)

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

      Equations
        Instances For
          source
          instance SimplexCategoryGenRel.instIsSplitEpiσ {n : ℕ} {i : Fin (n + 1)} :
          CategoryTheory.IsSplitEpi (σ i)
          source
          @[reducible, inline]
          abbrev SimplexCategoryGenRel.P_σ :
          CategoryTheory.MorphismProperty SimplexCategoryGenRel

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

          Equations
            Instances For
              source
              @[reducible, inline]
              abbrev SimplexCategoryGenRel.P_δ :
              CategoryTheory.MorphismProperty SimplexCategoryGenRel

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

              Equations
                Instances For
                  source
                  theorem SimplexCategoryGenRel.P_σ.σ {n : ℕ} (i : Fin (n + 1)) :
                  P_σ (SimplexCategoryGenRel.σ i)
                  source
                  theorem SimplexCategoryGenRel.P_δ.δ {n : ℕ} (i : Fin (n + 2)) :
                  P_δ (SimplexCategoryGenRel.δ i)
                  source
                  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.

                  source
                  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.

                  source
                  theorem SimplexCategoryGenRel.isSplitEpi_toSimplexCategory_map_of_P_σ {x y : SimplexCategoryGenRel} {e : x ⟶ y} (he : P_σ e) :
                  CategoryTheory.IsSplitEpi (toSimplexCategory.map e)
                  source
                  theorem SimplexCategoryGenRel.isSplitMono_toSimplexCategory_map_of_P_δ {x y : SimplexCategoryGenRel} {m : x ⟶ y} (hm : P_δ m) :
                  CategoryTheory.IsSplitMono (toSimplexCategory.map m)
                  source
                  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
                  source
                  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_δ.

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