existsUnique_isIdempotentElem_eq_of_ker_isNilpotent

English

If f has nilpotent kernel and e ∈ S is idempotent with a lift, then this lift is unique among idempotents mapping to e.

Русский

Если ядро f нильпотентно и e идемпотент, и имеется подъем, то этот подъем единственен среди идемпотентов, сопоставляемых e.

LaTeX

$$$\\exists! e' : R, IsIdempotentElem e' \\wedge f e' = e$$$

Lean4

@[stacks 00J9]
theorem existsUnique_isIdempotentElem_eq_of_ker_isNilpotent (h : ∀ x ∈ RingHom.ker f, IsNilpotent x) (e : S)
    (he : e ∈ f.range) (he' : IsIdempotentElem e) : ∃! e' : R, IsIdempotentElem e' ∧ f e' = e :=
  by
  obtain ⟨e', he₂, rfl⟩ := exists_isIdempotentElem_eq_of_ker_isNilpotent f h e he he'
  exact
    ⟨e', ⟨he₂, rfl⟩, fun x ⟨hx, hx'⟩ ↦
      eq_of_isNilpotent_sub_of_isIdempotentElem hx he₂ (h _ (by rw [RingHom.mem_ker, map_sub, hx', sub_self]))⟩

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