We want to understand internal right Kan lifts in $\boldsymbol {\mathsf{Rel}}$, which look like this:
that is right adjoint to the postcomposition by $R$ functor
Let $A$, $B$, and $X$ be sets and let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ and $F\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be relations.
We want to understand internal right Kan lifts in $\boldsymbol {\mathsf{Rel}}$, which look like this:
that is right adjoint to the postcomposition by $R$ functor
The internal right Kan lift of $F$ along $R$ is the relation $\operatorname {\mathrm{Rift}}_{R}(F)$ described as follows:
Viewing relations from $X$ to $A$ as subsets of $X\times A$, we have
Viewing relations as functions $X\times A\to \{ \mathsf{true},\mathsf{false}\} $, we have
where the meet $\bigwedge $ is taken in the poset $(\{ \mathsf{true},\mathsf{false}\} ,\preceq )$ of Chapter 3: Sets, Definition 3.2.2.1.3.
Viewing relations as functions $X\to \mathcal{P}(A)$, we have
for each $a\in A$.
We have
is right adjoint to the postcomposition functor $R\mathbin {\diamond }-$, being thus the right Kan lift along $R$. Here we have used the following results, respectively (i.e. for each $\cong $ sign):
This finishes the proof.
Here are some examples of internal right Kan lifts of relations.
Pullbacks. Let $p\colon A\to B$ and $f\colon X\to B$ be functions. We have
Thus, as a subset of $X\times A$, the right Kan lift $\operatorname {\mathrm{Rift}}_{\operatorname {\mathrm{Gr}}(p)}(\operatorname {\mathrm{Gr}}(f))$ corresponds precisely to the pullback $X\times _{B}A$ of $X$ and $A$ along $p$ and $f$ of Chapter 4: Constructions With Sets, Section 4.1.4.
Let $A$, $B$, $C$ and $X$ be sets and let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$, $S\colon B\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}C$, and $F\colon X\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be relations.
Functoriality. The assignments $R,F,(R,F)\mapsto \operatorname {\mathrm{Rift}}_{R}(F)$ define functors
In other words, given relations
Interaction With Composition. We have
and an equality
Interaction With Converses. We have
Interaction With Inverse Images. We have
for each $U\in \mathcal{P}(A)$, so we have
for each $a\in A$.
for each $x\in X$, so we therefore have $\operatorname {\mathrm{Rift}}_{R_{2}}(F_{1})\subset \operatorname {\mathrm{Rift}}_{R_{1}}(F_{2})$.
We have $x\in \operatorname {\mathrm{Rift}}_{R}(F)^{\dagger }(a)$ iff $a\in \operatorname {\mathrm{Rift}}_{R}(F)(x)$.
This holds iff $R(a)\subset F(x)$.
This holds iff, for each $b\in R(a)$, we have $b\in F(x)$.
This holds iff, for each $b\in R(a)$, we have $x\in F^{-1}(b)$.
This holds iff $x\in \bigcap _{b\in R(a)}F^{-1}(b)$.
This finishes the proof.