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

Projective objectsπŸ”—

Let be a precategory. An object is projective if for every morphism and epimorphism there merely exists a such that as in the following diagram:

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

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 lets us pick a of from the preimage of a along every This endows with an internal version of the axiom of choice.

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

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 we can factorize to get our desired section

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 projectives1, and many categories inherit their epimorphisms from However, it is still possible to have projectives if epis in are extremely structured, or there are very few maps out of some

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 has an initial object 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 is projective if and only if the preserves epimorphisms.

For the forward direction, recall that in epis are surjective. This means that if is an epi in then is surjective, as 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 be projective, be an epi, and be a pair of functions into an arbitrary set such that for any To show that preserves epis, we must show that which follows directly from the existence of a lift for every

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 and are both projective, then their coproduct 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 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 has a zero object and a projective coproduct 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 has a zero object and 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 is said to have enough projectives if for object there is some with projective. We will refer to these projectives as projective presentations of

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

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