Factoring through subobjects

The predicate h : P.Factors f, for P : Subobject Y and f : X ⟶ Y asserts the existence of some P.factorThru f : X ⟶ (P : C) making the obvious diagram commute.

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

When f : X ⟶ Y and P : MonoOver 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.

Equations

• CategoryTheory.MonoOver.Factors P f = ∃ (g : X ⟶ P.obj.left), CategoryTheory.CategoryStruct.comp g (CategoryTheory.MonoOver.arrow P) = f

theorem CategoryTheory.MonoOver.factors_congr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {f : CategoryTheory.MonoOver X} {g : CategoryTheory.MonoOver X} {Y : C} (h : Y ⟶ X) (e : f ≅ g) : CategoryTheory.MonoOver.Factors f h ↔ CategoryTheory.MonoOver.Factors g h

def CategoryTheory.MonoOver.factorThru {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (P : CategoryTheory.MonoOver Y) (f : X ⟶ Y) (h : CategoryTheory.MonoOver.Factors P f) : X ⟶ P.obj.left

P.factorThru f h provides a factorisation of f : X ⟶ Y through some P : MonoOver Y, given the evidence h : P.Factors f that such a factorisation exists.

Equations

• CategoryTheory.MonoOver.factorThru P f h = Classical.choose h

def CategoryTheory.Subobject.Factors {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (P : CategoryTheory.Subobject Y) (f : 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.

Equations

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

@[simp]

theorem CategoryTheory.Subobject.mk_factors_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : Y ⟶ X) [CategoryTheory.Mono f] (g : Z ⟶ X) : CategoryTheory.Subobject.Factors (CategoryTheory.Subobject.mk f) g ↔ CategoryTheory.MonoOver.Factors (CategoryTheory.MonoOver.mk' f) g

theorem CategoryTheory.Subobject.mk_factors_self {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Subobject.Factors (CategoryTheory.Subobject.mk f) f

theorem CategoryTheory.Subobject.factors_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (P : CategoryTheory.Subobject Y) (f : X ⟶ Y) : CategoryTheory.Subobject.Factors P f ↔ CategoryTheory.MonoOver.Factors (CategoryTheory.Subobject.representative.toPrefunctor.obj P) f

theorem CategoryTheory.Subobject.factors_self {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Subobject X) : CategoryTheory.Subobject.Factors P (CategoryTheory.Subobject.arrow P)

theorem CategoryTheory.Subobject.factors_comp_arrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {P : CategoryTheory.Subobject Y} (f : X ⟶ CategoryTheory.Subobject.underlying.toPrefunctor.obj P) : CategoryTheory.Subobject.Factors P (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Subobject.arrow P))

theorem CategoryTheory.Subobject.factors_of_factors_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {P : CategoryTheory.Subobject Z} (f : X ⟶ Y) {g : Y ⟶ Z} (h : CategoryTheory.Subobject.Factors P g) : CategoryTheory.Subobject.Factors P (CategoryTheory.CategoryStruct.comp f g)

theorem CategoryTheory.Subobject.factors_zero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} {P : CategoryTheory.Subobject Y} : CategoryTheory.Subobject.Factors P 0

theorem CategoryTheory.Subobject.factors_of_le {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} {Z : C} {P : CategoryTheory.Subobject Y} {Q : CategoryTheory.Subobject Y} (f : Z ⟶ Y) (h : P ≤ Q) : CategoryTheory.Subobject.Factors P f → CategoryTheory.Subobject.Factors Q f

def CategoryTheory.Subobject.factorThru {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (P : CategoryTheory.Subobject Y) (f : X ⟶ Y) (h : CategoryTheory.Subobject.Factors P f) : X ⟶ CategoryTheory.Subobject.underlying.toPrefunctor.obj P

P.factorThru f h provides a factorisation of f : X ⟶ Y through some P : Subobject Y, given the evidence h : P.Factors f that such a factorisation exists.

Equations

• CategoryTheory.Subobject.factorThru P f h = Classical.choose (_ : CategoryTheory.MonoOver.Factors (CategoryTheory.Subobject.representative.toPrefunctor.obj P) f)

@[simp]

theorem CategoryTheory.Subobject.factorThru_arrow_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (P : CategoryTheory.Subobject Y) (f : X ⟶ Y) (h : CategoryTheory.Subobject.Factors P f) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.factorThru P f h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.arrow P) h) = CategoryTheory.CategoryStruct.comp f h

@[simp]

theorem CategoryTheory.Subobject.factorThru_arrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (P : CategoryTheory.Subobject Y) (f : X ⟶ Y) (h : CategoryTheory.Subobject.Factors P f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.factorThru P f h) (CategoryTheory.Subobject.arrow P) = f

@[simp]

theorem CategoryTheory.Subobject.factorThru_self {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Subobject X) (h : CategoryTheory.Subobject.Factors P (CategoryTheory.Subobject.arrow P)) : CategoryTheory.Subobject.factorThru P (CategoryTheory.Subobject.arrow P) h = CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.toPrefunctor.obj P)

@[simp]

theorem CategoryTheory.Subobject.factorThru_mk_self {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Subobject.factorThru (CategoryTheory.Subobject.mk f) f (_ : CategoryTheory.Subobject.Factors (CategoryTheory.Subobject.mk f) f) = (CategoryTheory.Subobject.underlyingIso f).inv

@[simp]

theorem CategoryTheory.Subobject.factorThru_comp_arrow {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {P : CategoryTheory.Subobject Y} (f : X ⟶ CategoryTheory.Subobject.underlying.toPrefunctor.obj P) (h : CategoryTheory.Subobject.Factors P (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Subobject.arrow P))) : CategoryTheory.Subobject.factorThru P (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Subobject.arrow P)) h = f

@[simp]

theorem CategoryTheory.Subobject.factorThru_eq_zero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} {P : CategoryTheory.Subobject Y} {f : X ⟶ Y} {h : CategoryTheory.Subobject.Factors P f} : CategoryTheory.Subobject.factorThru P f h = 0 ↔ f = 0

theorem CategoryTheory.Subobject.factorThru_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {P : CategoryTheory.Subobject Z} (f : X ⟶ Y) (g : Y ⟶ Z) (h : CategoryTheory.Subobject.Factors P g) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Subobject.factorThru P g h) = CategoryTheory.Subobject.factorThru P (CategoryTheory.CategoryStruct.comp f g) (_ : CategoryTheory.Subobject.Factors P (CategoryTheory.CategoryStruct.comp f g))

@[simp]

theorem CategoryTheory.Subobject.factorThru_zero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C} {Y : C} {P : CategoryTheory.Subobject Y} (h : CategoryTheory.Subobject.Factors P 0) : CategoryTheory.Subobject.factorThru P 0 h = 0

theorem CategoryTheory.Subobject.factorThru_ofLE {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Y : C} {Z : C} {P : CategoryTheory.Subobject Y} {Q : CategoryTheory.Subobject Y} {f : Z ⟶ Y} (h : P ≤ Q) (w : CategoryTheory.Subobject.Factors P f) : CategoryTheory.Subobject.factorThru Q f (_ : CategoryTheory.Subobject.Factors Q f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.factorThru P f w) (CategoryTheory.Subobject.ofLE P Q h)

theorem CategoryTheory.Subobject.factors_add {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} {P : CategoryTheory.Subobject Y} (f : X ⟶ Y) (g : X ⟶ Y) (wf : CategoryTheory.Subobject.Factors P f) (wg : CategoryTheory.Subobject.Factors P g) : CategoryTheory.Subobject.Factors P (f + g)

theorem CategoryTheory.Subobject.factorThru_add {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} {P : CategoryTheory.Subobject Y} (f : X ⟶ Y) (g : X ⟶ Y) (w : CategoryTheory.Subobject.Factors P (f + g)) (wf : CategoryTheory.Subobject.Factors P f) (wg : CategoryTheory.Subobject.Factors P g) : CategoryTheory.Subobject.factorThru P (f + g) w = CategoryTheory.Subobject.factorThru P f wf + CategoryTheory.Subobject.factorThru P g wg

theorem CategoryTheory.Subobject.factors_left_of_factors_add {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} {P : CategoryTheory.Subobject Y} (f : X ⟶ Y) (g : X ⟶ Y) (w : CategoryTheory.Subobject.Factors P (f + g)) (wg : CategoryTheory.Subobject.Factors P g) : CategoryTheory.Subobject.Factors P f

@[simp]

theorem CategoryTheory.Subobject.factorThru_add_sub_factorThru_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} {P : CategoryTheory.Subobject Y} (f : X ⟶ Y) (g : X ⟶ Y) (w : CategoryTheory.Subobject.Factors P (f + g)) (wg : CategoryTheory.Subobject.Factors P g) : CategoryTheory.Subobject.factorThru P (f + g) w - CategoryTheory.Subobject.factorThru P g wg = CategoryTheory.Subobject.factorThru P f (_ : CategoryTheory.Subobject.Factors P f)

theorem CategoryTheory.Subobject.factors_right_of_factors_add {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} {P : CategoryTheory.Subobject Y} (f : X ⟶ Y) (g : X ⟶ Y) (w : CategoryTheory.Subobject.Factors P (f + g)) (wf : CategoryTheory.Subobject.Factors P f) : CategoryTheory.Subobject.Factors P g

@[simp]

theorem CategoryTheory.Subobject.factorThru_add_sub_factorThru_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {X : C} {Y : C} {P : CategoryTheory.Subobject Y} (f : X ⟶ Y) (g : X ⟶ Y) (w : CategoryTheory.Subobject.Factors P (f + g)) (wf : CategoryTheory.Subobject.Factors P f) : CategoryTheory.Subobject.factorThru P (f + g) w - CategoryTheory.Subobject.factorThru P f wf = CategoryTheory.Subobject.factorThru P g (_ : CategoryTheory.Subobject.Factors P g)