objEquiv — Mathlib

English

There is a canonical bijection between (stdSimplex.obj n).obj m and morphisms m.unop ⟶ n, given by objEquiv.

Русский

Существует каноническая биекция между (stdSimplex.obj n).obj m и морфизмами m.unop ⟶ n, задаваемая objEquiv.

LaTeX

$$$(stdSimplex.obj n).obj m \cong (m.unop \to n)$ via $\text{objEquiv}$$$

Lean4

/-- Simplices of the standard simplex identify to morphisms in `SimplexCategory`. -/
def objEquiv {n : SimplexCategory} {m : SimplexCategoryᵒᵖ} : (stdSimplex.{u}.obj n).obj m ≃ (m.unop ⟶ n) :=
  Equiv.ulift.{u, 0}

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