English
Let f: P → P' be linear and g: M → N → P be a bilinear map. Then composing f with the bilinear map equals applying the bilinear map with the composed inner map on the codomain: map f (map₂ g p q) = map₂ (g.compr₂ f) p q for submodules p ⊆ M and q ⊆ N.
Русский
Пусть f: P → P' линейно и g: M → N → P билинейно. Тогда композиция f с билинейной картой равна применению билинейной карты к композиции по основании: map f (map₂ g p q) = map₂ (g.compr₂ f) p q для подмодулей p ⊆ M и q ⊆ N.
LaTeX
$$$\\operatorname{map} f (\\operatorname{map_2} g\\ p\\ q) = \\operatorname{map_2} (g.\\text{compr_2} f)\\ p\\ q$$$
Lean4
theorem map_map₂ (f : P →ₗ[R] P₂) (g : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
map f (map₂ g p q) = map₂ (g.compr₂ f) p q :=
map_iSup _ _ |>.trans <| iSup_congr fun _ => map_comp _ _ _ |>.symm
