Metacategory Induces Morphisms-Only Metacategory

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $\mathbf C$ be a metacategory.


Then the collection of morphisms $\mathbf C_1$ of $\mathbf C$ is a morphisms-only metacategory.


Proof

In order to check that $\mathbf C_1$ is a morphisms-only metacategory, we need to interpret the symbols $\operatorname{dom}$, $\operatorname{cod}$ and $R_\circ$.

Set $\operatorname{dom} x := \operatorname{id}_{\operatorname{dom} x}$, and $\operatorname{cod} x := \operatorname{id}_{\operatorname{cod} x}$ with the symbols on the right as defined in $\mathbf C$.

Further, put $R_\circ \left({x, y, z}\right) \iff x \circ y = z$.


Now we can proceed to verify the axioms for a morphisms-only metacategory.

For $(MOCT0)$, i.e. (omitting universal quantifiers):

$\left({R_\circ \left({x, y, z}\right) \land R_\circ \left({x, y, z'}\right)}\right) \implies z = z'$

we conclude that the antecedent holds iff $z = x \circ y = z'$, hence $(MOCT0)$ holds.

$\Box$


The content of $(MOCT1)$ is:

$\operatorname{dom} x = \operatorname{cod} y \iff \exists z: R_\circ \left({x, y, z}\right)$

This is precisely saying that a composite morphism $x \circ y$ is defined iff $x$ and $y$ are composable morphisms.

$\Box$


Axiom $(MOCT2)$ is the statement:

$R_\circ \left({x, y, z}\right) \implies \left({\operatorname{dom} z = \operatorname{dom} y \land \operatorname{cod} z = \operatorname{cod} x}\right)$

which prescribes the domain and codomain of $x \circ y$.

That this is satisfied by $\mathbf C_1$ follows directly from axiom $(C1)$ for metacategories.

$\Box$


Axiom $(MOCT3)$ is:

$R_\circ \left({x, y, a}\right) \land R_\circ \left({y, z, b}\right) \implies \left({\exists w: R_\circ \left({x, b, w}\right) \land R_\circ \left({a, z, w}\right)}\right)$

which expresses that $\circ$ is an associative operation, exactly as axiom $(C3)$ for metacategories specifies.

$\Box$


Finally, axiom $(MOCT4)$ is the statement:

$R_\circ \left({x, \operatorname{dom} x, x}\right) \land R_\circ \left({\operatorname{cod} x, x, x}\right)$

which will hold iff $x \circ \operatorname{id}_{\operatorname{dom} x} = x$ and $\operatorname{id}_{\operatorname{cod} x} \circ x = x$.

This is the content of axiom $(C2)$ for metacategories.

$\Box$


Having verified the axioms, we conclude $\mathbf C_1$ to be a morphisms-only metacategory.

$\blacksquare$


Also see