open import Cat.Diagram.Coequaliser.RegularEpi
open import Cat.Diagram.Coproduct.Copower
open import Cat.Diagram.Coproduct.Indexed
open import Cat.Diagram.Limit.Finite
open import Cat.Functor.Conservative
open import Cat.Instances.Sets
open import Cat.Functor.Joint
open import Cat.Functor.Hom
open import Cat.Prelude

import Cat.Morphism.Strong.Epi
import Cat.Diagram.Separator
import Cat.Reasoning

module Cat.Diagram.Separator.Strong
  {o ℓ}
  (C : Precategory o ℓ)
  (coprods : (I : Set ℓ) → has-coproducts-indexed-by C ∣ I ∣)
  where

open Cat.Morphism.Strong.Epi C
open Cat.Diagram.Separator C
open Cat.Reasoning C
open Copowers coprods

private variable
  s : Ob

Strong separators🔗

Recall that a separating object $S$ lets us determine equality of morphisms solely by examining $S -generalized$ objects. This leads to a natural question: what other properties of morphisms can we compute like this? In our case: can we determine if a map $f : C (X, Y)$ is invertible by restricting to generalized objects? Generally speaking, the answer is no, but it is possible if we strengthen our notion of separating object.

Let $C$ be a category with set-indexed coproducts. An object $S$ is a strong separator if the canonical map $∐_{C (S, X)} S \to X$ is a strong epi.

is-strong-separator : Ob → Type (o ⊔ ℓ)
is-strong-separator s = ∀ {x} → is-strong-epi (⊗!.match (Hom s x) s λ e → e)

We can also weaken this definition to a family of objects.

A family of objects $S_{i}$ is a strong separating family if the canonical map $∐_{Σ (i : I), C (S_{i}, X)} S_{i} \to X$ is a strong epi.

is-strong-separating-family
  : ∀ (Idx : Set ℓ)
  → (sᵢ : ∣ Idx ∣ → Ob)
  → Type (o ⊔ ℓ)
is-strong-separating-family Idx sᵢ =
  ∀ {x} → is-strong-epi (∐!.match (Σ[ i ∈ ∣ Idx ∣ ] (Hom (sᵢ i) x)) (sᵢ ⊙ fst) snd)

Strong separators are separators. This follows from the fact that an object $S$ is a separator if and only if the canonical map $∐_{C (S, X)} S \to X$ is an epi.

strong-separator→separator
  : is-strong-separator s
  → is-separator s
strong-separator→separator strong =
  epi→separator coprods (strong .fst)

A similar line of reasoning shows that strong separating families are separating families.

strong-separating-family→separating-family
  : ∀ (Idx : Set ℓ) (sᵢ : ∣ Idx ∣ → Ob)
  → is-strong-separating-family Idx sᵢ
  → is-separating-family sᵢ
strong-separating-family→separating-family Idx sᵢ strong =
  epi→separating-family coprods Idx sᵢ (strong .fst)

Extremal separators🔗

For reasons that we will see shortly, it is useful to weaken the notion of strong separators to extremal epimorphisms.

Let $C$ be a category with set-indexed coproducts. An object $S$ is a strong separator if the canonical map $∐_{C (S, X)} S \to X$ is an extremal epi.

is-extremal-separator : Ob → Type (o ⊔ ℓ)
is-extremal-separator s = ∀ {x} → is-extremal-epi (⊗!.match (Hom s x) s λ e → e)

A family of objects $S_{i}$ is a extremal separating family if the canonical map $∐_{Σ (i : I), C (S_{i}, X)} S_{i} \to X$ is a strong epi.

is-extremal-separating-family
  : ∀ (Idx : Set ℓ)
  → (sᵢ : ∣ Idx ∣ → Ob)
  → Type (o ⊔ ℓ)
is-extremal-separating-family Idx sᵢ =
  ∀ {x} → is-extremal-epi (∐!.match (Σ[ i ∈ ∣ Idx ∣ ] (Hom (sᵢ i) x)) (sᵢ ⊙ fst) snd)

Via a general result involving strong and extremal epis, strong separators are extremal.

strong-separator→extremal-separator
  : is-strong-separator s
  → is-extremal-separator s
strong-separator→extremal-separator strong =
  is-strong-epi→is-extremal-epi strong

strong-separating-family→extremal-separating-family
  : ∀ (Idx : Set ℓ)
  → (sᵢ : ∣ Idx ∣ → Ob)
  → is-strong-separating-family Idx sᵢ
  → is-extremal-separating-family Idx sᵢ
strong-separating-family→extremal-separating-family Idx sᵢ strong =
  is-strong-epi→is-extremal-epi strong

Moreover, if $C$ has all finite limits, then extremal separators are strong.

lex+extremal-separator→strong-separator
  : Finitely-complete C
  → is-extremal-separator s
  → is-strong-separator s
lex+extremal-separator→strong-separator lex extremal =
  is-extremal-epi→is-strong-epi lex extremal

lex+extremal-separating-family→strong-separating-family
  : ∀ (Idx : Set ℓ)
  → (sᵢ : ∣ Idx ∣ → Ob)
  → Finitely-complete C
  → is-extremal-separating-family Idx sᵢ
  → is-strong-separating-family Idx sᵢ
lex+extremal-separating-family→strong-separating-family Idx sᵢ lex extremal =
  is-extremal-epi→is-strong-epi lex extremal

Functorial definitions🔗

We shall now prove our claim that a strong separator $S$ allows us to distinguish invertible morphisms purely by checking invertibility at $S -generalized$ elements. More precisely, if $S$ is a strong separator, then $C (S, -)$ is conservative.

strong-separator→conservative
  : ∀ {s}
  → is-strong-separator s
  → is-conservative (Hom-from C s)

Suppose that $f : C (X, Y)$ is a morphism such that $f \circ e$ is invertible for every $e : C (S, X) .$ We shall show that $f$ itself is invertible by showing that it is both a strong epi and a monomorphism.

strong-separator→conservative {s = s} strong {A = a} {B = b} {f = f} f∘-inv =
  strong-epi+mono→invertible
    f-strong-epi
    f-mono
  where
    module f∘- = Equiv (f ∘_ , is-invertible→is-equiv f∘-inv)

Showing that $f$ is monic is pretty straightforward. Suppose that we have $u, v : C (X, A)$ such that $f \circ u = f \circ v .$ Because $S$ is a separator, we can show that $u = v$ by showing that $u \circ e = v \circ e$ for some $S -generalized$ element $e .$ Moreover, postcomposition with $f$ is injective on morphisms with domain $S$ so it suffices to prove that $f \circ u \circ e = f \circ v \circ e;$ this follows directly from our hypothesis.

    f-mono : is-monic f
    f-mono u v p =
      strong-separator→separator strong λ e →
      f∘-.injective (extendl p)

Proving that $f$ is a strong epi is a bit more work. First, note that we can construct a map $f^{*} : ∐_{C (S, B)} \to A$ by applying the inverse of $f \circ - : C (S, A) \to C (S, B);$ moreover, this map factorizes the canonical map $∐_{C (S, B)} S \to B .$

    f* : Hom ((Hom s b) ⊗! s) a
    f* = ⊗!.match (Hom s b) s λ e → f∘-.from e

    f*-factors : f ∘ f* ≡ ⊗!.match (Hom s b) s (λ e → e)
    f*-factors = ⊗!.unique _ _ _ λ e →
      (f ∘ f*) ∘ ⊗!.ι (Hom s b) s e ≡⟨ pullr (⊗!.commute (Hom s b) s) ⟩≡
      f ∘ f∘-.from e                ≡⟨ f∘-.ε e ⟩≡
      e                             ∎

By definition, the canonical map $∐_{C (S, B)} S \to B$ is a strong epi. Moreover, if a composite $f \circ g$ is a strong epi, then $f$ is a strong epi. If we apply this observation to our factorization, we immediately see that $f$ is a strong epi.

    f-strong-epi : is-strong-epi f
    f-strong-epi =
      strong-epi-cancelr f f* $
      subst is-strong-epi (sym f*-factors) strong

Conversely, if $C (S, -)$ is conservative, then $S$ is an extremal separator. The proof here is some basic data manipulation, so we do not dwell on it too deeply.

conservative→extremal-separator
  : ∀ {s}
  → is-conservative (Hom-from C s)
  → is-extremal-separator s
conservative→extremal-separator f∘-conservative m f p =
  f∘-conservative $
  is-equiv→is-invertible $
  is-iso→is-equiv $ iso
    (λ e → f ∘ ⊗!.ι _ _ e)
    (λ f* → pulll (sym p) ∙ ⊗!.commute _ _)
    (λ e → m .monic _ _ (pulll (sym p) ∙ ⊗!.commute _ _))

In particular, if $C$ is finitely complete, then conservativity of $C (S, -)$ implies that $S$ is a strong separator.

lex+conservative→strong-separator
  : ∀ {s}
  → Finitely-complete C
  → is-conservative (Hom-from C s)
  → is-strong-separator s
lex+conservative→strong-separator lex f∘-conservative =
  is-extremal-epi→is-strong-epi lex $
  conservative→extremal-separator f∘-conservative

We can generalize these results to separating families by considering jointly conservative functors.

strong-separating-family→jointly-conservative
  : ∀ (Idx : Set ℓ) (sᵢ : ∣ Idx ∣ → Ob)
  → is-strong-separating-family Idx sᵢ
  → is-jointly-conservative (λ i → Hom-from C (sᵢ i))

jointly-conservative→extremal-separating-family
  : ∀ (Idx : Set ℓ) (sᵢ : ∣ Idx ∣ → Ob)
  → Finitely-complete C
  → is-jointly-conservative (λ i → Hom-from C (sᵢ i))
  → is-extremal-separating-family Idx sᵢ

lex+jointly-conservative→strong-separating-family
  : ∀ (Idx : Set ℓ) (sᵢ : ∣ Idx ∣ → Ob)
  → Finitely-complete C
  → is-jointly-conservative (λ i → Hom-from C (sᵢ i))
  → is-strong-separating-family Idx sᵢ

The proofs are identical to their non-familial counterparts, so we omit the details.

strong-separating-family→jointly-conservative Idx sᵢ strong {x = a} {y = b} {f = f} f∘ᵢ-inv =
  strong-epi+mono→invertible
    f-strong-epi
    f-mono
  where
    module f∘- {i : ∣ Idx ∣} = Equiv (_ , is-invertible→is-equiv (f∘ᵢ-inv i))

    f-mono : is-monic f
    f-mono u v p =
      strong-separating-family→separating-family Idx sᵢ strong λ eᵢ →
      f∘-.injective (extendl p)

    f* : Hom (∐! (Σ[ i ∈ ∣ Idx ∣ ] (Hom (sᵢ i) b)) (sᵢ ⊙ fst)) a
    f* = ∐!.match _ _ (f∘-.from ⊙ snd)

    f*-factors : f ∘ f* ≡ ∐!.match (Σ[ i ∈ ∣ Idx ∣ ] (Hom (sᵢ i) b)) (sᵢ ⊙ fst) snd
    f*-factors =
      ∐!.unique _ _ _ λ (i , eᵢ) →
      (f ∘ f*) ∘ ∐!.ι _ _ (i , eᵢ) ≡⟨ pullr (∐!.commute _ _) ⟩≡
      f ∘ f∘-.from eᵢ              ≡⟨ f∘-.ε eᵢ ⟩≡
      eᵢ                           ∎

    f-strong-epi : is-strong-epi f
    f-strong-epi =
      strong-epi-cancelr f f* $
      subst is-strong-epi (sym f*-factors) strong

jointly-conservative→extremal-separating-family Idx sᵢ lex f∘-conservative m f p =
  f∘-conservative $ λ i →
  is-equiv→is-invertible $
  is-iso→is-equiv $ iso
    (λ eᵢ → f ∘ ∐!.ι _ _ (i , eᵢ))
    (λ f* → pulll (sym p) ∙ ∐!.commute _ _)
    (λ eᵢ → m .monic _ _ (pulll (sym p) ∙ ∐!.commute _ _))

lex+jointly-conservative→strong-separating-family Idx sᵢ lex f∘-conservative =
  is-extremal-epi→is-strong-epi lex $
  jointly-conservative→extremal-separating-family Idx sᵢ lex f∘-conservative