English
The lifting of an idempotent along a nilpotent kernel is unique among idempotents mapping to the same image.
Русский
Подъем идемпотента вдоль нильпотентного ядра уникален среди идемпотентов, слепленных в один образ.
LaTeX
$$$\\exists! e' : R, IsIdempotentElem e' \\wedge f e' = e$$$
Lean4
/-- If `e` and `f` are idempotent elements such that `e + f = 1` and `e * f = 0`,
`S` is isomorphic as an `R`-algebra to `S ⧸ (e) × S ⧸ (f)`. -/
@[simps! -isSimp apply, simps! apply_fst apply_snd]
noncomputable def prodQuotientOfIsIdempotentElem {S : Type*} [CommRing S] [Algebra R S] {e f : S}
(he : IsIdempotentElem e) (hf : IsIdempotentElem f) (hef₁ : e + f = 1) (hef₂ : e * f = 0) :
S ≃ₐ[R] (S ⧸ Ideal.span { e }) × S ⧸ Ideal.span { f } :=
AlgEquiv.ofBijective ((Ideal.Quotient.mkₐ _ _).prod (Ideal.Quotient.mkₐ _ _)) <|
RingHom.prod_bijective_of_isIdempotentElem he hf hef₁ hef₂
