English
There is a natural equivalence of localizations induced by a base ring equivalence h, giving an iff between IsLocalization M S and IsLocalization (M.map h) S.
Русский
Существуют естественные эквивалентности локализаций, индуцируемые базовым эквивалентом кольца h, образующие эквивалентность IsLocalization M S и IsLocalization (M.map h) S.
LaTeX
$$$$ \\text{IsLocalization } M S \\ \\Longleftrightarrow\\ \\text{IsLocalization } (M.map h) S $$$$
Lean4
theorem isLocalization_iff_of_base_ringEquiv (h : R ≃+* P) :
IsLocalization M S ↔
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
refine ⟨fun _ => isLocalization_of_base_ringEquiv M S h, ?_⟩
intro (H : IsLocalization (Submonoid.map (h : R ≃* P) M) S)
convert isLocalization_of_base_ringEquiv (Submonoid.map (h : R ≃* P) M) S h.symm
· rw [← Submonoid.map_coe_toMulEquiv, RingEquiv.coe_toMulEquiv_symm, ← Submonoid.comap_equiv_eq_map_symm,
Submonoid.comap_map_eq_of_injective]
exact h.toEquiv.injective
rw [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc]
simp only [RingHom.comp_id, RingEquiv.symm_symm, RingEquiv.symm_toRingHom_comp_toRingHom]
apply Algebra.algebra_ext
intro r
rw [RingHom.algebraMap_toAlgebra]
