Projective objects: isomorphism closure and coproducts #
The object property CategoryTheory.isProjective C of being projective is closed under
isomorphisms, so it can serve as the resolving property of finite resolutions, which are
transported along isomorphisms.
The point of any colimit cofan of a family of projective objects is projective. Mathlib's
instance for the chosen coproduct ∐ X requires the index type to live in the universe of the
morphisms of the category; the version here accepts any colimit cofan with any index type, for
instance a coproduct of a sequence of modules indexed by ℕ in ModuleCat.{v} R.
instance
CategoryTheory.isClosedUnderIsomorphisms_isProjective
{C : Type u_1}
[Category.{v_1, u_1} C]
:
Being projective is invariant under isomorphism.
theorem
CategoryTheory.Projective.of_isColimit_cofan
{C : Type u_1}
[Category.{v_1, u_1} C]
{ι : Type u_2}
{X : ι → C}
[∀ (i : ι), Projective (X i)]
{c : Limits.Cofan X}
(hc : Limits.IsColimit c)
:
Projective c.pt
The point of a colimit cofan of projective objects is projective.