II — Mathlib · SciLib

Lean4
/-- The functor `SimplexCategory ⥤ SimplexCategoryᵒᵖ` (i.e. a cosimplicial
object in `SimplexCategoryᵒᵖ`) which sends `⦋n⦌` to the object in `SimplexCategoryᵒᵖ`
that is associated to the linearly ordered type `⦋n + 1⦌` (which could be
identified to the ordered type `⦋n⦌ →o ⦋1⦌`). -/
@[simps obj]
def II : CosimplicialObject SimplexCategoryᵒᵖ
    where
  obj n := op ⦋n.len + 1⦌
  map
    f :=
    op
      (Hom.mk
        { toFun := II.map' f.toOrderHom
          monotone' := II.monotone_map' _ })
  map_id
    n :=
    Quiver.Hom.unop_inj
      (by
        ext x : 3
        exact II.map'_id x)
  map_comp {m n p} f
    g :=
    Quiver.Hom.unop_inj
      (by
        ext x : 3
        exact (II.map'_map' _ _ _).symm)
Похожие утверждения