English
Let R and S be commutative semirings with an R-algebra structure, and r in R. If r is a unit in R and the underlying algebra map R → S is bijective, then the localization of S away from r exists (IsLocalization.Away r S).
Русский
Пусть R и S — коммутативные полуприводные кольца с R-алгеброй, и элемент r из R является единицей. Если отображение R → S биекция, то существует локализация кольца S away от r.
LaTeX
$$$\text{IsLocalization.Away } r S$$$
Lean4
theorem away_of_isUnit_of_bijective {R : Type*} (S : Type*) [CommSemiring R] [CommSemiring S] [Algebra R S] {r : R}
(hr : IsUnit r) (H : Function.Bijective (algebraMap R S)) : IsLocalization.Away r S :=
{ map_units := by
rintro ⟨_, n, rfl⟩
exact (algebraMap R S).isUnit_map (hr.pow _)
surj := fun z => by
obtain ⟨z', rfl⟩ := H.2 z
exact ⟨⟨z', 1⟩, by simp⟩
exists_of_eq := fun {x y} => by
rw [H.1.eq_iff]
rintro rfl
exact ⟨1, rfl⟩ }
