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βY$ and strong epi $e:XβY,$ there merely exists a $s:PβX$ such that $eβ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)

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)

module _ (coprods : (Idx : Set β) β has-coproducts-indexed-by C β£ Idx β£) where open Cat.Diagram.Separator.Strong C coprods open Copowers coprods

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:Idx)(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}β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))