rev — Mathlib

Lean4
/-- 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`. -/
@[simps obj]
def rev : SimplexCategory ⥤ SimplexCategory where
  obj n := n
  map {n m}
    f :=
    Hom.mk
      ⟨fun i ↦ (f i.rev).rev, fun i j hij ↦ by
        rw [Fin.rev_le_rev]
        exact f.toOrderHom.monotone (by rwa [Fin.rev_le_rev])⟩
Похожие утверждения