module Cat.Diagram.Projective.Strong
{o β}
(C : Precategory o β)
where

# Strong projective objectsπ

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

More explicitly, is a strong projective object if for every morphism and strong epi there merely exists a such that 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 is a strong projective if and only if the 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 has a zero object and a strong projective coproduct 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 is said to have enough strong projectives if for object there is some strong epi with strong 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 strong 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 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 has set-indexed coproducts, and is a strong separating family with each a strong projective, then has enough strong projectives if 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 for every Moreover, 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))