CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj
theorem CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : C),
CategoryTheory.Projective P ↔ (CategoryTheory.coyoneda.obj (Opposite.op P)).PreservesEpimorphisms
This theorem states that for any category `C` and any object `P` in `C`, `P` is projective if and only if the functor `CategoryTheory.coyoneda.obj (Opposite.op P)` preserves epimorphisms. Here, "projective" means that for every epimorphism and every morphism from `P`, there exists a morphism from `P` making the relevant diagram commute. The functor `CategoryTheory.coyoneda.obj (Opposite.op P)` takes any object of the opposite category `Cᵒᵖ` to the set of morphisms from `P` to that object in `C`. "Preserves epimorphisms" means that if a morphism in the domain category is an epimorphism, then its image under the functor is also an epimorphism in the codomain category.
More concisely: A object P in a category C is projective if and only if the functor taking an object to the set of morphisms from P to it preserves epimorphisms in the opposite category.
|
CategoryTheory.Projective.factorThru_comp
theorem CategoryTheory.Projective.factorThru_comp :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P X E : C} [inst_1 : CategoryTheory.Projective P]
(f : P ⟶ X) (e : E ⟶ X) [inst_2 : CategoryTheory.Epi e],
CategoryTheory.CategoryStruct.comp (CategoryTheory.Projective.factorThru f e) e = f
The theorem `CategoryTheory.Projective.factorThru_comp` states that for every category `C` with a projective object `P` and objects `X` and `E`, given a morphism `f` from `P` to `X` and an epimorphism `e` from `E` to `X`, the composition of the morphism `f` factored through `e` (using the `CategoryTheory.Projective.factorThru` function) and `e` itself is equal to `f`. This shows that the factoring of `f` through `e` preserves the original transformation `f` when followed by `e`.
More concisely: Given a category with a projective object, for any morphism from the projective object to an object and an epimorphism to that object, the factorization of the morphism through the epimorphism equals the original morphism.
|
CategoryTheory.Adjunction.map_projective
theorem CategoryTheory.Adjunction.map_projective :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
{F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C},
(F ⊣ G) →
∀ [inst_2 : G.PreservesEpimorphisms] (P : C),
CategoryTheory.Projective P → CategoryTheory.Projective (F.obj P)
This theorem states that for any categories `C` and `D`, and any functors `F` from `C` to `D` and `G` from `D` to `C`, if `F` is a left adjoint to `G` and `G` preserves epimorphisms, then for any object `P` in `C` that is projective, the object `F.obj P` in `D` is also projective. Here, an object is said to be projective if every morphism from it to an epimorphism can be factored through the epimorphism.
More concisely: Given categories `C`, `D`, functors `F: C -> D` left adjoint to `G: D -> C`, and `G` preserving epimorphisms, if `P` is a projective object in `C`, then `F.obj P` is a projective object in `D`.
|