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

Strong projective objects🔗

Let $C$ be a precategory. An object $P : C$ is a strong projective object if it has the left-lifting property against strong epimorphisms.

More explicitly, $P$ is a strong projective object if for every morphism $p : P \to Y$ and strong epi $e : X ↠ Y,$ there merely exists a $s : P \to X$ such that $e \circ s = p,$ as in the following diagram:

is-strong-projective : (P : Ob) → Type _
is-strong-projective P =
  ∀ {X Y} (p : Hom P Y) (e : Hom X Y)
  → is-strong-epi e
  → ∃[ s ∈ Hom P X ] (e ∘ s ≡ p)

Warning

Being a strong projective object is actually a weaker condition than being a projective object: strong projectives only need to lift against strong epis, whereas projectives need to lift against all epis.

projective→strong-projective
  : ∀ {P}
  → is-projective P
  → is-strong-projective P
projective→strong-projective pro p e e-strong =
  pro p (record { mor = e ; epic = e-strong .fst })

A functorial definition🔗

Like their non-strong counterparts, we can give a functorial definition of strong projectives. In particular, an object $P : C$ is a strong projective if and only if the $Hom -functor$ $C (P, -)$ preserves strong epimorphisms.

preserves-strong-epis→strong-projective
  : ∀ {P}
  → preserves-strong-epis (Hom-from C P)
  → is-strong-projective P

strong-projective→preserves-strong-epis
  : ∀ {P}
  → is-strong-projective P
  → preserves-strong-epis (Hom-from C P)

These proofs are essentially the same as the corresponding ones for projective objects, so we omit the details.

preserves-strong-epis→strong-projective {P = P} hom-epi {X = X} {Y = Y} p e e-strong =
  epi→surjective (el! (Hom P X)) (el! (Hom P Y))
    (e ∘_)
    (λ {c} → hom-epi e-strong .fst {c = c})
    p

strong-projective→preserves-strong-epis {P = P} pro {X} {Y} {f = f} f-strong =
    surjective→strong-epi (el! (Hom P X)) (el! (Hom P Y)) (f ∘_) $ λ p →
    pro p f f-strong

Closure of strong projectives🔗

Like projective objects, strong projectives are closed under coproducts indexed by set-projective types and retracts.

indexed-coproduct-strong-projective
  : ∀ {κ} {Idx : Type κ}
  → {P : Idx → Ob} {∐P : Ob} {ι : ∀ i → Hom (P i) ∐P}
  → is-set-projective Idx ℓ
  → (∀ i → is-strong-projective (P i))
  → is-indexed-coproduct C P ι
  → is-strong-projective ∐P

retract→strong-projective
  : ∀ {R P}
  → is-strong-projective P
  → (s : Hom R P)
  → has-retract s
  → is-strong-projective R

These proofs are more or less identical to the corresponding ones for projective objects.

indexed-coproduct-strong-projective {P = P} {ι = ι} Idx-pro P-pro coprod {X = X} {Y = Y} p e e-strong = do
  s ← Idx-pro
        (λ i → Σ[ sᵢ ∈ Hom (P i) X ] (e ∘ sᵢ ≡ p ∘ ι i)) (λ i → hlevel 2)
        (λ i → P-pro i (p ∘ ι i) e e-strong)
  pure (match (λ i → s i .fst) , unique₂ (λ i → pullr commute ∙ s i .snd))
  where open is-indexed-coproduct coprod

retract→strong-projective P-pro s r p e e-strong = do
  (t , t-factor) ← P-pro (p ∘ r .retract) e e-strong
  pure (t ∘ s , pulll t-factor ∙ cancelr (r .is-retract))

Moreover, if $C$ has a zero object and a strong projective coproduct $∐_{I} P_{i}$ indexed by a discrete type, then each component of the coproduct is a strong projective.

zero+indexed-coproduct-strong-projective→strong-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-strong-projective ∐P
  → ∀ i → is-strong-projective (P i)

Following the general theme, the proof is identical to the non-strong case.

zero+indexed-coproduct-strong-projective→strong-projective {ι = ι} z coprod ∐P-pro i =
  retract→strong-projective ∐P-pro (ι i) $
  zero→ι-has-retract C coprod z i

Enough strong projectives🔗

A category $C$ is said to have enough strong projectives if for object $X : C$ there is some strong epi $P ↠ X$ with $P$ strong 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 strong 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 Strong-projectives : Type (o ⊔ ℓ) where
  field
    Pro : Ob → Ob
    present : ∀ {X} → Hom (Pro X) X
    present-strong-epi : ∀ {X} → is-strong-epi (present {X})
    projective : ∀ {X} → is-strong-projective (Pro X)

If $C$ has set-indexed coproducts, and $P_{i}$ is a strong separating family with each $P_{i}$ a strong projective, then $C$ has enough strong projectives if $Σ (i : I d x) (C (P_{i}, X))$ is a set-projective type.

  strong-projective-separating-faily→strong-projectives
    : ∀ {Idx : Set ℓ} {Pᵢ : ∣ Idx ∣ → Ob}
    → (∀ X → is-set-projective (Σ[ i ∈ ∣ Idx ∣ ] (Hom (Pᵢ i) X)) ℓ)
    → (∀ i → is-strong-projective (Pᵢ i))
    → is-strong-separating-family Idx Pᵢ
    → Strong-projectives

The hypotheses of this theorem basically give the game away: by definition, there is a strong epimorphism $∐_{Σ (i : I) C (P_{i}, X)} S_{i} \to X$ for every $X .$ Moreover, $Σ (i : I) C (P_{i}, X)$ is set-projective, so the corresponding coproduct is a strong projective.

  strong-projective-separating-faily→strong-projectives
    {Idx} {Pᵢ} Idx-pro Pᵢ-pro strong-sep = strong-projectives where
    open Strong-projectives

    strong-projectives : Strong-projectives
    strong-projectives .Pro X =
      ∐! (Σ[ i ∈ ∣ Idx ∣ ] (Hom (Pᵢ i) X)) (Pᵢ ⊙ fst)
    strong-projectives .present {X = X} =
      ∐!.match (Σ[ i ∈ ∣ Idx ∣ ] (Hom (Pᵢ i) X)) (Pᵢ ⊙ fst) snd
    strong-projectives .present-strong-epi =
      strong-sep
    strong-projectives .projective {X = X} =
      indexed-coproduct-strong-projective
        (Idx-pro X)
        (Pᵢ-pro ⊙ fst)
        (∐!.has-is-ic (Σ[ i ∈ ∣ Idx ∣ ] (Hom (Pᵢ i) X)) (Pᵢ ⊙ fst))