Idempotent completeness from nilpotent functor kernels

An idempotent lifts along a surjective ring homomorphism when every element of its kernel is nilpotent. Applied to endomorphism rings, this shows that a full, essentially surjective additive functor out of an idempotent-complete category has idempotent-complete target as soon as its endomorphism kernels are elementwise nilpotent.

def MBDVendor.QSE.CategoryTheory.IdempotentLifting.FunctorKernelSquareZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) : Prop

The kernel ideal of an additive functor is square-zero: any composite of two composable morphisms killed by the functor vanishes.

theorem MBDVendor.QSE.CategoryTheory.IdempotentLifting.reflectsIso_of_kernelSquareZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Full] (hF : FunctorKernelSquareZero F) {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso (F.map f)] : CategoryTheory.IsIso f

A full additive functor with square-zero kernel reflects isomorphisms. This is the categorical inverse-lifting argument used for separated representations.

theorem MBDVendor.QSE.CategoryTheory.IdempotentLifting.reflectsIsomorphisms_of_kernelSquareZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Full] (hF : FunctorKernelSquareZero F) : F.ReflectsIsomorphisms

Package inverse lifting as the standard categorical reflection property.

noncomputable def MBDVendor.QSE.CategoryTheory.IdempotentLifting.isoOfMapIsoOfKernelSquareZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Full] (hF : FunctorKernelSquareZero F) {X Y : C} (e : F.obj X ≅ F.obj Y) : X ≅ Y

Any isomorphism between two functor images lifts to an isomorphism between the source objects.

theorem MBDVendor.QSE.CategoryTheory.IdempotentLifting.image_idempotent_splits {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.IsIdempotentComplete C] (X : C) (hsurjective : Function.Surjective fun (f : CategoryTheory.End X) => F.map f) (hker : ∀ (f : CategoryTheory.End X), F.map f = 0 → IsNilpotent f) (p : CategoryTheory.End (F.obj X)) (hp : CategoryTheory.CategoryStruct.comp p p = p) : ∃ (Y : D) (i : Y ⟶ F.obj X) (e : F.obj X ⟶ Y), CategoryTheory.CategoryStruct.comp i e = CategoryTheory.CategoryStruct.id Y ∧ CategoryTheory.CategoryStruct.comp e i = p

An idempotent on the image of an object splits when the endomorphism map is surjective, its kernel is elementwise nilpotent, and idempotents split in the source category.

theorem MBDVendor.QSE.CategoryTheory.IdempotentLifting.isIdempotentComplete_of_ker_mapEnd_isNilpotent {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Full] [F.EssSurj] [CategoryTheory.IsIdempotentComplete C] (hker : ∀ (X : C) (f : CategoryTheory.End X), F.map f = 0 → IsNilpotent f) : CategoryTheory.IsIdempotentComplete D

A full, essentially surjective additive functor with elementwise nilpotent endomorphism kernels transports idempotent completeness to its target.

theorem MBDVendor.QSE.CategoryTheory.IdempotentLifting.isIdempotentComplete_of_objectwise_nilpotent_kernel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] [F.Full] [CategoryTheory.IsIdempotentComplete C] (hcover : ∀ (Y : D), ∃ (X : C) (x : F.obj X ≅ Y), ∀ (f : CategoryTheory.End X), F.map f = 0 → IsNilpotent f) : CategoryTheory.IsIdempotentComplete D

It suffices to have, for each target object, one isomorphic functor image on whose endomorphism ring the functor kernel is elementwise nilpotent. This form permits discarding direct summands which the functor sends to zero.