isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul

English

A submodule S is primary iff S ≠ ⊤ and for all r in R and x in M/S, x ≠ 0 and r•x = 0 implies ∃n with r^n•⊤ ≤ S.

Русский

Подмодуль S примарный тогда и только тогда, когда S ≠ ⊤ и ∀ r ∈ R, x ∈ M/S: x ≠ 0 и r•x = 0 ⇒ ∃ n:ℕ, r^n•⊤ ≤ S.

LaTeX

$$S.IsPrimary ↔ (S ≠ ⊤ ∧ ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ n : ℕ, r ^ n • (⊤ : Submodule R (M ⧸ S)) ≤ S)$$

Lean4

theorem isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul :
    S.IsPrimary ↔ S ≠ ⊤ ∧ ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ n : ℕ, r ^ n • (⊤ : Submodule R (M ⧸ S)) = ⊥ :=
  by
  refine (and_congr_right fun _ ↦ ?_)
  simp_rw [S.mkQ_surjective.forall, ← map_smul, ne_eq, ← LinearMap.mem_ker, ker_mkQ]
  congr! 2
  rw [forall_comm, ← or_iff_not_imp_left, ← LinearMap.range_eq_top.mpr S.mkQ_surjective, ← map_top]
  simp_rw [eq_bot_iff, ← map_pointwise_smul, map_le_iff_le_comap, comap_bot, ker_mkQ]

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