open import Cat.Diagram.Product.Indexed
open import Cat.Diagram.Product
open import Cat.Prelude

import Cat.Reasoning

module Cat.Morphism.Joint.Mono {o β„“} (C : Precategory o β„“) where

open Cat.Reasoning C

Joint monomorphismsπŸ”—

A pair of morphisms and are jointly monic if for every if and 

is-jointly-monic : βˆ€ {x y z} β†’ Hom x y β†’ Hom x z β†’ Type (o βŠ” β„“)
is-jointly-monic {x = x} f g =
  βˆ€ {a} β†’ (h k : Hom a x) β†’ f ∘ h ≑ f ∘ k β†’ g ∘ h ≑ g ∘ k β†’ h ≑ k

More generally, an family of morphisms is a jointly monic family if for every if for every 

is-jointly-monic-fam
  : βˆ€ {β„“'} {I : Type β„“'}
  β†’ {x : Ob} {yα΅’ : I β†’ Ob}
  β†’ (fα΅’ : βˆ€ i β†’ Hom x (yα΅’ i))
  β†’ Type (o βŠ” β„“ βŠ” β„“')
is-jointly-monic-fam {x = x} fα΅’ =
  βˆ€ {a} β†’ (h k : Hom a x) β†’ (βˆ€ i β†’ fα΅’ i ∘ h ≑ fα΅’ i ∘ k) β†’ h ≑ k

Joint monomorphisms and productsπŸ”—

If has products, then a pair of morphisms is jointly monic if and only if is monic.

module _ (all-products : has-products C) where
  open Binary-products C all-products

The forward direction follows from a short calculation.

  ⟨⟩-monicβ†’jointly-monic
    : βˆ€ {x y z} {f : Hom x y} {g : Hom x z}
    β†’ is-monic ⟨ f , g ⟩
    β†’ is-jointly-monic f g
  ⟨⟩-monicβ†’jointly-monic {f = f} {g = g} ⟨f,g⟩-mono h k p q =
    ⟨f,g⟩-mono h k $
      ⟨ f , g ⟩ ∘ h     β‰‘βŸ¨ ⟨⟩∘ h βŸ©β‰‘
      ⟨ f ∘ h , g ∘ h ⟩ β‰‘βŸ¨ apβ‚‚ ⟨_,_⟩ p q βŸ©β‰‘
      ⟨ f ∘ k , g ∘ k ⟩ β‰‘Λ˜βŸ¨ ⟨⟩∘ k βŸ©β‰‘Λ˜
      ⟨ f , g ⟩ ∘ k     ∎

The reverse direction is a bit trickier, but only just. Suppose that are jointly monic, and let such that

Our goal is to show that As and are jointly monic, it suffices to show that and We can re-arrange our hypothesis to get that

If we apply first and second projections to this equation, then we get exactly the pair of equalities that we were looking for.

  jointly-monicβ†’βŸ¨βŸ©-monic
    : βˆ€ {x y z} {f : Hom x y} {g : Hom x z}
    β†’ is-jointly-monic f g
    β†’ is-monic ⟨ f , g ⟩
  jointly-monicβ†’βŸ¨βŸ©-monic {f = f} {g = g} fg-joint-mono h k p =
    fg-joint-mono h k (by-π₁ ⟨fh,gh⟩=⟨fk,gk⟩) (by-Ο€β‚‚ ⟨fh,gh⟩=⟨fk,gk⟩)
    where
      ⟨fh,gh⟩=⟨fk,gk⟩ : ⟨ f ∘ h , g ∘ h ⟩ ≑ ⟨ f ∘ k , g ∘ k ⟩
      ⟨fh,gh⟩=⟨fk,gk⟩ =
        ⟨ f ∘ h , g ∘ h ⟩ β‰‘Λ˜βŸ¨ ⟨⟩∘ h βŸ©β‰‘Λ˜
        ⟨ f , g ⟩ ∘ h     β‰‘βŸ¨ p βŸ©β‰‘
        ⟨ f , g ⟩ ∘ k     β‰‘βŸ¨ ⟨⟩∘ k βŸ©β‰‘
        ⟨ f ∘ k , g ∘ k ⟩ ∎

This result provides the main motivation for joint monomorphisms. Namely, joint monos let us talk about subobjects of products, even when those products may not exist. Put another way, joint monos offer an alternative characterisation of relations internal to that works even when lacks products.

Joint monos are also slightly more ergonomic than subobjects of products. Typically, if we want to prove that some is monic, then our first step is to invoke the universal property of joint monos factor out this first step into the definition!

Jointly monic families and indexed productsπŸ”—

We can obtain a similar result for jointly monic families and indexed products: if has products, then a family of morphisms is jointly monic if and only if the universal map is monic.

module _ {β„“} {I : Type β„“} (indexed-products : has-products-indexed-by C I) where
  private module ∏ {xα΅’ : I β†’ Ob} = Indexed-product (indexed-products xα΅’)

  tuple-monic→jointly-monic-fam
    : βˆ€ {x} {yα΅’ : I β†’ Ob}
    β†’ {fα΅’ : βˆ€ i β†’ Hom x (yα΅’ i)}
    β†’ is-monic (∏.tuple fα΅’)
    β†’ is-jointly-monic-fam fα΅’

  jointly-monic-fam→tuple-monic
    : βˆ€ {x} {yα΅’ : I β†’ Ob}
    β†’ {fα΅’ : βˆ€ i β†’ Hom x (yα΅’ i)}
    β†’ is-jointly-monic-fam fα΅’
    β†’ is-monic (∏.tuple fα΅’)
The proofs are almost identical to the non-indexed case, so we omit the details in the interest of brevity. 
  tuple-monic→jointly-monic-fam {yᡒ = yᡒ} {fᡒ = fᡒ} tuple-mono h k p =
    tuple-mono h k $
      ∏.tuple fα΅’ ∘ h           β‰‘βŸ¨ tuple∘ C yα΅’ (indexed-products yα΅’) fα΅’ βŸ©β‰‘
      ∏.tuple (Ξ» i β†’ fα΅’ i ∘ h) β‰‘βŸ¨ ap ∏.tuple (funext p) βŸ©β‰‘
      ∏.tuple (Ξ» i β†’ fα΅’ i ∘ k) β‰‘Λ˜βŸ¨ tuple∘ C yα΅’ (indexed-products yα΅’) fα΅’ βŸ©β‰‘Λ˜
      ∏.tuple fᡒ ∘ k           ∎

  jointly-monic-fam→tuple-monic {yᡒ = yᡒ} {fᡒ = fᡒ} fᡒ-joint-mono h k p =
    fα΅’-joint-mono h k Ξ» i β†’
      fα΅’ i ∘ h               β‰‘βŸ¨ pushl (sym ∏.commute) βŸ©β‰‘
      ∏.Ο€ i ∘ ∏.tuple fα΅’ ∘ h β‰‘βŸ¨ ap (∏.Ο€ i ∘_) p βŸ©β‰‘
      ∏.Ο€ i ∘ ∏.tuple fα΅’ ∘ k β‰‘βŸ¨ pulll ∏.commute βŸ©β‰‘
      fᡒ i ∘ k               ∎

If we apply the same line of reasoning that we used at the end of the previous section, we will notice that jointly monic families are relations internal to

Closure properties of joint monosπŸ”—

If are jointly monic and is monic, then and are jointly monic.

jointly-monic-∘
  : βˆ€ {w x y z} {f : Hom x y} {g : Hom x z} {h : Hom w x}
  β†’ is-jointly-monic f g
  β†’ is-monic h
  β†’ is-jointly-monic (f ∘ h) (g ∘ h)
jointly-monic-∘ {h = h} fg-joint-mono h-mono k₁ kβ‚‚ p q =
  h-mono k₁ kβ‚‚ $
  fg-joint-mono (h ∘ k₁) (h ∘ kβ‚‚)
    (assoc _ _ _ Β·Β· p Β·Β· sym (assoc _ _ _))
    (assoc _ _ _ Β·Β· q Β·Β· sym (assoc _ _ _))

Moreover, if and are jointly monic, then is monic.

jointly-monic-cancell
  : βˆ€ {w x y z} {f : Hom x y} {g : Hom x z} {h : Hom w x}
  β†’ is-jointly-monic (f ∘ h) (g ∘ h)
  β†’ is-monic h
jointly-monic-cancell fgh-joint-mono k₁ kβ‚‚ p =
  fgh-joint-mono k₁ kβ‚‚ (extendr p) (extendr p)

We get a similar pair of results for jointly monic families.

jointly-monic-fam-∘
  : βˆ€ {β„“'} {I : Type β„“'} {x y} {zα΅’ : I β†’ Ob}
  β†’ {fα΅’ : βˆ€ i β†’ Hom y (zα΅’ i)} {g : Hom x y}
  β†’ is-jointly-monic-fam fα΅’
  β†’ is-monic g
  β†’ is-jointly-monic-fam (Ξ» i β†’ fα΅’ i ∘ g)
jointly-monic-fam-∘ {g = g} fα΅’-joint-mono g-mono k₁ kβ‚‚ p =
  g-mono k₁ kβ‚‚ $
  fα΅’-joint-mono (g ∘ k₁) (g ∘ kβ‚‚) Ξ» i β†’
    assoc _ _ _ Β·Β· p i Β·Β· sym (assoc _ _ _)

jointly-monic-fam-cancell
  : βˆ€ {β„“'} {I : Type β„“'} {x y} {zα΅’ : I β†’ Ob}
  β†’ {fα΅’ : βˆ€ i β†’ Hom y (zα΅’ i)} {g : Hom x y}
  β†’ is-jointly-monic-fam (Ξ» i β†’ fα΅’ i ∘ g)
  β†’ is-monic g
jointly-monic-fam-cancell fα΅’g-joint-mono k₁ kβ‚‚ p =
  fα΅’g-joint-mono k₁ kβ‚‚ Ξ» i β†’ extendr p

If either of or are monic, then and are jointly monic.

left-monic→jointly-monic
  : βˆ€ {x y z} {f : Hom x y} {g : Hom x z}
  β†’ is-monic f
  β†’ is-jointly-monic f g
left-monicβ†’jointly-monic f-mono k₁ kβ‚‚ p q =
  f-mono k₁ kβ‚‚ p

right-monic→jointly-monic
  : βˆ€ {x y z} {f : Hom x y} {g : Hom x z}
  β†’ is-monic g
  β†’ is-jointly-monic f g
right-monicβ†’jointly-monic g-mono k₁ kβ‚‚ p q =
  g-mono k₁ kβ‚‚ q

Similarly, if any component of a family of maps is monic, then is a jointly monic family.

monic→jointly-monic-fam
  : βˆ€ {β„“'} {I : Type β„“'} {x} {yα΅’ : I β†’ Ob}
  β†’ {fα΅’ : βˆ€ i β†’ Hom x (yα΅’ i)}
  β†’ (i : I) β†’ is-monic (fα΅’ i)
  β†’ is-jointly-monic-fam fα΅’
monicβ†’jointly-monic-fam i fα΅’-monic k₁ kβ‚‚ p =
  fα΅’-monic k₁ kβ‚‚ (p i)

The previous result has an easy generalization: if is a family of morphisms such is jointly monic when restricted along a map then is jointly monic.

restrict-jointly-monic-fam
  : βˆ€ {β„“' β„“''} {I : Type β„“'} {J : Type β„“''}
  β†’ βˆ€ {x} {yβ±Ό : J β†’ Ob} {fβ±Ό : βˆ€ j β†’ Hom x (yβ±Ό j)}
  β†’ (Οƒ : I β†’ J)
  β†’ is-jointly-monic-fam (Ξ» i β†’ fβ±Ό (Οƒ i))
  β†’ is-jointly-monic-fam fβ±Ό
restrict-jointly-monic-fam Οƒ fβ±Ό-joint-mono k₁ kβ‚‚ p =
  fβ±Ό-joint-mono k₁ kβ‚‚ (Ξ» j β†’ p (Οƒ j))

If is jointly monic with itself, then is monic. Moreover, if the constant family is jointly monic, then is monic.

self-jointly-monic→monic
  : βˆ€ {x y} {f : Hom x y}
  β†’ is-jointly-monic f f
  β†’ is-monic f
self-jointly-monicβ†’monic f-joint-monic k₁ kβ‚‚ p =
  f-joint-monic k₁ kβ‚‚ p p

self-jointly-monic-fam→monic
  : βˆ€ {β„“'} {I : Type β„“'} {x y} {f : Hom x y}
  β†’ is-jointly-monic-fam (Ξ» (i : I) β†’ f)
  β†’ is-monic f
self-jointly-monic-famβ†’monic f-joint-mono k₁ kβ‚‚ p =
  f-joint-mono k₁ kβ‚‚ (Ξ» _ β†’ p)

Joint monos via representabilityπŸ”—

Like most things categorical, joint monos admit a definition via representability: and are jointly monic if and only if the map induced by postcomposition is an embedding.

jointly-monic→postcomp-embedding
  : βˆ€ {x y z} {f : Hom x y} {g : Hom x z}
  β†’ is-jointly-monic f g
  β†’ βˆ€ {a} β†’ is-embedding {B = Hom a y Γ— Hom a z} (Ξ» h β†’ f ∘ h , g ∘ h)
jointly-monic→postcomp-embedding fg-joint-mono =
  injectiveβ†’is-embedding! Ξ» {k₁} {kβ‚‚} p β†’
    fg-joint-mono k₁ kβ‚‚ (ap fst p) (ap snd p)

postcomp-embedding→jointly-monic
  : βˆ€ {x y z} {f : Hom x y} {g : Hom x z}
  β†’ (βˆ€ {a} β†’ is-embedding {B = Hom a y Γ— Hom a z} (Ξ» h β†’ f ∘ h , g ∘ h))
  β†’ is-jointly-monic f g
postcomp-embeddingβ†’jointly-monic {f = f} {g = g} postcomp-embed k₁ kβ‚‚ p q =
  ap fst $ postcomp-embed (f ∘ kβ‚‚ , g ∘ kβ‚‚) (k₁ , p ,β‚š q) (kβ‚‚ , refl)

More generally, is a jointly monic family if and only if the map induced by postcomposition is an embedding.

jointly-monic-fam→postcomp-embedding
  : βˆ€ {β„“} {I : Type β„“} {x} {yα΅’ : I β†’ Ob}
  β†’ {fα΅’ : βˆ€ i β†’ Hom x (yα΅’ i)}
  β†’ is-jointly-monic-fam fα΅’
  β†’ βˆ€ {a} β†’ is-embedding {B = (i : I) β†’ Hom a (yα΅’ i)} (Ξ» g i β†’ fα΅’ i ∘ g)
jointly-monic-fam→postcomp-embedding fᡒ-joint-mono =
  injectiveβ†’is-embedding! Ξ» {k₁} {kβ‚‚} p β†’
    fα΅’-joint-mono k₁ kβ‚‚ (apply p)

postcomp-embedding→jointly-monic-fam
  : βˆ€ {β„“} {I : Type β„“} {x} {yα΅’ : I β†’ Ob}
  β†’ {fα΅’ : βˆ€ i β†’ Hom x (yα΅’ i)}
  β†’ (βˆ€ {a} β†’ is-embedding {B = (i : I) β†’ Hom a (yα΅’ i)} (Ξ» g i β†’ fα΅’ i ∘ g))
  β†’ is-jointly-monic-fam fα΅’
postcomp-embeddingβ†’jointly-monic-fam {fα΅’ = fα΅’} postcomp-embed k₁ kβ‚‚ p =
  ap fst $ postcomp-embed (Ξ» i β†’ fα΅’ i ∘ kβ‚‚) (k₁ , funext p) (kβ‚‚ , refl)