MathLabs
TheoremProved

Functors preserve isomorphisms

Statement

If F:C→DF : \mathcal{C} \to \mathcal{D} is a functor and f:A→Bf : A \to B is an isomorphism in C\mathcal{C} with inverse g:B→Ag : B \to A, then F(f):F(A)→F(B)F(f) : F(A) \to F(B) is an isomorphism in D\mathcal{D}, with inverse F(g)F(g).

Why is it true?

This is what makes functors trustworthy translators: a functor can never accidentally break an equivalence into two genuinely different objects, so classifying objects "up to isomorphism" is a question functors respect.

Proof sketch

Since ff and gg are mutually inverse, g∘f=1Ag \circ f = 1_A and f∘g=1Bf \circ g = 1_B.

Apply FF to the first equation. Functors preserve composition, so F(g∘f)=F(g)∘F(f)F(g \circ f) = F(g) \circ F(f); functors preserve identities, so F(1A)=1F(A)F(1_A) = 1_{F(A)}. Combining these with g∘f=1Ag \circ f = 1_A gives F(g)∘F(f)=1F(A)F(g) \circ F(f) = 1_{F(A)}.

Apply FF to the second equation in the same way: F(f∘g)=F(f)∘F(g)F(f \circ g) = F(f) \circ F(g) and F(1B)=1F(B)F(1_B) = 1_{F(B)}, so from f∘g=1Bf \circ g = 1_B we get F(f)∘F(g)=1F(B)F(f) \circ F(g) = 1_{F(B)}.

The two displayed equations say exactly that F(g)F(g) is a two-sided inverse of F(f)F(f). A morphism with a two-sided inverse is an isomorphism, so F(f):F(A)→F(B)F(f) : F(A) \to F(B) is an isomorphism with inverse F(g)F(g), as claimed.

Topics that use this theorem

Step-by-step proofs

No step-by-step proof yet for this theorem.

References

  1. Saunders Mac Lane (1998). Categories for the Working Mathematician
  2. Emily Riehl (2016). Category Theory in Context
  3. David I. Spivak (2012). Functorial Data Migration · arXiv:1009.1166