English
Let R be a commutative ring and M an R-module. Then M is flat over R if and only if every finite linear relation in M is trivial; equivalently, for every finite index l and families f : Fin l → R, x : Fin l → M, the relation ∑ i f i · x i = 0 is trivial.
Русский
Пусть R — коммутативное кольцо и M — R-модуль. Тогда M плосок над R тогда и только тогда, когда любая конечная линейная зависимость в M тривиальна; эквивалентно: для каждого конечного индекса l и семей f : Fin l → R, x : Fin l → M сумма ∑ i f i · x i = 0 образует тривиальные отношения.
LaTeX
$$$Flat(R,M) \;\Longleftrightarrow\; \forall l\in\mathbb{N}, \forall f: \{1,\dots,l\} \to R, \forall x: \{1,\dots,l\} \to M, \; \sum_{i=1}^l f(i)\,x(i) = 0 \Rightarrow \text{IsTrivialRelation}(f,x) $$$
Lean4
/-- **Equational criterion for flatness**:
a module $M$ is flat if and only if every relation $\sum_i f_i x_i = 0$ in $M$ is trivial. -/
@[stacks 00HK]
theorem iff_forall_isTrivialRelation :
Flat R M ↔ ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → IsTrivialRelation f x :=
(tfae_equational_criterion R M).out 0 3
