module Cat.Diagram.Projective {o β} (C : Precategory o β) where

# Projective objectsπ

Let
$C$
be a precategory. An object
$P:C$
is **projective** if for every morphism
$p:PβY$
and epimorphism
$e:XβY,$
there merely exists a
$s:PβX$
such that
$eβs=p,$
as in the following diagram:

More concisely, $P$ is projective if it has the left-lifting property relative to epimorphisms in $C.$

is-projective : (P : Ob) β Type _ is-projective P = β {X Y} (p : Hom P Y) (e : X β Y) β β[ s β Hom P X ] (e .mor β s β‘ p)

If we take the perspective of generalized elements, then a projective object $P$ lets us pick a $P-element$ of $X$ from the preimage $e_{β1}(y)$ of a $P-element$ $y:Y$ along every $e:XβY.$ This endows $C$ with an internal $P-relative$ version of the axiom of choice.

This intuition can be made more precise by noticing that every object of $C$ is projective if and only if every epimorphism (merely) splits. For the forward direction, let $e:XβY$ have a section $s:YβX,$ and note that $sβp$ factorizes $p$ through $e.$

epis-splitβall-projective : (β {X Y} β (e : X β Y) β β₯ has-section (e .mor) β₯) β β {P} β is-projective P epis-splitβall-projective epi-split p e = do s β epi-split e pure (s .section β p , cancell (s .is-section)) where open has-section

Conversely, given an epi $XβY,$ we can factorize $id:YβY$ to get our desired section $s:YβX.$

all-projectiveβepis-split : (β {P} β is-projective P) β β {X Y} β (e : X β Y) β β₯ has-section (e .mor) β₯ all-projectiveβepis-split pro e = do (s , p) β pro id e pure (make-section s p)

This suggests that projective objects are quite hard to come by in
constructive foundations! For the most part, this is true:
constructively, the category of sets has very few projectives^{1}, and many categories inherit their
epimorphisms from
$Sets.$
However, it is still possible to have projectives if epis in
$C$
are extremely structured, or there are very few maps out of some
$P.$

For instance, observe that every epi splits in a pregroupoid, so every every object in a pregroupoid must be projective.

pregroupoidβall-projective : is-pregroupoid C β β {P} β is-projective P pregroupoidβall-projective pregroupoid = epis-splitβall-projective Ξ» e β pure (invertibleβto-has-section (pregroupoid (e .mor)))

Likewise, if $C$ has an initial object $β₯:C,$ then $β₯$ is projective, as there is a unique map out of $β₯.$

module _ (initial : Initial C) where open Initial initial initial-projective : is-projective bot initial-projective p e = pure (Β‘ , Β‘-uniqueβ (e .mor β Β‘) p)

## A functorial definitionπ

Some authors prefer to define projective objects via a functorial approach. In particular, an object $P:C$ is projective if and only if the $Hom-functor$ $C(P,β)$ preserves epimorphisms.

For the forward direction, recall that in $Sets,$ epis are surjective. This means that if $e:XβY$ is an epi in $C,$ then $eββ:C(P,X)βC(P,Y)$ is surjective, as $C(P,β)$ preserves epis. This directly gives us the factorization we need!

preserves-episβprojective : β {P} β preserves-epis (Hom-from C P) β is-projective P preserves-episβprojective {P = P} hom-epi {X = X} {Y = Y} p e = epiβsurjective (el! (Hom P X)) (el! (Hom P Y)) (e .mor β_) (Ξ» {c} β hom-epi (e .epic) {c = c}) p

For the reverse direciton, let $P$ be projective, $f:XβY$ be an epi, and $g,h:C(P,X)βA$ be a pair of functions into an arbitrary set $A$ such that $g(fβs)=h(fβs)$ for any $s:C(P,X).$ To show that $C(P,β)$ preserves epis, we must show that $g=h,$ which follows directly from the existence of a lift for every $C(P,X).$

projectiveβpreserves-epis : β {P} β is-projective P β preserves-epis (Hom-from C P) projectiveβpreserves-epis pro {f = f} f-epi g h p = ext Ξ» k β rec! (Ξ» s s-section β g k β‘Λβ¨ ap g s-section β©β‘Λ g (f β s) β‘β¨ p $β s β©β‘ h (f β s) β‘β¨ ap h s-section β©β‘ h k β) (pro k (record { epic = f-epi }))

## Closure of projectivesπ

Projective objects are equipped with a mapping-out property, so they tend to interact nicely with other constructions that also have a mapping-out property. For instance, f $P$ and $Q$ are both projective, then their coproduct $P+Q$ is projective (if it exists).

coproduct-projective : β {P Q P+Q} {ΞΉβ : Hom P P+Q} {ΞΉβ : Hom Q P+Q} β is-projective P β is-projective Q β is-coproduct C ΞΉβ ΞΉβ β is-projective P+Q coproduct-projective {ΞΉβ = ΞΉβ} {ΞΉβ = ΞΉβ} P-pro Q-pro coprod p e = do (sβ , sβ-factor) β P-pro (p β ΞΉβ) e (sβ , sβ-factor) β Q-pro (p β ΞΉβ) e pure $ [ sβ , sβ ] , uniqueβ (pullr []βΞΉβ β sβ-factor) (pullr []βΞΉβ β sβ-factor) refl refl where open is-coproduct coprod

We can extend this result to indexed coproducts, provided that the indexing type is set projective.

indexed-coproduct-projective : β {ΞΊ} {Idx : Type ΞΊ} β {P : Idx β Ob} {βP : Ob} {ΞΉ : β i β Hom (P i) βP} β is-set-projective Idx β β (β i β is-projective (P i)) β is-indexed-coproduct C P ΞΉ β is-projective βP indexed-coproduct-projective {P = P} {ΞΉ = ΞΉ} Idx-pro P-pro coprod {X = X} {Y = Y} p e = do s β Idx-pro (Ξ» i β Ξ£[ sα΅’ β Hom (P i) X ] (e .mor β sα΅’ β‘ p β ΞΉ i)) (Ξ» i β hlevel 2) (Ξ» i β P-pro i (p β ΞΉ i) e) pure (match (Ξ» i β s i .fst) , uniqueβ (Ξ» i β pullr commute β s i .snd)) where open is-indexed-coproduct coprod

Note that this projectivity requirement is required: if projective objects were closed under arbitrary coproducts, then we would immediately be able to prove the axiom of choice: the singleton set is both a projective object and a dense separator in $Sets,$ so closure under arbitrary coproducts would mean that every set is projective, which is precisely the axiom of choice.

Putting coproducts aside for a moment, note that projectives are closed under retracts. This follows by a straightforward bit of algebra.

retractβprojective : β {R P} β is-projective P β (s : Hom R P) β has-retract s β is-projective R retractβprojective P-pro s r p e = do (t , t-factor) β P-pro (p β r .retract) e pure (t β s , pulll t-factor β cancelr (r .is-retract))

A nice consequence of this is that if $C$ has a zero object and a projective coproduct $β_{I}P_{i}$ indexed by a discrete type, then each component of the coproduct is also projective.

zero+indexed-coproduct-projectiveβprojective : β {ΞΊ} {Idx : Type ΞΊ} β¦ Idx-Discrete : Discrete Idx β¦ β {P : Idx β Ob} {βP : Ob} {ΞΉ : β i β Hom (P i) βP} β Zero C β is-indexed-coproduct C P ΞΉ β is-projective βP β β i β is-projective (P i)

This follows immediately from the fact that if $C$ has a zero object and $β_{I}P_{i}$ is indexed by a discrete type, then each coproduct inclusion has a retract.

zero+indexed-coproduct-projectiveβprojective {ΞΉ = ΞΉ} z coprod βP-pro i = retractβprojective βP-pro (ΞΉ i) $ zeroβΞΉ-has-retract C coprod z i

## Enough projectivesπ

A category
$C$
is said to have **enough projectives** if for object
$X:C$
there is some
$PβX$
with
$P$
projective. We will refer to these projectives as **projective
presentations** of
$X.$

Note that there are two variations on this condition: one where there
*merely* exists a projective presentation for every
$X,$
and another where those presentations are provided as structure. We
prefer to work with the latter, as it tends to be less painful to work
with.

record Projectives : Type (o β β) where field Pro : Ob β Ob present : β {X} β Pro X β X projective : β {X} β is-projective (Pro X)

In fact, it is consistent that the only projective sets are the finite sets!β©οΈ