Theorems · Definition · category theory

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.

Defined in

Mathlib.AlgebraicTopology.SimplexCategory.Rev

Cited by

18 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Quot.sound