free_of_maximalIdeal_rTensor_injective

English

If M is a finitely presented module over a local ring such that the residue-field-tensor map is injective, then M is free.

Русский

Если M — конечная презентация модуля над локальным кольцом и тензорное отображение остаточного поля инъективно, тогда M свободен.

LaTeX

$$$ [Module.FinitePresentation R M] \Rightarrow\; [Module.Flat R M] \Rightarrow \text{Free}_R(M). $$$

Lean4

/-- If `M` is a finitely presented module over a local ring `(R, 𝔪)` such that `m ⊗ M → M` is
injective, then `M` is free.
-/
theorem free_of_maximalIdeal_rTensor_injective [Module.FinitePresentation R M]
    (H : Function.Injective ((𝔪).subtype.rTensor M)) : Module.Free R M :=
  by
  obtain ⟨_, _, b, _⟩ := exists_basis_of_span_of_maximalIdeal_rTensor_injective H id (by simp)
  exact Free.of_basis b

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