English
If for every finite free module R^l, every f ∈ R^l and every linear map x: R^l → M with x(f)=0 there exist a factorization x = y ∘ a with a(f)=0, then M is flat over R.
Русский
Если для каждого конечного свободного модуля R^l, каждого f ∈ R^l и каждого линейного отображения x: R^l → M при x(f)=0 существуют разложения x = y ∘ a с a(f)=0, то M плосок над R.
LaTeX
$$(∀ {l} {f : Fin l → R} {x : (Fin l → R) → M}, x f = 0 → ∃ k, a, y, x = y ∘ a ∧ a f = 0) → Flat(R,M)$$
Lean4
/-- **Equational criterion for flatness**, backward direction, alternate form.
Let $M$ be a module over a commutative ring $R$. Suppose that for all finite free modules $R^l$,
all $f \in R^l$, and all linear maps $x \colon R^l \to M$ such that $x(f) = 0$, there
exist a finite free module $R^k$ and linear maps $a \colon R^l \to R^k$ and
$y \colon R^k \to M$ such that $x = y \circ a$ and $a(f) = 0$. Then $M$ is flat. -/
@[stacks 058D "(2) → (1)"]
theorem of_forall_exists_factorization
(h :
∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M},
x f = 0 → ∃ (k : ℕ) (a : (Fin l →₀ R) →ₗ[R] (Fin k →₀ R)) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0) :
Flat R M :=
iff_forall_exists_factorization.mpr h
