Documentation

Mathlib.RingTheory.Flat.EquationalCriterion

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:

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 #

@[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) :

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
Instances For
    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 = 0TensorProduct.VanishesTrivially R f x, ∀ {ι : Type u} [inst : Fintype ι] {f : ιR} {x : ιM}, i : ι, f i x i = 0Module.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 = 0Module.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) :

    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 = 0Module.IsTrivialRelation f x) :

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

    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.