English
Let R be a commutative ring and a,b ∈ R with a a non-zero-divisor. Then the a-torsion submodule of the quotient R/(a b) is precisely the span of the class of b in that quotient; i.e., the torsion by a is generated by the image of b.
Русский
Пусть R — коммутативное кольцо, a,b ∈ R и a не является нулевой делителем. Тогда a-тормционная подпольная подмодуль вR/(ab) порождается образом m(b) класса b, то есть множество якорено классом b.
LaTeX
$$$ torsionBy_R\\left(R \\big/ (R \\cdot a b)\\right) a = R \\cdot \\overline{b}, \\quad \\text{where } \\overline{b} = \\mathrm{mk}\\left(R \\cdot a b\\right) b$$$
Lean4
theorem torsionBy_eq_span_singleton {R : Type w} [CommRing R] (a b : R) (ha : a ∈ R⁰) :
torsionBy R (R ⧸ R ∙ a * b) a = R ∙ mk (R ∙ a * b) b :=
by
ext x; rw [mem_torsionBy_iff, Submodule.mem_span_singleton]
obtain ⟨x, rfl⟩ := mk_surjective x; constructor <;> intro h
· rw [← mk_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero, Submodule.mem_span_singleton] at h
obtain ⟨c, h⟩ := h
rw [smul_eq_mul, smul_eq_mul, mul_comm, mul_assoc, mul_cancel_left_mem_nonZeroDivisors ha, mul_comm] at h
use c
rw [← h, ← mk_eq_mk, ← Quotient.mk_smul, smul_eq_mul, mk_eq_mk]
· obtain ⟨c, h⟩ := h
rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul, (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _,
smul_zero]
