634: Functor Maps Isomorphism to Isomorphism

<The previous article in this series | The table of contents of this series | The next article in this series>

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 }\}$
$⟹$
$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=i{d}_{O_1}\wedge f\circ f^{-1}=i{d}_{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(i{d}_{O_1})=i{d}_{F(O_1)}$; $F(f)\circ F(f^{-1})=F(f\circ f^{-1})=F(i{d}_{O_2})=i{d}_{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(i{d}_{O_1})=i{d}_{F(O_1)}$; $F(f^{-1})\circ F(f)=F(f\circ f^{-1})=F(i{d}_{O_2})=i{d}_{F(O_2)}$, which means that $F(f)$ is a $C_2$ isomorphism.

---

References

<The previous article in this series | The table of contents of this series | The next article in this series>