isSMulRegular_quotient_iff_mem_of_smul_mem

English

Let R be a ring, M an R-module, N a submodule of M, and r an element of R. The action of r is regular on the quotient M/N if and only if for every x in M, r · x ∈ N implies x ∈ N.

Русский

Пусть R — кольцо, M — модуль над R, N — подсистема M и r ∈ R. Действие на M/N регуларно по r тогда и только тогда, когда для каждого x ∈ M выполняется: r · x ∈ N ⇒ x ∈ N.

LaTeX

$$$\operatorname{IsSMulRegular}(M/N)\, r \iff \forall x \in M,\ r \cdot x \in N \rightarrow x \in N$$$

Lean4

theorem isSMulRegular_quotient_iff_mem_of_smul_mem : IsSMulRegular (M ⧸ N) r ↔ ∀ x : M, r • x ∈ N → x ∈ N :=
  isSMulRegular_iff_right_eq_zero_of_smul.trans <|
    N.mkQ_surjective.forall.trans <| by simp_rw [← map_smul, N.mkQ_apply, Submodule.Quotient.mk_eq_zero]

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