English
A faithfully flat module M reflects triviality: M is faithfully flat over R if and only if M is flat and for every N, Subsingleton(M ⊗R N) implies Subsingleton(N).
Русский
Верно: верноподобный модуль M сохраняет тривиальность: M верноподобен над R тогда и только тогда, когда M плосок и для каждого N из R-модулей Subsingleton(M ⊗R N) ⇒ Subsingleton(N).
LaTeX
$$$\mathrm{FaithfullyFlat}_R(M) \iff \left( \mathrm{Flat}_R(M) \land \forall N\,(\operatorname{Subsingleton}(M \otimes_R N) \rightarrow \operatorname{Subsingleton}(N))\right)$$$
Lean4
theorem iff_flat_and_lTensor_reflects_triviality :
FaithfullyFlat R M ↔
(Flat R M ∧ ∀ (N : Type max u v) [AddCommGroup N] [Module R N], Subsingleton (M ⊗[R] N) → Subsingleton N) :=
iff_flat_and_lTensor_faithful R M |>.trans <|
and_congr_right_iff.2 fun _ =>
iff_of_eq <|
forall_congr fun N =>
forall_congr fun _ =>
forall_congr fun _ => iff_iff_eq.1 <| by simp only [← not_subsingleton_iff_nontrivial]; tauto
