English
If M is flat, then for every injective f, the map f.rTensor M is injective.
Русский
Если M плоский модуль, то для любого инъективного отображения f отображение f.rTensor M инъективно.
LaTeX
$$$\text{Flat } R M \Rightarrow \forall f, (f.rTensor M) \\text{ injective}$$$
Lean4
/-- If `M` is a flat module, then `f ⊗ 𝟙 M` is injective for all injective linear maps `f`. -/
theorem rTensor_preserves_injective_linearMap [Flat R M] (f : N →ₗ[R] P) (hf : Function.Injective f) :
Function.Injective (f.rTensor M) :=
by
refine rTensor_injective_of_fg fun N P Nfg Pfg le ↦ ?_
rw [← Finite.iff_fg] at Nfg Pfg
have := Finite.small R P
let se := (Shrink.linearEquiv R P).symm
have := Module.Finite.equiv se
rw [rTensor_injective_iff_subtype (fun _ _ ↦ (Subtype.ext <| hf <| Subtype.ext_iff.mp ·)) se]
exact (flat_iff R M).mp ‹_› _ (Finite.iff_fg.mp inferInstance)
