English
There is a canonical ring isomorphism between the residue field at a maximal ideal p of R and the residue field at its localization R_p, i.e., R/p ≃ R_p / m_p.
Русский
Существует каноническое кольцевое изоморфизм между остаточным полем R/p и остаточным полем локализации R_p, т.е. R/p ≃ R_p / m_p.
LaTeX
$$$R/p \\cong R_p / \\mathfrak{m}_{R_p}$$$
Lean4
/-- The isomorphism `R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ`, where `Rₚ` satisfies
`IsLocalization.AtPrime Rₚ p`. In particular, localization preserves the residue field. -/
noncomputable def equivQuotMaximalIdealOfIsLocalization : R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ :=
by
refine
(Ideal.quotEquivOfEq ?_).trans (RingHom.quotientKerEquivOfSurjective (f := algebraMap R (Rₚ ⧸ maximalIdeal Rₚ)) ?_)
·
rw [IsScalarTower.algebraMap_eq R Rₚ, ← RingHom.comap_ker, Ideal.Quotient.algebraMap_eq, Ideal.mk_ker,
IsLocalization.AtPrime.comap_maximalIdeal Rₚ p]
· intro x
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective p.primeCompl x
obtain ⟨s', hs⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p s)⁻¹
simp only [IsScalarTower.algebraMap_eq R Rₚ (Rₚ ⧸ _), Ideal.Quotient.algebraMap_eq, RingHom.comp_apply]
use x * s'
rw [← sub_eq_zero, ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
have : algebraMap R Rₚ s ∉ maximalIdeal Rₚ :=
by
rw [← Ideal.mem_comap, IsLocalization.AtPrime.comap_maximalIdeal Rₚ p]
exact s.prop
refine ((inferInstanceAs <| (maximalIdeal Rₚ).IsPrime).mem_or_mem ?_).resolve_left this
rw [mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul, IsLocalization.mk'_mul_cancel_left, ← map_mul, ← map_sub, ←
Ideal.mem_comap, IsLocalization.AtPrime.comap_maximalIdeal Rₚ p, mul_left_comm, ← Ideal.Quotient.eq_zero_iff_mem,
map_sub, map_mul, map_mul, hs, mul_inv_cancel₀, mul_one, sub_self]
rw [Ne, Ideal.Quotient.eq_zero_iff_mem]
exact s.prop
