Equivalence of categories
Collection
context | C,D … categories |
definiendum | F in D≃C |
inclusion | F in D⟶C |
exists | G in C⟶D |
exists | α in FG≅IdC |
exists | β in IdD≅GF |
Discussion
Elaboration
Here IdC denotes the identity functor on C.
Motivation
We want to formalize when two categories are “exchangeable in terms of results which can be workout in them”. We would call a functors F “invertible” if there is a another functor G so that G∘F=IdD and F∘G=IdC. However, since one is generally interested in statements involving objects up to isomorphism only, we define a functor to give an “equivalence” by the above definition.
Comparison with homotopy theory: The postulate then looks essentially the same as the one for homotopy equivalent spaces. The natural transformations α,β play the role of homotopy equivalences. Working up to isomorphism amounts to working with just any one representative of a homotopy type.
See also my equivalence of categories.
Reference
Wikipedia: Equivalence of categories