English
If you have surjective ring homomorphisms fitting certain compatibility conditions, localization transfers across the functor, yielding a localization of the mapped submonoid.
Русский
При сюръективности гомоморфизмов и совместимости локализация сохраняется и распространяется через отображение.
LaTeX
$$$\\text{IsLocalization.of_surjective} \\; f,g,H,H' : \\; \\text{IsLocalization} (M.map f) S'$$$
Lean4
theorem of_surjective {R' S' : Type*} [CommRing R'] [CommRing S'] [Algebra R' S'] (f : R →+* R')
(hf : Function.Surjective f) (g : S →+* S') (hg : Function.Surjective g)
(H : g.comp (algebraMap R S) = (algebraMap _ _).comp f)
(H' : RingHom.ker g ≤ (RingHom.ker f).map (algebraMap R S)) : IsLocalization (M.map f) S'
where
map_units := by
rintro ⟨_, y, hy, rfl⟩
simpa only [← RingHom.comp_apply, H] using (IsLocalization.map_units S ⟨y, hy⟩).map g
surj := by
intro z
obtain ⟨z, rfl⟩ := hg z
obtain ⟨⟨r, s⟩, e⟩ := IsLocalization.surj M z
refine ⟨⟨f r, _, s.1, s.2, rfl⟩, ?_⟩
simpa only [map_mul, ← RingHom.comp_apply, H] using DFunLike.congr_arg g e
exists_of_eq := by
intro x y e
obtain ⟨x, rfl⟩ := hf x
obtain ⟨y, rfl⟩ := hf y
rw [← sub_eq_zero, ← map_sub, ← map_sub, ← RingHom.comp_apply, ← H, RingHom.comp_apply, ←
IsLocalization.mk'_one (M := M)] at e
obtain ⟨r, hr, hr'⟩ := (IsLocalization.mk'_mem_map_algebraMap_iff M _ _ _ _).mp (H' e)
exact ⟨⟨_, r, hr, rfl⟩, by simpa [sub_eq_zero, mul_sub] using hr'⟩
