iff_characterModule_injective — Mathlib

English

Flatness of M over R is equivalent to injectivity of CharacterModule M.

Русский

Плоскость M над R эквивалентна инъективности CharacterModule M.

LaTeX

$$$\\text{Flat}(R,M) \\iff \\text{Baer}(R, \\text{CharacterModule}(M))$$$

Lean4

/-- `CharacterModule M` is an injective module iff `M` is flat.
See [Lambek_1964] for a self-contained proof. -/
theorem iff_characterModule_injective [Small.{v} R] : Flat R M ↔ Module.Injective R (CharacterModule M) := by
  rw [injective_characterModule_iff_rTensor_preserves_injective_linearMap, iff_rTensor_preserves_injective_linearMap']

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