Module docstring
{"# Finitely generated submodules and bilinear maps
"}
Submodule.FG.map₂
theorem
(f : M →ₗ[R] N →ₗ[R] P) {p : Submodule R M} {q : Submodule R N} (hp : p.FG) (hq : q.FG) : (map₂ f p q).FG
Full source
theorem FG.map₂ (f : M →ₗ[R] N →ₗ[R] P) {p : Submodule R M} {q : Submodule R N} (hp : p.FG)
(hq : q.FG) : (map₂ f p q).FG :=
let ⟨sm, hfm, hm⟩ := fg_def.1 hp
let ⟨sn, hfn, hn⟩ := fg_def.1 hq
fg_def.2
⟨Set.image2 (fun m n => f m n) sm sn, hfm.image2 _ hfn,
map₂_span_span R f sm sn ▸ hm ▸ hn ▸ rfl⟩Informal description
Let $R$ be a ring, and let $M$, $N$, and $P$ be $R$-modules. Given a bilinear map $f \colon M \times N \to P$ and finitely generated submodules $p \subseteq M$ and $q \subseteq N$, the image of $p \times q$ under $f$ is a finitely generated submodule of $P$.