English
If M is flat over S and N is flat over R with appropriate towers, then M ⊗_R N is flat over S.
Русский
Если M плосок над S и N плосок над R с подходящей башней, тогда M ⊗_R N плосок над S.
LaTeX
$$$\text{Flat}(S,M) \land \text{Flat}(R,N) \Rightarrow \text{Flat}(S, M \otimes_R N)$$$
Lean4
/-- If `M` is flat then `- ⊗ M` is an exact functor. -/
theorem rTensor_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.rTensor M) (g.rTensor 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.rTensor M) (π.rTensor M)
by
rw [show g = ι.comp π from rfl, rTensor_comp]
exact
exact1.comp_injective _
(rTensor_preserves_injective_linearMap ι <| by simpa [ι, -Subtype.val_injective] using Subtype.val_injective)
(map_zero _)
exact _root_.rTensor_exact M (fun x ↦ by simp [π]) Quotient.mk''_surjective
