map₂ — Mathlib

English

If p and q are FG (finitely generated) submodules, then the image under map₂ is FG as well.

Русский

Если p и q — FG-подмодули, то подобраз map₂ тоже FG.

LaTeX

$$$\\text{FG}(p) \\land \\text{FG}(q) \\Rightarrow \\text{FG}(\\mathrm{map}_2\\ f\\ p\\ q)$$$

Lean4

theorem 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⟩

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