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.

source

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

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

Instances For

source

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

f.Factors h ↔ g.Factors h

source

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

P.factorThru f h = Classical.choose h

Instances For

source

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

P.Factors f = Quotient.liftOn' P (fun (P : CategoryTheory.MonoOver Y) => P.Factors f) ⋯

Instances For

source

@[simp]

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

(mk f).Factors g ↔ (MonoOver.mk' f).Factors g

source

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

(mk f).Factors f

source

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

P.Factors f ↔ (representative.obj P).Factors f

source

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

P.Factors P.arrow

source

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

P.Factors (CategoryStruct.comp f P.arrow)

source

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

P.Factors (CategoryStruct.comp f g)

source

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

P.Factors 0

source

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

P.Factors f → Q.Factors f

source

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

X ⟶ underlying.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

P.factorThru f h = Classical.choose ⋯

Instances For

source

@[simp]

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

CategoryStruct.comp (P.factorThru f h) P.arrow = f

source

@[simp]

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

CategoryStruct.comp (P.factorThru f h) (CategoryStruct.comp P.arrow h✝) = CategoryStruct.comp f h✝

source

@[simp]

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

P.factorThru P.arrow h = CategoryStruct.id (underlying.obj P)

source

@[simp]

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

(mk f).factorThru f ⋯ = (underlyingIso f).inv

source

@[simp]

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

P.factorThru (CategoryStruct.comp f P.arrow) h = f

source

@[simp]

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

P.factorThru f h = 0 ↔ f = 0

source

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

CategoryStruct.comp f (P.factorThru g h) = P.factorThru (CategoryStruct.comp f g) ⋯

source

@[simp]

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

P.factorThru 0 h = 0

source

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

Q.factorThru f ⋯ = CategoryStruct.comp (P.factorThru f w) (P.ofLE Q h)

source

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

P.Factors (f + g)

source

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

P.factorThru (f + g) w = P.factorThru f wf + P.factorThru g wg

source

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

P.Factors f

source

@[simp]

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

P.factorThru (f + g) w - P.factorThru g wg = P.factorThru f ⋯

source

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

P.Factors g

source

@[simp]

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

P.factorThru (f + g) w - P.factorThru f wf = P.factorThru g ⋯

Documentation

Mathlib.CategoryTheory.Subobject.FactorThru

Factoring through subobjects #