linearMap_subsingleton_of_mem_annihilator

English

If reg on M and r annihilates N, then any linear map N → M is unique (zero).

Русский

Если r действует как регуляр на M, а r аннигилирует N, то всякое линейное отображение N → M уникально (нулевое).

LaTeX

$$$\text{If } \mathrm{IsSmulRegular}(M,r) \text{ and } r\in\mathrm{Ann}(N),\; (N\to_R M)\text{ is a singleton.}$$$

Lean4

theorem linearMap_subsingleton_of_mem_annihilator {r : R} (reg : IsSMulRegular M r)
    (mem_ann : r ∈ Module.annihilator R N) : Subsingleton (N →ₗ[R] M) :=
  by
  apply subsingleton_of_forall_eq 0 (fun f ↦ ext fun x ↦ ?_)
  have : r • (f x) = r • 0 := by rw [smul_zero, ← map_smul, Module.mem_annihilator.mp mem_ann x, map_zero]
  simpa using reg this

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