English
Equational criterion for flatness: several equivalent formulations hold, including flatness, injectivity of tensor with ideals, vanishing trivially, trivial relations, and a finite-step factorization property.
Русский
Эквивалентные формулировки для плоскости: ровно пять условий равны друг другу, связанные плоскостью, инъективностью тензорирования с идеалами, тривиальной исчезающей частью, тривиальным отношением и конечной факторизацией.
LaTeX
$$\text{tfae_equational_criterion} : List.TFAE [Flat R M, \cdots, ∥] $$
Lean4
/-- If the relation given by $(f_i)_{i \in \iota}$ and $(x_i)_{i \in \iota}$ is trivial, then
$\sum_i f_i x_i$ is actually equal to $0$. -/
theorem sum_smul_eq_zero_of_isTrivialRelation (h : IsTrivialRelation f x) : ∑ i, f i • x i = 0 := by
simpa using
congr_arg (TensorProduct.lid R M) <|
sum_tmul_eq_zero_of_vanishesTrivially R (isTrivialRelation_iff_vanishesTrivially.mp h)
