English
If M is flat, then for any finite free module N ≅ R^l, any f ∈ N, and any linear map x: N → M with x(f)=0 there exist a finite free module R^k and linear maps a: N → R^k and y: R^k → M such that x = y ∘ a and a(f) = 0.
Русский
Если M плосок, то для любого конечного свободного модуля N ≅ R^l, любого f ∈ N и линейного отображения x: N → M с x(f)=0 существуют конечный свободный модуль R^k и линейные отображения a: N → R^k, y: R^k → M такие, что x = y ∘ a и a(f) = 0.
LaTeX
$$[(Flat R M)] ⇒ ∀ {N} [Free R N] {f ∈ N} {x: N → M}, x f = 0 → ∃ k, a: N → R^k, y: R^k → M, x = y ∘ a ∧ a f = 0$$
Lean4
/-- **Equational criterion for flatness**, forward direction, second alternate form.
Let $M$ be a flat module over a commutative ring $R$. Let $N$ be a finite free module over $R$,
let $f \in N$, and let $x \colon N \to M$ be a linear map such that $x(f) = 0$. Then there exist a
finite free module $R^k$ and linear maps $a \colon N \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 exists_factorization_of_apply_eq_zero_of_free [Flat R M] {N : Type*} [AddCommGroup N] [Module R N] [Free R N]
[Module.Finite R N] {f : N} {x : N →ₗ[R] M} (h : x f = 0) :
∃ (k : ℕ) (a : N →ₗ[R] (Fin k →₀ R)) (y : (Fin k →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0 :=
have e := ((Module.Free.chooseBasis R N).reindex (Fintype.equivFin _)).repr.symm
have ⟨k, a, y, hya, haf⟩ :=
iff_forall_exists_factorization.mp ‹Flat R M› (f := e.symm f) (x := x ∘ₗ e) (by simpa using h)
⟨k, a ∘ₗ e.symm, y, by rwa [← comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm], haf⟩
