map_id — Mathlib

English

The standard simplex functor maps the identity at n to the identity, i.e., SSet.stdSimplex.map id = 𝟙 on each object.

Русский

Функтор \text{stdSimplex} отображает тождественный морфин, то есть SSet.stdSimplex.map id = 𝟙 на каждом объекте.

LaTeX

$$$SSet.stdSimplex.map\ ((OrderHom.id) : n ⟶ n) = 𝟙$$$

Lean4

@[simp]
theorem map_id (n : SimplexCategory) : (SSet.stdSimplex.map (SimplexCategory.Hom.mk OrderHom.id : n ⟶ n)) = 𝟙 _ :=
  CategoryTheory.Functor.map_id _ _

Похожие утверждения