Natural isomorphism

A natural isomorphism is an isomorphism in a functor category, #m/def/cat thus a natural transformation for which there exists a such that and for all . If such an isomorphism exists we write .

A useful lemma is that a natural transformation is a natural isomorphism iff is an isomorphism for every . That is, the inverse of a natural family of morphisms is automatically natural. #m/thm/cat

Proof

Suppose is a natural family of isomorphisms, i.e. for any we have . Then , so the inverse is also natural.

The idea was first proposed in A general theory of natural equivalences, which is also the originating paper of category theory. See Equivalence of categories

#state/tidy | #lang/en | #SemBr