isIdempotentComplete_iff_idempotents_have_kernels

English

A pseudoabelian (idempotent-complete) category is equivalent to having kernels for all idempotent endomorphisms.

Русский

Псевдоабелевая (idempotent complete) категория эквивалентна существованию ядер для всех идемпотентных концевых отображений.

LaTeX

$$$ \\text{IsIdempotentComplete } C \\iff \\forall X,p, p^2=p \\Rightarrow HasKernel(p) $$$

Lean4

/-- A preadditive category is pseudoabelian iff all idempotent endomorphisms have a kernel. -/
theorem isIdempotentComplete_iff_idempotents_have_kernels [Preadditive C] :
    IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p :=
  by
  rw [isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent]
  constructor
  · intro h X p hp
    haveI : HasEqualizer (𝟙 X) (𝟙 X - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
    convert hasKernel_of_hasEqualizer (𝟙 X) (𝟙 X - p)
    rw [sub_sub_cancel]
  · intro h X p hp
    haveI : HasKernel (𝟙 _ - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
    apply Preadditive.hasEqualizer_of_hasKernel

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