Endomorphism rings under isomorphisms and additive functors

In a preadditive category, isomorphic objects have isomorphic endomorphism rings: conjugation Iso.conj is additive. The corner of End X at a split idempotent is the endomorphism ring of its image. An additive functor F induces a ring homomorphism End X →+* End (F.obj X), refining the monoid homomorphism Functor.mapEnd, and it is surjective when F is full.

Main definitions

• CategoryTheory.Iso.endRingEquiv: the ring isomorphism End X ≃+* End Y induced by X ≅ Y.
• CategoryTheory.Functor.mapEndRingHom: the ring homomorphism End X →+* End (F.obj X) of an additive functor.
• IsIdempotentElem.endRingEquivCorner: for an idempotent e = p ≫ i of X split through Y (i ≫ p = 𝟙 Y), the corner e (End X) e is the endomorphism ring of Y.

Main results

• CategoryTheory.Iso.endRingEquiv_apply_asHom and CategoryTheory.Functor.mapEndRingHom_apply_asHom: the underlying morphisms.
• CategoryTheory.Functor.mapEndRingHom_surjective: a full additive functor is surjective on endomorphism rings.
• TauCeti.isSplitEpi_or_isSplitEpi_of_add_eq_id and TauCeti.isSplitMono_or_isSplitMono_of_add_eq_id: when an object has a local endomorphism ring, a decomposition of its identity into two composites singles out a split factor.

def CategoryTheory.Iso.endRingEquiv {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {X Y : C} (φ : X ≅ Y) : End X ≃+* End Y

Isomorphic objects have isomorphic endomorphism rings: Iso.conj is additive.

@[simp]

theorem CategoryTheory.Iso.endRingEquiv_apply_asHom {C : Type u_1} [Category.{v_1, u_1} C] [Preadditive C] {X Y : C} (φ : X ≅ Y) (f : End X) : (φ.endRingEquiv f).asHom = CategoryStruct.comp φ.inv (CategoryStruct.comp f.asHom φ.hom)

The ring isomorphism of φ : X ≅ Y conjugates an endomorphism by φ.

def CategoryTheory.Functor.mapEndRingHom {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) : End X →+* End (F.obj X)

An additive functor induces a ring homomorphism on endomorphism rings, refining CategoryTheory.Functor.mapEnd.

@[simp]

theorem CategoryTheory.Functor.mapEndRingHom_apply_asHom {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) (f : End X) : ((F.mapEndRingHom X) f).asHom = F.map f.asHom

The ring homomorphism of an additive functor applies the functor to an endomorphism.

theorem CategoryTheory.Functor.mapEndRingHom_surjective {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] [F.Full] (X : C) : Function.Surjective ⇑(F.mapEndRingHom X)

A full additive functor induces a surjection on endomorphism rings.

noncomputable def IsIdempotentElem.endRingEquivCorner {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} {e : CategoryTheory.End X} (he : IsIdempotentElem e) (i : Y ⟶ X) (p : X ⟶ Y) (hip : CategoryTheory.CategoryStruct.comp i p = CategoryTheory.CategoryStruct.id Y) (hpi : CategoryTheory.CategoryStruct.comp p i = e.asHom) : CategoryTheory.End Y ≃+* he.Corner

The corner of End X at a split idempotent is the endomorphism ring of its image: if e = p ≫ i with i ≫ p = 𝟙 Y, then g ↦ p ≫ g ≫ i identifies End Y with e (End X) e.

@[simp]

theorem IsIdempotentElem.endRingEquivCorner_apply_val_asHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} {e : CategoryTheory.End X} (he : IsIdempotentElem e) (i : Y ⟶ X) (p : X ⟶ Y) (hip : CategoryTheory.CategoryStruct.comp i p = CategoryTheory.CategoryStruct.id Y) (hpi : CategoryTheory.CategoryStruct.comp p i = e.asHom) (g : CategoryTheory.End Y) : (↑((he.endRingEquivCorner i p hip hpi) g)).asHom = CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp g.asHom i)

@[simp]

theorem IsIdempotentElem.endRingEquivCorner_symm_apply_asHom {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} {e : CategoryTheory.End X} (he : IsIdempotentElem e) (i : Y ⟶ X) (p : X ⟶ Y) (hip : CategoryTheory.CategoryStruct.comp i p = CategoryTheory.CategoryStruct.id Y) (hpi : CategoryTheory.CategoryStruct.comp p i = e.asHom) (c : he.Corner) : ((he.endRingEquivCorner i p hip hpi).symm c).asHom = CategoryTheory.CategoryStruct.comp i (CategoryTheory.CategoryStruct.comp (↑c).asHom p)

theorem TauCeti.isSplitEpi_or_isSplitEpi_of_add_eq_id {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {Z A B : C} [IsLocalRing (CategoryTheory.End Z)] {a : Z ⟶ A} {x : A ⟶ Z} {b : Z ⟶ B} {y : B ⟶ Z} (h : CategoryTheory.CategoryStruct.comp a x + CategoryTheory.CategoryStruct.comp b y = CategoryTheory.CategoryStruct.id Z) : CategoryTheory.IsSplitEpi x ∨ CategoryTheory.IsSplitEpi y

The identity of an object with a local endomorphism ring cannot be a sum of two morphisms factoring through non-split-epimorphisms into it.

theorem TauCeti.isSplitMono_or_isSplitMono_of_add_eq_id {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Preadditive C] {Z A B : C} [IsLocalRing (CategoryTheory.End Z)] {x : Z ⟶ A} {a : A ⟶ Z} {y : Z ⟶ B} {b : B ⟶ Z} (h : CategoryTheory.CategoryStruct.comp x a + CategoryTheory.CategoryStruct.comp y b = CategoryTheory.CategoryStruct.id Z) : CategoryTheory.IsSplitMono x ∨ CategoryTheory.IsSplitMono y

The identity of an object with a local endomorphism ring cannot be a sum of two morphisms factoring through non-split-monomorphisms out of it.