map₂_map_right — Mathlib

English

For a bilinear map f: M →ₗ[R] N →ₗ[R] P, a linear map g: N →ₗ[R] N₂, and submodules p ⊆ M, q ⊆ N, we have the equality map₂ f p (map g q) = map₂ (f.compl₂ g) p q.

Русский

Для билинейного отображения f: M →ₗ[R] N →ₗ[R] P, линейного отображения g: N →ₗ[R] N₂ и подмодулов p ⊆ M, q ⊆ N выполняется равенство map₂ f p (map g q) = map₂ (f.compl₂ g) p q.

LaTeX

$$$\\operatorname{map_2} f\\ p\\ (\\operatorname{map} g\\ q) = \\operatorname{map_2} (f.\\text{compl_2} g)\\ p\\ q$$$

Lean4

theorem map₂_map_right (f : M →ₗ[R] N₂ →ₗ[R] P) (g : N →ₗ[R] N₂) (p : Submodule R M) (q : Submodule R N) :
    map₂ f p (map g q) = map₂ (f.compl₂ g) p q :=
  iSup_congr fun _ => map_comp _ _ _ |>.symm

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