iff_lTensor_injective — Mathlib

English

An R-module M is flat if and only if every finitely generated ideal I of R induces an injective map I ⊗ M → M.

Русский

Модуль M над R плоский тогда и только тогда, когда для каждого финитно порожденного идеала I кольца R соответствующее отображение I ⊗ M → M инъективно.

LaTeX

$$$\text{Flat } R M \iff \forall I,\; I. FG \to (I.\mathrm{subtype}.lTensor M)\text{ инъективно}$$$

Lean4

/-- The `lTensor`-variant of `iff_rTensor_injective`. -/
theorem iff_lTensor_injective : Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective (I.subtype.lTensor M) := by
  simpa [← comm_comp_rTensor_comp_comm_eq] using iff_rTensor_injective

Похожие утверждения