comap_jacobson — Mathlib

English

The comaps of Jacobson radical satisfy: comap f K.jacobson = sInf (comap f '' {J : Ideal S | K ≤ J ∧ J.IsMaximal}).

Русский

Комап Якобиана удовлетворяет равенству: comap f K.jacobson = sInf (comap f '' {J : Ideал S | K ≤ J ∧ J.IsMaximal}).

LaTeX

$$$\operatorname{comap} f K^{\mathrm{jacobson}} = \bigwedge \operatorname{comap} f '' \{ J : \mathrm{Ideal}(S) \mid K \le J \land J \text{ maximal} \}$$$

Lean4

theorem comap_jacobson {f : R →+* S} {K : Ideal S} :
    comap f K.jacobson = sInf (comap f '' {J : Ideal S | K ≤ J ∧ J.IsMaximal}) :=
  Trans.trans (comap_sInf' f _) sInf_eq_iInf.symm

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