open import Cat.Diagram.Coproduct.Indexed
open import Cat.Diagram.Coproduct
open import Cat.Functor.Morphism
open import Cat.Diagram.Initial
open import Cat.Diagram.Zero
open import Cat.Functor.Hom
open import Cat.Groupoid
open import Cat.Prelude

open import Data.Set.Projective
open import Data.Set.Surjection
open import Data.Dec

import Cat.Reasoning

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

open Cat.Reasoning C

Projective objects🔗

Let $\mathcal{C}$ be a precategory. An object $P:\mathcal{C}$ is projective if for every morphism $p:P\to Y$ and epimorphism $e:X\twoheadrightarrow Y\text{,}$ there merely exists a $s:P\to X$ such that $e\circ s=p\text{,}$ as in the following diagram:

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

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\text{-element}$ of $X$ from the preimage $e^{-1}(y)$ of a $P\text{-element}$ $y:Y$ along every $e:X\twoheadrightarrow Y\text{.}$ This endows $\mathcal{C}$ with an internal $P\text{-relative}$ version of the axiom of choice.

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

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\twoheadrightarrow Y\text{,}$ we can factorize $\mathrm{id}:Y\to Y$ to get our desired section $s:Y\to X\text{.}$

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 $\mathbf{Sets}\text{.}$ However, it is still possible to have projectives if epis in $\mathcal{C}$ are extremely structured, or there are very few maps out of some $P\text{.}$

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 $\mathcal{C}$ has an initial object $\perp :\mathcal{C}\text{,}$ then $\perp$ is projective, as there is a unique map out of $\perp \text{.}$

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:\mathcal{C}$ is projective if and only if the $\mathbf{Hom}\text{-functor}$ $\mathcal{C}(P,-)$ preserves epimorphisms.

For the forward direction, recall that in $\mathbf{Sets}\text{,}$ epis are surjective. This means that if $e:X\twoheadrightarrow Y$ is an epi in $\mathcal{C}\text{,}$ then $e\circ -:\mathcal{C}(P,X)\to \mathcal{C}(P,Y)$ is surjective, as $\mathcal{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\twoheadrightarrow Y$ be an epi, and $g,h:\mathcal{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:\mathcal{C}(P,X)\text{.}$ To show that $\mathcal{C}(P,-)$ preserves epis, we must show that $g=h\text{,}$ which follows directly from the existence of a lift for every $\mathcal{C}(P,X)\text{.}$

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 )
        (λ 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 $\mathbf{Sets}\text{,}$ 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 $\mathcal{C}$ has a zero object and a projective coproduct ${\coprod }_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 $\mathcal{C}$ has a zero object and ${\coprod }_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 $\mathcal{C}$ is said to have enough projectives if for object $X:\mathcal{C}$ there is some $P\twoheadrightarrow X$ with $P$ projective. We will refer to these projectives as projective presentations of $X\text{.}$

Note that there are two variations on this condition: one where there merely exists a projective presentation for every $X\text{,}$ 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)