quotient_of_isIdempotentElem — Mathlib

English

If e is an idempotent element of R, then R localized away from e is isomorphic to the quotient of R by the ideal generated by 1 − e; equivalently, the localization away from e factors through the quotient R/(1−e).

Русский

Если e — идемпотентный элемент кольца R, то локализация по e эквивалентна фактор-мированию по идеалу, порождаемому 1−e, то есть R/(1−e) является локализацией по e.

LaTeX

$$$\operatorname{IsLocalization.Away}\,e\bigl(R \big/ \operatorname{Ideal.span}\{1 - e\}\bigr)\,,$$$

Lean4

theorem quotient_of_isIdempotentElem {e : R} (he : IsIdempotentElem e) :
    IsLocalization.Away e (R ⧸ Ideal.span {1 - e}) :=
  away_of_isIdempotentElem he Ideal.mk_ker Quotient.mk_surjective

Похожие утверждения