Factoring through subobjects #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The predicate h : P.factors f, for P : subobject Y and f : X ⟶ Y
asserts the existence of some P.factor_thru f : X ⟶ (P : C) making the obvious diagram commute.
def
category_theory.mono_over.factors
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(P : category_theory.mono_over Y)
(f : X ⟶ Y) :
Prop
When f : X ⟶ Y and P : mono_over 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.factor_thru f h.
theorem
category_theory.mono_over.factors_congr
{C : Type u₁}
[category_theory.category C]
{X : C}
{f g : category_theory.mono_over X}
{Y : C}
(h : Y ⟶ X)
(e : f ≅ g) :
noncomputable
def
category_theory.mono_over.factor_thru
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(P : category_theory.mono_over Y)
(f : X ⟶ Y)
(h : P.factors f) :
P.factor_thru f h provides a factorisation of f : X ⟶ Y through some P : mono_over Y,
given the evidence h : P.factors f that such a factorisation exists.
Equations
- P.factor_thru f h = classical.some h
def
category_theory.subobject.factors
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(P : category_theory.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.factor_thru f h.
Equations
- P.factors f = quotient.lift_on' P (λ (P : category_theory.mono_over Y), P.factors f) _
@[simp]
theorem
category_theory.subobject.mk_factors_iff
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : Y ⟶ X)
[category_theory.mono f]
(g : Z ⟶ X) :
theorem
category_theory.subobject.mk_factors_self
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
theorem
category_theory.subobject.factors_iff
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(P : category_theory.subobject Y)
(f : X ⟶ Y) :
theorem
category_theory.subobject.factors_self
{C : Type u₁}
[category_theory.category C]
{X : C}
(P : category_theory.subobject X) :
theorem
category_theory.subobject.factors_comp_arrow
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{P : category_theory.subobject Y}
(f : X ⟶ ↑P) :
theorem
category_theory.subobject.factors_of_factors_right
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{P : category_theory.subobject Z}
(f : X ⟶ Y)
{g : Y ⟶ Z}
(h : P.factors g) :
theorem
category_theory.subobject.factors_zero
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{P : category_theory.subobject Y} :
P.factors 0
theorem
category_theory.subobject.factors_of_le
{C : Type u₁}
[category_theory.category C]
{Y Z : C}
{P Q : category_theory.subobject Y}
(f : Z ⟶ Y)
(h : P ≤ Q) :
noncomputable
def
category_theory.subobject.factor_thru
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(P : category_theory.subobject Y)
(f : X ⟶ Y)
(h : P.factors f) :
P.factor_thru 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.factor_thru f h = classical.some _
@[simp]
theorem
category_theory.subobject.factor_thru_arrow
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(P : category_theory.subobject Y)
(f : X ⟶ Y)
(h : P.factors f) :
P.factor_thru f h ≫ P.arrow = f
@[simp]
theorem
category_theory.subobject.factor_thru_arrow_assoc
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(P : category_theory.subobject Y)
(f : X ⟶ Y)
(h : P.factors f)
{X' : C}
(f' : Y ⟶ X') :
@[simp]
theorem
category_theory.subobject.factor_thru_self
{C : Type u₁}
[category_theory.category C]
{X : C}
(P : category_theory.subobject X)
(h : P.factors P.arrow) :
P.factor_thru P.arrow h = 𝟙 ↑P
@[simp]
theorem
category_theory.subobject.factor_thru_mk_self
{C : Type u₁}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
@[simp]
theorem
category_theory.subobject.factor_thru_comp_arrow
{C : Type u₁}
[category_theory.category C]
{X Y : C}
{P : category_theory.subobject Y}
(f : X ⟶ ↑P)
(h : P.factors (f ≫ P.arrow)) :
P.factor_thru (f ≫ P.arrow) h = f
@[simp]
theorem
category_theory.subobject.factor_thru_eq_zero
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{P : category_theory.subobject Y}
{f : X ⟶ Y}
{h : P.factors f} :
P.factor_thru f h = 0 ↔ f = 0
theorem
category_theory.subobject.factor_thru_right
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{P : category_theory.subobject Z}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(h : P.factors g) :
f ≫ P.factor_thru g h = P.factor_thru (f ≫ g) _
@[simp]
theorem
category_theory.subobject.factor_thru_zero
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{P : category_theory.subobject Y}
(h : P.factors 0) :
P.factor_thru 0 h = 0
theorem
category_theory.subobject.factor_thru_of_le
{C : Type u₁}
[category_theory.category C]
{Y Z : C}
{P Q : category_theory.subobject Y}
{f : Z ⟶ Y}
(h : P ≤ Q)
(w : P.factors f) :
Q.factor_thru f _ = P.factor_thru f w ≫ P.of_le Q h
theorem
category_theory.subobject.factors_add
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{P : category_theory.subobject Y}
(f g : X ⟶ Y)
(wf : P.factors f)
(wg : P.factors g) :
theorem
category_theory.subobject.factor_thru_add
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{P : category_theory.subobject Y}
(f g : X ⟶ Y)
(w : P.factors (f + g))
(wf : P.factors f)
(wg : P.factors g) :
P.factor_thru (f + g) w = P.factor_thru f wf + P.factor_thru g wg
theorem
category_theory.subobject.factors_left_of_factors_add
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{P : category_theory.subobject Y}
(f g : X ⟶ Y)
(w : P.factors (f + g))
(wg : P.factors g) :
P.factors f
@[simp]
theorem
category_theory.subobject.factor_thru_add_sub_factor_thru_right
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{P : category_theory.subobject Y}
(f g : X ⟶ Y)
(w : P.factors (f + g))
(wg : P.factors g) :
P.factor_thru (f + g) w - P.factor_thru g wg = P.factor_thru f _
theorem
category_theory.subobject.factors_right_of_factors_add
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{P : category_theory.subobject Y}
(f g : X ⟶ Y)
(w : P.factors (f + g))
(wf : P.factors f) :
P.factors g
@[simp]
theorem
category_theory.subobject.factor_thru_add_sub_factor_thru_left
{C : Type u₁}
[category_theory.category C]
[category_theory.preadditive C]
{X Y : C}
{P : category_theory.subobject Y}
(f g : X ⟶ Y)
(w : P.factors (f + g))
(wf : P.factors f) :
P.factor_thru (f + g) w - P.factor_thru f wf = P.factor_thru g _