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

open Cat.Morphism.StrongEpi 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→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}→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→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→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}→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∘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→is-invertible f-mono f-strong-epi 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∘u=f∘v.$ Because $S$ is a separator, we can show that $u=v$ by showing that $u∘e=v∘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∘u∘e=f∘v∘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)}→A$ by applying the inverse of $f∘−:C(S,A)→C(S,B);$ moreover, this map factorizes the canonical map $∐_{C(S,B)}S→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→B$ is a strong epi. Moreover, if a composite $f∘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-cancell 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→is-invertible f-mono f-strong-epi 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-cancell 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