English
There exists a canonical ring isomorphism between the quotient S/ pS and the localized quotient S_p / pS_p, constructed from the universal properties of quotient and localization in the given setting.
Русский
Существует канонический кольцевой изоморфизм между фактором S/ pS и локализованным фактором S_p / pS_p, строящийся из универсальных свойств факторирования и локализации.
LaTeX
$$$S/ pS \\cong S_p / pS_p$$$
Lean4
/-- The isomorphism `S ⧸ pS ≃+* Sₚ ⧸ pSₚ`. -/
noncomputable def quotMapEquivQuotMapMaximalIdealOfIsLocalization : S ⧸ pS ≃+* Sₚ ⧸ pSₚ :=
by
haveI h : pSₚ = Ideal.map (algebraMap S Sₚ) pS := by
rw [← IsLocalization.AtPrime.map_eq_maximalIdeal p Rₚ, Ideal.map_map, ← IsScalarTower.algebraMap_eq, Ideal.map_map,
← IsScalarTower.algebraMap_eq]
refine (Ideal.quotEquivOfEq ?_).trans (RingHom.quotientKerEquivOfSurjective (f := algebraMap S (Sₚ ⧸ pSₚ)) ?_)
·
rw [IsScalarTower.algebraMap_eq S Sₚ, Ideal.Quotient.algebraMap_eq, ← RingHom.comap_ker, Ideal.mk_ker, h,
Ideal.map_map, ← IsScalarTower.algebraMap_eq, comap_map_eq_map_of_isLocalization_algebraMapSubmonoid]
· intro x
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
obtain ⟨x, s, rfl⟩ := IsLocalization.mk'_surjective (Algebra.algebraMapSubmonoid S p.primeCompl) x
obtain ⟨α, hα : α ∉ p, e⟩ := s.prop
obtain ⟨β, γ, hγ, hβ⟩ : ∃ β γ, γ ∈ p ∧ α * β = 1 + γ :=
by
obtain ⟨β, hβ⟩ := Ideal.Quotient.mk_surjective (I := p) (Ideal.Quotient.mk p α)⁻¹
refine ⟨β, α * β - 1, ?_, ?_⟩
· rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, map_one, map_mul, hβ, mul_inv_cancel₀, sub_self]
rwa [Ne, Ideal.Quotient.eq_zero_iff_mem]
· rw [add_sub_cancel]
use β • x
rw [IsScalarTower.algebraMap_eq S Sₚ (Sₚ ⧸ pSₚ), Ideal.Quotient.algebraMap_eq, RingHom.comp_apply, ← sub_eq_zero, ←
map_sub, Ideal.Quotient.eq_zero_iff_mem]
rw [h, IsLocalization.mem_map_algebraMap_iff (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
refine ⟨⟨⟨γ • x, ?_⟩, s⟩, ?_⟩
· rw [Algebra.smul_def]
apply Ideal.mul_mem_right
exact Ideal.mem_map_of_mem _ hγ
simp only
rw [mul_comm, mul_sub, IsLocalization.mul_mk'_eq_mk'_of_mul, IsLocalization.mk'_mul_cancel_left, ← map_mul, ← e, ←
Algebra.smul_def, smul_smul, hβ, ← map_sub, add_smul, one_smul, add_comm x, add_sub_cancel_right]
