open import Cat.Instances.Functor open import Cat.Functor.Adjoint open import Cat.Functor.Base open import Cat.Univalent open import Cat.Prelude import Cat.Functor.Reasoning as Fr import Cat.Reasoning module Cat.Functor.Equivalence where
Equivalencesπ
A functor is an equivalence of categories when it has a right adjoint , with the unit and counit natural transformations being natural isomorphisms. This immediately implies that our adjoint pair extends to an adjoint triple .
record is-equivalence (F : Functor C D) : Type (adj-level C D) where private module C = Cat.Reasoning C module D = Cat.Reasoning D module [C,C] = Cat.Reasoning Cat[ C , C ] module [D,D] = Cat.Reasoning Cat[ D , D ] field Fβ»ΒΉ : Functor D C Fβ£Fβ»ΒΉ : F β£ Fβ»ΒΉ open _β£_ Fβ£Fβ»ΒΉ public field unit-iso : β x β C.is-invertible (unit.Ξ· x) counit-iso : β x β D.is-invertible (counit.Ξ΅ x)
The first thing we note is that having a natural family of invertible morphisms gives isomorphisms in the respective functor categories:
FβFβ»ΒΉβ Id : (F Fβ Fβ»ΒΉ) [D,D].β Id FβFβ»ΒΉβ Id = [D,D].invertibleβiso counit (componentwise-invertibleβinvertible _ counit-iso) Idβ Fβ»ΒΉβF : Id [C,C].β (Fβ»ΒΉ Fβ F) Idβ Fβ»ΒΉβF = [C,C].invertibleβiso unit (componentwise-invertibleβinvertible _ unit-iso) unitβ»ΒΉ = [C,C]._β _.from Idβ Fβ»ΒΉβF counitβ»ΒΉ = [D,D]._β _.from FβFβ»ΒΉβ Id
We chose, for definiteness, the above definition of equivalence of categories, since it provides convenient access to the most useful data: The induced natural isomorphisms, the adjunction unit/counit, and the triangle identities. It is a lot of data to come up with by hand, though, so we provide some alternatives:
Fully faithful, essentially surjectiveπ
Any fully faithful and (split!) essentially surjective functor determines an equivalence of precategories. Recall that βsplit essentially surjectiveβ means we have some determined procedure for picking out an essential fibre over any object : an object together with a specified isomorphism .
module _ {F : Functor C D} (ff : is-fully-faithful F) (eso : is-split-eso F) where import Cat.Reasoning C as C import Cat.Reasoning D as D private module di = D._β _ private ffβ»ΒΉ : β {x y} β D.Hom (F .Fβ x) (F .Fβ y) β C.Hom _ _ ffβ»ΒΉ = equivβinverse ff module ff {x} {y} = Equiv (_ , ff {x} {y})
It remains to show that, when is fully faithful, this assignment of essential fibres extends to a functor . For the object part, we send to the specified preimage. For the morphism part, the splitting gives us isomorphisms and , so that we may form the composite ; Fullness then completes the construction.
ff+split-esoβinverse : Functor D C ff+split-esoβinverse .Fβ x = eso x .fst ff+split-esoβinverse .Fβ {x} {y} f = ffβ»ΒΉ (f*y-iso .D._β _.from D.β f D.β f*x-iso .D._β _.to) where open Ξ£ (eso x) renaming (fst to f*x ; snd to f*x-iso) open Ξ£ (eso y) renaming (fst to f*y ; snd to f*y-iso)
We must then, as usual, prove that this definition preserves identities and distributes over composites, so that we really have a functor. Preservation of identities is immediate; Distribution over composites is by faithfulness.
ff+split-esoβinverse .F-id {x} = ffβ»ΒΉ (f*x-iso .di.from D.β β D.id D.β f*x-iso .di.to β) β‘β¨ ap! (D.idl _) β©β‘ ffβ»ΒΉ (f*x-iso .di.from D.β f*x-iso .di.to) β‘β¨ ap ffβ»ΒΉ (f*x-iso .di.invr) β©β‘ ffβ»ΒΉ D.id β‘Λβ¨ ap ffβ»ΒΉ (F-id F) β©β‘Λ ffβ»ΒΉ (Fβ F C.id) β‘β¨ ff.Ξ· _ β©β‘ C.id β where open Ξ£ (eso x) renaming (fst to f*x ; snd to f*x-iso) ff+split-esoβinverse .F-β {x} {y} {z} f g = fully-faithfulβfaithful {F = F} ff ( Fβ F (ffβ»ΒΉ (ffz D.β (f D.β g) D.β ftx)) β‘β¨ ff.Ξ΅ _ β©β‘ ffz D.β (f D.β g) D.β ftx β‘β¨ cat! D β©β‘ ffz D.β f D.β β D.id β D.β g D.β ftx β‘Λβ¨ apΒ‘ (f*y-iso .di.invl) β©β‘Λ ffz D.β f D.β (fty D.β ffy) D.β g D.β ftx β‘β¨ cat! D β©β‘ (ffz D.β f D.β fty) D.β (ffy D.β g D.β ftx) β‘Λβ¨ apβ D._β_ (ff.Ξ΅ _) (ff.Ξ΅ _) β©β‘Λ Fβ F (ffβ»ΒΉ _) D.β Fβ F (ffβ»ΒΉ _) β‘Λβ¨ F-β F _ _ β©β‘Λ Fβ F (ffβ»ΒΉ _ C.β ffβ»ΒΉ _) β ) where open Ξ£ (eso x) renaming (fst to f*x ; snd to f*x-iso) open Ξ£ (eso y) renaming (fst to f*y ; snd to f*y-iso) open Ξ£ (eso z) renaming (fst to f*z ; snd to f*z-iso) ffz = f*z-iso .di.from ftz = f*z-iso .di.to ffy = f*y-iso .di.from fty = f*y-iso .di.to ffx = f*x-iso .di.from ftx = f*x-iso .di.to
We will, for brevity, refer to the functor weβve just built as
,
rather than its βproper nameβ ff+split-esoβinverse. Hercules now only has
11 labours to go: We must construct unit and counit natural
transformations, prove that they satisfy the triangle identities, and
prove that the unit/counit we define are componentwise invertible. Iβll
keep the proofs of naturality in <details>
tags
since.. theyβre rough.
private G = ff+split-esoβinverse
For the unit, we have an object and weβre asked to provide a morphism β where, recall, the notation represents the chosen essential fibre of over . By fullness, it suffices to provide a morphism ; But recall that the essential fibre comes equipped with an isomorphism .
ff+split-esoβunit : Id => (G Fβ F) ff+split-esoβunit .Ξ· x = ffβ»ΒΉ (f*x-iso .di.from) where open Ξ£ (eso (Fβ F x)) renaming (fst to f*x ; snd to f*x-iso)
Naturality of ff+split-esoβunit.
ff+split-esoβunit .is-natural x y f = fully-faithfulβfaithful {F = F} ff ( Fβ F (ffβ»ΒΉ ffy C.β f) β‘β¨ F-β F _ _ β©β‘ β Fβ F (ffβ»ΒΉ ffy) β D.β Fβ F f β‘β¨ ap! (ff.Ξ΅ _) β©β‘ ffy D.β β Fβ F f β β‘β¨ ap! (sym (D.idr _) β ap (Fβ F f D.β_) (sym (f*x-iso .di.invl))) β©β‘ ffy D.β Fβ F f D.β ftx D.β ffx β‘β¨ cat! D β©β‘ (ffy D.β Fβ F f D.β ftx) D.β ffx β‘Λβ¨ apβ D._β_ (ff.Ξ΅ _) (ff.Ξ΅ _) β©β‘Λ Fβ F (ffβ»ΒΉ (ffy D.β Fβ F f D.β ftx)) D.β Fβ F (ffβ»ΒΉ ffx) β‘Λβ¨ F-β F _ _ β©β‘Λ Fβ F (ffβ»ΒΉ (ffy D.β Fβ F f D.β ftx) C.β ffβ»ΒΉ ffx) β‘β¨β© Fβ F (Fβ (G Fβ F) f C.β xβf*x) β ) where open Ξ£ (eso (Fβ F x)) renaming (fst to f*x ; snd to f*x-iso) open Ξ£ (eso (Fβ F y)) renaming (fst to f*y ; snd to f*y-iso) ffy = f*y-iso .di.from fty = f*y-iso .di.to ffx = f*x-iso .di.from ftx = f*x-iso .di.to xβf*x : C.Hom x f*x xβf*x = ffβ»ΒΉ (f*x-iso .di.from) yβf*y : C.Hom y f*y yβf*y = ffβ»ΒΉ (f*y-iso .di.from)
For the counit, we have to provide a morphism ; We can again pick the given isomorphism.
ff+split-esoβcounit : (F Fβ G) => Id ff+split-esoβcounit .Ξ· x = f*x-iso .di.to where open Ξ£ (eso x) renaming (fst to f*x ; snd to f*x-iso)
Naturality of ff+split-esoβcounit
ff+split-esoβcounit .is-natural x y f = fty D.β β Fβ F (ffβ»ΒΉ (ffy D.β f D.β ftx)) β β‘β¨ ap! (ff.Ξ΅ _) β©β‘ fty D.β ffy D.β f D.β ftx β‘β¨ D.cancell (f*y-iso .di.invl) β©β‘ f D.β ftx β where open Ξ£ (eso x) renaming (fst to f*x ; snd to f*x-iso) open Ξ£ (eso y) renaming (fst to f*y ; snd to f*y-iso) ffy = f*y-iso .di.from fty = f*y-iso .di.to ftx = f*x-iso .di.to
Checking the triangle identities, and that the adjunction unit/counit defined above are natural isomorphisms, is routine. We present the calculations without commentary:
open _β£_ ff+split-esoβFβ£inverse : F β£ G ff+split-esoβFβ£inverse .unit = ff+split-esoβunit ff+split-esoβFβ£inverse .counit = ff+split-esoβcounit ff+split-esoβFβ£inverse .zig {x} = ftx D.β Fβ F (ffβ»ΒΉ ffx) β‘β¨ ap (ftx D.β_) (ff.Ξ΅ _) β©β‘ ftx D.β ffx β‘β¨ f*x-iso .di.invl β©β‘ D.id β
The zag identity needs an appeal to faithfulness:
ff+split-esoβFβ£inverse .zag {x} = fully-faithfulβfaithful {F = F} ff ( Fβ F (ffβ»ΒΉ (ffx D.β ftx D.β fftx) C.β ffβ»ΒΉ fffx) β‘β¨ F-β F _ _ β©β‘ Fβ F (ffβ»ΒΉ (ffx D.β ftx D.β fftx)) D.β Fβ F (ffβ»ΒΉ fffx) β‘β¨ apβ D._β_ (ff.Ξ΅ _) (ff.Ξ΅ _) β©β‘ (ffx D.β ftx D.β fftx) D.β fffx β‘β¨ cat! D β©β‘ (ffx D.β ftx) D.β (fftx D.β fffx) β‘β¨ apβ D._β_ (f*x-iso .di.invr) (f*f*x-iso .di.invl) β©β‘ D.id D.β D.id β‘β¨ D.idl _ β sym (F-id F) β©β‘ Fβ F C.id β )
Now to show they are componentwise invertible:
open is-equivalence ff+split-esoβis-equivalence : is-equivalence F ff+split-esoβis-equivalence .Fβ»ΒΉ = G ff+split-esoβis-equivalence .Fβ£Fβ»ΒΉ = ff+split-esoβFβ£inverse ff+split-esoβis-equivalence .counit-iso x = record { inv = f*x-iso .di.from ; inverses = record { invl = f*x-iso .di.invl ; invr = f*x-iso .di.invr } } where open Ξ£ (eso x) renaming (fst to f*x ; snd to f*x-iso)
Since the unit is defined in terms of fullness, showing it is invertible needs an appeal to faithfulness (two, actually):
ff+split-esoβis-equivalence .unit-iso x = record { inv = ffβ»ΒΉ (f*x-iso .di.to) ; inverses = record { invl = fully-faithfulβfaithful {F = F} ff ( Fβ F (ffβ»ΒΉ ffx C.β ffβ»ΒΉ ftx) β‘β¨ F-β F _ _ β©β‘ Fβ F (ffβ»ΒΉ ffx) D.β Fβ F (ffβ»ΒΉ ftx) β‘β¨ apβ D._β_ (ff.Ξ΅ _) (ff.Ξ΅ _) β©β‘ ffx D.β ftx β‘β¨ f*x-iso .di.invr β©β‘ D.id β‘Λβ¨ F-id F β©β‘Λ Fβ F C.id β) ; invr = fully-faithfulβfaithful {F = F} ff ( Fβ F (ffβ»ΒΉ ftx C.β ffβ»ΒΉ ffx) β‘β¨ F-β F _ _ β©β‘ Fβ F (ffβ»ΒΉ ftx) D.β Fβ F (ffβ»ΒΉ ffx) β‘β¨ apβ D._β_ (ff.Ξ΅ _) (ff.Ξ΅ _) β©β‘ ftx D.β ffx β‘β¨ f*x-iso .di.invl β©β‘ D.id β‘Λβ¨ F-id F β©β‘Λ Fβ F C.id β) } } where open Ξ£ (eso (Fβ F x)) renaming (fst to f*x ; snd to f*x-iso) ffx = f*x-iso .di.from ftx = f*x-iso .di.to
Between categoriesπ
Above, we made an equivalence out of any fully faithful and split essentially surjective functor. In set-theoretic mathematics (and indeed between strict categories), the splitting condition can not be lifted constructively: the statement βevery (ff, eso) functor between strict categories is an equivalenceβ is equivalent to the axiom of choice.
However, between univalent categories, the situation is different: Any essentially surjective functor splits. In particular, any functor between univalent categories has propositional essential fibres, so a βmereβ essential surjection is automatically split. However, note that both the domain and codomain have to be categories for the argument to go through.
module _ (F : Functor C D) (ccat : is-category C) (dcat : is-category D) (ff : is-fully-faithful F) where private module C = Cat.Reasoning C module D = Cat.Reasoning D
So, suppose we have categories and , together with a fully faithful functor . For any , weβre given an inhabitant of , which we want to βget outβ from under the truncation. For this, weβll show that the type being truncated is a proposition, so that we may βuntruncateβ it.
Essential-fibre-between-cats-is-prop : β y β is-prop (Essential-fibre F y) Essential-fibre-between-cats-is-prop z (x , i) (y , j) = they're-equal where
For this magic trick, assume weβre given a , together with objects and isomorphisms and . We must show that , and that over this path, . Since is fully faithful, we can find an isomorphism in , which sends back to .
Fxβ Fy : Fβ F x D.β Fβ F y Fxβ Fy = i D.βIso (j D.Isoβ»ΒΉ) xβ y : x C.β y xβ y = is-ffβessentially-injective {F = F} ff Fxβ Fy
Furthermore, since weβre working with categories, these isomorphisms restrict to paths and . Weβre half-done: weβve shown that some exists, and it remains to show that over this path we have . More specifically, we must give a path laying over .
xβ‘y : x β‘ y xβ‘y = ccat .to-path xβ y Fxβ‘Fy : Fβ F x β‘ Fβ F y Fxβ‘Fy = dcat .to-path Fxβ Fy
Rather than showing it over
directly, weβll show it over the path
we constructed independently. This is because we can use the helper
Hom-pathp-reflr-iso
to establish
the result with far less computation:
overβ² : PathP (Ξ» i β Fxβ‘Fy i D.β z) i j overβ² = D.β -pathp Fxβ‘Fy refl (Univalent.Hom-pathp-refll-iso dcat (D.cancell (i .D._β _.invl)))
We must then connect with this path . But since we originally got by full faithfulness of , they are indeed the same path:
abstract square : ap (Fβ F) xβ‘y β‘ Fxβ‘Fy square = ap (Fβ F) xβ‘y β‘β¨ F-map-path F xβ y ccat dcat β©β‘ dcat .to-path β F-map-iso F xβ y β β‘β¨ ap! (equivβcounit (is-ffβF-map-iso-is-equiv {F = F} ff) _) β©β‘ dcat .to-path Fxβ Fy β over : PathP (Ξ» i β Fβ F (xβ‘y i) D.β z) i j over = transport (Ξ» l β PathP (Ξ» m β square (~ l) m D.β z) i j) overβ²
Hence β blink and youβll miss it β the essential fibres of over any are propositions, so it suffices for them to be merely inhabited for the functor to be split eso. With tongue firmly in cheek we call this result the theorem of choice.
they're-equal = Ξ£-pathp xβ‘y over Theorem-of-choice : is-eso F β is-split-eso F Theorem-of-choice eso y = β₯-β₯-elim (Ξ» _ β Essential-fibre-between-cats-is-prop y) (Ξ» x β x) (eso y)
This theorem implies that any fully faithful, βmerelyβ essentially surjective functor between categories is an equivalence:
ff+esoβis-equivalence : is-eso F β is-equivalence F ff+esoβis-equivalence eso = ff+split-esoβis-equivalence ff (Theorem-of-choice eso)
Isomorphismsπ
Another, more direct way of proving that a functor is an equivalence of precategories is proving that it is an isomorphism of precategories: Itβs fully faithful, thus a typal equivalence of morphisms, and in addition its action on objects is an equivalence of types.
record is-precat-iso (F : Functor C D) : Type (adj-level C D) where no-eta-equality constructor iso field has-is-ff : is-fully-faithful F has-is-iso : is-equiv (Fβ F)
Such a functor is (immediately) fully faithful, and the inverse has-is-iso means that it is split essentially surjective; For given , the inverse of gives us an object ; We must then provide an isomorphism , but those are identical, hence isomorphic.
module _ {F : Functor C D} (p : is-precat-iso F) where open is-precat-iso p is-precat-isoβis-split-eso : is-split-eso F is-precat-isoβis-split-eso ob = equivβinverse has-is-iso ob , isom where isom = pathβiso {C = D} (equivβcounit has-is-iso _)
Thus, by the theorem above, is an adjoint equivalence of precategories.
is-precat-isoβis-equivalence : is-equivalence F is-precat-isoβis-equivalence = ff+split-esoβis-equivalence has-is-ff is-precat-isoβis-split-eso