English
If M is flat then rTensor preserves exact sequences: f ⟶ g exact implies f.rTensor M ⟶ g.rTensor M exact.
Русский
Если M плоский, тогда rTensor сохраняет точные последовательности: при точности f ⟶ g следует точность f⊗M ⟶ g⊗M.
LaTeX
$$$\forall f,g,\, \text{Exact}(f,g) \Rightarrow \text{Exact}(f\mathrm{rTensor} M, g\mathrm{rTensor} M)$$$
Lean4
/-- `M` is flat if and only if `- ⊗ M` is an exact functor.
See `Module.Flat.iff_rTensor_exact'` to generalize the universe of
`N, N', N''` to any universe that is higher than `R` and `M`. -/
theorem iff_rTensor_exact :
Flat R M ↔
∀ ⦃N N' N'' : Type (max u v)⦄ [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [Module R N] [Module R N']
[Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄,
Function.Exact f g → Function.Exact (f.rTensor M) (g.rTensor M) :=
iff_rTensor_exact'
