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)
:
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
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)
:
f.Factors h ↔ g.Factors 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 : 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
def
CategoryTheory.Subobject.Factors
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
{Y : C}
(P : CategoryTheory.Subobject Y)
(f : X ⟶ Y)
:
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
@[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.mk f).Factors g ↔ (CategoryTheory.MonoOver.mk' f).Factors 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.mk f).Factors 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)
:
P.Factors f ↔ (CategoryTheory.Subobject.representative.obj P).Factors f
theorem
CategoryTheory.Subobject.factors_self
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(P : CategoryTheory.Subobject X)
:
P.Factors P.arrow
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.obj P)
:
P.Factors (CategoryTheory.CategoryStruct.comp f P.arrow)
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 : P.Factors g)
:
P.Factors (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}
:
P.Factors 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)
:
P.Factors f → Q.Factors 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 : P.Factors f)
:
X ⟶ CategoryTheory.Subobject.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
@[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 : P.Factors f)
:
CategoryTheory.CategoryStruct.comp (P.factorThru f h) P.arrow = 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 : P.Factors f)
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (P.factorThru f h✝) (CategoryTheory.CategoryStruct.comp P.arrow h) = CategoryTheory.CategoryStruct.comp f h
@[simp]
theorem
CategoryTheory.Subobject.factorThru_self
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X : C}
(P : CategoryTheory.Subobject X)
(h : P.Factors P.arrow)
:
P.factorThru P.arrow h = CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.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.mk f).factorThru 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.obj P)
(h : P.Factors (CategoryTheory.CategoryStruct.comp f P.arrow))
:
P.factorThru (CategoryTheory.CategoryStruct.comp f P.arrow) 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 : P.Factors f}
:
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 : P.Factors g)
:
CategoryTheory.CategoryStruct.comp f (P.factorThru g h) = P.factorThru (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 : P.Factors 0)
:
P.factorThru 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 : P.Factors f)
:
Q.factorThru f ⋯ = CategoryTheory.CategoryStruct.comp (P.factorThru f w) (P.ofLE 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 : P.Factors f)
(wg : P.Factors g)
:
P.Factors (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 : P.Factors (f + g))
(wf : P.Factors f)
(wg : P.Factors g)
:
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 : P.Factors (f + g))
(wg : P.Factors g)
:
P.Factors 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 : P.Factors (f + g))
(wg : P.Factors g)
:
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 : P.Factors (f + g))
(wf : P.Factors f)
:
P.Factors 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 : P.Factors (f + g))
(wf : P.Factors f)
: