Equivalences of quotients by morphism ideals

Let F : C ⥤ D be an additive functor carrying a morphism ideal I of C into a morphism ideal J of D, so that F induces I.map J F hF : C/I ⥤ D/J. This file records how the properties of F pass to the induced functor:

• the induced functor is faithful exactly when I contains every morphism that F sends into J, that is when J.comap F ≤ I; no faithfulness of F itself is needed;
• it is full when F ⋙ J.quotientFunctor is full, and essentially surjective when this composite is; in particular, these properties descend from F itself;
• a full, essentially surjective F ⋙ J.quotientFunctor with J.comap F ≤ I induces an equivalence of quotients, without requiring F to be faithful;
• consequently an equivalence e : C ≌ D with I = J.comap e.functor induces an equivalence C/I ≌ D/J, whose inverse is the functor induced by e.inverse.

Pulling back along an equivalence is inverse to pulling back along its inverse, so the hypothesis I = J.comap e.functor says precisely that e carries I onto J.

This is the mechanism by which an equivalence of additive categories matching two ideals, such as an exact equivalence matching projective-injective objects, identifies the corresponding quotient categories.

Main definitions

• TauCeti.MorphismIdeal.mapEquivalence: the equivalence C/I ≌ D/J induced by an equivalence C ≌ D carrying I onto J.

Main results

• TauCeti.MorphismIdeal.faithful_lift_iff, full_lift, essSurj_lift, and isEquivalence_lift: faithfulness, fullness, essential surjectivity, and equivalence for a functor lifted through the quotient by an ideal in its kernel.
• TauCeti.MorphismIdeal.map_map_quotientFunctor_map_eq_iff: two morphisms become equal under the induced functor exactly when F sends their difference into J.
• TauCeti.MorphismIdeal.faithful_map_iff: the induced functor is faithful if and only if J.comap F ≤ I.
• TauCeti.MorphismIdeal.full_map and TauCeti.MorphismIdeal.essSurj_map: fullness and essential surjectivity descend from the composite with the target quotient functor.
• TauCeti.MorphismIdeal.isEquivalence_map: a full, essentially surjective composite with the target quotient functor induces an equivalence when J.comap F ≤ I.
• TauCeti.MorphismIdeal.comap_inverse_comap_functor and TauCeti.MorphismIdeal.comap_functor_comap_inverse: pullback along an equivalence and along its inverse are mutually inverse.

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.

Properties of induced functors

theorem TauCeti.MorphismIdeal.faithful_lift_iff {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) (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ F.kerIdeal) : (I.lift F hF).Faithful ↔ F.kerIdeal ≤ I

A functor lifted from a quotient is faithful exactly when its kernel is the quotient ideal.

instance TauCeti.MorphismIdeal.full_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) (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ F.kerIdeal) [F.Full] : (I.lift F hF).Full

The lift of a full functor is full.

instance TauCeti.MorphismIdeal.essSurj_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) (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ F.kerIdeal) [F.EssSurj] : (I.lift F hF).EssSurj

The lift of an essentially surjective functor is essentially surjective.

theorem TauCeti.MorphismIdeal.isEquivalence_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) (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ F.kerIdeal) [F.Full] [F.EssSurj] (h : F.kerIdeal ≤ I) : (I.lift F hF).IsEquivalence

A full, essentially surjective functor induces an equivalence after quotienting by its kernel ideal.

theorem TauCeti.MorphismIdeal.map_map_quotientFunctor_map_eq_iff {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 g : X ⟶ Y) : (I.map J F hF).map (I.quotientFunctor.map f) = (I.map J F hF).map (I.quotientFunctor.map g) ↔ f - g ∈ (J.comap F).hom X Y

Two morphisms of C have the same image under the quotient functor followed by the induced functor exactly when F sends their difference into J.

theorem TauCeti.MorphismIdeal.faithful_map_iff {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).Faithful ↔ J.comap F ≤ I

The functor induced on quotients is faithful exactly when every morphism that F sends into J already lies in I.

instance TauCeti.MorphismIdeal.full_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) [(F.comp J.quotientFunctor).Full] : (I.map J F hF).Full

The induced functor on quotients is full when the composite with the target quotient functor is full. In particular, this holds when F is full.

instance TauCeti.MorphismIdeal.essSurj_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) [(F.comp J.quotientFunctor).EssSurj] : (I.map J F hF).EssSurj

The induced functor on quotients is essentially surjective when the composite with the target quotient functor is essentially surjective. In particular, this holds when F is essentially surjective.

theorem TauCeti.MorphismIdeal.isEquivalence_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) [(F.comp J.quotientFunctor).Full] [(F.comp J.quotientFunctor).EssSurj] (h : J.comap F ≤ I) : (I.map J F hF).IsEquivalence

If the composite with the target quotient functor is full and essentially surjective, and J.comap F ≤ I, then F induces an equivalence of quotients.

Ideals along an equivalence

@[simp]

theorem TauCeti.MorphismIdeal.comap_inverse_comap_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (e : C ≌ D) [e.functor.Additive] (J : MorphismIdeal D) : (J.comap e.functor).comap e.inverse = J

Pulling an ideal back along an equivalence and then along its inverse recovers the ideal.

@[simp]

theorem TauCeti.MorphismIdeal.comap_functor_comap_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (e : C ≌ D) [e.functor.Additive] (I : MorphismIdeal C) : (I.comap e.inverse).comap e.functor = I

Pulling an ideal back along the inverse of an equivalence and then along the equivalence recovers the ideal.

theorem TauCeti.MorphismIdeal.le_comap_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (e : C ≌ D) [e.functor.Additive] (I : MorphismIdeal C) (J : MorphismIdeal D) (h : I = J.comap e.functor) : J ≤ I.comap e.inverse

If e carries I onto J, then its inverse carries J into I.

noncomputable def TauCeti.MorphismIdeal.mapEquivalence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (e : C ≌ D) [e.functor.Additive] (I : MorphismIdeal C) (J : MorphismIdeal D) (h : I = J.comap e.functor) : I.Quotient ≌ J.Quotient

An equivalence e : C ≌ D carrying the ideal I onto the ideal J induces an equivalence of the quotient categories C/I ≌ D/J. Its functor and inverse are the functors induced by e.functor and e.inverse.

Equations

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

@[simp]

theorem TauCeti.MorphismIdeal.mapEquivalence_functor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (e : C ≌ D) [e.functor.Additive] (I : MorphismIdeal C) (J : MorphismIdeal D) (h : I = J.comap e.functor) : (mapEquivalence e I J h).functor = I.map J e.functor ⋯

The functor of the induced equivalence is the functor induced by e.functor.

instance TauCeti.MorphismIdeal.mapEquivalence_functor_additive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (e : C ≌ D) [e.functor.Additive] (I : MorphismIdeal C) (J : MorphismIdeal D) (h : I = J.comap e.functor) : (mapEquivalence e I J h).functor.Additive

The functor of the induced equivalence is additive.

@[simp]

theorem TauCeti.MorphismIdeal.mapEquivalence_inverse {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (e : C ≌ D) [e.functor.Additive] (I : MorphismIdeal C) (J : MorphismIdeal D) (h : I = J.comap e.functor) : (mapEquivalence e I J h).inverse = J.map I e.inverse ⋯

The inverse of the induced equivalence is the functor induced by e.inverse.