English
The image of spanSingleton under a canonical equivalence across localizations corresponds to a spanSingleton of the localized image.
Русский
Образ spanSingleton при каноническом эквивалентном отображении через локализации равен SpanSingleton локализованного образа.
LaTeX
$$$canonicalEquiv S P P' (spanSingleton S x) = spanSingleton S\\,(IsLocalization.map P' (RingHom.id R) (\\lambda y (hy : y ∈ S) => RingHom.id R y ∈ S) x)$$$
Lean4
@[simp]
theorem canonicalEquiv_spanSingleton {P'} [CommRing P'] [Algebra R P'] [IsLocalization S P'] (x : P) :
canonicalEquiv S P P' (spanSingleton S x) =
spanSingleton S
(IsLocalization.map P' (RingHom.id R) (fun y (hy : y ∈ S) => show RingHom.id R y ∈ S from hy) x) :=
by
apply SetLike.ext_iff.mpr
intro y
constructor <;> intro h
· rw [mem_spanSingleton]
obtain ⟨x', hx', rfl⟩ := (mem_canonicalEquiv_apply _ _ _).mp h
obtain ⟨z, rfl⟩ := (mem_spanSingleton _).mp hx'
use z
rw [IsLocalization.map_smul, RingHom.id_apply]
· rw [mem_canonicalEquiv_apply]
obtain ⟨z, rfl⟩ := (mem_spanSingleton _).mp h
use z • x
use (mem_spanSingleton _).mpr ⟨z, rfl⟩
simp [IsLocalization.map_smul]
