annihilator_eq_bot — Mathlib

English

An R-action on M is faithful iff the annihilator is the bottom ideal.

Русский

Действие кольца R на модуль M тождественно верно тогда и только тогда, когда аннигилятор равен нулю.

LaTeX

$$$\\operatorname{Ann}_R(M) = \\perp \\iff \\text{FaithfulSMul } R M$$$

Lean4

theorem annihilator_eq_bot {R M} [Ring R] [AddCommGroup M] [Module R M] :
    Module.annihilator R M = ⊥ ↔ FaithfulSMul R M :=
  by
  rw [← le_bot_iff]
  refine ⟨fun H ↦ ⟨fun {r s} H' ↦ ?_⟩, fun ⟨H⟩ {a} ha ↦ ?_⟩
  · rw [← sub_eq_zero]
    exact H (Module.mem_annihilator (r := r - s).mpr (by simp only [sub_smul, H', sub_self, implies_true]))
  · exact @H a 0 (by simp [Module.mem_annihilator.mp ha])

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