description/proof of that functor maps isomorphism to isomorphism
Topics
About: category
The table of contents of this article
- Starting Context
- Target Context
- Orientation
- Main Body
- 1: Structured Description
- 2: Natural Language Description
- 3: Proof
Starting Context
- The reader knows a definition of covariant functor.
- The reader knows a definition of contravariant functor.
- The reader knows a definition of %category name% isomorphism.
Target Context
- The reader will have a description and a proof of the proposition that any functor maps any isomorphism to an isomorphism.
Orientation
There is a list of definitions discussed so far in this site.
There is a list of propositions discussed so far in this site.
Main Body
1: Structured Description
Here is the rules of Structured Description.
Entities:
\(C_1\): \(\in \{\text{ the categories }\}\)
\(C_2\): \(\in \{\text{ the categories }\}\)
\(F\): \(\in \{\text{ the functors from } C_1 \text{ to } C_2\}\)
\(O_1\): \(\in Obj (C_1)\)
\(O_2\): \(\in Obj (C_1)\)
\(f\): \(\in Mor (O_1, O_2)\)
//
Statements:
\(f \in \{\text{ the } C_1 \text{ isomorphisms }\}\)
\(\implies\)
\(F (f) \in \{\text{ the } C_2 \text{ isomorphisms }\}\)
//
2: Natural Language Description
For any categories, \(C_1, C_2\), any functor, \(F\), from \(C_1\) to \(C_2\), any objects, \(O_1, O_2 \in Obj (C_1)\), and any morphism, \(f \in Mor (O_1, O_2)\), if \(f\) is a \(C_1\) isomorphism, \(F (f) \in Mor (F (O_1), F (O_2))\) is a \(C_2\) isomorphism.
3: Proof
There is a morphism, \(f^{-1} \in Mor (O_2, O_1)\), such that \(f^{-1} \circ f = id_{O_1} \land f \circ f^{-1} = id_{O_2}\).
Let us suppose that \(F\) is a covariant functor.
By the definition of covariant functor, \(F (f^{-1}) \circ F (f) = F (f^{-1} \circ f) = F (id_{O_1}) = id_{F (O_1)}\); \(F (f) \circ F (f^{-1}) = F (f \circ f^{-1}) = F (id_{O_2}) = id_{F (O_2)}\), which means that \(F (f)\) is a \(C_2\) isomorphism.
Let us suppose that \(F\) is a contravariant functor.
By the definition of contravariant functor, \(F (f) \circ F (f^{-1}) = F (f^{-1} \circ f) = F (id_{O_1}) = id_{F (O_1)}\); \(F (f^{-1}) \circ F (f) = F (f \circ f^{-1}) = F (id_{O_2}) = id_{F (O_2)}\), which means that \(F (f)\) is a \(C_2\) isomorphism.
