English
If M is a finitely presented module over R and flat, then there exists a basis realizing a given generating family after a suitable base-change.
Русский
Если M — конечно презентационный модуль над R и плоский, существует база, реализующая заданное порождающее множество после подходящего базового изменения.
LaTeX
$$$ [Module.FinitePresentation R M] [Module.Flat R M] \Rightarrow \exists (\kappa)(a: \kappa \to 1) (b: Basis \kappa R M), \; \forall i, b i = v i. $$$
Lean4
/-- If `M` is a finitely presented module over a local ring `(R, 𝔪)` such that `m ⊗ M → M` is
injective, then every generating family contains a basis.
-/
theorem exists_basis_of_span_of_maximalIdeal_rTensor_injective [Module.FinitePresentation R M]
(H : Function.Injective ((𝔪).subtype.rTensor M)) {ι : Type u} (v : ι → M)
(hv : Submodule.span R (Set.range v) = ⊤) : ∃ (κ : Type u) (a : κ → ι) (b : Basis κ R M), ∀ i, b i = v (a i) :=
by
have := (map_tensorProduct_mk_eq_top (N := Submodule.span R (Set.range v))).mpr hv
rw [← Submodule.span_image, ← Set.range_comp, eq_top_iff, ← SetLike.coe_subset_coe, Submodule.top_coe] at this
have : Submodule.span k (Set.range (TensorProduct.mk R k M 1 ∘ v)) = ⊤ :=
by
rw [eq_top_iff]
exact Set.Subset.trans this (Submodule.span_subset_span _ _ _)
obtain ⟨κ, a, ha, hsp, hli⟩ := exists_linearIndependent' k (TensorProduct.mk R k M 1 ∘ v)
rw [this] at hsp
obtain ⟨b, hb⟩ := exists_basis_of_basis_baseChange (v ∘ a) hli hsp H
use κ, a, b, hb
