map₂_map_left — Mathlib

English

Let f: M₂ →ₗ[R] N →ₗ[R] P and g: M →ₗ[R] M₂ be linear maps. Then map₂ f (map g p) q = map₂ (f ∘ₗ g) p q for submodules p ⊆ M and q ⊆ N.

Русский

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

LaTeX

$$$\\operatorname{map_2} f (\\operatorname{map} g\\ p) q = \\operatorname{map_2} (f \\circ g) p q$$$

Lean4

theorem map₂_map_left (f : M₂ →ₗ[R] N →ₗ[R] P) (g : M →ₗ[R] M₂) (p : Submodule R M) (q : Submodule R N) :
    map₂ f (map g p) q = map₂ (f ∘ₗ g) p q :=
  by
  rw [← map₂_flip, map₂_map_right, ← map₂_flip]
  rfl

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