initial_incl — Mathlib

English

If 0 < n ≤ m, then the inclusion incl_n_m from the n-truncated simplex category to the m-truncated simplex category is initial.

Русский

Если 0 < n ≤ m, то включение incl_n_m из n-усеченной симплициальной категории в m-усеченную начально.

LaTeX

$$$$ \operatorname{Initial}(\mathrm{incl}_{n,m}) $$$$

Lean4

/-- For `0 < n ≤ m`, the inclusion functor from the `n`-truncated simplex category to the
`m`-truncated simplex category is initial. -/
theorem initial_incl {n m : ℕ} [NeZero n] (hm : n ≤ m) : (incl n m).Initial :=
  by
  have : (incl n m hm ⋙ inclusion m).Initial := Functor.initial_of_natIso (inclCompInclusion _).symm
  apply Functor.initial_of_comp_full_faithful _ (inclusion m)

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