Morphisms factoring through a class of objects

Given an object property P in a category, this file defines P.FactorsThrough f: the morphism f admits a CategoryTheory.Factorisation whose midpoint satisfies P. It records the closure properties of this predicate — enlarging P, composing on either side, and, in a preadditive category, negating a factorization and adding two of them when P is closed under binary products, the sum then factoring through the biproduct of the two intermediate objects.

Everything here lives in Mathlib's root CategoryTheory.ObjectProperty namespace, so that P.FactorsThrough f elaborates as dot notation on an object property; a copy of that namespace nested in TauCeti would break it.

Main definitions

• CategoryTheory.ObjectProperty.FactorsThrough P f: the morphism f factors through an object satisfying P.

Main results

• CategoryTheory.ObjectProperty.factorsThrough_iff: the characterization of the predicate by an explicit intermediate object and two factors.
• CategoryTheory.ObjectProperty.factorsThrough_id_iff: when P is stable under retracts, an identity factors through a P-object exactly when its source satisfies P.
• CategoryTheory.ObjectProperty.FactorsThrough.add: over a preadditive category with binary biproducts, a sum of factorizations through a product-closed P again factors through a single 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.

def CategoryTheory.ObjectProperty.FactorsThrough {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X Y : C} (f : X ⟶ Y) : Prop

A morphism factors through an object satisfying P if it has a factorisation whose midpoint satisfies P.

Equations

• P.FactorsThrough f = ∃ (d : CategoryTheory.Factorisation f), P d.mid

@[simp]

theorem CategoryTheory.ObjectProperty.factorsThrough_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X Y : C} (f : X ⟶ Y) : P.FactorsThrough f ↔ ∃ (Q : C), P Q ∧ ∃ (i : X ⟶ Q) (p : Q ⟶ Y), f = CategoryStruct.comp i p

A morphism factors through a P-object if and only if it is a composite whose intermediate object satisfies P. This unfolds FactorsThrough into an explicit intermediate object and two factors.

theorem CategoryTheory.ObjectProperty.factorsThrough_comp {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) {X Q Y : C} (hQ : P Q) (i : X ⟶ Q) (p : Q ⟶ Y) : P.FactorsThrough (CategoryStruct.comp i p)

A composite through a P-object factors through a P-object.

@[simp]

theorem CategoryTheory.ObjectProperty.factorsThrough_id_iff {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.IsStableUnderRetracts] (X : C) : P.FactorsThrough (CategoryStruct.id X) ↔ P X

If P is stable under retracts, the identity of X factors through a P-object exactly when X itself satisfies P.

theorem CategoryTheory.ObjectProperty.FactorsThrough.mono {C : Type u} [Category.{v, u} C] {P Q : ObjectProperty C} {X Y : C} {f : X ⟶ Y} (hf : P.FactorsThrough f) (hPQ : P ≤ Q) : Q.FactorsThrough f

Enlarging the class of intermediate objects preserves factorization.

theorem CategoryTheory.ObjectProperty.FactorsThrough.comp_left {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {W X Y : C} {f : X ⟶ Y} (hf : P.FactorsThrough f) (g : W ⟶ X) : P.FactorsThrough (CategoryStruct.comp g f)

Precomposing preserves factorization through a P-object.

theorem CategoryTheory.ObjectProperty.FactorsThrough.comp_right {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {X Y Z : C} {f : X ⟶ Y} (hf : P.FactorsThrough f) (g : Y ⟶ Z) : P.FactorsThrough (CategoryStruct.comp f g)

Postcomposing preserves factorization through a P-object.

theorem CategoryTheory.ObjectProperty.FactorsThrough.zero {C : Type u} [Category.{v, u} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) [P.Nonempty] (X Y : C) : P.FactorsThrough 0

The zero morphism factors through a P-object when P is nonempty.

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

Negating a morphism preserves factorization through a P-object.

theorem CategoryTheory.ObjectProperty.FactorsThrough.add {C : Type u} [Category.{v, u} C] [Preadditive C] {P : ObjectProperty C} {X Y : C} [Limits.HasBinaryBiproducts C] [P.IsClosedUnderBinaryProducts] {f g : X ⟶ Y} (hf : P.FactorsThrough f) (hg : P.FactorsThrough g) : P.FactorsThrough (f + g)

With binary biproducts, the sum of two factorizations through P factors through the biproduct of their intermediate objects.