le_comap_jacobson — Mathlib

English

For a surjective f with ker f ≤ jacobson R M, comap f (jacobson R₂ M₂) = jacobson R M.

Русский

Для сюръективного f с ker f ≤ jacobson(R,M) выполняется comap f (jacobson R₂ M₂) = jacobson R M.

LaTeX

$$comap f (jacobson R₂ M₂) = jacobson R M$$

Lean4

theorem le_comap_jacobson : jacobson R M ≤ comap f (jacobson R₂ M₂) :=
  by
  conv_rhs => rw [jacobson, sInf_eq_iInf', comap_iInf]
  refine le_iInf_iff.mpr fun S m hm ↦ ?_
  obtain h | h := isCoatom_comap_or_eq_top f S.2
  · exact mem_sInf.mp hm _ h
  · simpa only [h] using mem_top

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