map_jacobson_of_ker_le — Mathlib

English

If N ≤ jacobson R M, then jacobson R (M / N) = map N.mkQ (jacobson R M).

Русский

Если N ≤ jacobson(R,M), то jacobson(R, M/N) = map N.mkQ (jacobson R M).

LaTeX

$$le ⇒ jacobson R (M / N) = map N.mkQ (jacobson R M)$$

Lean4

theorem map_jacobson_of_ker_le (surj : Function.Surjective f) (le : LinearMap.ker f ≤ jacobson R M) :
    map f (jacobson R M) = jacobson R₂ M₂ :=
  le_antisymm (map_jacobson_le f) <| by
    rw [jacobson, sInf_eq_iInf'] at le
    conv_rhs => rw [jacobson, sInf_eq_iInf', map_iInf_of_ker_le surj le]
    exact le_iInf fun m ↦ sInf_le (isCoatom_map_of_ker_le surj (le_iInf_iff.mp le m) m.2)

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