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:R^{\iota }\to M$ such that $x(f)=0$, there exist a finite index type $\kappa$ and module homomorphisms $a:R^{\iota }\to R^{\kappa }$ and $y: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:K\to N$ and $x:N\to M$ be homomorphisms such that $x\circ f=0$. Then there exist a finite index type $\kappa$ and module homomorphisms $a:N\to R^{\kappa }$ and $y: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:R^{\iota }\to M$ such that $x(f)=0$, there exist a finite index type $\kappa$ and module homomorphisms $a:R^{\iota }\to R^{\kappa }$ and $y: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:N\to M$ such that $x(f)=0$, there exist a finite index type $\kappa$ and module homomorphisms $a:N\to R^{\kappa }$ and $y: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:R^{\iota }\to M$ such that $x(f)=0$, there exist a finite free module $R^{\kappa }$ and homomorphisms $a:R^{\iota }\to R^{\kappa }$ and $y: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:R^{\iota }\to M$ be a homomorphism such that $x(f)=0$. Then there exist a finite free module $R^{\kappa }$ and homomorphisms $a:R^{\iota }\to R^{\kappa }$ and $y: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:R^{\iota }\to M$ such that $x(f)=0$, there exist a finite free module $R^{\kappa }$ and homomorphisms $a:R^{\iota }\to R^{\kappa }$ and $y: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:N\to M$ be a homomorphism such that $x(f)=0$. Then there exist a finite index type $\kappa$ and module homomorphisms $a:N\to R^{\kappa }$ and $y: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:K\to N$ and $x:N\to M$ be homomorphisms such that $x\circ f=0$. Then there exist a finite index type $\kappa$ and module homomorphisms $a:N\to R^{\kappa }$ and $y: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.