map — Mathlib

English

Pushforwards of finite submodules under a linear map are finite.

Русский

Образы конечных подмодулей под линейным отображением конечны.

LaTeX

$$$\\forall p\\; [\\text{Module.Finite } R p]\\; (f: M \\to N)\\;\\Rightarrow\\; \\text{Module.Finite } R (p \\mapsto f)$$

Lean4

/-- Pushforwards of finite submodules are finite. -/
instance map (p : Submodule R M) [Module.Finite R p] (f : M →ₗ[R] N) : Module.Finite R (p.map f) :=
  of_surjective (f.restrict fun _ => Submodule.mem_map_of_mem) fun ⟨_, _, hy, hy'⟩ => ⟨⟨_, hy⟩, Subtype.ext hy'⟩

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