English
A finite (or arbitrary) direct sum of faithfully flat R-modules is faithfully flat.
Русский
Директная сумма любое семейство верноподобных по основанию R-модулей остаётся верноподобной.
LaTeX
$$$\forall \{M_i\}_{i\in I},\ \forall [\forall i, \text{FaithfullyFlat}_R(M_i)],\ \text{FaithfullyFlat}_R\Big(\bigoplus_{i\in I} M_i\Big)$$$
Lean4
/-- A direct sum of faithfully flat `R`-modules is faithfully flat. -/
instance directSum {ι : Type*} [Nonempty ι] (M : ι → Type*) [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)]
[∀ i, FaithfullyFlat R (M i)] : FaithfullyFlat R (⨁ i, M i) := by
classical
rw [iff_flat_and_lTensor_faithful]
refine ⟨inferInstance, fun N _ _ hN ↦ ?_⟩
obtain ⟨i⟩ := ‹Nonempty ι›
obtain ⟨x, y, hxy⟩ := Nontrivial.exists_pair_ne (α := M i ⊗[R] N)
haveI : Nontrivial (⨁ (i : ι), M i ⊗[R] N) :=
⟨DirectSum.of _ i x, DirectSum.of _ i y, fun h ↦ hxy (DirectSum.of_injective i h)⟩
apply (TensorProduct.directSumLeft R M N).toEquiv.nontrivial
