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

• Stacks: Flat modules and flat ring maps
• Stacks: Characterizing flatness

@[reducible, inline]

abbrev Module.IsTrivialRelation {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] (f : ι → R) (x : ι → M) : Prop

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

• Module.IsTrivialRelation f x = ∃ (k : ℕ) (a : ι → Fin k → R) (y : Fin k → M), (∀ (i : ι), x i = ∑ j : Fin k, a i j • y j) ∧ ∀ (j : Fin k), ∑ i : ι, f i * a i j = 0

theorem Module.isTrivialRelation_iff_vanishesTrivially {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] {f : ι → R} {x : ι → M} : Module.IsTrivialRelation f x ↔ TensorProduct.VanishesTrivially R f x

Module.IsTrivialRelation is equivalent to the predicate TensorProduct.VanishesTrivially defined in Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean.

theorem Equiv.isTrivialRelation_comp {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] {f : ι → R} {x : ι → M} {κ : Type u_4} [Fintype κ] (e : κ ≃ ι) : Module.IsTrivialRelation (f ∘ ⇑e) (x ∘ ⇑e) ↔ Module.IsTrivialRelation f x

theorem Module.sum_smul_eq_zero_of_isTrivialRelation {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u_3} [Fintype ι] {f : ι → R} {x : ι → M} (h : Module.IsTrivialRelation f x) : ∑ i : ι, f i • x i = 0

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 Module.Flat.tfae_equational_criterion (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : [Module.Flat R M, ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I)), ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i ⊗ₜ[R] x i = 0 → TensorProduct.VanishesTrivially R f x, ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → Module.IsTrivialRelation f x, ∀ {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 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 00HK

Stacks Tag 058D (except (3))

theorem Module.Flat.iff_forall_isTrivialRelation {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → Module.IsTrivialRelation f x

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.

Stacks Tag 00HK

theorem Module.Flat.isTrivialRelation_of_sum_smul_eq_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] {ι : Type u_3} [Fintype ι] {f : ι → R} {x : ι → M} (h : ∑ i : ι, f i • x i = 0) : Module.IsTrivialRelation f x

Equational criterion for flatness, forward direction.

If $M$ is flat, then every relation $\sum_i f_i x_i = 0$ in $M$ is trivial.

Stacks Tag 00HK

theorem Module.Flat.of_forall_isTrivialRelation {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (hfx : ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i : Fin l, f i • x i = 0 → Module.IsTrivialRelation f x) : Module.Flat R M

Equational criterion for flatness, backward direction.

If every relation $\sum_i f_i x_i = 0$ in $M$ is trivial, then $M$ is flat.

Stacks Tag 00HK

theorem Module.Flat.iff_forall_exists_factorization {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] : Module.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

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))

theorem Module.Flat.of_forall_exists_factorization {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (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) : Module.Flat R M

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))

theorem Module.Flat.exists_factorization_of_apply_eq_zero_of_free {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] {N : Type u_3} [AddCommGroup N] [Module R N] [Module.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

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))

@[deprecated Module.Flat.exists_factorization_of_apply_eq_zero_of_free (since := "2025-01-03")]

theorem Module.Flat.exists_factorization_of_apply_eq_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] {N : Type u_3} [AddCommGroup N] [Module R N] [Module.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

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))

theorem Module.Flat.exists_factorization_of_comp_eq_zero_of_free {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] {K : Type u_3} {N : Type u_4} [AddCommGroup K] [Module R K] [Module.Finite R K] [AddCommGroup N] [Module R N] [Module.Free R N] [Module.Finite R N] {f : K →ₗ[R] 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

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))

theorem Module.Flat.exists_factorization_of_isFinitelyPresented {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] {P : Type u_3} [AddCommGroup P] [Module R P] [Module.FinitePresentation R P] (h₁ : P →ₗ[R] M) : ∃ (k : ℕ) (h₂ : P →ₗ[R] Fin k →₀ R) (h₃ : (Fin k →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂

Every homomorphism from a finitely presented module to a flat module factors through a finite free module.

Stacks Tag 058E (only if)

theorem Module.Flat.projective_of_finitePresentation {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] [Module.FinitePresentation R M] : Module.Projective R M

Stacks Tag 00NX ((1) → (2))