Two-sided ideals of a preadditive category and their quotients

A two-sided ideal I of a preadditive category C assigns to every pair of objects an additive subgroup I(X, Y) of the hom group X ⟶ Y, stable under composition with arbitrary morphisms on either side. Two parallel morphisms are congruent modulo I when their difference lies in I; this is a congruence, and the quotient category C/I has the objects of C and the hom groups (X ⟶ Y) ⧸ I(X, Y).

Such quotients are how stable categories arise: the stable category of a Frobenius exact category is the quotient by the ideal of morphisms factoring through a projective-injective object, and the homotopy category of complexes is the quotient by the ideal of null-homotopic chain maps. This file supplies the generic part of that construction, for an arbitrary ideal:

• the quotient category is preadditive, the quotient functor is additive, full and essentially surjective, and its hom groups are the quotient groups (X ⟶ Y) ⧸ I(X, Y);
• every ideal is the kernel of its quotient functor, and conversely the morphisms an additive functor sends to zero form an ideal;
• an additive functor factors through C/I exactly when it kills I, and the factorization is additive (and linear, when the functor is);
• over an R-linear category every ideal is automatically stable under the scalar action, so the quotient is R-linear with an R-linear quotient functor.

The quotient is Mathlib's CategoryTheory.Quotient by the congruence TauCeti.MorphismIdeal.rel, so its general API — uniqueness of factorizations (CategoryTheory.Quotient.lift_unique'), descent of natural transformations (CategoryTheory.Quotient.natTransLift), and fullness and faithfulness of precomposition with the quotient functor — applies to C/I unchanged.

Main definitions

• TauCeti.MorphismIdeal C: a two-sided ideal of the preadditive category C, ordered by inclusion.
• CategoryTheory.Functor.kerIdeal F: the ideal of morphisms an additive functor F sends to zero.
• TauCeti.MorphismIdeal.rel I: congruence modulo I.
• TauCeti.MorphismIdeal.Quotient I and TauCeti.MorphismIdeal.quotientFunctor I: the quotient category C/I and the quotient functor C ⥤ C/I.
• TauCeti.MorphismIdeal.homAddEquiv I X Y: the identification of the hom group of C/I with the quotient group (X ⟶ Y) ⧸ I(X, Y).
• TauCeti.MorphismIdeal.lift I F hF: the factorization through C/I of a functor killing I.

Main results

• TauCeti.MorphismIdeal.quotientFunctor_map_eq_zero_iff: a morphism becomes zero in C/I exactly when it lies in I, and TauCeti.MorphismIdeal.kerIdeal_quotientFunctor the resulting statement that I is the kernel of its quotient functor.
• TauCeti.MorphismIdeal.exists_quotientFunctor_comp_eq_iff: an additive functor factors through C/I exactly when its kernel contains I.
• TauCeti.MorphismIdeal.smul_mem: an ideal of an R-linear category is stable under scalars.
• TauCeti.MorphismIdeal.isZero_quotientFunctor_obj_iff: an object becomes zero in C/I exactly when its identity belongs to I.
• TauCeti.MorphismIdeal.isIso_quotientFunctor_map_iff: a morphism becomes invertible in C/I exactly when it admits a two-sided inverse modulo I.

References

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

structure TauCeti.MorphismIdeal (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Type (max u v)

A two-sided ideal of a preadditive category C: for every pair of objects an additive subgroup hom X Y of the morphisms X ⟶ Y, such that a composite of morphisms lies in the ideal as soon as one of its two factors does.

• hom (X Y : C) : AddSubgroup (X ⟶ Y)

  The morphisms X ⟶ Y belonging to the ideal, an additive subgroup of the hom group.

• comp_mem_left {X Y Z : C} (f : X ⟶ Y) {g : Y ⟶ Z} : g ∈ self.hom Y Z → CategoryTheory.CategoryStruct.comp f g ∈ self.hom X Z

  Precomposing a member of the ideal with any morphism stays in the ideal.

• comp_mem_right {X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) : f ∈ self.hom X Y → CategoryTheory.CategoryStruct.comp f g ∈ self.hom X Z

  Postcomposing a member of the ideal with any morphism stays in the ideal.

theorem TauCeti.MorphismIdeal.hom_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : Function.Injective hom

theorem TauCeti.MorphismIdeal.ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I J : MorphismIdeal C} (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), f ∈ I.hom X Y ↔ f ∈ J.hom X Y) : I = J

Two ideals with the same members are equal.

theorem TauCeti.MorphismIdeal.ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I J : MorphismIdeal C} : I = J ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), f ∈ I.hom X Y ↔ f ∈ J.hom X Y

@[instance_reducible]

instance TauCeti.MorphismIdeal.instPartialOrder {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] : PartialOrder (MorphismIdeal C)

Ideals are ordered by inclusion.

Equations

• TauCeti.MorphismIdeal.instPartialOrder = PartialOrder.lift TauCeti.MorphismIdeal.hom ⋯

theorem TauCeti.MorphismIdeal.le_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {I J : MorphismIdeal C} : I ≤ J ↔ ∀ ⦃X Y : C⦄, ∀ f ∈ I.hom X Y, f ∈ J.hom X Y

theorem TauCeti.MorphismIdeal.smul_mem {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {R : Type u_1} [Semiring R] [CategoryTheory.Linear R C] (I : MorphismIdeal C) (a : R) {X Y : C} {f : X ⟶ Y} (hf : f ∈ I.hom X Y) : a • f ∈ I.hom X Y

Over an R-linear category an ideal is automatically stable under the scalar action, since a • f = (a • 𝟙 X) ≫ f.

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

The kernel of an additive functor F: the ideal of morphisms that F sends to zero.

Equations

• F.kerIdeal = { hom := fun (x x_1 : C) => F.mapAddHom.ker, comp_mem_left := ⋯, comp_mem_right := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mem_kerIdeal_hom {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.Additive] {X Y : C} {f : X ⟶ Y} : f ∈ F.kerIdeal.hom X Y ↔ F.map f = 0

The congruence modulo an ideal

def TauCeti.MorphismIdeal.rel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : HomRel C

Congruence modulo I: two parallel morphisms are related when their difference lies in I.

Equations

• I.rel f g = (f - g ∈ I.hom X Y)

theorem TauCeti.MorphismIdeal.rel_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {X Y : C} {f g : X ⟶ Y} : I.rel f g ↔ f - g ∈ I.hom X Y

instance TauCeti.MorphismIdeal.instCongruenceRel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : CategoryTheory.Congruence I.rel

theorem TauCeti.MorphismIdeal.rel_add {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {X Y : C} {f₁ f₂ g₁ g₂ : X ⟶ Y} (hf : I.rel f₁ f₂) (hg : I.rel g₁ g₂) : I.rel (f₁ + g₁) (f₂ + g₂)

The quotient category

@[reducible, inline]

abbrev TauCeti.MorphismIdeal.Quotient {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : Type u

The quotient category C/I: the objects of C, with morphisms taken modulo I. It is Mathlib's quotient category by the congruence I.rel, whose API it inherits.

Equations

• I.Quotient = CategoryTheory.Quotient I.rel

@[reducible, inline]

abbrev TauCeti.MorphismIdeal.quotientFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : CategoryTheory.Functor C I.Quotient

The quotient functor C ⥤ C/I. It is full and essentially surjective by CategoryTheory.Quotient.full_functor and CategoryTheory.Quotient.essSurj_functor.

Equations

• I.quotientFunctor = CategoryTheory.Quotient.functor I.rel

@[instance_reducible]

noncomputable instance TauCeti.MorphismIdeal.instPreadditiveQuotient {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : CategoryTheory.Preadditive I.Quotient

Equations

• I.instPreadditiveQuotient = CategoryTheory.Quotient.preadditive I.rel ⋯

instance TauCeti.MorphismIdeal.instAdditiveQuotientQuotientFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.quotientFunctor.Additive

theorem TauCeti.MorphismIdeal.quotientFunctor_map_eq_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {X Y : C} {f g : X ⟶ Y} : I.quotientFunctor.map f = I.quotientFunctor.map g ↔ f - g ∈ I.hom X Y

@[simp]

theorem TauCeti.MorphismIdeal.quotientFunctor_map_eq_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {X Y : C} {f : X ⟶ Y} : I.quotientFunctor.map f = 0 ↔ f ∈ I.hom X Y

A morphism becomes zero in the quotient category exactly when it lies in the ideal.

@[simp]

theorem TauCeti.MorphismIdeal.isZero_quotientFunctor_obj_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) (X : C) : CategoryTheory.Limits.IsZero (I.quotientFunctor.obj X) ↔ CategoryTheory.CategoryStruct.id X ∈ I.hom X X

An object becomes zero in the quotient exactly when its identity belongs to the ideal.

theorem TauCeti.MorphismIdeal.isIso_quotientFunctor_map_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {X Y : C} (f : X ⟶ Y) : CategoryTheory.IsIso (I.quotientFunctor.map f) ↔ ∃ (g : Y ⟶ X), CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.id X ∈ I.hom X X ∧ CategoryTheory.CategoryStruct.comp g f - CategoryTheory.CategoryStruct.id Y ∈ I.hom Y Y

A morphism is invertible in the quotient exactly when it has a two-sided inverse modulo the ideal. The lift of the inverse need not be invertible in the original category.

@[simp]

theorem TauCeti.MorphismIdeal.kerIdeal_quotientFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) : I.quotientFunctor.kerIdeal = I

Every ideal is the kernel of its quotient functor.

noncomputable def TauCeti.MorphismIdeal.homAddEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) (X Y : C) : (X ⟶ Y) ⧸ I.hom X Y ≃+ (I.quotientFunctor.obj X ⟶ I.quotientFunctor.obj Y)

The hom group of the quotient category between the images of X and Y is the quotient group (X ⟶ Y) ⧸ I(X, Y).

Equations

• I.homAddEquiv X Y = QuotientAddGroup.liftEquiv (I.hom X Y) ⋯ ⋯

@[simp]

theorem TauCeti.MorphismIdeal.homAddEquiv_mk {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {X Y : C} (f : X ⟶ Y) : (I.homAddEquiv X Y) ↑f = I.quotientFunctor.map f

The universal property

theorem CategoryTheory.Functor.rel_kerIdeal_iff {C : Type u} [Category.{v, u} C] [Preadditive C] {D : Type u'} [Category.{v', u'} D] [Preadditive D] (F : Functor C D) [F.Additive] {X Y : C} {f g : X ⟶ Y} : F.kerIdeal.rel f g ↔ F.homRel f g

Congruence modulo the kernel of F is Mathlib's relation F.homRel of having the same image under F.

theorem TauCeti.MorphismIdeal.map_eq_of_rel {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ F.kerIdeal) {X Y : C} {f g : X ⟶ Y} (h : I.rel f g) : F.map f = F.map g

A functor killing I sends morphisms congruent modulo I to the same morphism.

@[reducible, inline]

abbrev TauCeti.MorphismIdeal.lift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ F.kerIdeal) : CategoryTheory.Functor I.Quotient D

The factorization through the quotient category of an additive functor killing I. It restricts to F along the quotient functor by CategoryTheory.Quotient.lift_spec, and is the unique such functor by CategoryTheory.Quotient.lift_unique.

Equations

• I.lift F hF = CategoryTheory.Quotient.lift I.rel F ⋯

instance TauCeti.MorphismIdeal.instAdditiveQuotientLift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] (hF : I ≤ F.kerIdeal) : (I.lift F hF).Additive

theorem TauCeti.MorphismIdeal.exists_quotientFunctor_comp_eq_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive] : (∃ (G : CategoryTheory.Functor I.Quotient D), I.quotientFunctor.comp G = F) ↔ I ≤ F.kerIdeal

An additive functor factors through the quotient category exactly when it kills the ideal.

Linear quotients

theorem TauCeti.MorphismIdeal.rel_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) (R : Type u_1) [Semiring R] [CategoryTheory.Linear R C] (a : R) {X Y : C} {f g : X ⟶ Y} (h : I.rel f g) : I.rel (a • f) (a • g)

@[instance_reducible]

noncomputable instance TauCeti.MorphismIdeal.instLinearQuotient {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) (R : Type u_1) [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Linear R I.Quotient

Over an R-linear category, the quotient by any ideal is R-linear.

Equations

• I.instLinearQuotient R = CategoryTheory.Quotient.linear R I.rel ⋯

instance TauCeti.MorphismIdeal.instLinearQuotientQuotientFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) (R : Type u_1) [Semiring R] [CategoryTheory.Linear R C] : CategoryTheory.Functor.Linear R I.quotientFunctor

instance TauCeti.MorphismIdeal.instLinearQuotientLift {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (I : MorphismIdeal C) (R : Type u_1) [Semiring R] [CategoryTheory.Linear R C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear R D] {F : CategoryTheory.Functor C D} [F.Additive] [CategoryTheory.Functor.Linear R F] (hF : I ≤ F.kerIdeal) : CategoryTheory.Functor.Linear R (I.lift F hF)

The factorization of an R-linear functor through the quotient category is R-linear.