The semi-simplex category

We define a category SemiSimplexCategory so that semi-simplicial objects can be defined (TODO) as functors from SemiSimplexCategoryᵒᵖ similarly as simplicial objects are functors from SimplexCategory.

structure SemiSimplexCategory : Type

The category whose objects are denoted ⦋n⦌ₛ for n : ℕ and morphisms ⦋n⦌ₛ ⟶ ⦋m⦌ₛ are order embeddings Fin (n.len + 1) ↪o Fin (m.len + 1). (This identifies to a wide subcategory of the category SemiSimplex, which has the "same" objects, and morphisms Fin (n.len + 1) →o Fin (m.len + 1), see the faithful functor SemiSimplexCategory.toSimplexCategory.)

• len : ℕ

  The length of an object in SemiSimplexCategory

theorem SemiSimplexCategory.ext_iff {x y : SemiSimplexCategory} : x = y ↔ x.len = y.len

theorem SemiSimplexCategory.ext {x y : SemiSimplexCategory} (len : x.len = y.len) : x = y

def Simplicial.«term⦋_⦌ₛ» : Lean.ParserDescr

The object of SemiSimplexCategory corresponding to n : ℕ is denoted ⦋n⦌ₛ.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def SemiSimplexCategory.Hom (n m : SemiSimplexCategory) : Type

The type of morphisms in the semi-simplex category are order embeddings. This type is made irreducible: use SemiSimplexCategory.homEquiv to make the conversion.

Equations

• n.Hom m = (Fin (n.len + 1) ↪o Fin (m.len + 1))

@[implicit_reducible]

instance SemiSimplexCategory.smallCategory : CategoryTheory.SmallCategory SemiSimplexCategory

Equations

• One or more equations did not get rendered due to their size.

def SemiSimplexCategory.homEquiv {n m : SemiSimplexCategory} : (n ⟶ m) ≃ (Fin (n.len + 1) ↪o Fin (m.len + 1))

Morphisms n ⟶ m in SemiSimplexCategory identify to order embeddings Fin (n.len + 1) ↪o Fin (m.len + 1).

Equations

• SemiSimplexCategory.homEquiv = Equiv.refl (n ⟶ m)

@[simp]

theorem SemiSimplexCategory.homEquiv_id (a : SemiSimplexCategory) : homEquiv (CategoryTheory.CategoryStruct.id a) = RelEmbedding.refl fun (x1 x2 : Fin (a.len + 1)) => x1 ≤ x2

@[simp]

theorem SemiSimplexCategory.homEquiv_comp {a b c : SemiSimplexCategory} (f : a ⟶ b) (g : b ⟶ c) : homEquiv (CategoryTheory.CategoryStruct.comp f g) = RelEmbedding.trans (homEquiv f) (homEquiv g)

theorem SemiSimplexCategory.hom_ext {a b : SemiSimplexCategory} {f g : a ⟶ b} (h : homEquiv f = homEquiv g) : f = g

theorem SemiSimplexCategory.hom_ext_iff {a b : SemiSimplexCategory} {f g : a ⟶ b} : f = g ↔ homEquiv f = homEquiv g

def SemiSimplexCategory.toSimplexCategory : CategoryTheory.Functor SemiSimplexCategory SimplexCategory

The inclusion functor SemiSimplexCategory ⥤ SimplexCategory.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SemiSimplexCategory.toSimplexCategory_obj (n : ℕ) : toSimplexCategory.obj { len := n } = { len := n }

instance SemiSimplexCategory.instFaithfulSimplexCategoryToSimplexCategory : toSimplexCategory.Faithful

instance SemiSimplexCategory.instMonoSimplexCategoryMapToSimplexCategory {n m : SemiSimplexCategory} (f : n ⟶ m) : CategoryTheory.Mono (toSimplexCategory.map f)

instance SemiSimplexCategory.instMono {n m : SemiSimplexCategory} (f : n ⟶ m) : CategoryTheory.Mono f

def SemiSimplexCategory.homOfMono {n m : SemiSimplexCategory} (f : toSimplexCategory.obj n ⟶ toSimplexCategory.obj m) [CategoryTheory.Mono f] : n ⟶ m

Constructor for morphisms in SemiSimplexCategory which takes as an input a monomorphism in SimplexCategory.

Equations

• SemiSimplexCategory.homOfMono f = SemiSimplexCategory.homEquiv.symm (OrderEmbedding.ofStrictMono ⇑(SimplexCategory.Hom.toOrderHom f) ⋯)

@[simp]

theorem SemiSimplexCategory.toSimplexCategory_map_homOfMono {n m : SemiSimplexCategory} (f : toSimplexCategory.obj n ⟶ toSimplexCategory.obj m) [CategoryTheory.Mono f] : toSimplexCategory.map (homOfMono f) = f