map₂_map_map — Mathlib

English

For bilinear f, linear g on M and linear h on N, we have map₂ f (map g p) (map h q) = map₂ (f.compl₁₂ g h) p q for submodules p ⊆ M, q ⊆ N.

Русский

Для билинейного отображения f, линейного отображения g на M и линейного h на N имеем map₂ f (map g p) (map h q) = map₂ (f.compl₁₂ g h) p q для подмодулей p ⊆ M, q ⊆ N.

LaTeX

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

Lean4

theorem map₂_map_map (f : M₂ →ₗ[R] N₂ →ₗ[R] P) (g : M →ₗ[R] M₂) (h : N →ₗ[R] N₂) (p : Submodule R M)
    (q : Submodule R N) : map₂ f (map g p) (map h q) = map₂ (f.compl₁₂ g h) p q :=
  by
  rw [map₂_map_right, map₂_map_left]
  rfl

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