Lean4
/-- **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 00HK, stacks 058D "(1) ↔ (2)"]
theorem tfae_equational_criterion :
List.TFAE
[Flat R M, ∀ I : Ideal R, Function.Injective (rTensor M I.subtype),
∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ x i = (0 : R ⊗[R] M) → VanishesTrivially R f x,
∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → 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] :=
by
classical
tfae_have 1 ↔ 2 := iff_rTensor_injective'
tfae_have 3 ↔ 2 := forall_vanishesTrivially_iff_forall_rTensor_injective R
tfae_have 3 ↔ 4 := by simp [(TensorProduct.lid R M).injective.eq_iff.symm, isTrivialRelation_iff_vanishesTrivially]
tfae_have 4 → 5
| h₄, l, f, x, hfx => by
let f' : Fin l → R := f
let x' : Fin l → M := fun i ↦ x (single i 1)
have :=
calc
∑ i, f' i • x' i
_ = ∑ i, f i • x (single i 1) := rfl
_ = x (∑ i, f i • Finsupp.single i 1) := by simp_rw [map_sum, map_smul]
_ = x f := by simp_rw [smul_single, smul_eq_mul, mul_one, univ_sum_single]
_ = 0 := hfx
obtain ⟨k, a', y', ⟨ha'y', ha'⟩⟩ := h₄ this
use k
use Finsupp.linearCombination R (fun i ↦ equivFunOnFinite.symm (a' i))
use Finsupp.linearCombination R y'
constructor
· apply Finsupp.basisSingleOne.ext
intro i
simpa [linearCombination_apply, sum_fintype, Finsupp.single_apply] using ha'y' i
· ext j
simp only [linearCombination_apply, zero_smul, implies_true, sum_fintype, finset_sum_apply]
exact ha' j
tfae_have 5 → 4
| h₅, l, f, x, hfx => by
let f' : Fin l →₀ R := equivFunOnFinite.symm f
let x' : (Fin l →₀ R) →ₗ[R] M := Finsupp.linearCombination R x
have : x' f' = 0 := by simpa [x', f', linearCombination_apply, sum_fintype] using hfx
obtain ⟨k, a', y', ha'y', ha'⟩ := h₅ this
refine ⟨k, fun i ↦ a' (single i 1), fun j ↦ y' (single j 1), fun i ↦ ?_, fun j ↦ ?_⟩
· simpa [x', ← map_smul, ← map_sum, smul_single] using LinearMap.congr_fun ha'y' (Finsupp.single i 1)
· simp_rw [← smul_eq_mul, ← Finsupp.smul_apply, ← map_smul, ← finset_sum_apply, ← map_sum, smul_single,
smul_eq_mul, mul_one, ← (fun _ ↦ equivFunOnFinite_symm_apply_toFun _ _ : ∀ x, f' x = f x), univ_sum_single]
simpa using DFunLike.congr_fun ha' j
tfae_finish
