English
Let I, J, K, L, R, R' be types with I and J finite, K a commutative semiring, R a semiring, an algebra structure of R over K, and decidable equality on I and J. Then the inverse of the block-algebra isomorphism compAlgEquiv I J R K, when applied to M ∈ Matrix I I (Matrix J J R), coincides with the inverse block-composition map, i.e. (compAlgEquiv I J R K).symm M = (comp I I J J R).symm M.
Русский
Пусть I, J, K, L, R, R' — множества, I и J — конечны, K — коммутативная полугруппа, R — полугруппа, имеется структура алгебры над K, и задано равенство по элементам на I и J. Тогда обратное блочное изоморфизм compAlgEquiv I J R K при приложении к M даёт тот же результат, что и обратная блочная композиционная карта: (compAlgEquiv I J R K).symm M = (comp I I J J R).symm M.
LaTeX
$$$(\\operatorname{compAlgEquiv}_{I,J,R,K})^{-1}(M) = (\\operatorname{comp}_{I,I,J,J,R})^{-1}(M)$$$
Lean4
@[simp]
theorem compAlgEquiv_symm_apply (M : Matrix (I × J) (I × J) R) :
(compAlgEquiv I J R K).symm M = (comp I I J J R).symm M :=
rfl
