The button will add this page to my log of things to fix. Use it for broken links, equations not rendering correctly, etc. Submit other issues on GitHub.
Equivalence
Let and be categories.
An equivalence between and consists of Functors:
which we can do as is Full (existence) and Faithfull (uniqueness)
Uniqueness implies functoriality:
given , and have the same image under
so they’re equal.
By construction, is a Natural Isomorphism
Define to be the unique Morphism
whose inverse under is
As we already saw, is an Isomorphism for all ,
and Naturality Squares for are mapped by
to naturality squares for so they commute.
is also equivalent to
the functor sends to
and a matrix to the linear map
which it represents wrt the standard bases
To define , choose a basis for each finite dim space,
and define and matrix representing w.r.t the chosen basis
Now provided we choose the standard bases for the spaces but the chosen basis for yields an isomorphism
and these form a Natural Transformation isomorphism