Theorems · Definition · category theory

CategoryTheory.Subobject.Factors

{C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → CategoryTheory.Subobject Y → (X ⟶ Y) → Prop

When f : X ⟶ Y and P : Subobject Y, P.Factors f expresses that there exists a factorisation of f through P. Given h : P.Factors f, you can recover the morphism as P.factorThru f h.

Defined in

Mathlib.CategoryTheory.Subobject.FactorThru

Cited by

56 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category