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 \to Y$ and epimorphism $e : X ↠ Y,$ there merely exists a $s : P \to X$ such that $e \circ 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 \to X,$ and note that $s \circ 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 \to Y$ to get our desired section $s : Y \to 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¹, 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 \circ - : C (P, X) \to 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) \to A$ be a pair of functions into an arbitrary set $A$ such that $g (f \circ s) = h (f \circ 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!↩︎