The covariant involution of the simplex category

In this file, we introduce the functor rev : SimplexCategory ⥤ SimplexCategory which, via the equivalence between the simplex category and the category of nonempty finite linearly ordered types, corresponds to the covariant functor which sends a type α to αᵒᵈ.

def SimplexCategory.rev : CategoryTheory.Functor SimplexCategory SimplexCategory

The covariant involution rev : SimplexCategory ⥤ SimplexCategory which, via the equivalence between the simplex category and the category of nonempty finite linearly ordered types, corresponds to the covariant functor which sends a type α to αᵒᵈ. This functor sends the object ⦋n⦌ to ⦋n⦌ and a map f : ⦋n⦌ ⟶ ⦋m⦌ is sent to the monotone map (i : Fin (n + 1)) ↦ (f i.rev).rev.

@[simp]

theorem SimplexCategory.rev_obj (n : SimplexCategory) : rev.obj n = n

@[simp]

theorem SimplexCategory.rev_map_apply {n m : SimplexCategory} (f : n ⟶ m) (i : Fin (n.len + 1)) : (Hom.toOrderHom (rev.map f)) i = ((Hom.toOrderHom f) i.rev).rev

@[simp]

theorem SimplexCategory.rev_map_δ {n : ℕ} (i : Fin (n + 2)) : rev.map (δ i) = δ i.rev

@[simp]

theorem SimplexCategory.rev_map_σ {n : ℕ} (i : Fin (n + 1)) : rev.map (σ i) = σ i.rev

def SimplexCategory.revCompRevIso : rev.comp rev ≅ CategoryTheory.Functor.id SimplexCategory

The functor SimplexCategory.rev : SimplexCategory ⥤ SimplexCategory is a covariant involution.

@[simp]

theorem SimplexCategory.revCompRevIso_inv_app (X : SimplexCategory) : revCompRevIso.inv.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem SimplexCategory.revCompRevIso_hom_app (X : SimplexCategory) : revCompRevIso.hom.app X = CategoryTheory.CategoryStruct.id X

@[simp]

theorem SimplexCategory.rev_map_rev_map {n m : SimplexCategory} (f : n ⟶ m) : rev.map (rev.map f) = f

def SimplexCategory.revEquivalence : SimplexCategory ≌ SimplexCategory

The functor SimplexCategory.rev : SimplexCategory ⥤ SimplexCategory as an equivalence of category.

@[simp]

theorem SimplexCategory.revEquivalence_unitIso : revEquivalence.unitIso = revCompRevIso.symm

@[simp]

theorem SimplexCategory.revEquivalence_counitIso : revEquivalence.counitIso = revCompRevIso

@[simp]

theorem SimplexCategory.revEquivalence_inverse : revEquivalence.inverse = rev

@[simp]

theorem SimplexCategory.revEquivalence_functor : revEquivalence.functor = rev