Theorems · Theorem · commutative algebra

Module.Flat.iff_forall_exists_factorization

∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔ ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, 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$.

Defined in

Mathlib.RingTheory.Flat.EquationalCriterion

Cited by

2 results in Mathlib

Foundations

Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModule