Theorems · Theorem · ring theory

exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent

∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (∀ x ∈ RingHom.ker f, IsNilpotent x) →
    ∀ e₁ ∈ f.range,
      IsIdempotentElem e₁ →
        ∀ (e₂ : R),
          IsIdempotentElem e₂ →
            e₁ * f e₂ = 0 → f e₂ * e₁ = 0 → ∃ e', IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0 ∧ e₂ * e' = 0

Orthogonal idempotents lift along nil ideals.

Defined in

Mathlib.RingTheory.Idempotents

Cited by

2 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingRing