open import Cat.Diagram.Pullback.Properties
open import Cat.Diagram.Product.Indexed
open import Cat.Diagram.Pullback.Along
open import Cat.Diagram.Pullback
open import Cat.Functor.Morphism
open import Cat.Diagram.Product
open import Cat.Diagram.Omega
open import Cat.Functor.Hom
open import Cat.Prelude hiding (Ω; true)

open import Data.Set.Projective
open import Data.Set.Surjection

import Cat.Displayed.Instances.Subobjects.Reasoning as Subr
import Cat.Displayed.Instances.Subobjects as Subobjs
import Cat.Reasoning

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

open Cat.Reasoning C
open Subobjs C

private variable
  A X Y : Ob

Injective objects🔗

Let $\mathcal{C}$ be a precategory. An object $A:\mathcal{C}$ is injective if for every morphism $i:X\to A$ and monomorphism $e:X\twoheadrightarrow Y\text{,}$ there merely exists an extension $r:Y\to A$ such that $r\circ m=i\text{,}$ as in the following diagram:

More concisely, $A$ is injective if it has the right-lifting property relative to monomorphisms in $\mathcal{C}\text{.}$

is-injective : (A : Ob) → Type _
is-injective A =
  ∀ {X Y} (i : Hom X A) (m : X ↪ Y)
  → ∃[ r ∈ Hom Y A ] (r ∘ m .mor ≡ i)

Classically, injective objects are usually very easy to find. For example. the law of excluded middle implies that every pointed set is injective in the category of sets. To extend a map $i:X\to A$ along an injection $m:X\hookrightarrow Y\text{,}$ just decide if each $y:Y$ is in the image of $m\text{.}$ If it is, we can use $i\text{.}$ If it isn’t, we can send it to the designated point.

Constructively, injective objects are a bit harder to come by, as we can’t use excluded middle to decide if some fibre is empty. However, they are much more abundant than projective objects. For example, the type of partial elements is injective for every type $A\text{.}$

A functorial definition🔗

Some authors prefer to define injective objects via a functorial approach. In particular, an object $A:\mathcal{C}$ is injective if and only if the $\mathbf{Hom}\text{-functor}$ $\mathcal{C}(-,A):{\mathcal{C}}^{\mathrm{op}}\to \mathbf{Sets}$ preserves epimorphisms.

For the forward direction, recall that in $\mathbf{Sets}\text{,}$ epis are surjective. Moreover, epimorphisms in ${\mathcal{C}}^{\mathrm{op}}$ are monomorphisms in $\mathcal{C}\text{.}$ This means that if $m:X\hookrightarrow Y$ is a mono in $\mathcal{C}\text{,}$ then $-\circ m:\mathcal{C}(Y,A)\to \mathcal{C}(X,A)$ is surjective, as $\mathcal{C}(-,A)$ preserves epis. This directly gives us the factorization we need!

preserves-epis→injective
  : preserves-epis (Hom-into C A)
  → is-injective A
preserves-epis→injective {A = A} hom-epi {X = X} {Y = Y} i m =
  epi→surjective (el! (Hom Y A)) (el! (Hom X A))
    (_∘ m .mor)
    (λ {c} → hom-epi (m .monic) {c = c})
    i

For the reverse direction, let $A$ be injective, $m:X\hookrightarrow Y$ be a mono, and $g,h:\mathcal{C}(X,A)\to K$ be a pair of functions into an arbitrary set $K$ such that $g(r\circ m)=h(r\circ m)$ for any $r:\mathcal{C}(X,A)\text{.}$ To show that $\mathcal{C}(P,-)$ preserves epis, we must show that $g=h\text{,}$ which follows directly from the existence of an extension for every $\mathcal{C}(X,A)\text{.}$

injective→preserves-epis
  : is-injective A
  → preserves-epis (Hom-into C A)
injective→preserves-epis inj {f = m} m-mono g h p =
  ext λ k →
    rec! (λ r r-retract →
      g k        ≡˘⟨ ap g r-retract ⟩≡˘
      g (r ∘ m)  ≡⟨ p $ₚ r ⟩≡
      h (r ∘ m)  ≡⟨ ap h r-retract ⟩≡
      h k  ∎)
      (inj k (make-mono m m-mono))

Closure of injectives🔗

Projective objects are equipped with a mapping-in property, so they tend to interact nicely with other constructions that are also characterised via mapping-in properties. For instance, f $P$ and $Q$ are both injective, then their product $P+Q$ is injective (if it exists).

product-injective
  : ∀ {A B A×B} {π₁ : Hom A×B A} {π₂ : Hom A×B B}
  → is-injective A
  → is-injective B
  → is-product C π₁ π₂
  → is-injective A×B

The proof is a nice extension chase. Our goal is to fill the dashed line in the following diagram.

Both $A$ and $B$ are projective, so we can extend ${\pi }_1\circ i$ and ${\pi }_2\circ i$ along $m$ to get a pair of maps $r_1:Y\to A$ and $r_2:Y\to B\text{.}$

Finally, we can use the universal property of the product to combine $r_1$ and $r_2$ into a map $⟨r_1,r_2⟩:Y\to A\times B\text{.}$ Moreover, ${\pi }_1\circ ⟨r_1,r_2⟩\circ m=r_1\circ m=i$ and ${\pi }_2\circ ⟨r_1,r_2⟩\circ m=r_2\circ m=i\text{,}$ so $⟨r_1,r_2⟩$ is a valid extension.

product-injective {π₁ = π₁} {π₂ = π₂} A-inj B-inj prod i m = do
  (r₁ , r₁-factor) ← A-inj (π₁ ∘ i) m
  (r₂ , r₂-factor) ← B-inj (π₂ ∘ i) m
  pure (⟨ r₁ , r₂ ⟩ , unique₂ (pulll π₁∘⟨⟩) (pulll π₂∘⟨⟩) (sym r₁-factor) (sym r₂-factor))
  where open is-product prod

We can extend this result to indexed products, provided that the indexing type is set projective.

indexed-coproduct-projective
  : ∀ {κ} {Idx : Type κ}
  → {Aᵢ : Idx → Ob} {∏Aᵢ : Ob} {π : ∀ i → Hom ∏Aᵢ (Aᵢ i)}
  → is-set-projective Idx ℓ
  → (∀ i → is-injective (Aᵢ i))
  → is-indexed-product C Aᵢ π
  → is-injective ∏Aᵢ

The idea of the proof is the same as the non-indexed case. We start with a diagram of the following shape.

Our plan is to construct componentwise extensions $r_i:\mathcal{C}(Y,A_i)$ for each of the components of the product, and then use the universal property to staple them all together into a single extension $⟨r_i⟩:\mathcal{C}(Y,{\prod }_{i:I}{A}_i)\text{.}$

However, there is a snag in this plan: we only get the mere existence of each extension $r_i$ for each $i:I\text{,}$ whereas we need the mere existence of all the extensions simultaneously. In general, this requires the axiom of choice, but we can avoid this by requiring that $I$ be set-projective.

indexed-coproduct-projective {Aᵢ = Aᵢ} {π = π} Idx-pro Aᵢ-inj prod {X = X} {Y = Y} ι m = do
  r ← Idx-pro
    (λ i → Σ[ rᵢ ∈ Hom Y (Aᵢ i) ] rᵢ ∘ m .mor ≡ π i ∘ ι)
    (λ _ → hlevel )
    (λ i → Aᵢ-inj i (π i ∘ ι) m)
  pure (tuple (λ i → r i .fst) , unique₂ (λ i → pulll commute ∙ r i .snd))
  where open is-indexed-product prod

Injectives are also closed under sections. This follows by a straightforward bit of algebra.

section→injective
  : ∀ {S A}
  → is-injective A
  → (r : Hom A S)
  → has-section r
  → is-injective S
section→injective A-inj r s i m = do
  (t , t-factor) ← A-inj (s .section ∘ i) m
  pure (r ∘ t , pullr t-factor ∙ cancell (s .is-section))

If $\mathcal{C}$ has all pullbacks, then every subobject classifier is injective.

Ω-injective
  : {Ω : Ob} {true : Subobject Ω}
  → has-pullbacks C
  → is-generic-subobject C true
  → is-injective Ω

Let $(\Omega ,\mathrm{true})$ be a subobject classifier in $\mathcal{C}\text{,}$ and consider the following extension problem.

Ω-injective {Ω = Ω} {true = true} pullbacks Ω-subobj {X} {Y} i m =
  pure extension
  where
    open is-generic-subobject Ω-subobj
    open Pullbacks C pullbacks
    open props pullbacks (record { true = true ; generic = Ω-subobj })

At first glance, it seems like we might be able to just classify the subobject $m$ to get an extension $\mathrm{name}(m):\mathcal{C}(Y,\Omega )\text{.}$ Though this map does have the right type, it is not actually an extension of $i\text{.}$ The core of the problem is that $\mathrm{name}(m)$ classifies generalized elements of $Y$ that lie within $m\text{,}$ but we need to classify generalized elements of $Y$ that lie within $i$ instead!

We can do this by pulling back $i$ along $\mathrm{true}$ to get a subobject $[i]$ of $X\text{,}$ which we can then compose with $m$ to get a subobject of $Y\text{.}$

    [i] : Subobject X
    [i] = named i

    m∩[i] : Subobject Y
    m∩[i] = cutₛ (∘-is-monic (m .monic) ([i] .monic))

We can then classify our subobject $m\circ [i]$ to get a map $\mathrm{name}(m\circ [i]):\mathcal{C}(Y,\Omega )\text{,}$ which is an extension of $i\text{.}$

To see this, recall that two maps $f,g:\mathcal{C}(X,\Omega )$ are equal when $[g]:\mathcal{C}(\mathrm{dom}(g),X)$ is a pullback of $\mathrm{true}$ along $f\text{.}$ In our case, this means that we must show that the following square is a pullback square.

We can re-arrange this square a bit to get the following diagram.

The right-hand square is a pullback square, as $\mathrm{name}(m\circ [i])$ classifies the subobject $m\circ [i]\text{.}$ Moreover, the left-hand square is also a pullback square, as every $f$ is the pullback of $m\circ f$ along $m$ when $m$ is monic. We can paste these two squares together to get our original square, which must also be a pullback by pasting. This means that $\mathrm{name}(m\circ [i])\circ m=i\text{,}$ which completes the proof.

    extension : Σ[ i* ∈ Hom Y Ω ] i* ∘ m .mor ≡ i
    extension .fst = name m∩[i]
    extension .snd =
      Ω-unique₂ $
      paste-is-pullback-along
        (classifies m∩[i])
        (is-pullback-along-monic (m .monic))
        refl

Enough injectives🔗

Note that there are two variations on this condition: one where there merely exists a injective resolution for every $X\text{,}$ and another where those resolutions are provided as structure. We prefer to work with the latter, as it tends to be less painful to work with.

record Injectives : Type (o ⊔ ℓ) where
  field
    Inj : Ob → Ob
    inj-resolve : ∀ {X} → X ↪ Inj X
    inj-injective : ∀ {X} → is-injective (Inj X)