mathlib documentation

algebraic_topology.simplex_category

The simplex category #

We construct a skeletal model of the simplex category, with objects and the morphism n ⟶ m being the monotone maps from fin (n+1) to fin (m+1).

We show that this category is equivalent to NonemptyFinLinOrd.

Remarks #

The definitions simplex_category and simplex_category.hom are marked as irreducible.

We provide the following functions to work with these objects:

  1. simplex_category.mk creates an object of simplex_category out of a natural number. Use the notation [n] in the simplicial locale.
  2. simplex_category.len gives the "length" of an object of simplex_category, as a natural.
  3. simplex_category.hom.mk makes a morphism out of a monotone map between fin's.
  4. simplex_category.hom.to_order_hom gives the underlying monotone map associated to a term of simplex_category.hom.
@[irreducible]
def simplex_category  :
Type

The simplex category:

  • objects are natural numbers n : ℕ
  • morphisms from n to m are monotone functions fin (n+1) → fin (m+1)
Equations
Instances for simplex_category

Interpet a natural number as an object of the simplex category.

Equations

The length of an object of simplex_category.

Equations
@[ext]
theorem simplex_category.ext (a b : simplex_category) :
a.len = b.lena = b
@[simp]
@[protected]
def simplex_category.rec {F : simplex_categorySort u_1} (h : Π (n : ), F (simplex_category.mk n)) (X : simplex_category) :
F X

A recursor for simplex_category. Use it as induction Δ using simplex_category.rec.

Equations
@[protected, nolint, irreducible]

Morphisms in the simplex_category.

Equations
def simplex_category.hom.mk {a b : simplex_category} (f : fin (a.len + 1) →o fin (b.len + 1)) :
a.hom b

Make a moprhism in simplex_category from a monotone map of fin's.

Equations
def simplex_category.hom.to_order_hom {a b : simplex_category} (f : a.hom b) :
fin (a.len + 1) →o fin (b.len + 1)

Recover the monotone map from a morphism in the simplex category.

Equations
@[ext]
theorem simplex_category.hom.ext {a b : simplex_category} (f g : a.hom b) :
@[simp]
def simplex_category.hom.comp {a b c : simplex_category} (f : b.hom c) (g : a.hom b) :
a.hom c

Composition of morphisms of simplex_category.

Equations
@[protected, instance]
Equations
@[simp]
theorem simplex_category.small_category_comp (_x _x_1 _x_2 : simplex_category) (f : _x _x_1) (g : _x_1 _x_2) :
@[simp]

The constant morphism from [0].

Equations
@[simp]
theorem simplex_category.const_comp (x y : simplex_category) (i : fin (x.len + 1)) (f : x y) :
@[simp]

Make a morphism [n] ⟶ [m] from a monotone map between fin's. This is useful for constructing morphisms beetween [n] directly without identifying n with [n].len.

Equations

Generating maps for the simplex category #

TODO: prove that the simplex category is equivalent to one given by the following generators and relations.

The i-th face map from [n] to [n+1]

Equations
Instances for simplex_category.δ

The i-th degeneracy map from [n+1] to [n]

Equations
Instances for simplex_category.σ

The generic case of the first simplicial identity

The special case of the first simplicial identity

The first part of the third simplicial identity

The second part of the third simplicial identity

def simplex_category.truncated (n : ) :
Type

The truncated simplex category.

Equations
Instances for simplex_category.truncated

The fully faithful inclusion of the truncated simplex category into the usual simplex category.

Equations
Instances for simplex_category.truncated.inclusion
@[protected, instance]
Equations

A morphism in simplex_category is a monomorphism precisely when it is an injective function

A morphism in simplex_category is an epimorphism if and only if it is a surjective function

A monomorphism in simplex_category must increase lengths

An epimorphism in simplex_category must decrease lengths

@[protected, instance]
theorem simplex_category.eq_comp_δ_of_not_surjective' {n : } {Δ : simplex_category} (θ : Δ simplex_category.mk (n + 1)) (i : fin (n + 2)) (hi : ∀ (x : fin (Δ.len + 1)), (simplex_category.hom.to_order_hom θ) x i) :
∃ (θ' : Δ simplex_category.mk n), θ = θ' simplex_category.δ i
theorem simplex_category.image_eq {Δ Δ' Δ'' : simplex_category} {φ : Δ Δ''} {e : Δ Δ'} [category_theory.epi e] {i : Δ' Δ''} [category_theory.mono i] (fac : e i = φ) :
@[simp]