English
The composition functor acts on a matrix built from a singleton in each index by sending the singleton to the corresponding singleton in the rearranged indices.
Русский
Композиционная операция переведёт единичные элементы в соответствующие единичные элементы в переставленных индексах.
LaTeX
$$$ \mathrm{comp}(I,J,K,L,R)(\mathrm{single}(i,j,\mathrm{single}(k,l,r))) = \mathrm{single}((i,k),(j,l),r) $$$
Lean4
@[simp]
theorem comp_single_single [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] [Zero R] (i j k l r) :
comp I J K L R (single i j (single k l r)) = single (i, k) (j, l) r :=
by
ext ⟨i', k'⟩ ⟨j', l'⟩
dsimp [comp_apply]
obtain hi | rfl := ne_or_eq i i'
· rw [single_apply_of_row_ne hi, single_apply_of_row_ne (ne_of_apply_ne Prod.fst hi), Matrix.zero_apply]
obtain hj | rfl := ne_or_eq j j'
· rw [single_apply_of_col_ne _ _ hj, single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.fst hj), Matrix.zero_apply]
rw [single_apply_same]
obtain hk | rfl := ne_or_eq k k'
· rw [single_apply_of_row_ne hk, single_apply_of_row_ne (ne_of_apply_ne Prod.snd hk)]
obtain hj | rfl := ne_or_eq l l'
· rw [single_apply_of_col_ne _ _ hj, single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.snd hj)]
rw [single_apply_same, single_apply_same]
