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$, 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 all finite index types $\iota$, all elements $f \in R^{\iota}$, and all homomorphisms $x \colon R^{\iota} \to M$ such that $x(f) = 0$, there exist a finite index type $\kappa$ and module homomorphisms $a \colon R^{\iota} \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a(f) = 0$.

Of course, the module $R^\iota$ 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 homomorphisms such that $x \circ f = 0$. Then there exist a finite index type $\kappa$ and module homomorphisms $a \colon N \to R^{\kappa}$ and $y \colon R^{\kappa} \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^\iota$. This is used in the proof of Lazard's theorem.

We conclude that every homomorphism from a finitely presented module to a flat module factors through a finite free module (Module.Flat.exists_factorization_of_isFinitelyPresented).

References

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

@[reducible, inline]

abbrev Module.IsTrivialRelation {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u} [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$, 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 = ∃ (κ : Type ?u.63) (x_1 : Fintype κ) (a : ι → κ → R) (y : κ → M), (∀ (i : ι), x i = ∑ j : κ, a i j • y j) ∧ ∀ (j : κ), ∑ i : ι, f i * a i j = 0

theorem Module.isTrivialRelation_iff_vanishesTrivially {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u} [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 Module.sum_smul_eq_zero_of_isTrivialRelation {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {ι : Type u} [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) (M : Type u) [CommRing R] [AddCommGroup M] [Module R M] : [Module.Flat R M, ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I)), ∀ {ι : Type u} [inst : Fintype ι] {f : ι → R} {x : ι → M}, ∑ i : ι, f i ⊗ₜ[R] x i = 0 → TensorProduct.VanishesTrivially R f x, ∀ {ι : Type u} [inst : Fintype ι] {f : ι → R} {x : ι → M}, ∑ i : ι, f i • x i = 0 → Module.IsTrivialRelation f x, ∀ {ι : Type u} [inst : Fintype ι] {f : ι →₀ R} {x : (ι →₀ R) →ₗ[R] M}, x f = 0 → ∃ (κ : Type u) (x_1 : Fintype κ) (a : (ι →₀ R) →ₗ[R] κ →₀ R) (y : (κ →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0, ∀ {N : Type u} [inst : AddCommGroup N] [inst_1 : Module R N] [inst_2 : Module.Free R N] [inst_3 : Module.Finite R N] {f : N} {x : N →ₗ[R] M}, x f = 0 → ∃ (κ : Type u) (x_1 : Fintype κ) (a : N →ₗ[R] κ →₀ R) (y : (κ →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0].TFAE

Equational criterion for flatness Stacks 00HK, 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 index types $\iota$, all elements $f \in R^{\iota}$, and all homomorphisms $x \colon R^{\iota} \to M$ such that $x(f) = 0$, there exist a finite index type $\kappa$ and module homomorphisms $a \colon R^{\iota} \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a(f) = 0$.
• For all finite free modules $N$, all elements $f \in N$, and all homomorphisms $x \colon N \to M$ such that $x(f) = 0$, there exist a finite index type $\kappa$ and module homomorphisms $a \colon N \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a(f) = 0$.

theorem Module.Flat.iff_forall_isTrivialRelation {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ {ι : Type u} [inst : Fintype ι] {f : ι → R} {x : ι → M}, ∑ i : ι, f i • x i = 0 → Module.IsTrivialRelation f x

Equational criterion for flatness Stacks 00HK.

A module $M$ is flat if and only if every relation $\sum_i f_i x_i = 0$ in $M$ is trivial.

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

Equational criterion for flatness Stacks 00HK, forward direction.

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

theorem Module.Flat.of_forall_isTrivialRelation {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (hfx : ∀ {ι : Type u} [inst : Fintype ι] {f : ι → R} {x : ι → M}, ∑ i : ι, f i • x i = 0 → Module.IsTrivialRelation f x) : Module.Flat R M

Equational criterion for flatness Stacks 00HK, backward direction.

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

theorem Module.Flat.iff_forall_exists_factorization {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] : Module.Flat R M ↔ ∀ {ι : Type u} [inst : Fintype ι] {f : ι →₀ R} {x : (ι →₀ R) →ₗ[R] M}, x f = 0 → ∃ (κ : Type u) (x_1 : Fintype κ) (a : (ι →₀ R) →ₗ[R] κ →₀ R) (y : (κ →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0

Equational criterion for flatness Stacks 00HK, alternate form.

A module $M$ is flat if and only if for all finite free modules $R^\iota$, all $f \in R^{\iota}$, and all homomorphisms $x \colon R^{\iota} \to M$ such that $x(f) = 0$, there exist a finite free module $R^\kappa$ and homomorphisms $a \colon R^{\iota} \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a(f) = 0$.

theorem Module.Flat.exists_factorization_of_apply_eq_zero {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] {ι : Type u} [Finite ι] {f : ι →₀ R} {x : (ι →₀ R) →ₗ[R] M} (h : x f = 0) : ∃ (κ : Type u) (x_1 : Fintype κ) (a : (ι →₀ R) →ₗ[R] κ →₀ R) (y : (κ →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0

Equational criterion for flatness Stacks 00HK, forward direction, alternate form.

Let $M$ be a flat module. Let $R^\iota$ be a finite free module, let $f \in R^{\iota}$ be an element, and let $x \colon R^{\iota} \to M$ be a homomorphism such that $x(f) = 0$. Then there exist a finite free module $R^\kappa$ and homomorphisms $a \colon R^{\iota} \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a(f) = 0$.

theorem Module.Flat.of_forall_exists_factorization {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] (h : ∀ {ι : Type u} [inst : Fintype ι] {f : ι →₀ R} {x : (ι →₀ R) →ₗ[R] M}, x f = 0 → ∃ (κ : Type u) (x_1 : Fintype κ) (a : (ι →₀ R) →ₗ[R] κ →₀ R) (y : (κ →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0) : Module.Flat R M

Equational criterion for flatness Stacks 00HK, backward direction, alternate form.

Let $M$ be a module over a commutative ring $R$. Suppose that for all finite free modules $R^\iota$, all $f \in R^{\iota}$, and all homomorphisms $x \colon R^{\iota} \to M$ such that $x(f) = 0$, there exist a finite free module $R^\kappa$ and homomorphisms $a \colon R^{\iota} \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a(f) = 0$. Then $M$ is flat.

theorem Module.Flat.exists_factorization_of_apply_eq_zero_of_free {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] {N : Type u} [AddCommGroup N] [Module R N] [Module.Free R N] [Module.Finite R N] {f : N} {x : N →ₗ[R] M} (h : x f = 0) : ∃ (κ : Type u) (x_1 : Fintype κ) (a : N →ₗ[R] κ →₀ R) (y : (κ →₀ R) →ₗ[R] M), x = y ∘ₗ a ∧ a f = 0

Equational criterion for flatness Stacks 00HK, 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 homomorphism such that $x(f) = 0$. Then there exist a finite index type $\kappa$ and module homomorphisms $a \colon N \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a(f) = 0$.

theorem Module.Flat.exists_factorization_of_comp_eq_zero_of_free {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] {K : Type u} {N : Type u} [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) : ∃ (κ : Type u) (x_1 : Fintype κ) (a : N →ₗ[R] κ →₀ R) (y : (κ →₀ 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 homomorphisms such that $x \circ f = 0$. Then there exist a finite index type $\kappa$ and module homomorphisms $a \colon N \to R^{\kappa}$ and $y \colon R^{\kappa} \to M$ such that $x = y \circ a$ and $a \circ f = 0$.

theorem Module.Flat.exists_factorization_of_isFinitelyPresented {R : Type u} {M : Type u} [CommRing R] [AddCommGroup M] [Module R M] [Module.Flat R M] {P : Type u} [AddCommGroup P] [Module R P] [Module.FinitePresentation R P] (h₁ : P →ₗ[R] M) : ∃ (κ : Type u) (x : Fintype κ) (h₂ : P →ₗ[R] κ →₀ R) (h₃ : (κ →₀ R) →ₗ[R] M), h₁ = h₃ ∘ₗ h₂

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