English
Flatness of M is equivalent to the following factorization property: for all finite free modules R^l, all f ∈ R^l, and all linear maps x: R^l → M with x(f) = 0, there exist k, a, y with x = y ∘ a and a(f) = 0.
Русский
Плоскость M эквивалентна следующему свойству факторизации: для всех конечных свободных модулей R^l, для всех f ∈ R^l и линейных отображений x: R^l → M с x(f)=0 существуют k, a, y такие, что x = y ∘ a и a(f)=0.
LaTeX
$$$Flat(R,M) \iff \forall l, f : R^l, x : (R^l) → M, (x(f)=0) \Rightarrow \exists k, a: R^l → R^k, y: R^k → M, x = y \circ a \land a(f)=0$$$
Lean4
/-- **Equational criterion for flatness**, alternate form.
A module $M$ is flat if and only if 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$. -/
@[stacks 058D "(1) ↔ (2)"]
theorem iff_forall_exists_factorization :
Flat R M ↔
∀ {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 :=
(tfae_equational_criterion R M).out 0 4
