English
The local ring structure on Localization.P.primeCompl is established; i.e., the localization at the prime complement is a local ring.
Русский
Структура локального кольца на Localization.P.primeCompl установлена; то есть локализация по дополнению к простому идеалу является локальным кольцом.
LaTeX
$$$$ \text{IsLocalRing}( Localization.P.primeCompl ) $$$$
Lean4
theorem isLocalRing [IsLocalization.AtPrime S P] : IsLocalRing S :=
letI := AtPrime.nontrivial S P
IsLocalRing.of_nonunits_add
(by
intro x y hx hy hu
obtain ⟨z, hxyz⟩ := isUnit_iff_exists_inv.1 hu
have : ∀ {r : R} {s : P.primeCompl}, mk' S r s ∈ nonunits S → r ∈ P := fun {r s} =>
not_imp_comm.1 fun nr =>
isUnit_iff_exists_inv.2
⟨mk' S ↑s (⟨r, nr⟩ : P.primeCompl), mk'_mul_mk'_eq_one' _ _ <| show r ∈ P.primeCompl from nr⟩
rcases mk'_surjective P.primeCompl x with ⟨rx, sx, hrx⟩
rcases mk'_surjective P.primeCompl y with ⟨ry, sy, hry⟩
rcases mk'_surjective P.primeCompl z with ⟨rz, sz, hrz⟩
rw [← hrx, ← hry, ← hrz, ← mk'_add, ← mk'_mul, ← mk'_self S P.primeCompl.one_mem] at hxyz
rw [← hrx] at hx
rw [← hry] at hy
obtain ⟨t, ht⟩ := IsLocalization.eq.1 hxyz
simp only [mul_one, one_mul, Submonoid.coe_mul] at ht
suffices (t : R) * (sx * sy * sz) ∈ P from
not_or_intro (mt hp.mem_or_mem <| not_or_intro sx.2 sy.2) sz.2
(hp.mem_or_mem <| (hp.mem_or_mem this).resolve_left t.2)
rw [← ht]
exact
P.mul_mem_left _ <|
P.mul_mem_right _ <| P.add_mem (P.mul_mem_right _ <| this hx) <| P.mul_mem_right _ <| this hy)
