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:
: (P : Ob) → Type _
is-strong-projective =
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 (record { mor = e ; epic = e-strong .fst }) pro p
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.
{P = P} hom-epi {X = X} {Y = Y} p e e-strong =
preserves-strong-epis→strong-projective (el! (Hom P X)) (el! (Hom P Y))
epi→surjective (e ∘_)
(λ {c} → hom-epi e-strong .fst {c = c})
p
{P = P} pro {X} {Y} {f = f} f-strong =
strong-projective→preserves-strong-epis (el! (Hom P X)) (el! (Hom P Y)) (f ∘_) $ λ p →
surjective→strong-epi 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.
{P = P} {ι = ι} Idx-pro P-pro coprod {X = X} {Y = Y} p e e-strong = do
indexed-coproduct-strong-projective
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)
(match (λ i → s i .fst) , unique₂ (λ i → pullr commute ∙ s i .snd))
pure where open is-indexed-coproduct coprod
= do
retract→strong-projective P-pro s r p e e-strong (t , t-factor) ← P-pro (p ∘ r .retract) e e-strong
(t ∘ s , pulll t-factor ∙ cancelr (r .is-retract)) pure
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.
{ι = ι} z coprod ∐P-pro i =
zero+indexed-coproduct-strong-projective→strong-projective (ι i) $
retract→strong-projective ∐P-pro 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
: Ob → Ob
Pro : ∀ {X} → Hom (Pro X) X
present : ∀ {X} → is-strong-epi (present {X})
present-strong-epi : ∀ {X} → is-strong-projective (Pro X) projective
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 .Pro X =
strong-projectives (Σ[ i ∈ ∣ Idx ∣ ] (Hom (Pᵢ i) X)) (Pᵢ ⊙ fst)
∐! .present {X = X} =
strong-projectives .match (Σ[ i ∈ ∣ Idx ∣ ] (Hom (Pᵢ i) X)) (Pᵢ ⊙ fst) snd
∐!.present-strong-epi =
strong-projectives
strong-sep.projective {X = X} =
strong-projectives
indexed-coproduct-strong-projective(Idx-pro X)
(Pᵢ-pro ⊙ fst)
(∐!.has-is-ic (Σ[ i ∈ ∣ Idx ∣ ] (Hom (Pᵢ i) X)) (Pᵢ ⊙ fst))