Proposition 7.3.2.1.3 (00V2): Properties of the Transitive Closure of a Relation

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

Let $R$ be a relation on $A$.

Adjointness. We have an adjunction
witnessed by a bijection of sets
\[ \mathbf{Rel}^{\mathsf{trans}}\webleft (R^{\mathrm{trans}},S\webright ) \cong \mathbf{Rel}\webleft (R,S\webright ), \]

natural in $R\in \text{Obj}\webleft (\mathbf{Rel}^{\mathsf{trans}}\webleft (A,A\webright )\webright )$ and $S\in \text{Obj}\webleft (\mathbf{Rel}\webleft (A,B\webright )\webright )$.
The Transitive Closure of a Transitive Relation. If $R$ is transitive, then $R^{\mathrm{trans}}=R$.
Idempotency. We have
\[ \webleft (R^{\mathrm{trans}}\webright )^{\mathrm{trans}} = R^{\mathrm{trans}}. \]
Interaction With Inverses. We have
Interaction With Composition. We have

Item 1: Adjointness

This is a rephrasing of the universal property of the transitive closure of a relation, stated in Definition 7.3.2.1.1.

Item 2: The Transitive Closure of a Transitive Relation

Clear.

Item 3: Idempotency

This follows from Item 2.

Item 4: Interaction With Inverses

We have

\begin{align*} \webleft (R^{\dagger }\webright )^{\mathrm{trans}} & = \bigcup _{n=1}^{\infty }\webleft (R^{\dagger }\webright )^{\mathbin {\diamond }n}\\ & = \bigcup _{n=1}^{\infty }\webleft (R^{\mathbin {\diamond }n}\webright )^{\dagger }\\ & = \webleft (\bigcup _{n=1}^{\infty }R^{\mathbin {\diamond }n}\webright )^{\dagger }\\ & = \webleft (R^{\mathrm{trans}}\webright )^{\dagger }, \end{align*}

where we have used, respectively:

Item 5: Interaction With Composition

This follows from Item 2 of Proposition 7.3.1.1.4.