The simplex category #
We construct a skeletal model of the simplex category, with objects ℕ
and the
morphisms n ⟶ m
being the monotone maps from Fin (n + 1)
to Fin (m + 1)
.
In Mathlib.AlgebraicTopology.SimplexCategory.Basic
, we show that this category
is equivalent to NonemptyFinLinOrd
.
Remarks #
The definitions SimplexCategory
and SimplexCategory.Hom
are marked as irreducible.
We provide the following functions to work with these objects:
SimplexCategory.mk
creates an object ofSimplexCategory
out of a natural number. Use the notation⦋n⦌
in theSimplicial
locale.SimplexCategory.len
gives the "length" of an object ofSimplexCategory
, as a natural.SimplexCategory.Hom.mk
makes a morphism out of a monotone map betweenFin
's.SimplexCategory.Hom.toOrderHom
gives the underlying monotone map associated to a term ofSimplexCategory.Hom
.
Notations #
⦋n⦌
denotes then
-dimensional simplex. This notation is available withopen Simplicial
.⦋m⦌ₙ
denotes them
-dimensional simplex in then
-truncated simplex category. The truncation proofp : m ≤ n
can also be provided using the syntax⦋m, p⦌ₙ
. This notation is available withopen SimplexCategory.Truncated
.
Interpret a natural number as an object of the simplex category.
Equations
- SimplexCategory.mk n = n
Instances For
the n
-dimensional simplex can be denoted ⦋n⦌
Equations
- One or more equations did not get rendered due to their size.
Instances For
The length of an object of SimplexCategory
.
Instances For
A recursor for SimplexCategory
. Use it as induction Δ using SimplexCategory.rec
.
Equations
- SimplexCategory.rec h n = h n.len
Instances For
Make a morphism in SimplexCategory
from a monotone map of Fin
's.
Equations
Instances For
Recover the monotone map from a morphism in the simplex category.
Equations
- f.toOrderHom = f
Instances For
Composition of morphisms of SimplexCategory
.
Equations
- f.comp g = SimplexCategory.Hom.mk (f.toOrderHom.comp g.toOrderHom)
Instances For
The truncated simplex category.
Equations
- SimplexCategory.Truncated n = CategoryTheory.FullSubcategory fun (a : SimplexCategory) => a.len ≤ n
Instances For
Equations
Equations
- SimplexCategory.Truncated.instInhabited = { default := { obj := SimplexCategory.mk 0, property := ⋯ } }
The fully faithful inclusion of the truncated simplex category into the usual simplex category.
Equations
- SimplexCategory.Truncated.inclusion n = CategoryTheory.fullSubcategoryInclusion fun (a : SimplexCategory) => a.len ≤ n
Instances For
A proof that the full subcategory inclusion is fully faithful
Equations
Instances For
For m ≤ n
, ⦋m⦌ₙ
is the m
-dimensional simplex in Truncated n
. The
proof p : m ≤ n
can also be provided using the syntax ⦋m, p⦌ₙ
.
Equations
- One or more equations did not get rendered due to their size.