The ideal of morphisms factoring through a class of objects

Given an object property P in a preadditive category, this file constructs the two-sided morphism ideal generated by the maps that factor through a P-object. Taking the additive closure is essential in an arbitrary preadditive category: a sum of two factorizations need not itself have a single intermediate object.

When the category has binary biproducts and P is nonempty and closed under binary products, every member of the generated ideal does factor through one P-object. The sum of factorizations through Q₁ and Q₂ factors through Q₁ ⊞ Q₂; the zero and negation cases use zero morphisms and negating one factor. In particular, this applies when P contains a zero object and is closed under finite biproducts, as for the projective-injective objects used in stable categories.

The factorization predicate itself, together with its closure properties, is in TauCeti.CategoryTheory.ObjectProperty.FactorsThrough; only the generated ideal needs the preadditive morphism-ideal API. Everything here lives in Mathlib's root CategoryTheory.ObjectProperty namespace, so that P.factorIdeal elaborates as dot notation on an object property; a copy of that namespace nested in TauCeti would break it.

Main definitions

• CategoryTheory.ObjectProperty.factorIdeal P: the two-sided ideal additively generated by the maps factoring through an object satisfying P.

Main results

• CategoryTheory.ObjectProperty.factorIdeal_le_iff: the universal property of the generated ideal.
• CategoryTheory.ObjectProperty.mem_factorIdeal_iff: under the stated closure hypotheses, membership in the generated ideal is equivalent to a single factorization through a P-object.

References

• M. Auslander, I. Reiten, S. Smalø, Representation Theory of Artin Algebras, Cambridge Studies in Advanced Mathematics 36, 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), Chapter I, Section 2.

def CategoryTheory.ObjectProperty.factorIdeal {C : Type u} [Category.{v, u} C] [Preadditive C] (P : ObjectProperty C) : TauCeti.MorphismIdeal C

The two-sided morphism ideal additively generated by maps factoring through objects satisfying P.

Equations

• P.factorIdeal = { hom := fun (X Y : C) => AddSubgroup.closure {f : X ⟶ Y | P.FactorsThrough f}, comp_mem_left := ⋯, comp_mem_right := ⋯ }

theorem CategoryTheory.ObjectProperty.mem_factorIdeal_of_factorsThrough {C : Type u} [Category.{v, u} C] [Preadditive C] {P : ObjectProperty C} {X Y : C} {f : X ⟶ Y} (hf : P.FactorsThrough f) : f ∈ P.factorIdeal.hom X Y

A map factoring through a P-object belongs to the ideal generated by such maps.

theorem CategoryTheory.ObjectProperty.comp_mem_factorIdeal {C : Type u} [Category.{v, u} C] [Preadditive C] {P : ObjectProperty C} {X Y Z : C} (hZ : P Z) (i : X ⟶ Z) (p : Z ⟶ Y) : CategoryStruct.comp i p ∈ P.factorIdeal.hom X Y

A composite through a P-object belongs to factorIdeal P.

@[simp]

theorem CategoryTheory.ObjectProperty.factorIdeal_le_iff {C : Type u} [Category.{v, u} C] [Preadditive C] {P : ObjectProperty C} {I : TauCeti.MorphismIdeal C} : P.factorIdeal ≤ I ↔ ∀ {X Y Z : C}, P Z → ∀ (i : X ⟶ Z) (p : Z ⟶ Y), CategoryStruct.comp i p ∈ I.hom X Y

The universal property of factorIdeal P: it is the least morphism ideal containing all composites through P-objects.

theorem CategoryTheory.ObjectProperty.factorIdeal_mono {C : Type u} [Category.{v, u} C] [Preadditive C] {P Q : ObjectProperty C} (hPQ : P ≤ Q) : P.factorIdeal ≤ Q.factorIdeal

The ideal generated by factorizations is monotone in the class of allowed intermediate objects.

theorem CategoryTheory.ObjectProperty.factorsThrough_of_mem_factorIdeal {C : Type u} [Category.{v, u} C] [Preadditive C] {P : ObjectProperty C} {X Y : C} {f : X ⟶ Y} [Limits.HasBinaryBiproducts C] [P.Nonempty] [P.IsClosedUnderBinaryProducts] (hf : f ∈ P.factorIdeal.hom X Y) : P.FactorsThrough f

If P is nonempty and closed under binary products, every member of factorIdeal P is a single morphism factoring through a P-object.

@[simp]

theorem CategoryTheory.ObjectProperty.mem_factorIdeal_iff {C : Type u} [Category.{v, u} C] [Preadditive C] {P : ObjectProperty C} {X Y : C} {f : X ⟶ Y} [Limits.HasBinaryBiproducts C] [P.Nonempty] [P.IsClosedUnderBinaryProducts] : f ∈ P.factorIdeal.hom X Y ↔ P.FactorsThrough f

Under the standard closure hypotheses on P, the additive closure in the definition of factorIdeal P introduces no new kind of morphism: every member has one P-factorization.