English
If l is a linear map between finitely generated modules over a local ring and certain flatness and injectivity conditions hold, then l is injective.
Русский
Если l — линейное отображение между конечнопорожденными модулями над локальным кольцом и выполняются плоскость и инъективность, то l инъективно.
LaTeX
$$$ \text{Injective}(l) \Leftrightarrow \nexists \; 0 \neq x \; s.t. \; l(x)=0. $$$
Lean4
/-- If `M → N → P → 0` is a presentation of `P` over a local ring `(R, 𝔪, k)` with
`M` finite and `N` finite free, then injectivity of `k ⊗ M → k ⊗ N` implies that `P` is free.
-/
theorem free_of_lTensor_residueField_injective (hg : Surjective g) (h : Exact f g) [Module.Finite R M]
[Module.Finite R N] [Module.Free R N] (hf : Function.Injective (f.lTensor k)) : Module.Free R P :=
by
have :=
Module.finitePresentation_of_free_of_surjective g hg
(by rw [h.linearMap_ker_eq, LinearMap.range_eq_map]; exact (Module.Finite.fg_top).map f)
apply free_of_maximalIdeal_rTensor_injective
rw [← LinearMap.lTensor_inj_iff_rTensor_inj]
apply
lTensor_injective_of_exact_of_exact_of_rTensor_injective h hg (LinearMap.exact_subtype_mkQ 𝔪)
(Submodule.mkQ_surjective _) ((LinearMap.lTensor_inj_iff_rTensor_inj _ _).mp hf)
(Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective)
