English
A refined version shows how to replace parts of the data with IsLocalization.Away.map while preserving P.
Русский
Уточнённая версия показывает замену части данных на IsLocalization.Away.map, сохраняя P.
LaTeX
$$$f\\mapsto P(\\text{IsLocalization.Away.map}) \\Rightarrow P(f)$$$
Lean4
theorem ofIsLocalization (hP : RingHom.OfLocalizationSpanTarget P) (hP' : RingHom.RespectsIso P) {R S : Type u}
[CommRing R] [CommRing S] (f : R →+* S) (s : Set S) (hs : Ideal.span s = ⊤)
(hT :
∀ r : s,
∃ (T : Type u) (_ : CommRing T) (_ : Algebra S T) (_ : IsLocalization.Away (r : S) T),
P ((algebraMap S T).comp f)) :
P f := by
apply hP _ s hs
intro r
obtain ⟨T, _, _, _, hT⟩ := hT r
convert hP'.1 _ (Localization.algEquiv (R := S) (Submonoid.powers (r : S)) T).symm.toRingEquiv hT
rw [← RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_eq_coe, AlgEquiv.toRingEquiv_toRingHom,
Localization.coe_algEquiv_symm, IsLocalization.map_comp, RingHom.comp_id]
