English
Flatness of M is equivalent to preservation of injectivity by rTensor for all injections f.
Русский
Плоскостность M эквивалентна сохранению инъективности под действием rTensor для всех инъекций f.
LaTeX
$$$Flat\ R\ M \iff (\forall N,N'\ (f:\ N\to N'), \text{Injective}(f) \Rightarrow \text{Injective}(f\,\mathrm{rTensor}\ M))$$$
Lean4
/-- `M` is flat if and only if `f ⊗ 𝟙 M` is injective whenever `f` is an injective linear map.
See `Module.Flat.iff_rTensor_preserves_injective_linearMap` to specialize the universe of
`N, N', N''` to `Type (max u v)`. -/
theorem iff_rTensor_preserves_injective_linearMap' [Small.{v'} R] :
Flat R M ↔
∀ ⦃N N' : Type v'⦄ [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N'] (f : N →ₗ[R] N'),
Function.Injective f → Function.Injective (f.rTensor M) :=
⟨by introv _; apply rTensor_preserves_injective_linearMap, fun h ↦
iff_rTensor_preserves_injective_linearMapₛ.mpr fun P N _ _ _ _ ↦
by
letI := Module.addCommMonoidToAddCommGroup R (M := P)
letI := Module.addCommMonoidToAddCommGroup R (M := N)
apply h⟩
