The equational criterion for flatness #
Let $M$ be a module over a commutative ring $R$. Let us say that a relation
$\sum_{i \in \iota} f_i x_i = 0$ in $M$ is trivial (Module.IsTrivialRelation) if there exist a
finite index type $\kappa$ = Fin k, elements $(y_j)_{j \in \kappa}$ of $M$,
and elements $(a_{ij})_{i \in \iota, j \in \kappa}$ of $R$ such that for all $i$,
$$x_i = \sum_j a_{ij} y_j$$
and for all $j$,
$$\sum_i f_i a_{ij} = 0.$$
The equational criterion for flatness Stacks 00HK
(Module.Flat.iff_forall_isTrivialRelation) states that $M$ is flat if and only if every relation
in $M$ is trivial.
The equational criterion for flatness can be stated in the following form
(Module.Flat.iff_forall_exists_factorization). Let $M$ be an $R$-module. Then the following two
conditions are equivalent:
- $M$ is flat.
- For finite free modules $R^l$, all elements $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$.
Of course, the module $R^l$ in this statement can be replaced by an arbitrary free module
(Module.Flat.exists_factorization_of_apply_eq_zero_of_free).
We also have the following strengthening of the equational criterion for flatness
(Module.Flat.exists_factorization_of_comp_eq_zero_of_free): Let $M$ be a
flat module. Let $K$ and $N$ be finite $R$-modules with $N$ free, and let $f \colon K \to N$ and
$x \colon N \to M$ be linear maps such that $x \circ 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 \circ f = 0$. We recover the usual equational criterion for flatness if
$K = R$ and $N = R^l$. This is used in the proof of Lazard's theorem.
We conclude that every linear map from a finitely presented module to a flat module factors
through a finite free module (Module.Flat.exists_factorization_of_isFinitelyPresented), and
every finitely presented flat module is projective (Module.Flat.projective_of_finitePresentation).
References #
The proposition that the relation $\sum_i f_i x_i = 0$ in $M$ is trivial.
That is, there exist a finite index type $\kappa$ = Fin k, elements
$(y_j)_{j \in \kappa}$ of $M$, and elements $(a_{ij})_{i \in \iota, j \in \kappa}$ of $R$
such that for all $i$,
$$x_i = \sum_j a_{ij} y_j$$
and for all $j$,
$$\sum_i f_i a_{ij} = 0.$$
By Module.sum_smul_eq_zero_of_isTrivialRelation, this condition implies $\sum_i f_i x_i = 0$.
Equations
Instances For
Module.IsTrivialRelation is equivalent to the predicate TensorProduct.VanishesTrivially
defined in Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean.
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$.
Equational criterion for flatness, combined form.
Let $M$ be a module over a commutative ring $R$. The following are equivalent:
- $M$ is flat.
- For all ideals $I \subseteq R$, the map $I \otimes M \to M$ is injective.
- Every $\sum_i f_i \otimes x_i$ that vanishes in $R \otimes M$ vanishes trivially.
- Every relation $\sum_i f_i x_i = 0$ in $M$ is trivial.
- For all finite free modules $R^l$, all elements $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 Tag 058D (except (3))
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.
Equational criterion for flatness, forward direction.
If $M$ is flat, then every relation $\sum_i f_i x_i = 0$ in $M$ is trivial.
Equational criterion for flatness, backward direction.
If every relation $\sum_i f_i x_i = 0$ in $M$ is trivial, then $M$ is flat.
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 Tag 058D ((1) ↔ (2))
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 Tag 058D ((2) → (1))
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 Tag 058D ((1) → (2))
Alias of Module.Flat.exists_factorization_of_apply_eq_zero_of_free.
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 Tag 058D ((1) → (2))
Let $M$ be a flat module. Let $K$ and $N$ be finite $R$-modules with $N$ free, and let $f \colon K \to N$ and $x \colon N \to M$ be linear maps such that $x \circ 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 \circ f = 0$.
Stacks Tag 058D ((1) → (4))
Every homomorphism from a finitely presented module to a flat module factors through a finite free module.
Stacks Tag 058E (only if)
Stacks Tag 00NX ((1) → (2))