English
A restatement of rTensor injectivity criterion for flatness equivalence.
Русский
Переформулировка критерия инъективности rTensor для эквивалентности плоскостности.
LaTeX
$$$Flat\ R\ M \iff \forall {N,N'} (f:\ N \to N'), Injective(f) \Rightarrow Injective(f\,\mathrm{rTensor}\ M)$$$
Lean4
/-- `M` is flat if and only if `M ⊗ -` is an exact functor.
See `Module.Flat.iff_lTensor_exact'` to generalize the universe of
`N, N', N''` to any universe that is higher than `R` and `M`. -/
theorem iff_lTensor_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.lTensor M) (g.lTensor M) :=
iff_lTensor_exact'
