isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator

English

If a list rs lies in the Jacobson radical of the annihilator of M, then the regularity of M with respect to rs is equivalent to its weak regularity; i.e., IsRegular M rs ⇔ IsWeaklyRegular M rs.

Русский

Если rs лежит в радикале Якобсона аннигиллятора M, то регулярность M по rs эквивалентна слабой регулярности: IsRegular M rs ⇔ IsWeaklyRegular M rs.

LaTeX

$$$(\\forall r \\in rs)\\ r \\in \\mathrm{jacobson}(\\mathrm{Module.annihilator}(R,M)) \\;\\Rightarrow\\; IsRegular(M, rs) \\Leftrightarrow IsWeaklyRegular(M, rs)$$$

Lean4

theorem isRegular_iff_isWeaklyRegular_of_subset_jacobson_annihilator [Nontrivial M] [Module.Finite R M] {rs : List R}
    (h : ∀ r ∈ rs, r ∈ Ideal.jacobson (Module.annihilator R M)) : IsRegular M rs ↔ IsWeaklyRegular M rs :=
  Iff.trans (isRegular_iff M rs) <| and_iff_left <| top_ne_ideal_smul_of_le_jacobson_annihilator <| Ideal.span_le.mpr h

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