Functoriality of quotients by morphism ideals

An additive functor F : C ⥤ D pulls a morphism ideal of D back to one of C. Consequently, if F carries an ideal I into an ideal J, it induces an additive functor C/I ⥤ D/J. Natural transformations descend to these quotient functors, and the construction respects identities and composition.

This is the functorial part of the universal property of an additive quotient. In particular, it is the mechanism by which an additive functor preserving projective-injective objects will induce a functor between stable categories.

Main definitions

• TauCeti.MorphismIdeal.comap: the inverse image of a morphism ideal under an additive functor.
• TauCeti.MorphismIdeal.map: the functor induced between quotient categories.
• TauCeti.MorphismIdeal.mapNatTrans and TauCeti.MorphismIdeal.mapNatIso: the natural transformation and natural isomorphism induced between quotient functors.

Main results

• TauCeti.MorphismIdeal.comap_eq_of_iso: naturally isomorphic functors pull back an ideal to the same ideal.
• TauCeti.MorphismIdeal.map_id and TauCeti.MorphismIdeal.map_comp: quotient functors preserve identities and composition.
• TauCeti.MorphismIdeal.kerIdeal_comp_quotientFunctor and TauCeti.MorphismIdeal.map_eq_lift: the kernel of the composite with a quotient functor and the expression of map as a lift.
• TauCeti.MorphismIdeal.mapNatTrans_id and TauCeti.MorphismIdeal.comp_mapNatTrans: descent of natural transformations preserves identities and vertical composition.

References

• M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, CUP (1995), Chapter IV, Section 1.
• D. Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, LMS Lecture Note Series 119, CUP (1988), Section I.2.

Pullback of ideals

def TauCeti.MorphismIdeal.comap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (J : MorphismIdeal D) (F : CategoryTheory.Functor C D) [F.Additive] : MorphismIdeal C

The inverse image of a morphism ideal under an additive functor. A morphism belongs to J.comap F precisely when its image under F belongs to J.

Equations

• J.comap F = { hom := fun (X Y : C) => AddSubgroup.comap F.mapAddHom (J.hom (F.obj X) (F.obj Y)), comp_mem_left := ⋯, comp_mem_right := ⋯ }

@[simp]

theorem TauCeti.MorphismIdeal.mem_comap_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (J : MorphismIdeal D) (F : CategoryTheory.Functor C D) [F.Additive] {X Y : C} {f : X ⟶ Y} : f ∈ (J.comap F).hom X Y ↔ F.map f ∈ J.hom (F.obj X) (F.obj Y)

A morphism belongs to the pullback ideal exactly when its image belongs to the original ideal.

theorem TauCeti.MorphismIdeal.comap_mono {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] {J J' : MorphismIdeal D} (h : J ≤ J') : J.comap F ≤ J'.comap F

Pullback of ideals is monotone.

@[simp]

theorem TauCeti.MorphismIdeal.comap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.comap (CategoryTheory.Functor.id C) = I

Pulling an ideal back along the identity functor leaves it unchanged.

@[simp]

theorem TauCeti.MorphismIdeal.comap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Preadditive E] (K : MorphismIdeal E) (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.Additive] [G.Additive] : K.comap (F.comp G) = (K.comap G).comap F

Pullback along a composite functor is the composite of the two pullbacks.

theorem TauCeti.MorphismIdeal.comap_eq_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (J : MorphismIdeal D) {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F ≅ G) : J.comap F = J.comap G

Pullback of ideals only depends on the functor up to natural isomorphism.

theorem TauCeti.MorphismIdeal.le_comap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Preadditive E] (I : MorphismIdeal C) (J : MorphismIdeal D) (K : MorphismIdeal E) (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.Additive] [G.Additive] (hF : I ≤ J.comap F) (hG : J ≤ K.comap G) : I ≤ K.comap (F.comp G)

If F carries I into J and G carries J into K, then F ⋙ G carries I into K.

Functors between quotients

@[simp]

theorem TauCeti.MorphismIdeal.kerIdeal_comp_quotientFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (J : MorphismIdeal D) (F : CategoryTheory.Functor C D) [F.Additive] : (F.comp J.quotientFunctor).kerIdeal = J.comap F

The kernel ideal of a functor followed by a quotient functor is the pullback of the quotient ideal.

noncomputable def TauCeti.MorphismIdeal.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ J.comap F) : CategoryTheory.Functor I.Quotient J.Quotient

An additive functor carrying I into J induces a functor from C/I to D/J.

Equations

• I.map J F hF = I.lift (F.comp J.quotientFunctor) ⋯

instance TauCeti.MorphismIdeal.map_additive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ J.comap F) : (I.map J F hF).Additive

The functor induced on ideal quotients is additive.

@[simp]

theorem TauCeti.MorphismIdeal.quotientFunctor_comp_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ J.comap F) : I.quotientFunctor.comp (I.map J F hF) = F.comp J.quotientFunctor

Precomposing the induced functor with the source quotient functor recovers the original functor followed by the target quotient functor.

theorem TauCeti.MorphismIdeal.map_eq_lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ J.comap F) : I.map J F hF = I.lift (F.comp J.quotientFunctor) ⋯

The functor induced on ideal quotients is the lift of the composite with the target quotient functor.

@[simp]

theorem TauCeti.MorphismIdeal.map_obj_quotientFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ J.comap F) (X : C) : (I.map J F hF).obj (I.quotientFunctor.obj X) = J.quotientFunctor.obj (F.obj X)

On objects from the original category, the induced functor applies the original functor and then passes to the target quotient.

@[simp]

theorem TauCeti.MorphismIdeal.map_map_quotientFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ J.comap F) {X Y : C} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp ((I.map J F hF).map (I.quotientFunctor.map f)) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (J.quotientFunctor.map (F.map f))

On morphisms from the original category, the induced functor applies the original functor and then passes to the target quotient.

@[simp]

theorem TauCeti.MorphismIdeal.map_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.map I (CategoryTheory.Functor.id C) ⋯ = CategoryTheory.Functor.id I.Quotient

The identity functor on a category induces the identity functor on every ideal quotient.

theorem TauCeti.MorphismIdeal.map_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] {E : Type u''} [CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Preadditive E] (I : MorphismIdeal C) (J : MorphismIdeal D) (K : MorphismIdeal E) (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.Additive] [G.Additive] (hF : I ≤ J.comap F) (hG : J ≤ K.comap G) : I.map K (F.comp G) ⋯ = (I.map J F hF).comp (J.map K G hG)

Compatible functors induce the composite of their functors on ideal quotients.

Natural transformations between quotient functors

noncomputable def TauCeti.MorphismIdeal.mapNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (hF : I ≤ J.comap F) (hG : I ≤ J.comap G) (α : F ⟶ G) : I.map J F hF ⟶ I.map J G hG

A natural transformation between ideal-preserving functors descends to their induced functors on the quotients.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.MorphismIdeal.mapNatTrans_app_quotientFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (hF : I ≤ J.comap F) (hG : I ≤ J.comap G) (α : F ⟶ G) (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((I.mapNatTrans J hF hG α).app (I.quotientFunctor.obj X)) (CategoryTheory.eqToHom ⋯)) = J.quotientFunctor.map (α.app X)

On objects from the original category, a descended natural transformation is represented by the corresponding component of the original transformation.

@[simp]

theorem TauCeti.MorphismIdeal.mapNatTrans_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ J.comap F) : I.mapNatTrans J hF hF (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id (I.map J F hF)

Descent sends an identity natural transformation to an identity.

@[simp]

theorem TauCeti.MorphismIdeal.comp_mapNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) {F G H : CategoryTheory.Functor C D} [F.Additive] [G.Additive] [H.Additive] (hF : I ≤ J.comap F) (hG : I ≤ J.comap G) (hH : I ≤ J.comap H) (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.CategoryStruct.comp (I.mapNatTrans J hF hG α) (I.mapNatTrans J hG hH β) = I.mapNatTrans J hF hH (CategoryTheory.CategoryStruct.comp α β)

Descent preserves vertical composition of natural transformations.

noncomputable def TauCeti.MorphismIdeal.mapNatIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (hF : I ≤ J.comap F) (hG : I ≤ J.comap G) (α : F ≅ G) : I.map J F hF ≅ I.map J G hG

A natural isomorphism between ideal-preserving functors descends to a natural isomorphism between their induced functors on the quotients.

Equations

• I.mapNatIso J hF hG α = { hom := I.mapNatTrans J hF hG α.hom, inv := I.mapNatTrans J hG hF α.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem TauCeti.MorphismIdeal.mapNatIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (hF : I ≤ J.comap F) (hG : I ≤ J.comap G) (α : F ≅ G) : (I.mapNatIso J hF hG α).hom = I.mapNatTrans J hF hG α.hom

The forward component of a descended natural isomorphism is the descended transformation.

@[simp]

theorem TauCeti.MorphismIdeal.mapNatIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (I : MorphismIdeal C) (J : MorphismIdeal D) {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (hF : I ≤ J.comap F) (hG : I ≤ J.comap G) (α : F ≅ G) : (I.mapNatIso J hF hG α).inv = I.mapNatTrans J hG hF α.inv

The inverse component of a descended natural isomorphism is the descended inverse.