map₂ — Mathlib

English

Given a bilinear map f, the submodule map₂ f p q is defined as the submodule generated by all f(m,n) with m ∈ p and n ∈ q.

Русский

Задан билинейный отображение f, подмодуль map₂ f p q определяется как подмодуль, порожденный всеми элементами f(m,n) с m ∈ p, n ∈ q.

LaTeX

$$$\\mathrm{map}_2 f\\; p\\; q = \\big\\langle f(p) \\otimes q \\big\\rangle = \\bigvee_{s \\in p} q.map (f\\,s)$$$

Lean4

/-- Map a pair of submodules under a bilinear map.

This is the submodule version of `Set.image2`. -/
def map₂ (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) : Submodule R P :=
  ⨆ s : p, q.map (f s)

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