mkHom — Mathlib

English

There is a morphism in SimplexCategory corresponding to every order-preserving map between Fin-sets, obtained by the mk f construction.

Русский

Существует морфизм в SimplexCategory, соответствующий каждому сохраному порядку отображения между конечными множествами, получаемый конструктором mk f.

LaTeX

$$$\\text{mkHom}(f) = \\text{SimplexCategory.Hom.mk}(f).$$$

Lean4

/-- Make a morphism `⦋n⦌ ⟶ ⦋m⦌` from a monotone map between fin's.
This is useful for constructing morphisms between `⦋n⦌` directly
without identifying `n` with `⦋n⦌.len`.
-/
@[simp]
def mkHom {n m : ℕ} (f : Fin (n + 1) →o Fin (m + 1)) : ⦋n⦌ ⟶ ⦋m⦌ :=
  SimplexCategory.Hom.mk f

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