fg_iff_exists_fin_linearMap — Mathlib

English

A submodule N is finitely generated if and only if there exists n and a linear map f: (Fin n → R) → M such that range f = N.

Русский

Подмодуль N конечен тогда и только тогда, когда существует n и линейное отображение f: (Fin n → R) → M, для которого образ равен N.

LaTeX

$$$\\forall R M [\\text{Semiring } R] [\\text{Module } R M],\\ {N: Submodule R M}, N.FG \\iff \\exists n (f : (Fin n \to R) \to_\\!{R} M), \\operatorname{Range} f = N.$$$

Lean4

theorem fg_iff_exists_fin_linearMap {N : Submodule R M} :
    N.FG ↔ ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), LinearMap.range f = N :=
  by
  simp_rw [fg_iff_exists_fin_generating_family, ← ((Pi.basisFun R _).constr ℕ).exists_congr_right]
  simp [Basis.constr_range]

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