torsion_eq_bot — Mathlib

English

If M is a flat module over a commutative ring R, then the torsion submodule of M is {0}. In other words, flat modules have no torsion.

Русский

Если M — плоский модуль над коммутативной кольцом R, то торсионный подмодуль M равен нулю. Иными словами, у плоских модулей нет торсиона.

LaTeX

$$$\\operatorname{torsion}_R(M) = \\bot$$$

Lean4

/-- Flat modules have no torsion. -/
theorem torsion_eq_bot [Flat R M] : torsion R M = ⊥ :=
  by
  rw [eq_bot_iff]
    -- indeed the definition of torsion means "annihiliated by a nonzerodivisor"

  rintro m
    ⟨⟨r, hr⟩, h⟩
        -- and we just showed that 0 is the only element with this property

  exact isSMulRegular_of_nonZeroDivisors hr (by simpa using h)

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