English
Let R be a ring and M an R-module. M is faithfully flat over R if and only if M is flat and for every R-module N, N ≠ 0 implies M ⊗R N ≠ 0.
Русский
Пусть R — кольцо, M — R-модуль. M называется верноподобно плоским над R тогда и только тогда, когда M плоско, и для каждого R-модуля N, если N непустой, то M ⊗R N непустой.
LaTeX
$$$\mathrm{FaithfullyFlat}_R(M) \iff \left( \mathrm{Flat}_R(M) \land \forall N\,(N \neq 0 \Rightarrow M \otimes_R N \neq 0)\right)$$$
Lean4
theorem iff_flat_and_lTensor_faithful :
FaithfullyFlat R M ↔
(Flat R M ∧ ∀ (N : Type max u v) [AddCommGroup N] [Module R N], Nontrivial N → Nontrivial (M ⊗[R] N)) :=
iff_flat_and_rTensor_faithful R M |>.trans
⟨fun ⟨flat, faithful⟩ =>
⟨flat, fun N _ _ _ =>
letI := faithful N inferInstance;
(TensorProduct.comm R M N).toEquiv.nontrivial⟩,
fun ⟨flat, faithful⟩ =>
⟨flat, fun N _ _ _ =>
letI := faithful N inferInstance;
(TensorProduct.comm R M N).symm.toEquiv.nontrivial⟩⟩
