English
If M is finitely presented, there exists a basis b of M such that its elements coincide with a given generating family after a suitable isomorphism, i.e., the span of that generating family is the whole module.
Русский
Если M конечно презентационен, существует база b модуля M такая, что элементы b совпадают с заданной породной породой после подходящего изоморфизма; порождающее множество порождает весь модуль.
LaTeX
$$$ \exists (\kappa) (a: \kappa \to \iota) (b: Basis \kappa R M),\; \forall i, b i = v (a i). $$$
Lean4
theorem span_eq_top_of_tmul_eq_basis [Module.Finite R M] {ι} (f : ι → M) (b : Basis ι k (k ⊗[R] M))
(hb : ∀ i, 1 ⊗ₜ f i = b i) : Submodule.span R (Set.range f) = ⊤ :=
by
rw [← map_tensorProduct_mk_eq_top, Submodule.map_span, ←
Submodule.restrictScalars_span R k Ideal.Quotient.mk_surjective, Submodule.restrictScalars_eq_top_iff, ← b.span_eq,
← Set.range_comp]
simp only [Function.comp_def, mk_apply, hb, Basis.span_eq]
