English
Canonical algebra hom from I.ResidueField to J.ResidueField given I = J.comap f.
Русский
Каноническое алгебраическое отображение κ(I) → κ(J) при I = J.comap f.
LaTeX
$$$\mathrm{map}_a: I.\mathrm{ResidueField} \to J.\mathrm{ResidueField}.$$$
Lean4
/-- If `I = f⁻¹(J)`, then there is an canonical embedding `κ(I) ↪ κ(J)`. -/
noncomputable def mapₐ (I : Ideal R) [I.IsPrime] (J : Ideal A) [J.IsPrime] (hf : I = J.comap (algebraMap R A)) :
I.ResidueField →ₐ[R] J.ResidueField
where
__ := Ideal.ResidueField.map I J (algebraMap R A) hf
commutes'
r := by
rw [IsScalarTower.algebraMap_apply R (Localization.AtPrime I), IsLocalRing.ResidueField.algebraMap_eq]
simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_coe,
IsLocalRing.ResidueField.map_residue, Localization.localRingHom_to_map]
rfl
