English
If M is flat, then tensoring with M is an exact functor (lTensor).
Русский
Если M плоский, тогда тензорное умножение на M является точной функцией (lTensor).
LaTeX
$$$Flat\ R\ M \Rightarrow \text{lTensor exact for M}$$$
Lean4
/-- If `M` is flat then `M ⊗ -` is an exact functor. -/
theorem lTensor_exact [Flat R M] ⦃N N' N'' : Type*⦄ [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [Module R N]
[Module R N'] [Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄ (exact : Function.Exact f g) :
Function.Exact (f.lTensor M) (g.lTensor M) :=
by
let π : N' →ₗ[R] N' ⧸ LinearMap.range f := Submodule.mkQ _
let ι : N' ⧸ LinearMap.range f →ₗ[R] N'' :=
Submodule.subtype _ ∘ₗ
(LinearMap.quotKerEquivRange g).toLinearMap ∘ₗ
Submodule.quotEquivOfEq (LinearMap.range f) (LinearMap.ker g) (LinearMap.exact_iff.mp exact).symm
suffices exact1 : Function.Exact (f.lTensor M) (π.lTensor M)
by
rw [show g = ι.comp π from rfl, lTensor_comp]
exact
exact1.comp_injective _
(lTensor_preserves_injective_linearMap ι <| by simpa [ι, -Subtype.val_injective] using Subtype.val_injective)
(map_zero _)
exact _root_.lTensor_exact _ (fun x ↦ by simp [π]) Quotient.mk''_surjective
