English
Let R be a commutative semiring, S a submonoid of R, M and M' additive commutative monoids with R- and A-structures as in localization. For a linear map g: M → M' that is localized with respect to S, an element m ∈ M lies in the kernel of g if and only if there exists r ∈ S such that r • m = 0.
Русский
Пусть R — коммутативный полупдомножитель, S — подмоноид R, M и M' — коммутативные моноиды, с соответствующими модулярными структурами, локализованные по S. Для линейного отображения g: M → M', локализованного по S, элемент m ∈ M принадлежит ядру g тогда и только тогда, когда существует r ∈ S такое, что r • m = 0.
LaTeX
$$$\displaystyle m \in \ker g \quad\Longleftrightarrow\quad \exists r \in S,\ r \cdot m = 0$$$
Lean4
theorem mem_ker_iff (S : Submonoid R) {g : M →ₗ[R] M'} [IsLocalizedModule S g] {m : M} :
m ∈ LinearMap.ker g ↔ ∃ r ∈ S, r • m = 0 := by simpa using IsLocalizedModule.eq_zero_iff S g
