map — Mathlib

English

If I = f⁻¹(J) for prime ideals I, J, then there is a canonical embedding κ(I) ↪ κ(J).

Русский

Если I = f⁻¹(J) для простых идеалов I, J, существует каноническое вложение κ(I) ↪ κ(J).

LaTeX

$$$κ(I) \hookrightarrow κ(J) \text{ canonically, when } I = f^{-1}(J).$$$

Lean4

/-- If `I = f⁻¹(J)`, then there is an canonical embedding `κ(I) ↪ κ(J)`. -/
noncomputable abbrev map (I : Ideal R) [I.IsPrime] (J : Ideal A) [J.IsPrime] (f : R →+* A) (hf : I = J.comap f) :
    I.ResidueField →+* J.ResidueField :=
  IsLocalRing.ResidueField.map (Localization.localRingHom I J f hf)

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