English
If e is an idempotent element of a ring R, and certain compatibility and surjectivity conditions hold for the kernel of the algebra map and the relevant multiplicative set, then the localization away from e exists.
Русский
Если e является идемпотентом в кольце R, и выполняются соответствующие условия совместимости и сюръективности для ядра отображения алгебры и соответствующего множества, то локализация away от e существует.
LaTeX
$$$\text{Away } e S$$$
Lean4
theorem away_of_isIdempotentElem_of_mul {R S} [CommSemiring R] [CommSemiring S] [Algebra R S] {e : R}
(he : IsIdempotentElem e) (H : ∀ x y, algebraMap R S x = algebraMap R S y ↔ e * x = e * y)
(H' : Function.Surjective (algebraMap R S)) : IsLocalization.Away e S
where
map_units
r := by
obtain ⟨r, n, rfl⟩ := r
simp [show algebraMap R S e = 1 by rw [← (algebraMap R S).map_one, H, mul_one, he]]
surj
z := by
obtain ⟨z, rfl⟩ := H' z
exact ⟨⟨z, 1⟩, by simp⟩
exists_of_eq {x y} h := ⟨⟨e, Submonoid.mem_powers e⟩, (H x y).mp h⟩
