inverse in nLab

Proof

Let gg be a left inverse, hence such that g∘f=idg \circ f \,=\, id. Write f −1f^{-1} for the actual inverse, hence such that f −1∘f=idf^{-1} \circ f \,=\, id and f∘f −1=idf \circ f^{-1} \,=\, id.
Then the following sequence of equalities implies that g=f −1g = f^{-1}:

g =g∘id =g∘(f∘f −1) =(g∘f)∘f −1 =id∘f −1 =f −1. \begin{aligned} g & \;=\; g \circ id \\ & \;=\; g \circ ( f \circ f^{-1} ) \\ & \;=\; (g \circ f) \circ f^{-1} \\ & \;=\; id \circ f^{-1} \\ & \;=\; f^{-1} \,. \end{aligned}

Here all steps use just the definitions of the various morphisms, except the third step, which uses associativity of composition in any category.

An analogous argument applies to right inverses; and either argument applies to actual inverses.

Proposition

Let ff be an isomorphism (Def. ). Then the inverse morphism (f −1) −1\left(f^{-1}\right)^{-1} of an inverse morphism f −1f^{-1} (Def. ) exists and is equal to the original morphism:

(f −1) −1=f. \left(f^{-1}\right)^{-1} \;=\; f \,.

Proof

By the uniqueness of inverses (Prop. ) for f −1f^{-1}.