English
If f, g, f', g' are bilinear maps compatible through φ, then the two-step kroneckerMap composition equals the single kroneckerMap with composed maps, up to the isomorphism φ.
Русский
Если есть совместимые билинейные отображения, то композиция две стадии KroneckerMap эквивалентна одному KroneckerMap с композициями отображений, с учётом изоморфизма φ.
LaTeX
$$$(\mathrm{reindex} (\mathrm{prodAssoc}\ l\ n\ q) (\mathrm{prodAssoc}\ m\ p\ r)).trans (\mathrm{Equiv.mapMatrix} \phi) (\mathrm{kroneckerMap} g (\mathrm{kroneckerMap} f A B) D) = \mathrm{kroneckerMap} f' A (\mathrm{kroneckerMap} g' B D)$$$
Lean4
theorem kroneckerMap_assoc {δ ξ ω ω' : Type*} (f : α → β → γ) (g : γ → δ → ω) (f' : α → ξ → ω') (g' : β → δ → ξ)
(A : Matrix l m α) (B : Matrix n p β) (D : Matrix q r δ) (φ : ω ≃ ω')
(hφ : ∀ a b d, φ (g (f a b) d) = f' a (g' b d)) :
(reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)).trans (Equiv.mapMatrix φ)
(kroneckerMap g (kroneckerMap f A B) D) =
kroneckerMap f' A (kroneckerMap g' B D) :=
ext fun _ _ => hφ _ _ _
