Documentation

Mathlib.AlgebraicTopology.SimplexCategory.Rev

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 αᵒᵈ.

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem SimplexCategory.rev_obj (n : SimplexCategory) :
    rev.obj n = n
    source
    @[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
    source
    @[simp]
    theorem SimplexCategory.rev_map_δ {n : ℕ} (i : Fin (n + 2)) :
    rev.map (δ i) = δ i.rev
    source
    @[simp]
    theorem SimplexCategory.rev_map_σ {n : ℕ} (i : Fin (n + 1)) :
    rev.map (σ i) = σ i.rev
    source
    def SimplexCategory.revCompRevIso :
    rev.comp rev ≅ CategoryTheory.Functor.id SimplexCategory

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem SimplexCategory.revCompRevIso_hom_app (X : SimplexCategory) :
      revCompRevIso.hom.app X = CategoryTheory.CategoryStruct.id X
      source
      @[simp]
      theorem SimplexCategory.revCompRevIso_inv_app (X : SimplexCategory) :
      revCompRevIso.inv.app X = CategoryTheory.CategoryStruct.id X
      source
      @[simp]
      theorem SimplexCategory.rev_map_rev_map {n m : SimplexCategory} (f : n ⟶ m) :
      rev.map (rev.map f) = f
      source
      def SimplexCategory.revEquivalence :
      SimplexCategory ≌ SimplexCategory

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem SimplexCategory.revEquivalence_counitIso :
        revEquivalence.counitIso = revCompRevIso
        source
        @[simp]
        theorem SimplexCategory.revEquivalence_functor :
        revEquivalence.functor = rev
        source
        @[simp]
        theorem SimplexCategory.revEquivalence_inverse :
        revEquivalence.inverse = rev
        source
        @[simp]
        theorem SimplexCategory.revEquivalence_unitIso :
        revEquivalence.unitIso = revCompRevIso.symm