module Cat.Functor.Adjoint.Properties where
Basic properties of adjoints🔗
This file contains a collection of basic results about adjoint functors, particularly focusing on when a left/right adjoint is faithful, full, etc.
module _
{oc ℓc od ℓd}
{C : Precategory oc ℓc}
{D : Precategory od ℓd}
{L : Functor C D} {R : Functor D C}
(L⊣R : L ⊣ R)
where
private
module C = Cat.Reasoning C
module D = Cat.Reasoning D
module L = Cat.Functor.Reasoning L
module R = Cat.Functor.Reasoning R
open _⊣_ L⊣R
Faithful adjoints🔗
Let be a pair of adjoint functors. The following conditions are equivalent:
Let’s start with (1 ⇒ 2). Suppose that is faithful, and that is faithful, so it suffices to show that Moreover, is a left adjoint, so it suffices to show that the adjuncts and are equal. Finally, is natural, so it suffices to show that which is exactly our hypothesis.
left-faithful→unit-monic: is-faithful L
→ ∀ {x} → C.is-monic (η x)
{x} f g ηf=ηg =
left-faithful→unit-monic faithful .injective L⊣R (unit.naturall ηf=ηg) faithful $ L-adjunct
Proving that (2 ⇒ 1) is similarly easy. Suppose the unit is monic, and As is monic, it suffices to show that Additionally, is natural, so it suffices to show that which follows directly from our hypothesis.
unit-monic→left-faithful: (∀ {x} → C.is-monic (η x))
→ is-faithful L
{x} {y} {f} {g} Lf=Lg =
unit-monic→left-faithful η-monic .viewr R.⟨ Lf=Lg ⟩ η-monic f g $ unit
Next, let’s show that (3 ⇒ 2). This follows from a very short calculation.
left-reflects-monos→unit-monic: (∀ {x y} {f : C.Hom x y} → D.is-monic (L.₁ f) → C.is-monic f)
→ ∀ {x} → C.is-monic (η x)
{x} =
left-reflects-monos→unit-monic L-reflect λ f g p →
L-reflect .introl zig ⟩
f ≡⟨ D(ε (L.₀ x) D.∘ L.₁ (η x)) D.∘ f ≡⟨ D.extendr p ⟩
(ε (L.₀ x) D.∘ L.₁ (η x)) D.∘ g ≡⟨ D.eliml zig ⟩
g ∎
In general, faithful functors reflect monomorphisms so we get (1 ⇒ 3) for free, finishing the proof.
We also obtain dual results for faithful right adjoints, but we omit the (nearly identical) proofs.
right-faithful→counit-epic: is-faithful R
→ ∀ {x} → D.is-epic (ε x)
counit-epic→right-faithful: (∀ {x} → D.is-epic (ε x))
→ is-faithful R
right-reflects-epis→counit-epic: (∀ {x y} {f : D.Hom x y} → C.is-epic (R.₁ f) → D.is-epic f)
→ ∀ {x} → D.is-epic (ε x)
{x} f g fε=gε =
right-faithful→counit-epic faithful .injective L⊣R $ counit.naturalr fε=gε
faithful $ R-adjunct
{x} {y} {f} {g} Rf=Rg =
counit-epic→right-faithful ε-epic .viewl L.⟨ Rf=Rg ⟩
ε-epic f g $ counit
{x} =
right-reflects-epis→counit-epic R-reflect λ f g p →
R-reflect .intror zag ·· C.extendl p ·· C.elimr zag C
Full adjoints🔗
A left adjoint is full if and only if the unit is a split epimorphism.
For the forward direction, suppose that is full. We can then find a in the fibre of over Moreover, is a section of EG: By the usual adjunct yoga, it suffices to show that
which follows from a short calculation.
left-full→unit-split-epic: is-full L
→ ∀ {x} → C.is-split-epic (η x)
{x} = do
left-full→unit-split-epic full (f , p) ← full (ε (L.₀ x))
.make-section f $
pure $ C.injective L⊣R $
R-adjunct(L.₀ x) D.∘ L.₁ (η x C.∘ f) ≡⟨ L.removel zig ⟩
ε .F₁ f ≡⟨ p ⟩
L(L.₀ x) ≡⟨ D.intror L.F-id ⟩
ε (L.₀ x) D.∘ L.₁ C.id ∎ ε
For the reverse direction, suppose that every component the unit has a section, and let In particular, must have a section Next, note that thee composite is a morphism so all that remains is to check that
Now, is left adjoint, so we can take the adjunct of both sides of this equality, reducing the problem to showing that
Next, is natural, so we can re-arrange our equation like so.
Finally, as is a section.
unit-split-epic→left-full: (∀ {x} → C.is-split-epic (η x))
→ is-full L
{x} {y} f = do
unit-split-epic→left-full η-split-epic {y}
s ← η-split-epic let module s = C.has-section s
let in-im : L.₁ (s.section C.∘ L-adjunct L⊣R f) ≡ f
= L-adjunct.injective L⊣R $
in-im .₁ (L.₁ (s.section C.∘ R.₁ f C.∘ η _)) C.∘ η _ ≡˘⟨ unit.is-natural _ _ _ ⟩
R_ C.∘ s.section C.∘ R.F₁ f C.∘ η _ ≡⟨ C.cancell s.is-section ⟩
η .₁ f C.∘ η _ ∎
R(s.section C.∘ L-adjunct L⊣R f , in-im) pure
Dual results hold for full right adjoints and split monos.
right-full→counit-split-monic: is-full R
→ ∀ {x} → D.is-split-monic (ε x)
counit-split-monic→right-full: (∀ {x} → D.is-split-monic (ε x))
→ is-full R
{x} = do
right-full→counit-split-monic full (f , p) ← full (η (R.₀ x))
.make-retract f $
pure $ D.injective L⊣R $
L-adjunct.₁ (f D.∘ ε x) C.∘ η (R.₀ x) ≡⟨ R.remover zag ⟩
R.F₁ f ≡⟨ p ⟩
R(R.₀ x) ≡⟨ C.introl R.F-id ⟩
η .₁ D.id C.∘ η (R.F₀ x) ∎
R
{x} {y} f = do
counit-split-monic→right-full ε-split-monic {x}
r ← ε-split-monic let module r = D.has-retract r
pure $.∘ r.retract ,
R-adjunct L⊣R f D.injective L⊣R (counit.is-natural _ _ _ ∙ D.cancelr r.is-retract) R-adjunct