Category Axioms are Self-Dual
Until this has been finished, please leave {{refactor}} in the code.
New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.
Contents
Theorem
Morphisms-Only Category Theory
Let $\mathrm{MOCT}$ be the collection of axioms for morphisms-only category theory.
Then:
- $\mathrm{MOCT} = \mathrm{MOCT}^*$
where $\mathrm{MOCT}^*$ consists of the dual statements of those in $\mathrm{MOCT}$.
Object Category Theory
Let $\mathrm{CT}$ be the collection of seven axioms on Characterization of Metacategory via Equations.
Then:
- $\mathrm{CT} = \mathrm{CT}^*$
where $\mathrm{CT}^*$ consists of the dual statements of those in $\mathrm{CT}$.
Proof
Proof for Morphisms-Only Category Theory
To discuss it in more detail, feel free to use the talk page.
When this has been done, {{Finish}} should be removed from the code.
If you would welcome a second opinion as to whether your work is correct, add a call to {{Proofread}} the page.
Proof for Object Category Theory
The seven axioms are:
| \(\displaystyle \operatorname{dom} \operatorname{id}_A = A\) | \(\qquad\) | \(\displaystyle \operatorname{cod} \operatorname{id}_A = A\) | |||||||||||
| \(\displaystyle f \circ 1_{\operatorname{dom} f} = f\) | \(\) | \(\displaystyle 1_{\operatorname{cod} f} \circ f = f\) | |||||||||||
| \(\displaystyle \operatorname{dom} \left({g \circ f}\right) = \operatorname{dom} f\) | \(\) | \(\displaystyle \operatorname{cod} \left({g \circ f}\right) = \operatorname{cod} g\) | |||||||||||
| \(\displaystyle h \circ \left({g \circ f}\right)\) | \(=\) | \(\displaystyle \left({h \circ g}\right) \circ f\) |
Their duals are:
| \(\displaystyle \operatorname{cod} \operatorname{id}_A = A\) | \(\qquad\) | \(\displaystyle \operatorname{dom} \operatorname{id}_A = A\) | |||||||||||
| \(\displaystyle 1_{\operatorname{cod} f} \circ f = f\) | \(\) | \(\displaystyle f \circ 1_{\operatorname{dom} f} = f\) | |||||||||||
| \(\displaystyle \operatorname{cod} \left({f \circ g}\right) = \operatorname{cod} f\) | \(\) | \(\displaystyle \operatorname{dom} \left({f \circ g}\right) = \operatorname{dom} g\) | |||||||||||
| \(\displaystyle \left({f \circ g}\right) \circ h\) | \(=\) | \(\displaystyle f \circ \left({g \circ h}\right)\) |
It is seen that only names of the bound variables $f,g$ and $h$ have been changed at some places.
Therefore, we conclude:
- $\mathrm{CT}^* = \mathrm{CT}$
$\blacksquare$
Sources
- 2010: Steve Awodey: Category Theory (2nd ed.) ... (previous) ... (next): $\S 3.1$
