Additive functors on objects with local endomorphism rings

A full additive functor sends a local endomorphism ring to a local endomorphism ring, provided the image object is nonzero. It also reflects isomorphisms between objects with local endomorphism rings whose images are nonzero. Only surjectivity on the relevant hom-sets is needed. These results let additive quotients retain indecomposability and distinguish isomorphism classes even though they are not faithful.

No splitting of idempotents in the quotient is required: locality of its endomorphism ring already rules out nontrivial biproduct decompositions.

theorem CategoryTheory.Functor.isIso_of_map_eq_id_of_isLocalRing_end {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X : C} [IsLocalRing (End X)] (hX : ¬Limits.IsZero (F.obj X)) (f : X ⟶ X) (hf : F.map f = CategoryStruct.id (F.obj X)) : IsIso f

An endomorphism of an object with local endomorphism ring is invertible if an additive functor sends it to the identity of a nonzero object.

theorem CategoryTheory.Functor.indecomposable_obj_of_map_surjective_of_isLocalRing_end {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X : C} [Limits.HasBinaryBiproducts D] [IsLocalRing (End X)] (hX : ¬Limits.IsZero (F.obj X)) (hF : Function.Surjective F.map) : Indecomposable (F.obj X)

A nonzero image under an additive functor is indecomposable if the original object's endomorphism ring is local and the functor is surjective on its endomorphisms.

theorem CategoryTheory.Functor.isIso_of_map_isIso_of_isLocalRing_end {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X Y : C} [IsLocalRing (End X)] [IsLocalRing (End Y)] (hX : ¬Limits.IsZero (F.obj X)) (hF : Function.Surjective F.map) (f : X ⟶ Y) [IsIso (F.map f)] : IsIso f

An additive functor surjective on morphisms from Y to X reflects invertibility of a morphism from X to Y when their endomorphism rings are local and the source image is nonzero.

theorem CategoryTheory.Functor.nonempty_iso_obj_iff_of_isLocalRing_end {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Preadditive C] [Preadditive D] (F : Functor C D) [F.Additive] {X Y : C} [IsLocalRing (End X)] [IsLocalRing (End Y)] (hX : ¬Limits.IsZero (F.obj X)) (hF : Function.Surjective F.map) (hF' : Function.Surjective F.map) : Nonempty (F.obj X ≅ F.obj Y) ↔ Nonempty (X ≅ Y)

An additive functor surjective on morphisms in both directions between two objects detects their isomorphism classes when their endomorphism rings are local and the source image is nonzero.