inr'_eval — Mathlib

English

The right inclusion into a tensor product, evaluated at an index i, is given by a natural add-indexing shift, reflecting the right insertion into the tensor factor.

Русский

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

LaTeX

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

Lean4

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

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