English
Localizing an Artinian ring can only reduce the amount of elements; the canonical map R → L is surjective.
Русский
Локализация артинианова кольца не увеличивает множество элементов; каноническое отображение R → L сюръективно.
LaTeX
$$$\operatorname{Surjective}(\text{algebraMap } R L)$$$
Lean4
/-- Localizing an Artinian ring can only reduce the amount of elements. -/
theorem localization_surjective : Function.Surjective (algebraMap R L) :=
by
intro r'
obtain ⟨r₁, s, rfl⟩ := IsLocalization.mk'_surjective S r'
rsuffices ⟨r₂, h⟩ : ∃ r : R, IsLocalization.mk' L 1 s = algebraMap R L r
· exact ⟨r₁ * r₂, by rw [IsLocalization.mk'_eq_mul_mk'_one, map_mul, h]⟩
obtain ⟨n, r, hr⟩ := IsArtinian.exists_pow_succ_smul_dvd (s : R) (1 : R)
use r
rw [smul_eq_mul, smul_eq_mul, pow_succ, mul_assoc] at hr
apply_fun algebraMap R L at hr
simp only [map_mul] at hr
rw [← IsLocalization.mk'_one (M := S) L, IsLocalization.mk'_eq_iff_eq, mul_one, Submonoid.coe_one, ←
(IsLocalization.map_units L (s ^ n)).mul_left_cancel hr, map_mul]
