English
If e is idempotent in a ring R and ker(algebraMap R S) = span{1 − e} and the algebra map is surjective, then the localization away from e exists.
Русский
Если e идемпотент в кольце R и ker(алгебраическое отображение) равно дополнению 1−e и отображение на S сюръективно, то локализация away от e существует.
LaTeX
$$$\text{Away } e S$$$
Lean4
theorem away_of_isIdempotentElem {R S} [CommRing R] [CommRing S] [Algebra R S] {e : R} (he : IsIdempotentElem e)
(H : RingHom.ker (algebraMap R S) = Ideal.span {1 - e}) (H' : Function.Surjective (algebraMap R S)) :
IsLocalization.Away e S :=
away_of_isIdempotentElem_of_mul he
(fun x y ↦
by
rw [← sub_eq_zero, ← map_sub, ← RingHom.mem_ker, H, ← he.ker_toSpanSingleton_eq_span, LinearMap.mem_ker,
LinearMap.toSpanSingleton_apply, sub_smul, sub_eq_zero]
simp_rw [mul_comm e, smul_eq_mul])
H'
