CategoryTheory.Subobject.factors_of_le
theorem CategoryTheory.Subobject.factors_of_le :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z : C} {P Q : CategoryTheory.Subobject Y}
(f : Z ⟶ Y), P ≤ Q → P.Factors f → Q.Factors f
This theorem states that in any category `C`, for any two objects `Y` and `Z`, and any two subobjects `P` and `Q` of `Y`, if there is a morphism `f` from `Z` to `Y`, and if `P` is less than or equal to `Q`, then if there exists a factorization of `f` through `P`, there must also exist a factorization of `f` through `Q`. In other words, if `f` can be factored through a smaller subobject `P`, it can also be factored through a larger subobject `Q`.
More concisely: In any category, given two objects and two subobjects, if a morphism from one object to another factors through a smaller subobject, then it also factors through any larger subobject containing it.
|
CategoryTheory.Subobject.factors_iff
theorem CategoryTheory.Subobject.factors_iff :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (P : CategoryTheory.Subobject Y) (f : X ⟶ Y),
P.Factors f ↔ (CategoryTheory.Subobject.representative.obj P).Factors f
The theorem `CategoryTheory.Subobject.factors_iff` states that for any categories `X` and `Y` in a category `C`, a subobject `P` of `Y`, and a morphism `f` from `X` to `Y`, there exists a factorisation of `f` through `P` if and only if there exists a factorisation of `f` through the representative `MonoOver` of `P`. Simply put, it says that a morphism can be factored through a subobject if and only if it can be factored through a representative of that subobject.
More concisely: For any categories C, subobject P of Y, and morphism f from X to Y in C, there exists a factorization of f through P if and only if there exists a factorization of f through the monomorphism MonoOver(P).
|
CategoryTheory.Subobject.factorThru_arrow
theorem CategoryTheory.Subobject.factorThru_arrow :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (P : CategoryTheory.Subobject Y) (f : X ⟶ Y)
(h : P.Factors f), CategoryTheory.CategoryStruct.comp (P.factorThru f h) P.arrow = f
The theorem `CategoryTheory.Subobject.factorThru_arrow` states that for any category `C`, any objects `X` and `Y` in `C`, a subobject `P` of `Y`, and a morphism `f` from `X` to `Y` which factors through `P`, the composition of the factorization of `f` through `P` (denoted as `CategoryTheory.Subobject.factorThru P f h`) with the morphism from the underlying object of `P` to `Y` (denoted as `CategoryTheory.Subobject.arrow P`) is equal to `f`. In simpler terms, it states that if we first factor `f` through `P`, and then follow the arrow from `P` to `Y`, we end up with the original morphism `f`. This theorem is a formalization of the property of factorization in category theory.
More concisely: Given any category C, object X, object Y, subobject P of Y, and morphism f from X to Y factors through P, the composite of the factorization of f through P and the morphism from the subobject P to Y equals f.
|