Work in progress!
To be expanded.
$\newcommand\inclusion{{\text{inclusion}}}$
First, we give a categorical definition for $\rightadj{ \text{the floor, the right adjoint}}$ to $\leftadj{ \text{the inclusion} }$ of $\leftcat\Z$ in $\rightcat\R$.
(The above 2-categorical diagram in $\Cat$) should be compared to
the definition of floor in Graham, Knuth, and Patashnik's <i>Concrete Mathematicics</i> (3.1):
⌊x⌋ = the greatest integer less than or equal to x
Note how (the 2-categorical diagram in $\Cat$) makes explicit
( many entities and relations (arrows) )
which are implicit in (the GKP definition),
e.g.,
( (the set of objects of) $\rightcat{ ( \leftadj{ (\inclusion = L) } {} \downarrow x ) }$ )
is
(the collection of $\leftcat{\text{integers}} \rightcat{\text{ less than or equal to } x}$.
<hr />
The following section on terminal objects will be replaced by a reference to a stand-alone, dedicated post in that subject, expanding on what is below.
<hr />
<h3> What is a greatest element?</h3>
Here we drop back to recall and emphasize a key basic result in category theory:
Some alternative characterizations of (the "terminal object" ${\rightadj\top}_\calC$) in (an arbitrary category $\calC$).
The key result can be described as this:
\[ \boxed{ \displaystyle {\rightcat 0}_\calC \rightadj\limit \cong \top_\calC \cong {\leftcat 1}_\calC \leftadj\colimit } \; .\]
This references two functors into $\calC$, the least, ${\rightcat 0}_\calC$, and the greatest, ${\leftcat 1}_\calC$
( this situation should be compared to (the power set $XP$) of (an arbitrary set $X$), which has two extremal elements, (the empty, least, subset $\emptyset$), and (the greatest subset, $X$ itself) ):
\[ \begin{array} {} &&&&& \kern16em & \rightcat{ \hom {{{\leftadj !}_{\rightcat 0}}\leftcat c} {[0,\black\calC]} {0_\calC} } & \cong & 1 \\ \rightcat 0 & \rightcat{ \xrightarrow[\kern8em]{\textstyle 0_\calC \text{ empty functor}} } & \calC && && \llap{ \text{defn. } \rightadj( {\rightcat 0}_\calC \rightadj\limit \rightadj) \; } {\wr\Vert} && {\wr\Vert} \rlap{ \text{ defn. } {\top_\calC} } \\ \llap{ {\leftadj !}_{\rightcat 0} } \leftadj{\Bigg\downarrow} & \rightadj{ \llap\epsilon \Bigg\Uparrow \rlap{ { \textstyle \text{empty} \atop \textstyle \text{cone} } } } & \Bigg\Vert &&&& \hom {\leftcat c} {\leftcat\calC} { \rightadj( {\rightcat 0}_\calC \rightadj\limit \rightadj) } && \hom {\leftcat c} {\leftcat\calC} {\top_\calC} \\ 1 & \xrightarrow[\smash{\raise2.4ex{\displaystyle \top_\calC}}]{\kern8em} & \calC \\ \rightadj{ \llap{ !_{\leftcat\calC} } \Bigg\uparrow } & \leftadj{ \llap\eta \Bigg\Uparrow \rlap ! } & \Bigg\Vert & &&& \rightcat{ \hom { \leftadj ( \leftcat{1_\calC} \leftadj\colimit \leftadj ) } \calC c } \\ \leftcat\calC & \leftcat{ \xrightarrow[\textstyle 1_\calC \text{ identity functor}]{} } & \calC && && \llap{ \text{defn. } \leftadj( \leftcat{1_\calC} \leftadj\colimit \leftadj) \; } {\wr\Vert} \\ &&&&& & \leftcat{ \hom {1_\calC} {[\calC,\black\calC]} {{{\rightadj !}_\calC}\rightcat c} } \\ \end{array} \]
The isomorphism involving $\rightadj\limit$ is proved by the bijections at top right above.
The isomorphism involving $\leftadj\colimit$ is proved in the diagrams below;
the two on the left show that
(a terminal, denoted $\rightadj{\top[\leftadj !]}$) is (a colimit of the identity endofunctor $\leftcat{1_\calC}$),
while the two on the right show that
(a colimit, denoted $\leftadj{c_\infty[\iota]}$, of the identity endofunctor $\leftcat{1_\calC}$) is (a terminal in $\calC$).
\[ \boxed{ \begin{array} {ccccccccc|cccc} & {} \rlap{ \kern0em \rightadj{ \top[\leftadj !] } \text{ is initial in } ({\leftcat{1_\calC}} \downarrow \Delta), \text{ thus is } \leftadj{ (\leftcat{1_\calC} \colimit) [\iota] } } &&&& &&& && {} \rlap{ \kern2em \leftadj{ ( c_\infty = \leftcat{1_\calC} \colimit) [\iota] } \text{ is } \rightadj{ \top [\leftadj !] } } &&& \\ \\ \hline \kern5em & \rightadj\top & \leftcat{ \xrightarrow[\kern3em]{ \textstyle \lambda_{\rightadj\top} } } & \rightcat d & \kern8em & \rightadj\top & \leftcat{ \xrightarrow[\kern3em]{ \textstyle \rightcat f } } & \rightcat d & \kern2em & \kern4em & \leftadj{c_\infty} & \leftadj{ \xrightarrow[\kern3em]{ \textstyle \iota_{c_\infty} } } & \leftadj{c_\infty} & \kern2em & \kern2em & \leftadj{c_\infty} & \leftadj{ \xrightarrow[\kern3em]{ \textstyle \iota_{c_\infty} = 1_{c_\infty} } } & \leftadj{c_\infty} \\ & \leftadj{ \llap{ !_{\leftcat c} } \Big\uparrow } \rlap{ \kern.5em \leftcat\lambda_{ \leftadj!_{\leftcat c} } } & \leftcat{ \nearrow \rlap{\lambda_c} } &&& \leftadj{ \llap{ \rightadj{ {\leftadj !}_\top = 1_\top } } \Big\uparrow } \rlap{ \kern.5em \rightcat f } & \leftcat{ \nearrow \rlap{{\leftcat\lambda}_{\rightadj\top}} } & & && \leftadj{ \llap{ \iota_{\leftcat c} } \Big\uparrow \rlap{ \kern.5em \iota_{\iota_{\leftcat c}} } } & \leftadj{ \nearrow \rlap{ \iota_{\leftcat c} } } &&&& \leftcat{ \llap{ \forall f } \Big\uparrow \rlap{ \kern.5em {\leftadj\iota}_f } } & \leftadj{ \nearrow \rlap{ \iota_{\leftcat c} } } \\ & \leftcat c &&& & \rightadj\top &&& && \leftcat{ \llap\forall c } &&& && \leftcat c \\ \hline {} \rlap{ \kern-3em { { \textstyle \text{if } {\leftcat\lambda} : \leftcat{1_\calC \Rightarrow {\rightcat d}{\black\Delta} \text{ ($\lambda$ is a cocone from $\leftcat{1_\calC}$ to $\rightcat d$)} \, , } \atop \textstyle \text{then, in particular, $\leftcat{\forall c}$ the above ${\leftcat\lambda}_{ {\leftadj !}_{\leftcat c} }$ commutes,} } \atop \textstyle \text{i.e. $\leftcat\lambda$ factors through $\leftadj !$ by ${\leftcat\lambda}_{\rightadj\top}$} } } &&&& {} \rlap{ \kern4em { { \textstyle \text{if } \rightcat{ f : {\rightadj\top}[{\leftadj !}] \to {\rightcat d}[{\leftcat\lambda}] } \atop \textstyle \text{the above commutes;} } \atop \textstyle \text{hence $\rightcat f = {\leftcat\lambda}_{\rightadj\top}$ } } } &&&&& {} \rlap{ \kern-2em { { \textstyle \text{because $\leftadj\iota$ is a cocone, $\leftadj{ \iota : \leftcat{1_\calC} \Rightarrow c_\infty {\black\Delta} }$, } \atop \textstyle \text{$\leftcat{\forall c}$ the above $\leftadj{\iota_{ \iota_{\leftcat c}}}$ commutes;} } \atop \textstyle \text{hence, by the colimit property, $\leftadj{ \iota_{c_\infty} = 1_{c_\infty} }$} } } &&&&& {} \rlap{ \kern0em { { \textstyle \text{because $\leftadj\iota$ is a cocone,} \atop \textstyle \text{$\leftcat{\forall f}$ the above ${\leftadj\iota}_f$ commutes;} } \atop \textstyle \text{hence $\leftcat{\forall f}$ $\leftcat{ f = {\leftadj\iota}_c }$} } } \\ \end{array} } \]
In words:
To show $\rightadj{\top[{\leftadj !}]}$ is initial in the comma category $({\leftcat{1_\calC}} \downarrow \Delta)$,
let $\leftcat{ (\lambda : {1_\calC} \Rightarrow {\rightcat d} ) }$ be an arbitrary cocone over $\leftcat{1_\calC}$.
Since $\leftcat\lambda$ is a cocone, the triangle at left commutes.
Thus $\leftcat\lambda$ factors through $\leftadj !$ by ${\leftcat\lambda}_{\rightadj\top}$.
Further, recall $\rightadj{ {\leftadj !}_\top = 1_\top }$ by uniqueness in $\hom {\rightadj\top} \calC {\rightadj\top}$.
Thus if $\rightcat{ f : {\rightadj\top}[{\leftadj !}] \to {\rightcat d}[{\leftcat\lambda}] }$, taking $\leftcat{ c = {\rightadj\top} }$ yields $\rightcat{ f = {{\leftcat\lambda}_{\rightadj\top}} }$.
That proves the left assertion in the box above.
<hr />
\[ \boxed{ \begin{array} {} & \leftcat{ ( x \downarrow \rightadj{ (\inclusion = R) } ) } && \rightcat{ {} \rlap{ \kern-3em \xrightarrow [\kern8em] {\textstyle j = r} } } && \rightcat{ \Z =\calR } \\ \text{2-categorical diagram in $\Cat$ for } \leftadj{\text{ceiling} \left\lceil \leftcat x \right\rceil} & & \leftcat{ \llap ! \searrow } & \smash{ \raise.5ex{ \rightadj{ \llap \rho \Bigg\Uparrow } } } & \rightadj{ \nearrow \rlap{ \kern-2em \scriptstyle { {\rightcat r} \limit \atop {} = \leftadj{\left\lceil {\leftcat x} \right\rceil} } } } & \smash{ \leftadj{\Bigg\Uparrow} \rlap{ \leftcat x \leftadj\eta } } {} \rlap{ \kern-3em \leftcat{ \smash{ \raise0ex{\Bigg\Uparrow} } \rlap\lambda } } & \rightadj{ \searrow \rlap {\inclusion = R} } \\ & && \leftcat 1 && \leftcat{ {} \rlap{ \kern-4em \xrightarrow[\textstyle x] {\kern11em} } } && \leftcat{ \R = (\calR \text{ for } \rightadj{\text{floor} = \left\lfloor \rightcat x \right\rfloor} ) } = \leftcat{ (\calL \text{ for } \leftadj{\text{ceiling} = \left\lceil \leftcat x \right\rceil} ) } \\ \end{array} } \]
No comments:
Post a Comment