Natural isomorphism

A natural isomorphism $𝜂 : 𝐹 \Rightarrow 𝐺 : 𝖢 \to 𝖣$ is an isomorphism in a functor category, #m/def/cat thus a natural transformation $𝜂$ for which there exists a $𝜖 : 𝐺 \Rightarrow 𝐹 : 𝖢 \to 𝐷$ such that $𝜖 𝑥 \circ 𝜂 𝑥 = 1 𝐹 𝑥$ and $𝜂 𝑥 \circ 𝜖 𝑥 = 1 𝐺 𝑥$ for all $𝑥 \in 𝖢 0$ . If such an isomorphism exists we write $𝐹 ≃ 𝐺$ .

A useful lemma is that a natural transformation $𝜂 : 𝐹 \Rightarrow 𝐺 : 𝖢 \to 𝖣$ is a natural isomorphism iff $𝜂 𝑥$ is an isomorphism for every $𝑥 \in 𝖢 0$ . 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 $𝑓 \in 𝖢 (𝑥, 𝑦)$ we have $(𝐺 𝑓) 𝜂 𝑥 = 𝜂 𝑦 (𝐹 𝑓)$ . Then $𝜂 - 1 𝑥 (𝐺 𝑓) = (𝐹 𝑓) 𝜂 - 1 𝑦$ , 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