English
If M is a localization datum over R and h: R ≃+* P is a ring equivalence, then M maps to a localization of S via h.
Русский
Если M — локализационные данные над R и h: R ≃+* P является кольцевым эквивалентом, то M отображается в локализацию S через h.
LaTeX
$$$$ \\text{IsLocalization } M S \\Rightarrow \\text{IsLocalization } (M.map\, h) S $$$$
Lean4
theorem isLocalization_of_base_ringEquiv [IsLocalization M S] (h : R ≃+* P) :
haveI := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
IsLocalization (M.map h) S :=
by
letI : Algebra P S := ((algebraMap R S).comp h.symm.toRingHom).toAlgebra
constructor
· rintro ⟨_, ⟨y, hy, rfl⟩⟩
convert IsLocalization.map_units S ⟨y, hy⟩
dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply]
exact congr_arg _ (h.symm_apply_apply _)
· intro y
obtain ⟨⟨x, s⟩, e⟩ := IsLocalization.surj M y
refine ⟨⟨h x, _, _, s.prop, rfl⟩, ?_⟩
dsimp only [RingHom.algebraMap_toAlgebra, RingHom.comp_apply] at e ⊢
convert e <;> exact h.symm_apply_apply _
· intro x y
rw [RingHom.algebraMap_toAlgebra, RingHom.comp_apply, RingHom.comp_apply, IsLocalization.eq_iff_exists M S]
simp [← h.toEquiv.apply_eq_iff_eq]
