inl'_eval — Mathlib

English

The left inclusion into a tensor product, evaluated at an index i, is given by a shift-by-one map on indices, matching the usual concatenation convention for sums of lengths.

Русский

Левое включение в тензорный произведение, оценённое на индекс i, задаётся сдвигом на единицу по индексам, соответствующим обычной конвенции сложения длин.

LaTeX

$$$(\\,\\text{inl}'\\, x \\, y).\\mathrm{toOrderHom}\\, i = (i.castAdd\\,\\_).cast(\\mathrm{Nat.succ\\_add}\\, x.len\\, (y.len+1)).$$$

Lean4

theorem inl'_eval (x y : SimplexCategory) (i : Fin (x.len + 1)) :
    (inl' x y).toOrderHom i = (i.castAdd _).cast (Nat.succ_add x.len (y.len + 1)) :=
  by
  dsimp [inl', inl, MonoidalCategoryStruct.rightUnitor, MonoidalCategoryStruct.whiskerLeft, tensorHom, WithInitial.down,
    rightUnitor, tensorObj]
  ext
  simp [OrderEmbedding.toOrderHom]

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