English
If r is regular in R and M is flat, then scalar multiplication by r is injective on M.
Русский
Если r — регулярный элемент в кольце R и M плоский, то умножение на r на элементами M инъективно.
LaTeX
$$$IsSMulRegular M r$ given $IsRegular r$ and $Flat R M$$$
Lean4
/-- Scalar multiplication `m ↦ r • m` by a regular `r` is injective on a flat module. -/
theorem isSMulRegular_of_isRegular {r : R} (hr : IsRegular r) [Flat R M] : IsSMulRegular M r := by
-- `r ∈ R⁰` implies that `toSpanSingleton R R r`, i.e. `(r * ⬝) : R → R` is injective
-- Flatness implies that corresponding map `R ⊗[R] M →ₗ[R] R ⊗[R] M` is injective
have h := Flat.rTensor_preserves_injective_linearMap (M := M) (toSpanSingleton R R r) <| hr.right
have h2 :
(fun (x : M) ↦ r • x) =
((TensorProduct.lid R M) ∘ₗ (rTensor M (toSpanSingleton R R r)) ∘ₗ (TensorProduct.lid R M).symm) :=
by ext;
simp
-- Hence `(r • ·) : M → M` is also injective
rw [IsSMulRegular, h2]
simp [h, LinearEquiv.injective]
