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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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 QuotientSubmoduleEquidistribution.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.