English
Orthogonal idempotents lift along nil ideals: under hypotheses on a RingHom f, there exists e' ∈ R with e' idempotent and f e' = e₁ with e' annihilating e₂ from both sides.
Русский
Идемпотенты поднимаются через нильпотентные ядра: при условии на RingHom f существует e' ∈ R такого что e' идемпотентно и f e' = e₁, а e' и e₂ взаимно annihilируют.
LaTeX
$$∃ e' : R, IsIdempotentElem e' ∧ f e' = e₁ ∧ e' e₂ = 0 ∧ e₂ e' = 0$$
Lean4
/-- Orthogonal idempotents lift along nil ideals. -/
theorem exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) (e₁ : S)
(he : e₁ ∈ f.range) (he₁ : IsIdempotentElem e₁) (e₂ : R) (he₂ : IsIdempotentElem e₂) (he₁e₂ : e₁ * f e₂ = 0)
(he₂e₁ : f e₂ * e₁ = 0) : ∃ e' : R, IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0 ∧ e₂ * e' = 0 :=
by
obtain ⟨e', h₁, rfl, h₂⟩ := exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent_aux f h e₁ he he₁ e₂ he₂ he₁e₂
refine ⟨(1 - e₂) * e', ?_, ?_, ?_, ?_⟩
· rw [IsIdempotentElem, mul_assoc, ← mul_assoc e', mul_sub, mul_one, h₂, sub_zero, h₁.eq]
· rw [map_mul, map_sub, map_one, sub_mul, one_mul, he₂e₁, sub_zero]
· rw [mul_assoc, h₂, mul_zero]
· rw [← mul_assoc, mul_sub, mul_one, he₂.eq, sub_self, zero_mul]
