653 lines
50 KiB
Plaintext
653 lines
50 KiB
Plaintext
% !TeX spellcheck = <none>
|
|
\documentclass[12pt,a4paper,italian]{book}
|
|
\usepackage{graphicx} % Required for inserting images
|
|
|
|
|
|
\usepackage{amssymb} %to augment generic LaTeX; needed for \mathbb font
|
|
\usepackage{amsfonts} %reading in some AMS fonts
|
|
\usepackage{amsthm}
|
|
\usepackage{amsmath} %needed for \begin{align}... \end{align} environment
|
|
\usepackage{amsxtra}
|
|
|
|
|
|
\usepackage{tikz}
|
|
\usepackage{tikz-cd}
|
|
\usepackage{quiver}
|
|
|
|
\theoremstyle{definition}
|
|
\newtheorem{definition}{Definition}[section]
|
|
\newtheorem{proposition}[definition]{Proposition}
|
|
\newtheorem{theorem}[definition]{Theorem}
|
|
\newtheorem{lemma}[definition]{Lemma}
|
|
\newtheorem{corollary}[definition]{Corollary}
|
|
\newtheorem*{idea}{Idea}
|
|
\theoremstyle{remark}
|
|
\newtheorem{remark}[definition]{Remark}
|
|
\title{Tesi}
|
|
\author{saladinoflavio }
|
|
\date{March 2026}
|
|
|
|
|
|
\usepackage{biblatex}
|
|
\bibliography{Bibliografia.bib}
|
|
|
|
\begin{document}
|
|
|
|
\maketitle
|
|
|
|
|
|
\section{Introduction}
|
|
|
|
\section{Freyd cover of a category}
|
|
\begin{definition}[Comma Category]
|
|
Let $\mathcal{A,B,C}$ locally small categories and let $F: \mathcal{A} \to \mathcal{C}, G: \mathcal{B} \to \mathcal{C}$ two functors
|
|
% https://q.uiver.app/#q=WzAsMyxbMCwwLCJcXG1hdGhjYWx7QX0iXSxbMiwwLCJcXG1hdGhjYWx7Q30iXSxbNCwwLCJcXG1hdGhjYWx7Qn0iXSxbMCwxXSxbMiwxXV0=
|
|
\[\begin{tikzcd}
|
|
{\mathcal{A}} && {\mathcal{C}} && {\mathcal{B}}
|
|
\arrow[from=1-1, to=1-3]
|
|
\arrow[from=1-5, to=1-3]
|
|
\end{tikzcd}\]
|
|
Then we call comma category of F and G \footnote{the name "comma category" arises from the notation (F,G) used by Lawvere}, $(F \downarrow G)$, the category with:
|
|
\begin{itemize}
|
|
\item{Objects}: an object is a triple $(A,B,f)$ where $f: F(A) \to F(B)$ is a $\mathcal{C}$-morhpism
|
|
\item{Arrows}: a morphism from $(A,B,f)$ to $(A',B',f')$ is a pair $(h,k)$ of an $\mathcal{A}$-morphism $h: A \to A'$ and a $\mathcal{B}$-morphism $k: B \to B'$ such that the following diagram is commutative :
|
|
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJGKEEpIl0sWzIsMCwiRyhCKSJdLFswLDIsIkYoQScpIl0sWzIsMiwiRyhCJykiXSxbMCwxLCJmIl0sWzIsMywiZiciLDJdLFsxLDMsIkcoaykiXSxbMCwyLCJGKGgpIiwyXV0=
|
|
\[\begin{tikzcd}
|
|
{F(A)} && {G(B)} \\
|
|
\\
|
|
{F(A')} && {G(B')}
|
|
\arrow["f", from=1-1, to=1-3]
|
|
\arrow["{F(h)}"', from=1-1, to=3-1]
|
|
\arrow["{G(k)}", from=1-3, to=3-3]
|
|
\arrow["{f'}"', from=3-1, to=3-3]
|
|
\end{tikzcd}\]
|
|
\end{itemize}
|
|
\end{definition}
|
|
\begin{remark}
|
|
Notice that there are two canonical forgetful functors defined over the comma category:
|
|
\begin{itemize}
|
|
\item a functor $\Pi_1 : (F \downarrow G) \to \mathcal{A}$ that forget the comma structure preserving the "$\mathcal{A}$-structure" defined as:
|
|
% https://q.uiver.app/#q=WzAsNixbMCwxLCIoQSxCLGYpIl0sWzAsMywiKEEnLEInLGYnKSJdLFsyLDEsIkEiXSxbMiwzLCJBJyJdLFswLDAsIihGXFxkb3duYXJyb3cgRykiXSxbMiwwLCJcXG1hdGhjYWx7QX0iXSxbMCwxLCIoaCxrKSIsMl0sWzIsMywiaCJdLFs0LDVdLFs2LDcsIiIsMix7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sImxldmVsIjoxLCJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtYXBzIHRvIn19fV1d
|
|
\[\begin{tikzcd}
|
|
{(F\downarrow G)} && {\mathcal{A}} \\
|
|
{(A,B,f)} && A \\
|
|
\\
|
|
{(A',B',f')} && {A'}
|
|
\arrow["{\Pi_1}", from=1-1, to=1-3]
|
|
\arrow[""{name=0, anchor=center, inner sep=0}, "{(h,k)}"', from=2-1, to=4-1]
|
|
\arrow[""{name=1, anchor=center, inner sep=0}, "h", from=2-3, to=4-3]
|
|
\arrow[between={0.2}{0.8}, maps to, from=0, to=1]
|
|
\end{tikzcd}\]
|
|
\item a functor $\Pi_2 : (F \downarrow G) \to \mathcal{B}$ (preserving the "$\mathcal{B}$-structure") defined as:
|
|
% https://q.uiver.app/#q=WzAsNixbMCwxLCIoQSxCLGYpIl0sWzAsMywiKEEnLEInLGYnKSJdLFsyLDEsIkIiXSxbMiwzLCJCJyJdLFswLDAsIihGXFxkb3duYXJyb3cgRykiXSxbMiwwLCJcXG1hdGhjYWx7Qn0iXSxbMCwxLCIoaCxrKSIsMl0sWzIsMywiayJdLFs0LDUsIlxcUGlfMiJdLFs2LDcsIiIsMix7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sImxldmVsIjoxLCJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtYXBzIHRvIn19fV1d
|
|
\[\begin{tikzcd}
|
|
{(F\downarrow G)} && {\mathcal{B}} \\
|
|
{(A,B,f)} && B \\
|
|
\\
|
|
{(A',B',f')} && {B'}
|
|
\arrow["{\Pi_2}", from=1-1, to=1-3]
|
|
\arrow[""{name=0, anchor=center, inner sep=0}, "{(h,k)}"', from=2-1, to=4-1]
|
|
\arrow[""{name=1, anchor=center, inner sep=0}, "k", from=2-3, to=4-3]
|
|
\arrow[between={0.2}{0.8}, maps to, from=0, to=1]
|
|
\end{tikzcd}\]
|
|
\end{itemize}
|
|
|
|
\end{remark}
|
|
|
|
|
|
\begin{theorem}\label{completenesscomma}
|
|
Let $\mathcal{A}$ and $\mathcal{B}$ be two finitely cocomplete categories and let $F:\mathcal{A} \to \mathcal{C}$, $\mathcal{B} \to \mathcal{C}$ two functors. If $F$ is a cocontinous functor - i.e. preserves small colimits - then the comma category $(F\downarrow G)$ is finitely cocomplete; morover the forgetful functors are cocontinous. \\
|
|
Analogously if $\mathcal{A}$ and $\mathcal{B}$ are finitely complete categories and $G: \mathcal{A} \to \mathcal{C}$ is continous - i.e. preserves small limits - then $(F \downarrow G)$ is finitely complete and both forgetfoul functors are continous.
|
|
|
|
\end{theorem}
|
|
\begin{proof}
|
|
Let's begin by proving the cocomplete case. We will start from cocompleteness of the category and then we will move on to che cocontinuity of the forgetful functors. Recall that a a category is finitely cocomplete if and only if it admits initial object and pushouts; we will construct explicitely both objects: \\
|
|
\textbf{Initial Object}: We will construct the initial object of $(F, \downarrow G)$ by using the cocompletens of $\mathcal{A}$ and $\mathcal{B}$: indeed, let $0_\mathcal{A}$ be the initial object of $\mathcal{A}$ and $0_\mathcal{B}$ the initial object of $\mathcal{B}$. Now, since $F$ is a cocontinous functor $F(0_\mathcal{A}) = 0_\mathcal{C}$ where $0_\mathcal{C}$ is
|
|
in $\mathcal{C}$; thus there is a unique morphism $in: F(0_\mathcal{A})=0_\mathcal{C} \to G(0_\mathcal{B})$ in $\mathcal{C}$. Now, we claim $(0_\mathcal{A},0_\mathcal{B},in)$ to be initial in $(F\downarrow G)$:
|
|
\begin{itemize}
|
|
\item existence: let $(A,B,f)$ be an object of $(F\downarrow G)$; then there exists two unique morphisms $in_A, in_B$ respectively in $\mathcal{A}$ and $\mathcal{B}$ such that $in_A: 0_\mathcal{A} \to A $ and $in_B: 0_\mathcal{B} \to B$. Thus we have a candidate morphism $(in_A, in_B)$. In order to check that this morphism is a morphism of $(F \downarrow G)$ we need to show that the following diagram is commutative:
|
|
|
|
% https://q.uiver.app/#q=WzAsNCxbMCwwLCIwX1xcbWF0aGNhbHtDfSJdLFsyLDAsIkcwX1xcbWF0aGNhbHtCfSJdLFswLDIsIkZBIl0sWzIsMiwiR0IiXSxbMCwxLCJpbiIsMl0sWzAsMiwiRmluX0EiXSxbMiwzLCJmIl0sWzEsMywiR2luX0IiLDJdXQ==
|
|
\[\begin{tikzcd}
|
|
{F(0_\mathcal{A})=0_\mathcal{C}} && {G0_\mathcal{B}} \\
|
|
\\
|
|
FA && GB
|
|
\arrow["in"', from=1-1, to=1-3]
|
|
\arrow["{Fin_A}", from=1-1, to=3-1]
|
|
\arrow["{Gin_B}"', from=1-3, to=3-3]
|
|
\arrow["f", from=3-1, to=3-3]
|
|
\end{tikzcd}\]
|
|
The diagram above is trivially commutative: since $0_\mathcal{C}$ is intial in $\mathcal{C}$ both $f\circ Fin_A: 0_\mathcal{C} \to GB$ and $Gin_B \circ in: 0_\mathcal{C} \to GB$ must be equal to $in_{GB}: 0_\mathcal{C} \to GB$. Thus $$(0_\mathcal{A}, 0_\mathcal{B}, in) \xrightarrow{(in_A, in_B)} (A,B,f)$$ is a morphism in $(F \downarrow G)$
|
|
\item uniqueness: let $(0_\mathcal{A}, 0_\mathcal{B}, in) \xrightarrow[(h,k)]{(in_A, in_B)} (A,B,f)$ two arrows in $(F \downarrow G)$; then since $0_\mathcal{A}, 0_\mathcal{B}$ are initial, then $h = in_A$ and $k = in_B$; hence $(h,k)= (in_A,in_B)$ and so $(in_A,in_B)$ is unique
|
|
\end{itemize}
|
|
Thus $(F \downarrow G)$ admits initial object \\
|
|
\textbf{Pushouts}: As for the case above let construct the pushouts in $(F \downarrow G)$ by using pushout provided by cocompleteness of $\mathcal{A}, \mathcal{B}$. Take the following scenario in $(F \downarrow G)$
|
|
\begin{equation}\label{push_1}
|
|
% https://q.uiver.app/#q=WzAsMyxbMCwwLCIoQSxCLGYpIl0sWzIsMCwiKEEnLEInLGYnKSJdLFswLDIsIihBJycsQicnLGYnJykiXSxbMCwxLCIoaCxrKSIsMl0sWzAsMiwiKGgnLGsnKSJdXQ==
|
|
\begin{tikzcd}
|
|
{(A,B,f)} && {(A',B',f')} \\
|
|
\\
|
|
{(A'',B'',f'')}
|
|
\arrow["{(h,k)}"', from=1-1, to=1-3]
|
|
\arrow["{(h',k')}", from=1-1, to=3-1]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
then we can form two pushouts in $\mathcal{A} $ and $ \mathcal{B}$:
|
|
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJBIl0sWzIsMCwiQSciXSxbMCwyLCJBJyciXSxbMiwyLCJQX0EiXSxbMywwLCJCIl0sWzMsMiwiQScnIl0sWzUsMCwiQiciXSxbNSwyLCJQX0IiXSxbMCwxLCJoIiwyXSxbMCwyLCJoJyJdLFsyLDMsInBfMiJdLFsxLDMsInBfMSIsMl0sWzMsMCwiIiwxLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV0sWzQsNSwiayciXSxbNCw2LCJrIiwyXSxbNiw3LCJxXzEiLDJdLFs1LDcsInFfMiJdLFs3LDQsIiIsMSx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dXQ==
|
|
\[\begin{tikzcd}
|
|
A && {A'} & B && {B'} \\
|
|
\\
|
|
{A''} && {P_A} & {A''} && {P_B}
|
|
\arrow["h"', from=1-1, to=1-3]
|
|
\arrow["{h'}", from=1-1, to=3-1]
|
|
\arrow["{p_1}"', from=1-3, to=3-3]
|
|
\arrow["k"', from=1-4, to=1-6]
|
|
\arrow["{k'}", from=1-4, to=3-4]
|
|
\arrow["{q_1}"', from=1-6, to=3-6]
|
|
\arrow["{p_2}", from=3-1, to=3-3]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=3-3, to=1-1]
|
|
\arrow["{q_2}", from=3-4, to=3-6]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=180}, draw=none, from=3-6, to=1-4]
|
|
\end{tikzcd}\]
|
|
Now, follwoing the same idea of initial object we may expect the pushout in $(F \downarrow G)$ to be $(P_A, P_B, u)$ for some $u: F(P_A) \to G(P_B)$. Now, we need to construct a candidate for $u$. Firs of all, since $F$ preserves finite colimits, $F(P_A)=P_A'$ is the pushout of $Fh: FA \to FA'$ and $Fh': FA \to FA''$ in $\mathcal{C}$ (wiht projection $\pi_1: FA' \to P_A', \pi_2: FA'' \to P_A'$ equal to $Fp_1$ and $Fp_2$ up to isomorphism). Then we have the following diagram:
|
|
\begin{equation}\label{def-u}
|
|
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJGQSJdLFswLDIsIkZBJyciXSxbMiwwLCJGQSciXSxbMiwyLCJHUF9CIl0sWzEsMSwiUEEnIl0sWzAsMSwiRmgnIiwyXSxbMCwyLCJGaCJdLFsxLDRdLFsyLDRdLFs0LDMsIlxcZXhpc3RzICEgdSIsMl0sWzEsMywiRnFfMiBcXGNpcmMgZicnIiwyXSxbMiwzLCJGcV8xIFxcY2lyYyBmJyJdXQ==
|
|
\begin{tikzcd}
|
|
FA && {FA'} \\
|
|
& {P_A'} \\
|
|
{FA''} && {GP_B}
|
|
\arrow["Fh", from=1-1, to=1-3]
|
|
\arrow["{Fh'}"', from=1-1, to=3-1]
|
|
\arrow[from=1-3, to=2-2]
|
|
\arrow["{Fq_1 \circ f'}", from=1-3, to=3-3]
|
|
\arrow["{\exists ! u}"', from=2-2, to=3-3]
|
|
\arrow[from=3-1, to=2-2]
|
|
\arrow["{Fq_2 \circ f''}"', from=3-1, to=3-3]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
The external square is commutative since $Fq_1 \circ f' \circ Fh = Fq_1 \circ Fk \circ f = Fq_2 \circ Fk' \circ f = Fq_2 \circ f'' \circ Fh'$ (we used arrow condition of $(F \downarrow G)$ plus the fact that image under functor of commutative diagrams are indeed commutative). Thus there exists a unique $u: P_A' \to GP_B$ such $u \circ Fp_2 = Fq_2 \circ f''$ and $u \circ Fp_1 = Fp_1 \circ f'$. Now, we claim $(P_A,P_B,u)$ to be the pushout of (\ref{push_1}) with projections $(p_1,q_1): (A',B',f') \to (P_A,P_B,u)$ and $(p_2,q_2): (A'',B'',f'') \to (P_A, P_B, u)$.
|
|
|
|
% https://q.uiver.app/#q=WzAsNCxbMCwwLCIoQSxCLGYpIl0sWzIsMCwiKEEnLEInLGYnKSJdLFswLDIsIihBJycsQicnLGYnJykiXSxbMiwyLCIoUF9BLCBQX0IsIHUpIl0sWzAsMSwiKGgsaykiXSxbMCwyLCIoaCcsaycpIiwyXSxbMSwzLCIocF8xLHFfMSkiXSxbMiwzLCIocF8yLHFfMikiLDJdXQ==
|
|
\[\begin{tikzcd}
|
|
{(A,B,f)} && {(A',B',f')} \\
|
|
\\
|
|
{(A'',B'',f'')} && {(P_A, P_B, u)}
|
|
\arrow["{(h,k)}", from=1-1, to=1-3]
|
|
\arrow["{(h',k')}"', from=1-1, to=3-1]
|
|
\arrow["{(p_1,q_1)}", from=1-3, to=3-3]
|
|
\arrow["{(p_2,q_2)}"', from=3-1, to=3-3]
|
|
\end{tikzcd}\]
|
|
|
|
Now, we shall prove that the projections are actually arrows of $(F \downarrow G)$ and that the universal property holds. \\
|
|
We begin proving that the projections are actually arrow, i.e. that the following diagrams are commutative:
|
|
|
|
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJGQSciXSxbMiwwLCJHQiciXSxbMCwyLCJQJ19BIl0sWzIsMiwiR1BfQiJdLFszLDAsIkZBJyciXSxbMywyLCJQX0EnIl0sWzUsMCwiR0InJyJdLFs1LDIsIkdQX0IiXSxbMCwxLCJmJyJdLFswLDIsIkZwXzEiLDJdLFsxLDMsIkZxXzEiXSxbMiwzLCJ1IiwyXSxbNCw1LCJGcF8yIiwyXSxbNCw2LCJmJyciXSxbNSw3LCJ1IiwyXSxbNiw3LCJGcV8yIl1d
|
|
\[\begin{tikzcd}
|
|
{FA'} && {GB'} & {FA''} && {GB''} \\
|
|
\\
|
|
{P'_A} && {GP_B} & {P_A'} && {GP_B}
|
|
\arrow["{f'}", from=1-1, to=1-3]
|
|
\arrow["{Fp_1}"', from=1-1, to=3-1]
|
|
\arrow["{Gq_1}", from=1-3, to=3-3]
|
|
\arrow["{f''}", from=1-4, to=1-6]
|
|
\arrow["{Fp_2}"', from=1-4, to=3-4]
|
|
\arrow["{Gq_2}", from=1-6, to=3-6]
|
|
\arrow["u"', from=3-1, to=3-3]
|
|
\arrow["u"', from=3-4, to=3-6]
|
|
\end{tikzcd}\]
|
|
Both diagrams are commutative as consequence of the diagram (\ref{def-u}); hence projections are indeed arrows in $(F \downarrow G)$. \\
|
|
Now we prove that the universal propery holds:
|
|
\begin{itemize}
|
|
\item existence: assume the following diagram is commutative
|
|
% https://q.uiver.app/#q=WzAsNCxbMCwwLCIoQSxCLGYpIl0sWzIsMCwiKEEnLEInLGYnKSJdLFswLDIsIihBJycsQicnLGYnJykiXSxbMiwyLCIoWCxZLGcpIl0sWzAsMSwiKGgsaykiXSxbMCwyLCIoaCcsaycpIiwyXSxbMSwzLCIoeCcseScpIl0sWzIsMywiKHgnJyx5JycpIiwyXV0=
|
|
\[\begin{tikzcd}
|
|
{(A,B,f)} && {(A',B',f')} \\
|
|
\\
|
|
{(A'',B'',f'')} && {(X,Y,g)}
|
|
\arrow["{(h,k)}", from=1-1, to=1-3]
|
|
\arrow["{(h',k')}"', from=1-1, to=3-1]
|
|
\arrow["{(x',y')}", from=1-3, to=3-3]
|
|
\arrow["{(x'',y'')}"', from=3-1, to=3-3]
|
|
\end{tikzcd}\]
|
|
First notice that since $(x',y')$ and $(x'',y'')$ are arrows of $(F \downarrow G)$ then
|
|
\begin{align}\label{x'y'}
|
|
g \cdot Fx' = Gy' \cdot f' \\
|
|
g \cdot Fx'' = Gy'' \cdot f''\label{x''y''}
|
|
\end{align}
|
|
Second, since the square is commutative, then we have the following two commutative diagram in $\mathcal{A}$ and $\mathcal{B}$ thanks to the universal property of $P_A$ and $P_B$:
|
|
\begin{equation}\label{pushoutarrinAB}
|
|
% https://q.uiver.app/#q=WzAsMTAsWzAsMCwiQSJdLFsyLDAsIkEnIl0sWzAsMiwiQScnIl0sWzEsMSwiUF9BIl0sWzMsMCwiQiJdLFszLDIsIkEnJyJdLFs1LDAsIkInIl0sWzQsMSwiUF9CIl0sWzIsMiwiWCJdLFs1LDIsIlkiXSxbMCwxLCJoIl0sWzAsMiwiaCciLDJdLFsyLDMsInBfMiJdLFsxLDMsInBfMSIsMl0sWzQsNSwiayciLDJdLFs0LDYsImsiXSxbNiw3LCJxXzEiLDJdLFs1LDcsInFfMiJdLFsyLDgsIngnJyIsMl0sWzEsOCwieCciXSxbNyw5LCJcXGV4aXN0IXVfQiJdLFs2LDksInknIl0sWzUsOSwieScnIiwyXSxbMyw4LCJcXGV4aXN0ISB1X0EiLDFdXQ==
|
|
\begin{tikzcd}
|
|
A && {A'} & B && {B'} \\
|
|
& {P_A} &&& {P_B} \\
|
|
{A''} && X & {A''} && Y
|
|
\arrow["h", from=1-1, to=1-3]
|
|
\arrow["{h'}"', from=1-1, to=3-1]
|
|
\arrow["{p_1}"', from=1-3, to=2-2]
|
|
\arrow["{x'}", from=1-3, to=3-3]
|
|
\arrow["k", from=1-4, to=1-6]
|
|
\arrow["{k'}"', from=1-4, to=3-4]
|
|
\arrow["{q_1}"', from=1-6, to=2-5]
|
|
\arrow["{y'}", from=1-6, to=3-6]
|
|
\arrow["{\exists ! u_A}"{description}, from=2-2, to=3-3]
|
|
\arrow["{\exists !u_B}"{description}, from=2-5, to=3-6]
|
|
\arrow["{p_2}", from=3-1, to=2-2]
|
|
\arrow["{x''}"', from=3-1, to=3-3]
|
|
\arrow["{q_2}", from=3-4, to=2-5]
|
|
\arrow["{y''}"', from=3-4, to=3-6]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
Now, we claim that the following diagram is commutative:
|
|
\begin{equation}\label{goalpush}
|
|
% https://q.uiver.app/#q=WzAsNSxbMCwwLCIoQSxCLGYpIl0sWzAsMiwiKEEnJyxCJycsZicnKSJdLFsxLDEsIihQX0EsUF9CLHUpIl0sWzIsMCwiKEEnLEInLGYnKSJdLFsyLDIsIihYLFksZykiXSxbMCwxXSxbMCwzXSxbMywyLCIocF8xLHFfMSkiLDJdLFsxLDQsIih4JycseScnKSIsMl0sWzMsNCwiKHgnLHknKSJdLFsyLDQsIih1X2EsdV9iKSIsMV0sWzEsMiwiKHBfMixxXzIpIl1d
|
|
\begin{tikzcd}
|
|
{(A,B,f)} && {(A',B',f')} \\
|
|
& {(P_A,P_B,u)} \\
|
|
{(A'',B'',f'')} && {(X,Y,g)}
|
|
\arrow[from=1-1, to=1-3]
|
|
\arrow[from=1-1, to=3-1]
|
|
\arrow["{(p_1,q_1)}"', from=1-3, to=2-2]
|
|
\arrow["{(x',y')}", from=1-3, to=3-3]
|
|
\arrow["{(u_a,u_b)}"{description}, from=2-2, to=3-3]
|
|
\arrow["{(p_2,q_2)}", from=3-1, to=2-2]
|
|
\arrow["{(x'',y'')}"', from=3-1, to=3-3]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
If $(u _A,u_B)$ is an arrow of $(F \downarrow G)$ then we are done, since the square is commutative as a direct consequence of the commutativity of (\ref{pushoutarrinAB}). Then we claim $(u_A,u_B)$ to be an actual arrow of $(F \downarrow G)$, i.e. we claim that the following diagram is commutative:
|
|
\begin{equation}\label{uAuBarrow}
|
|
% https://q.uiver.app/#q=WzAsNCxbMCwwLCJQJ19BIl0sWzIsMCwiR1BfQiJdLFswLDIsIkZYIl0sWzIsMiwiR1kiXSxbMCwxLCJ1Il0sWzAsMiwiRnVfQSIsMl0sWzIsMywiZyIsMl0sWzEsMywiR3VfQiJdXQ==
|
|
\begin{tikzcd}
|
|
{P'_A} && {GP_B} \\
|
|
\\
|
|
FX && GY
|
|
\arrow["u", from=1-1, to=1-3]
|
|
\arrow["{Fu_A}"', from=1-1, to=3-1]
|
|
\arrow["{Gu_B}", from=1-3, to=3-3]
|
|
\arrow["g"', from=3-1, to=3-3]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
We will prove commutativity using that $P_A'$ is a pushout in $\mathcal{C}$. Indeed, consider the following diagram:
|
|
% https://q.uiver.app/#q=WzAsNyxbMSwyLCJQJ19BIl0sWzMsMiwiR1BfQiJdLFsxLDQsIkZYIl0sWzMsNCwiR1kiXSxbMiwwLCJGQSJdLFswLDEsIkZBJyJdLFs0LDEsIkZBJyciXSxbMCwxLCJ1Il0sWzAsMiwiRnVfQSIsMl0sWzIsMywiZyIsMl0sWzEsMywiR3VfQiJdLFs0LDUsIkZoJyIsMl0sWzQsNiwiRmgnJyJdLFs1LDIsIkZ4JyIsMix7ImN1cnZlIjoyfV0sWzYsMywiZ0Z4JyciLDAseyJjdXJ2ZSI6LTJ9XSxbMCwzLCJcXGV4aXN0cyAhIHYiLDFdLFs1LDAsIkZwXzIiLDAseyJjdXJ2ZSI6LTF9XSxbNiwwLCJGcF8yIiwyLHsiY3VydmUiOjF9XV0=
|
|
\[\begin{tikzcd}
|
|
&& FA && \\
|
|
{FA'} &&&& {FA''} \\
|
|
& {P'_A} && {GP_B} \\
|
|
\\
|
|
& FX && GY
|
|
\arrow["{Fh'}"', from=1-3, to=2-1]
|
|
\arrow["{Fh''}", from=1-3, to=2-5]
|
|
\arrow["{Fp_1}", curve={height=-6pt}, from=2-1, to=3-2]
|
|
\arrow["{Fx'}"', curve={height=12pt}, from=2-1, to=5-2]
|
|
\arrow["{Fp_2}"', curve={height=6pt}, from=2-5, to=3-2]
|
|
\arrow["{gFx''}", curve={height=-12pt}, from=2-5, to=5-4]
|
|
\arrow["u", from=3-2, to=3-4]
|
|
\arrow["{Fu_A}"', from=3-2, to=5-2]
|
|
\arrow["{\exists ! v}"{description}, from=3-2, to=5-4]
|
|
\arrow["{Gu_B}", from=3-4, to=5-4]
|
|
\arrow["g"', from=5-2, to=5-4]
|
|
\end{tikzcd}\]
|
|
Then using (\ref{x'y'}) and (\ref{x''y''}) we can show that the external square is commuative:
|
|
\begin{align*}
|
|
g Fx'' Fh'' = Gy'' f'' Fh' = Gy'' Gk' f = Gy'Gkf \\
|
|
g Fx' Fh = Gy' f' Fh = Gy'Gkf
|
|
\end{align*}
|
|
Thus, by $P'_A$ beeing pushout in $\mathcal{C}$ there exists an unique $v: P_A' \to GY$ such that $vFp_1 = gFx'$ and $vFp_2 = gFx''$. Now , consider $gFu_A, Gu_Bu: P_A' \to GY$, notice that:
|
|
\begin{align*}
|
|
gFu_AFp_1 = gFx' \\
|
|
gFu_BFp_2 = gFx'' \\
|
|
Gu_BuFp_1 = Gu_BGq_1f' = Gy'f' = gFx' \\
|
|
Gu_BuFp_2 = Gu_BGq_2f'' = Gy''f'' = gFx'' \\
|
|
\end{align*}
|
|
So by uniqueness of $v$ we get $gFu_A = Gu_B u$ and so, since the square (\ref{uAuBarrow}) is commutative, then $(u_A,u_B)$ is an arrow of $(F \downarrow G)$ and the diagram (\ref{goalpush}) is commutative.
|
|
\item uniqueness: the uniquness of $(u_A,u_B)$ comes almost for free: indee if there was antoher arrow $(l,m)$ satisfyng commutativity in (\ref{goalpush}), then, by universal property of pushouts $l=u_A$ in $\mathcal{A}$ and $m = u_B$ in $\mathcal{B}$. Therefore we would have $(l,m) = (u_A, u_B)$
|
|
\end{itemize}
|
|
Thus $(P_A, P_B, u)$ is the desired pushout and $(F \downarrow G)$ having initial object and pushouts is indeed finitely cocomplete. \\
|
|
\textbf{The forgetfoul functors are cocontinous}: the cocontinuity of $\Pi_1, \Pi_2$ arises immediatly from the structure of intial object and pushouts of $(F \downarrow G)$. Indeed take the inital object of $(F \downarrow G)$, $(0_A, 0_B, in)$; then $\Pi_1((0_A, 0_B, in))=0_A$ and $\Pi_2((0\_A, 0\_B, in)) = 0_B$ are respectively the initial object of $\mathcal{A}$ and $\mathcal{B}$. Since the same happens for the pushouts of $(F \downarrow G)$ then both $\Pi_1$ and $\Pi_2$ preserves finite colimits. \\
|
|
Now, let's move on to the finitely complete case; so suppose that both $\mathcal{A}$ and $\mathcal{B}$ are finitely complete and that $G$ is finitely continous. The structure of the proof is completely analogue \footnote{Notice that we can also argue that, beeing $(F \downarrow G)^{op} \cong (F^{op} \downarrow G^{op})$, the complete case comes for free from the cocomplete case} and so we will omit some details. \\
|
|
\textbf{Terminal Objects}: following the structure of the cocomplete proof we claim $(1_\mathcal{A}, 1_\mathcal{B}, un)$, where $un: F(1_\mathcal{A}) \to 1_\mathcal{C} = G(1_\mathcal{B})$ is the unique morphism granted by $G(1_\mathcal{B})$ be terminal in $\mathcal{C}$, to be the terminal object in $(F \downarrow G)$
|
|
\begin{itemize}
|
|
\item existence: let $(A,B,f)$ be an object of $(F\downarrow G)$; then there exists two unique morphisms $un_A, un_B$ respectively in $\mathcal{A}$ and $\mathcal{B}$ such that $un_A: A \to 1_\mathcal{A} $ and $un_B: B \to 1_\mathcal{B}$. Thus we have a candidate morphism $(un_A, un_B)$. In order to check that this morphism is a morphism of $(F \downarrow G)$ we need to show that the following diagram is commutative:
|
|
\[\begin{tikzcd}
|
|
{F1_\mathcal{A}} && {G1_\mathcal{B}= 1_\mathcal{C}} \\
|
|
\\
|
|
FA && GB
|
|
\arrow["un"', from=1-1, to=1-3]
|
|
\arrow["{Fun_A}", from=1-1, to=3-1]
|
|
\arrow["{Gun_B}"', from=1-3, to=3-3]
|
|
\arrow["f", from=3-1, to=3-3]
|
|
\end{tikzcd}\]
|
|
The diagram above is trivially commutative since $G1_\mathcal{B} = 1_\mathcal{C}$ is terminal in $\mathcal{C}$
|
|
\item uniqueness: the uniquness is directly inherited by uniness of $un_A$ and $un_B$ in $\mathcal{A}$ and $\mathcal{B}$
|
|
\end{itemize}
|
|
\textbf{Pullbacks}: As for the pushouts we claim the pullback of the following diagram:
|
|
% https://q.uiver.app/#q=WzAsMyxbMCwyLCIoQScsQicsZikiXSxbMiwyLCIoQScnLEInJyxmJycpIl0sWzIsMCwiKEEsQixmKSJdLFswLDEsIihoJyxrJykiXSxbMiwxLCIoaCxrKSIsMl1d
|
|
\[\begin{tikzcd}
|
|
&& {(A,B,f)} \\
|
|
\\
|
|
{(A',B',f)} && {(A'',B'',f'')}
|
|
\arrow["{(h,k)}"', from=1-3, to=3-3]
|
|
\arrow["{(h',k')}", from=3-1, to=3-3]
|
|
\end{tikzcd}\]
|
|
to be $(P_A , P_B, u)$ with projections $(p_1,q_1): (P_A,P_B,u) \to (A,B,f)$ and $(p_2,q_2): (P_A,P_B,u) \to (A',B',f')$ where $(P_A, p_1, p_2)$ and $(P_B, q_1, q_2)$ are pullbacks in $\mathcal{A}$ and $\mathcal{B}$ (Remember that $GP_B=P_B'$ is a pullback in $\mathcal{C}$ as was for $FP_A$ in the cocomplete case). $u: FP_A \to P_B'$ arises from the universal property of $P_B'$ as shown in the following diagram (whose commutativity is ensured by arrow condition in $(F \downarrow G)$ plus pullbacks condition of $(P_A, q_1, q_2)$ in $\mathcal{A}$):
|
|
% https://q.uiver.app/#q=WzAsNixbMSwzLCJHQiciXSxbMywzLCJHQicnIl0sWzMsMSwiR0IiXSxbMSwxLCJQJ19CIl0sWzAsMCwiUF9BIl0sWzEsNV0sWzAsMSwiR2snIl0sWzIsMSwiR2siLDJdLFszLDAsIkdxXzIiXSxbMywyLCJHcV8xIiwyXSxbNCwwLCJmJ0ZwXzIiLDIseyJjdXJ2ZSI6Mn1dLFs0LDIsImZGcF8xIiwyLHsiY3VydmUiOi0yfV0sWzQsMywiXFxleGlzdHMgISB1IiwxXV0=
|
|
\[\begin{tikzcd}
|
|
{P_A} &&& \\
|
|
& {P'_B} && GB \\
|
|
\\
|
|
& {GB'} && {GB''} \\
|
|
\\
|
|
& {}
|
|
\arrow["{\exists ! u}"{description}, from=1-1, to=2-2]
|
|
\arrow["{fFp_1}"', curve={height=-12pt}, from=1-1, to=2-4]
|
|
\arrow["{f'Fp_2}"', curve={height=12pt}, from=1-1, to=4-2]
|
|
\arrow["{Gq_1}"', from=2-2, to=2-4]
|
|
\arrow["{Gq_2}", from=2-2, to=4-2]
|
|
\arrow["Gk"', from=2-4, to=4-4]
|
|
\arrow["{Gk'}", from=4-2, to=4-4]
|
|
\end{tikzcd}\]
|
|
From the commutativity of this diagram we deduce that $(q_i, p_i)$ are actuall arrows of $(F \downarrow G)$, indeed:
|
|
\begin{align}
|
|
Gq_2u = f'Fp_2 \\
|
|
Gq_1u = fFp_1
|
|
\end{align}
|
|
Now, we cheeck that the universal propery holds
|
|
\begin{itemize}
|
|
\item Existence: assume the external square to be commutative:
|
|
\begin{equation}\label{pull}
|
|
% https://q.uiver.app/#q=WzAsNixbMSwzLCIoQScsQicsZicpIl0sWzMsMywiKEEnJyxCJycsZicnKSJdLFszLDEsIihBLEIsZikiXSxbMCwwLCIoWCxZLGcpIl0sWzEsNV0sWzEsMSwiKFBfQSxQX0IsdSkiXSxbMCwxLCIoaCcsaycpIl0sWzIsMSwiKGgsaykiLDJdLFszLDAsIih4Jyx5JykiLDIseyJjdXJ2ZSI6Mn1dLFszLDIsIih4JycseScnKSIsMCx7ImN1cnZlIjotMn1dLFs1LDIsIihwXzEscV8xKSJdLFs1LDAsIihwXzIscV8yKSJdXQ==
|
|
\begin{tikzcd}
|
|
{(X,Y,g)} &&& \\
|
|
& {(P_A,P_B,u)} && {(A,B,f)} \\
|
|
\\
|
|
& {(A',B',f')} && {(A'',B'',f'')} \\
|
|
\\
|
|
& {}
|
|
\arrow["{(x,y)}", curve={height=-12pt}, from=1-1, to=2-4]
|
|
\arrow["{(x',y')}"', curve={height=12pt}, from=1-1, to=4-2]
|
|
\arrow["{(p_1,q_1)}", from=2-2, to=2-4]
|
|
\arrow["{(p_2,q_2)}", from=2-2, to=4-2]
|
|
\arrow["{(h,k)}"', from=2-4, to=4-4]
|
|
\arrow["{(h',k')}", from=4-2, to=4-4]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
Then we can use universal property of $P_A$ and $P_B$ in $\mathcal{A}$ and $\mathcal{B}$:
|
|
\begin{equation}\label{pullstart}
|
|
% https://q.uiver.app/#q=WzAsMTAsWzAsMCwiWCJdLFsxLDEsIlBfQSJdLFszLDEsIkEiXSxbMSwzLCJBJyJdLFszLDMsIkEnJyJdLFs1LDEsIlBfQiJdLFs3LDEsIkIiXSxbNSwzLCJCJyJdLFs3LDMsIkInJyJdLFs0LDAsIlkiXSxbMSwyXSxbMSwzXSxbMyw0LCJoJyIsMl0sWzIsNCwiaCJdLFswLDMsIngnIiwwLHsiY3VydmUiOjJ9XSxbMCwyLCJ4IiwwLHsiY3VydmUiOi0yfV0sWzUsNl0sWzUsN10sWzcsOCwiayciLDJdLFs2LDgsImsiXSxbOSw3LCJ5JyIsMCx7ImN1cnZlIjoyfV0sWzksNiwieSIsMCx7ImN1cnZlIjotMn1dLFswLDEsIlxcZXhpc3RzICEgdV9BIiwxXSxbOSw1LCJcXGV4aXN0cyAhIHVfQiIsMV1d
|
|
\begin{tikzcd}
|
|
X &&&& Y &&& \\
|
|
& {P_A} && A && {P_B} && B \\
|
|
\\
|
|
& {A'} && {A''} && {B'} && {B''}
|
|
\arrow["{\exists ! u_A}"{description}, from=1-1, to=2-2]
|
|
\arrow["x", curve={height=-12pt}, from=1-1, to=2-4]
|
|
\arrow["{x'}", curve={height=12pt}, from=1-1, to=4-2]
|
|
\arrow["{\exists ! u_B}"{description}, from=1-5, to=2-6]
|
|
\arrow["y", curve={height=-12pt}, from=1-5, to=2-8]
|
|
\arrow["{y'}", curve={height=12pt}, from=1-5, to=4-6]
|
|
\arrow[from=2-2, to=2-4]
|
|
\arrow[from=2-2, to=4-2]
|
|
\arrow["h", from=2-4, to=4-4]
|
|
\arrow[from=2-6, to=2-8]
|
|
\arrow[from=2-6, to=4-6]
|
|
\arrow["k", from=2-8, to=4-8]
|
|
\arrow["{h'}"', from=4-2, to=4-4]
|
|
\arrow["{k'}"', from=4-6, to=4-8]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
Now, consider the couple $(u_A,u_B)$; by commutativity of (\ref{pullstart}) if $(u_A,u_B): (X,Y,g) \to (P_A,P_B, u)$ is an actual arrow of $(F \downarrow G)$ then it complete the diagram (\ref{pull}) to a commutative diagram. \\
|
|
We procede as in the case of pushouts; consider the following square:
|
|
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJGWCJdLFsxLDAsIkdZIl0sWzEsMSwiR3VfQiBcXGNvbmcgUF9CJyJdLFswLDEsIkZQX0EiXSxbMSwyLCJHQiciXSxbMiwyLCJHQicnIl0sWzIsMSwiR0IiXSxbMCwyLCJGQSciXSxbMCwxLCJnIl0sWzEsMl0sWzAsM10sWzMsMiwidSIsMl0sWzIsNCwiR3FfMiJdLFs0LDUsIkdrJyIsMl0sWzIsNiwiR3FfMSIsMl0sWzYsNSwiR2siXSxbMCwyLCJcXGV4aXN0cyAhIHYgIiwxXSxbMSw2LCJHeSIsMCx7ImN1cnZlIjotMn1dLFs3LDQsImYnIiwyXSxbMCw3LCJGeCciLDIseyJjdXJ2ZSI6NH1dXQ==
|
|
\[\begin{tikzcd}
|
|
FX & GY & \\
|
|
{FP_A} & {Gu_B \cong P_B'} & GB \\
|
|
{FA'} & {GB'} & {GB''}
|
|
\arrow["g", from=1-1, to=1-2]
|
|
\arrow[from=1-1, to=2-1]
|
|
\arrow["{\exists ! v }"{description}, from=1-1, to=2-2]
|
|
\arrow["{Fx'}"', curve={height=24pt}, from=1-1, to=3-1]
|
|
\arrow[from=1-2, to=2-2]
|
|
\arrow["Gy", curve={height=-12pt}, from=1-2, to=2-3]
|
|
\arrow["u"', from=2-1, to=2-2]
|
|
\arrow["{Gq_1}"', from=2-2, to=2-3]
|
|
\arrow["{Gq_2}", from=2-2, to=3-2]
|
|
\arrow["Gk", from=2-3, to=3-3]
|
|
\arrow["{f'}"', from=3-1, to=3-2]
|
|
\arrow["{Gk'}"', from=3-2, to=3-3]
|
|
\end{tikzcd}\]
|
|
Since $(x',y')$ and $(x,y)$ are arrows of $(F \downarrow G)$, the square (\ref{pull}) is commutative and using the definition of $(p_i,q_i)$ we can show that the external square commutes, indeed:
|
|
\begin{equation}
|
|
Gk'f'Fx'=Gk'Gy'g=GkGyg
|
|
\end{equation}
|
|
Thus, since $P_B'$ is the pullback of $GB \xrightarrow{Gk} GB''$ and $GB' \xrightarrow{Gk'} GB''$ there exists an unique $v : FX \to P_B'$ such $Gq_1v = Gy g$ and $Gq_2v = f' Fx'$. Now, consider $uFu_A,Gu_Bg : FX \to P_B'$ and notice that:
|
|
\begin{align*}
|
|
Gq_1uFu_A = f Fp_1 Fu_A = f Fx = Gyg \\
|
|
Gq_2uFu_A = f Fp_2Fu_A = f' Fp_2 F u_A = f'Fx' \\
|
|
Gq_1Gu_Bg = Gy g \\
|
|
Gq_2Gu_Bg = Gy'g = f'Fx' \\
|
|
\end{align*}
|
|
Thus by uniqueness of $v: FX \to P_B'$ then $uFu_A = Gu_B f$ and so $(u_A,u_B): (X,Y,g) \to (P_A,P_B,u)$ is an arrow of $(F \downarrow G)$ and complete the diagram (\ref{pull}) to a commutative diagram
|
|
\item uniqueness: uniqueness of $u_A$ and $u_B$ in $\mathcal{A}$ and $\mathcal{B}$ yields to uniqueness of $(u_A,u_B)$ in $(F \downarrow G)$
|
|
\end{itemize}
|
|
\textbf{Forgetful functors are continous}: the proof is analogue to the cocomplete case, since both $\Pi_1,\Pi_2$ preserves terminal object and pullbacks. \\
|
|
We proved that under the assumption of $\mathcal{A}$ and $\mathcal{B}$ beeing cocomplete and $F$ beeing cocontinous the comma category $(F \downarrow G)$ is cocomplete and that $\Pi_i$ is cocontinous; morevoer we proved the dual result with complteness assumption, therefore the statement is proved and we are done.
|
|
\end{proof}
|
|
|
|
\begin{definition}[Freyd Cover]
|
|
Let $\mathcal{C}$ be a small category (serve veramente sia piccola?) with a terminal odject $1$, then we call its \textit{Freyd Cover}, $Cov(\mathcal{C})$, the comma category $Id \downarrow \mathcal{C}(1,\text{-})$ where $Id: Set \to Set$ is the identical functor
|
|
\end{definition}
|
|
\begin{definition}[Projection Functor of Freyd Cover]
|
|
Recall that there are two canonical functors $\Pi_1,\Pi_2$ associated with a comma category. Let $\mathcal{C}$ be a category with terminal object and let $Cov(\mathcal{C})$ be its Frey Cover. We call the functor $\Pi_2: Cov(\mathcal{C}) \to \mathcal{C}$ the projection functor of the Freyd Cover.
|
|
\end{definition}
|
|
\begin{theorem}\label{cover of bicartesian}
|
|
Let $\mathcal{C}$ be a bicartesian category - i.e. a category with terminal object, initial object and binary products and coproducs - then $Cov(\mathcal{C})$ is bicartesian. Moreover $\Pi_2 : Cov(\mathcal{C}) \to \mathcal{C}$ is a cartesian closed functor
|
|
\end{theorem}
|
|
\begin{proof}
|
|
The proof follows a similar structure to the proof of \ref{completenesscomma}, so we will construct initial and terminal objects, binary products and copruducts and then we will prove that $\Pi_2$ is closed with respect to this constructions. \\
|
|
\textbf{Initial and Terminal Object}: the initial object of $Cov(\mathcal{C})$ is $(0_{Set}, 0_\mathcal{C}, in)$ and the terminal object is $(1_{Set}, 1_\mathcal{C}, un)$. The construction is the same of the construction in \ref{completenesscomma} and therefore the proof is ommitted \\
|
|
\textbf{Binary Products}: Recall that $\mathcal{C}(1_\mathcal{C},-): \mathcal{C} \to Set$ is a continous functor - i.e. preserves limits - and so in particular it preserves binary products. Therefore if $A,B$ are objects of $\mathcal{C}$ we have a set isomorphism $\sigma$:
|
|
% https://q.uiver.app/#q=WzAsNCxbMSwwLCJcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sQSBcXHRpbWVzIEIpIl0sWzAsMCwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LCBBKSBcXHRpbWVzIFxcbWF0aGNhbHtDfSgxX1xcbWF0aGNhbHtDfSxCKSJdLFswLDEsIihoLCBrKSJdLFsxLDEsIjwgaCxrID46IDFfXFxtYXRoY2Fse0N9IFxcdG8gQSBcXHRpbWVzIEIgIl0sWzEsMF0sWzIsMywiIiwwLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibWFwcyB0byJ9fX1dXQ==
|
|
\[\begin{tikzcd}
|
|
{\mathcal{C}(1_\mathcal{C}, A) \times \mathcal{C}(1_\mathcal{C},B)} & {\mathcal{C}(1_\mathcal{C},A \times B)} \\
|
|
{(h, k)} & {< h,k >: 1_\mathcal{C} \to A \times B }
|
|
\arrow[from=1-1, to=1-2]
|
|
\arrow[maps to, from=2-1, to=2-2]
|
|
\end{tikzcd}\]
|
|
Now, let $(X,A,f),(Y,B,g)$ be two object of $Cov(\mathcal{C})$; we claim their product to be $(X\times Y, A \times B, \sigma \circ (f \times g))$ where $\sigma \circ (f \times f)$ arises from the following produt diagram in $Set$:
|
|
% https://q.uiver.app/#q=WzAsNyxbMCwxLCJYIFxcdGltZXMgWSJdLFsxLDAsIlgiXSxbMSwyLCJZIl0sWzIsMCwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEEpIl0sWzIsMiwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEIpIl0sWzMsMSwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEEpXFx0aW1lcyBcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sQSkiXSxbNCwxLCJcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sQVxcdGltZXMgQikiXSxbMCwxLCJcXHBpX1giXSxbMCwyLCJcXHBpX1kiLDJdLFsxLDMsImYiXSxbMiw0LCJnIiwyXSxbNSwzLCJcXHBpXzEiLDJdLFs1LDQsIlxccGlfMiJdLFswLDUsIlxcZXhpc3RzICEgPGZcXHBpX3gsZ1xccGlfeT4gOj0gZiBcXHRpbWVzIGciXSxbNSw2LCJcXHNpZ21hIl1d
|
|
\[\begin{tikzcd}
|
|
& X & {\mathcal{C}(1_\mathcal{C},A)} && \\
|
|
{X \times Y} &&& {\mathcal{C}(1_\mathcal{C},A)\times \mathcal{C}(1_\mathcal{C},A)} & {\mathcal{C}(1_\mathcal{C},A\times B)} \\
|
|
& Y & {\mathcal{C}(1_\mathcal{C},B)}
|
|
\arrow["f", from=1-2, to=1-3]
|
|
\arrow["{\pi_X}", from=2-1, to=1-2]
|
|
\arrow["{\exists ! <f\pi_x,g\pi_y> := f \times g}", from=2-1, to=2-4]
|
|
\arrow["{\pi_Y}"', from=2-1, to=3-2]
|
|
\arrow["{\pi_1}"', from=2-4, to=1-3]
|
|
\arrow["\sigma", from=2-4, to=2-5]
|
|
\arrow["{\pi_2}", from=2-4, to=3-3]
|
|
\arrow["g"', from=3-2, to=3-3]
|
|
\end{tikzcd}\]
|
|
and we claim the projections of $(X\times Y, A \times B, \sigma \circ (f \times g))$ to be $(\pi_X,\pi_A):(X\times Y, A \times B, \sigma \circ (f \times g)) \to (X, A,f)$ and $(\pi_Y,\pi_B):(X\times Y, A \times B, \sigma \circ (f \times g)) \to (Y, B,f)$. \\
|
|
We start by checking that our candidate projections are arrows of $Cov(\mathcal{C})$ and then we will check that the universal property holds. In order to check that our projection are actual arrows we shall prove that $ \mathcal{C}(1_\mathcal{C},\pi_A) \sigma (f \times g) = f \pi_X$ and that $\mathcal{C}(1_\mathcal{C}, \pi_B) \sigma (f \times g) = \pi_B g$ but this two identities follow directly from the fact that $\mathcal{C}(1_\mathcal{C},-)$ preserves products and that products are unique up to ismorphism, thus $\pi_1 = \mathcal{C}(\_\mathcal{C},-)\pi_A$ and $\pi_2 = \mathcal{C}(\_\mathcal{C},-)\pi_B$ and so the indentity are trivial. Let's move on to the universal property.
|
|
\begin{itemize}
|
|
\item existence: let consider the following situation:
|
|
\begin{equation}\label{prodgoal}
|
|
% https://q.uiver.app/#q=WzAsNCxbMSwwLCIoWFxcdGltZXMgWSwgQSBcXHRpbWVzIEIsIFxcc2lnbWEgKGYgXFx0aW1lcyBnKSkiXSxbMCwyLCIoWCxBLGYpIl0sWzIsMiwiKFksQixnKSAiXSxbMSwyLCIoWixDLGgpIl0sWzAsMSwiKFxccGlfWCwgXFxwaV9BKSIsMl0sWzAsMiwiKFxccGlfWSwgXFxwaV9CKSJdLFszLDIsIihsJyxtJykiLDJdLFszLDEsIihsLG0pIl1d
|
|
\begin{tikzcd}
|
|
& {(X\times Y, A \times B, \sigma (f \times g))} & \\
|
|
\\
|
|
{(X,A,f)} & {(Z,C,h)} & {(Y,B,g) }
|
|
\arrow["{(\pi_X, \pi_A)}"', from=1-2, to=3-1]
|
|
\arrow["{(\pi_Y, \pi_B)}", from=1-2, to=3-3]
|
|
\arrow["{(l,m)}", from=3-2, to=3-1]
|
|
\arrow["{(l',m')}"', from=3-2, to=3-3]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
then, since $X \times Y$ and $A \times B$ are product rispectively in $Set$ and $\mathcal{C}$ we have the following commutative diagrams:
|
|
% https://q.uiver.app/#q=WzAsOCxbMSwwLCJYXFx0aW1lcyBZIl0sWzAsMSwiWCJdLFsyLDEsIlkiXSxbMSwxLCJaIl0sWzMsMSwiQSJdLFs0LDAsIkEgXFx0aW1lcyBCIl0sWzUsMSwiQiJdLFs0LDEsIkMiXSxbMCwxLCJcXHBpX1giLDJdLFswLDIsIlxccGlfWSJdLFszLDEsImwiXSxbMywyLCJsJyIsMl0sWzMsMCwiXFxleGlzdHMgISBcXGJhcntsfSIsMV0sWzUsNCwiXFxwaV9BIiwyXSxbNSw2LCJcXHBpX0IiXSxbNyw0LCJtIl0sWzcsNiwibSciLDJdLFs3LDUsIlxcZXhpc3RzICEgXFxiYXJ7bX0iLDFdXQ==
|
|
\[\begin{tikzcd}
|
|
& {X\times Y} &&& {A \times B} & \\
|
|
X & Z & Y & A & C & B
|
|
\arrow["{\pi_X}"', from=1-2, to=2-1]
|
|
\arrow["{\pi_Y}", from=1-2, to=2-3]
|
|
\arrow["{\pi_A}"', from=1-5, to=2-4]
|
|
\arrow["{\pi_B}", from=1-5, to=2-6]
|
|
\arrow["{\exists ! \bar{l}}"{description}, from=2-2, to=1-2]
|
|
\arrow["l", from=2-2, to=2-1]
|
|
\arrow["{l'}"', from=2-2, to=2-3]
|
|
\arrow["{\exists ! \bar{m}}"{description}, from=2-5, to=1-5]
|
|
\arrow["m", from=2-5, to=2-4]
|
|
\arrow["{m'}"', from=2-5, to=2-6]
|
|
\end{tikzcd}\]
|
|
Thus consider the couple $(\bar{l},\bar{m})$; if it is a morphism of $Cov(\mathcal{C})$ then it completes the diagram (\ref{prodgoal}) to a commutative diagram. Now, consider the following diagram:
|
|
% https://q.uiver.app/#q=WzAsOCxbMSwwLCJaIl0sWzIsMCwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEMpIl0sWzEsMSwiWCBcXHRpbWVzIFkiXSxbMiwxLCJcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sIEEgXFx0aW1lcyBCKSJdLFswLDEsIlkiXSxbMiwyLCJcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sIEEpXFx0aW1lcyBcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sIEIpIl0sWzMsMiwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LCBBKSJdLFsxLDIsIlxcbWF0aGNhbHtDfSgxX1xcbWF0aGNhbHtDfSxCKSJdLFswLDEsImgiXSxbMCwyLCJcXGJhcntsfSJdLFsyLDNdLFsxLDMsIlxcbWF0aGNhbHtDfSgxX1xcbWF0aGNhbHtDfSwgXFxiYXJ7bX0pIl0sWzAsNCwibCciLDJdLFsyLDUsImYgXFx0aW1lcyBnIiwxXSxbNSwzLCJcXHNpZ21hIiwwLHsiY3VydmUiOi0yfV0sWzMsNSwiXFxzaWdtYV4tMSIsMCx7Im9mZnNldCI6LTMsImN1cnZlIjotMX1dLFs1LDYsIlxccGlfMSIsMl0sWzUsNywiXFxwaV8yIl0sWzQsNywiZyIsMix7ImN1cnZlIjoyfV0sWzEsNiwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LG0pIiwwLHsiY3VydmUiOi01fV0sWzUsMywiXFxjb25nIiwxLHsic3R5bGUiOnsiYm9keSI6eyJuYW1lIjoibm9uZSJ9LCJoZWFkIjp7Im5hbWUiOiJub25lIn19fV1d
|
|
\[\begin{tikzcd}
|
|
& Z & {\mathcal{C}(1_\mathcal{C},C)} & \\
|
|
Y & {X \times Y} & {\mathcal{C}(1_\mathcal{C}, A \times B)} \\
|
|
& {\mathcal{C}(1_\mathcal{C},B)} & {\mathcal{C}(1_\mathcal{C}, A)\times \mathcal{C}(1_\mathcal{C}, B)} & {\mathcal{C}(1_\mathcal{C}, A)}
|
|
\arrow["h", from=1-2, to=1-3]
|
|
\arrow["{l'}"', from=1-2, to=2-1]
|
|
\arrow["{\bar{l}}", from=1-2, to=2-2]
|
|
\arrow["{\mathcal{C}(1_\mathcal{C}, \bar{m})}", from=1-3, to=2-3]
|
|
\arrow["{\mathcal{C}(1_\mathcal{C},m)}", curve={height=-30pt}, from=1-3, to=3-4]
|
|
\arrow["g"', curve={height=12pt}, from=2-1, to=3-2]
|
|
\arrow[from=2-2, to=2-3]
|
|
\arrow["{f \times g}"{description}, from=2-2, to=3-3]
|
|
\arrow["{\sigma^-1}", shift left=3, curve={height=-6pt}, from=2-3, to=3-3]
|
|
\arrow["\sigma", curve={height=-12pt}, from=3-3, to=2-3]
|
|
\arrow["\cong"{description}, draw=none, from=3-3, to=2-3]
|
|
\arrow["{\pi_2}", from=3-3, to=3-2]
|
|
\arrow["{\pi_1}"', from=3-3, to=3-4]
|
|
\end{tikzcd}\]
|
|
Since $\pi_1\sigma^{-1} \mathcal{C}(1_\mathcal{C}, \bar{m})h = \mathcal{C}(1_\mathcal{C}, m)h = \pi_1 (f \times g)\bar{l}$ and $\pi_2\sigma^{-1} \mathcal{C}(1_\mathcal{C}, \bar{m})h = gl' = \pi_2 (f \times g)\bar{l} $ then by the universal property of binary product $\sigma^{-1} \mathcal{C}(1_\mathcal{C}, \bar{m})h = \sigma^{-1} \sigma (f \times g) \bar{l}$ hence $\sigma (f \times g) \bar{l} = \mathcal{C}(1_\mathcal{C},\bar{m})h$ thus $(\bar{l}, \bar{m})$ is an arrow of $Cov(\mathcal{C})$ and complete the diagram (\ref{prodgoal}) to a commutative diagram
|
|
\item Uniqueness: uniqueness of $(\bar{l}, \bar{m})$ is directly inherited by uniqueness of $\bar{l}$ and $\bar{m}$ in $\mathcal{A}$ and $\mathcal{B}$
|
|
\end{itemize}
|
|
\textbf{Binary Coproducts}:
|
|
Let $(X,A ,f)$ and $(Y,B,g)$ be two objects of $Cov(\mathcal{C})$, then we claim their coprduct to be $(X \oplus Y, A \oplus B, f \oplus g)$ with injections $(\iota_X, \iota_A)$ and $(\iota_Y, \iota_B)$ where $f \oplus g$ arises from:
|
|
% https://q.uiver.app/#q=WzAsNixbMCwxLCJYIFxcb3BsdXMgWSJdLFsxLDAsIlgiXSxbMSwyLCJZIl0sWzIsMCwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEEpIl0sWzIsMiwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEIpIl0sWzMsMSwiXFxtYXRoY2Fse0N9KDFfXFxtYXRoY2Fse0N9LEEpXFxvcGx1c1xcbWF0aGNhbHtDfSgxX1xcbWF0aGNhbHtDfSxCKSBcXGNvbmcgXFxtYXRoY2Fse0MoMV9cXG1hdGhjYWx7Q319LEEgXFxvcGx1cyBCKSJdLFsxLDAsIlxcaW90YV9YIiwyXSxbMiwwLCJcXGlvdGFfWSJdLFsxLDMsImYiXSxbMiw0LCJnIiwyXSxbNCw1LCJcXGlvdGFfMiIsMl0sWzMsNSwiXFxpb3RhXzEiXSxbMCw1LCJcXGV4aXN0cyAhIGYgXFxvcGx1cyBnIiwyXV0=
|
|
\[\begin{tikzcd}
|
|
& X & {\mathcal{C}(1_\mathcal{C},A)} & \\
|
|
{X \oplus Y} &&& {\mathcal{C}(1_\mathcal{C},A)\oplus\mathcal{C}(1_\mathcal{C},B) \cong \mathcal{C}(1_\mathcal{C},A \oplus B)} \\
|
|
& Y & {\mathcal{C}(1_\mathcal{C},B)}
|
|
\arrow["f", from=1-2, to=1-3]
|
|
\arrow["{\iota_X}"', from=1-2, to=2-1]
|
|
\arrow["{\iota_1}", from=1-3, to=2-4]
|
|
\arrow["{\exists ! f \oplus g}"', from=2-1, to=2-4]
|
|
\arrow["{\iota_Y}", from=3-2, to=2-1]
|
|
\arrow["g"', from=3-2, to=3-3]
|
|
\arrow["{\iota_2}"', from=3-3, to=2-4]
|
|
\end{tikzcd}\]
|
|
The proof is analogue to the proof of binary product and so we omit the calculations. \\
|
|
\textbf{Projection is cartesian closed}: the proof of $\Pi_2$ beeing cartesian closed functor is identical to the proof of $\Pi_1$ beeing continous in \ref{completenesscomma}
|
|
\end{proof}
|
|
\begin{theorem}
|
|
Let $\mathcal{H}$ be an Heyting Algebra - i.e. an ordered bicartesian category which is also cartesian closed - then $Cov(\mathcal{H})$ is also bicartesian closed. Morover the projection $\Pi_2 : Cov(\mathcal{H}) \to \mathcal{H}$ is bicartesian closed.
|
|
\end{theorem}
|
|
\begin{proof}\label{coverheyting}
|
|
By \ref{cover of bicartesian} we know that $Cov(\mathcal{H})$ is bicartesian and that $\Pi_2$ is cartesian closed. So we need only to prove the existence of function spaces. \\
|
|
Let $(X,a,f)$ and $(Y,b,g)$ be objects of $Cov(\mathcal{C})$. We expect the exponential $(Y,b,g)^{(X,a,f)}$ to be something similar to $(Y^X, a \to b, \xi)$ where $Y^X = Set(X,Y)$ is the function space in $Set$, $a \to b$ is the heyting implication in $\mathcal{H}$ and $\xi$ is a function somehow defined using that beeing $\mathcal{H}$ an ordered category if $a \to b$ in nonempty the in terminal in $Set$. This intuition is almost correct, but there is a problem: in order to make $(Y^X, a \to b, \xi)$ an object of $\mathcal{H}$ we need $\xi: Y^X \to \mathcal{H}(1_\mathcal{H}, a \to b)$ to be a $Set$-morphism which is not possible if $ 1_\mathcal{H} \nleq_{\mathcal{H}} a \to b $ and $Y^X \neq \emptyset$. Thus we claim $(Y,b,g)^{(X,a,f)}$ to be $( (Y^X)_{a \leq b}, a \to b , \xi)$ where $(Y^X)_{a \leq b}$ is $Set(X,Y)$ if $a \leq_{\mathcal{H}} b$ - and so $\mathcal{H}(1_\mathcal{H}, a \to b) \neq \emptyset$ - and to be empty otherwise:
|
|
\begin{equation*}
|
|
(Y^X)_{a \leq b} := \{ h \in Y^X | \forall x \in X (f(x)\in \mathcal{H}(1_\mathcal{H},a) \implies g(h(x)) \in \mathcal{H}(1_\mathcal{H},b) )\}
|
|
\end{equation*}
|
|
with evaluation given by: $(Ev_{Set}, Ev_\mathcal{H}): ((Y^X)_{a \leq b}, a \to b, \xi) \to (Y, b, g)$ where $Ev_{Set} : (Y^X)_{a \leq b} \times X \to Y$ is the restriction of usual evaluation morphism in $Set$ and $Ev_\mathcal{H} = a \to b \land a \leq b$ is the counit of the adjunction of exponential functor in $\mathcal{H}$. Now, let $(u, c\land a \leq b) : (Z,c,h) \times (X,a,f) \to (Y,b,g)$, we claim its abstraction to be:
|
|
\begin{equation*}
|
|
(\hat{u}, c \leq a \to b) : (Z,c,h) \to ( (Y^X)_{a \leq b}, a \to b, \xi )
|
|
\end{equation*}
|
|
This couple is clearly an arrow of $Cov(\mathcal{C})$\footnote{the arrow condition is forced since if every definition is coherent than the commutativity of the arrow condition square follows from $\mathcal{H}(1_\mathcal{H}, a \to b)$ be either termial or empty}. We claim that, if the abstraction is well defined, then the following diagram is commutative:
|
|
\begin{equation}\label{exp goal}
|
|
% https://q.uiver.app/#q=WzAsMyxbMCwyLCIoKFleWClfe2EgXFxsZXEgYn0sIGEgXFx0byBiLCBcXHhpKSAiXSxbMCwwLCIoWCwgYSxmKSBcXHRpbWVzIChaLGMsIGgpIl0sWzIsMiwiKFkpIl0sWzEsMiwiKHUsIGMgXFxsYW5kIGEgXFxsZXEgYikiXSxbMCwyLCIoRXZfe1NldH0sRXZfXFxtYXRoY2Fse0h9KSIsMl0sWzEsMCwiKFxcaGF0e3V9LCBjIFxcbGVxIGEgXFx0byBiICApIiwyXV0=
|
|
\begin{tikzcd}
|
|
{(X, a,f) \times (Z,c, h)} && \\
|
|
\\
|
|
{((Y^X)_{a \leq b}, a \to b, \xi) } && {(Y)}
|
|
\arrow["{(\hat{u}, c \leq a \to b )}"', from=1-1, to=3-1]
|
|
\arrow["{(u, c \land a \leq b)}", from=1-1, to=3-3]
|
|
\arrow["{(Ev_{Set},Ev_\mathcal{H})}"', from=3-1, to=3-3]
|
|
\end{tikzcd}
|
|
\end{equation}
|
|
Now, commutativity at the level of $Set$ is ensured by universal property of $Y^X$ in $Set$ plus the coerence condition of $(Y^X)_{a \leq b}$ with respect to $a \to b$. Now, in $\mathcal{H}$ we have that $c \land a \leq b$ we have that $c\land a \leq b \iff c \leq a \to b$ so we have commutativity at the level of $\mathcal{H}$. It remains to check the well definition of the abstraction: let $Z \neq \emptyset$, then $h(m) \in \mathcal{H}(1_\mathcal{H}, c)$ for $m \in Z$, hence $1_\mathcal{H} \leq c$ and so, since $c \land a \leq b$, then $a \leq b$ and so $\hat{u} (m) \in (Y^X)_{a \leq b}$ wihch ensure well definition of abstraction arrows. Notice that uniqueness of abstraction follows directly form uniqueness of abstractions in $Set$ and $\mathcal{H}$. Thus $Cov(\mathcal{H})$ is a bicartesian cloed category.\\
|
|
Concerning $\Pi_2$, the proof is identical to \ref{completenesscomma} since the $\mathcal{H}$ level of the exponential object is the exponential object in $\mathcal{H}$ and so $\Pi_2$ is a bicartesian closed functor and we are done.
|
|
\end{proof}
|
|
|
|
\begin{definition}
|
|
Let $\mathcal{H}$ be an Heyting Algebra, then we call its Feryd cover the Frey-Heyting cover of $\mathcal{H}$
|
|
\end{definition}
|
|
\begin{definition}
|
|
We say that $\textbf{biCC}$ is the category with objects bicartesian closed categories and morphisms functors preserving the bicartesian structure up to isomorphism
|
|
\end{definition}
|
|
\begin{definition}[Global Set Functor]
|
|
Let $\mathcal{C}$ be a locally small category with terminal object $1_\mathcal{C}$. We define the global set functor as:
|
|
% https://q.uiver.app/#q=WzAsNixbMCwwLCJcXG1hdGhjYWx7Q30iXSxbMiwwLCJTZXQiXSxbMCwxLCJBIl0sWzAsMiwiQiJdLFsyLDEsIlxcR2FtbWEoQSk9IFxcbWF0aGNhbHtDfSgxX1xcbWF0aGNhbHtDfSxBKSJdLFsyLDIsIlxcR2FtbWEoQik9IFxcbWF0aGNhbHtDfSgxX1xcbWF0aGNhbHtDfSxCKSJdLFswLDEsIlxcR2FtbWEoLSkiXSxbMiwzXSxbNCw1LCJcXEdhbW1hKGYpPSBcXG1hdGhjYWx7Q30oMV9cXG1hdGhjYWx7Q30sZikiXSxbMiw0LCJcXEdhbW1hKC0pIiwwLHsic3R5bGUiOnsidGFpbCI6eyJuYW1lIjoibWFwcyB0byJ9fX1dLFs3LDgsIiIsMCx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sImxldmVsIjoxLCJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtYXBzIHRvIn19fV1d
|
|
\[\begin{tikzcd}
|
|
{\mathcal{C}} && Set \\
|
|
A && {\Gamma(A)= \mathcal{C}(1_\mathcal{C},A)} \\
|
|
B && {\Gamma(B)= \mathcal{C}(1_\mathcal{C},B)}
|
|
\arrow["{\Gamma(-)}", from=1-1, to=1-3]
|
|
\arrow["{\Gamma(-)}", maps to, from=2-1, to=2-3]
|
|
\arrow[""{name=0, anchor=center, inner sep=0}, from=2-1, to=3-1]
|
|
\arrow[""{name=1, anchor=center, inner sep=0}, "{\Gamma(f)= \mathcal{C}(1_\mathcal{C},f)}", from=2-3, to=3-3]
|
|
\arrow[between={0.2}{0.8}, maps to, from=0, to=1]
|
|
\end{tikzcd}\]
|
|
\end{definition}
|
|
\begin{lemma}
|
|
Let $\mathcal{C}$ be a category in \textbf{biCC}, then its freyd cover $Cov(\mathcal{C})$ is again in \textbf{biCC}
|
|
\end{lemma}
|
|
\begin{proof}
|
|
We want to generalize contstruction in \ref{coverheyting} for arbitrary bicartesian closed category. We mimic the construction in \cite{angiuli2022canonicity}. Let $\mathcal{C}$ be a bicartesian closed category and let $(X,A,f)$ and $(Y,B,g)$, we want to construct the exponential object $(Y,B,g)^{(X,A,g)}$. As in \ref{coverheyting} we expect the exponential to mimic $(Y^X,B^C,h)$ where $h: Y^X \to \Gamma(B^C)$; however we know that $(Y^X)$ cannot be the rigth $Set$-component of the exponential. morevoer the constuction of $h$ in this situation is slithely more complex. Let's begin by noticing that the global set functor is a product preserving functor and that, since $\mathcal{C}$ is CC, in $\mathcal{C}$ there is the exponential object $B^A$ with evaluation $ev_\mathcal{C}: B^A \times B \to A$. We can form the composition :
|
|
\begin{equation}
|
|
u : \Gamma(A) \times \Gamma (B^A) \xrightarrow{\cong} \Gamma ( A \times B^A) \xrightarrow{\Gamma(ev_\mathcal{C})} \Gamma(B)
|
|
\end{equation}
|
|
Now, we take the abstraction of $u$ in $Set$, $\hat{u}: \Gamma(A) \to \Gamma(B)^{\Gamma(A)}$. Consider now the following pullback diagram:
|
|
% https://q.uiver.app/#q=WzAsNSxbMCwwLCJIIl0sWzAsMiwiXFxHYW1tYShCXkEpIl0sWzEsMywiXFxHYW1tYShCKV57XFxHYW1tYShBKX0iXSxbMiwyLCJcXEdhbW1hKEQpXlgiXSxbMiwwLCJZXlgiXSxbMCwxLCJwXzEiLDJdLFsxLDIsIlxcaGF0e3V9IiwyXSxbMiwzLCIoXFxHYW1tYShEKSleZiIsMl0sWzEsM10sWzQsMywiZ15YIl0sWzAsNCwicF8yIl0sWzAsMywiIiwwLHsic3R5bGUiOnsibmFtZSI6ImNvcm5lciJ9fV1d
|
|
\[\begin{tikzcd}
|
|
H && {Y^X} \\
|
|
\\
|
|
{\Gamma(B^A)} && {\Gamma(B)^X} \\
|
|
& {\Gamma(B)^{\Gamma(A)}}
|
|
\arrow["{p_2}", from=1-1, to=1-3]
|
|
\arrow["{p_1}"', from=1-1, to=3-1]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=1-1, to=3-3]
|
|
\arrow["{g^X}", from=1-3, to=3-3]
|
|
\arrow[from=3-1, to=3-3]
|
|
\arrow["{\hat{u}}"', from=3-1, to=4-2]
|
|
\arrow["{(\Gamma(B))^f}"', from=4-2, to=3-3]
|
|
\end{tikzcd}\]
|
|
Where $(\Gamma (D))^f : \Gamma(B)^{\Gamma(A)} \to \Gamma(D)^X$ is defined by $\mu \to \mu \circ f$ and $g^X: Y^X \to \Gamma(B)$ is defined by $\omega \to g \circ \omega$. We claim $(H,B^A, h := p_1)$ to be the exponenetial object $(X,A,f)^{(Y,B,g)}$. We will prove this by checking that, provided $E = (Z,E,k)$, we have a natural ismoporphism $Cov(\mathcal{C})(E \times A, B)\cong Cov(\mathcal{C})(E, B^A)$\footnote{here we make an abuse of notation setting $A:= (X,A,f),B:=(Y,B,g)$}. Let $(\psi_{Set},\psi_{\mathcal{C}})$ in $Cov(\mathcal{C})(E \times A, B)$ then, $\psi_{Set}: Z \times X \to Y$ and $\psi_\mathcal{C}: E \times A \to B$. Thus, using that $Set$ and $\mathcal{C}$ are cartesian closed, we can take the abstractions $\hat{\psi}_{Set}: Z \to Y^X$ and $\hat{\psi}_{C}: E \to B^A$. Now, consider the following diagram:
|
|
% https://q.uiver.app/#q=WzAsNixbMSwxLCJIIl0sWzEsMywiXFxHYW1tYShCXkEpIl0sWzMsMywiXFxHYW1tYShEKV5YIl0sWzMsMSwiWV5YIl0sWzAsMCwiWiJdLFswLDIsIlxcR2FtbWEoRSkiXSxbMCwxLCJwXzEiLDJdLFsxLDIsIlxcR2FtbWEoRCleZiBcXGNpcmMgXFxoYXR7dX0iLDJdLFszLDIsImdeWCJdLFswLDMsInBfMiJdLFswLDIsIiIsMCx7InN0eWxlIjp7Im5hbWUiOiJjb3JuZXIifX1dLFs0LDMsIlxcaGF0e1xccHNpfV97U2V0fSIsMCx7ImN1cnZlIjotMn1dLFs0LDUsImsiLDJdLFs1LDEsIlxcR2FtbWEoXFxoYXR7XFxwc2l9X3tcXG1hdGhjYWx7Q319KSIsMl0sWzQsMCwiXFxleGlzdCAhIFxccGhpX3tTZXR9IiwxXV0=
|
|
\[\begin{tikzcd}
|
|
Z &&& \\
|
|
& H && {Y^X} \\
|
|
{\Gamma(E)} \\
|
|
& {\Gamma(B^A)} && {\Gamma(D)^X}
|
|
\arrow["{\exists ! \phi_{Set}}"{description}, from=1-1, to=2-2]
|
|
\arrow["{\hat{\psi}_{Set}}", curve={height=-12pt}, from=1-1, to=2-4]
|
|
\arrow["k"', from=1-1, to=3-1]
|
|
\arrow["{p_2}", from=2-2, to=2-4]
|
|
\arrow["{p_1}"', from=2-2, to=4-2]
|
|
\arrow["\lrcorner"{anchor=center, pos=0.125}, draw=none, from=2-2, to=4-4]
|
|
\arrow["{g^X}", from=2-4, to=4-4]
|
|
\arrow["{\Gamma(\hat{\psi}_{\mathcal{C}})}"', from=3-1, to=4-2]
|
|
\arrow["{\Gamma(D)^f \circ \hat{u}}"', from=4-2, to=4-4]
|
|
\end{tikzcd}\]
|
|
|
|
\end{proof}
|
|
\begin{proposition}
|
|
The Freyd Cover of a bicartesian closed category extend to an endofunctor
|
|
% https://q.uiver.app/#q=WzAsOCxbMCwwLCJcXHRleHRiZntiQ0N9Il0sWzIsMCwiXFx0ZXh0YmZ7YkNDfSJdLFswLDEsIlxcbWF0aGNhbHtBfSJdLFsyLDEsIkNvdihcXG1hdGhjYWx7QX0pIl0sWzAsMiwiXFxtYXRoY2Fse0J9Il0sWzIsMiwiQ292KFxcbWF0aGNhbHtCfSkiXSxbMywxLCIoWCxBLGYpIl0sWzMsMiwiKFgsIEZBLCBGZikiXSxbMCwxLCJDb3YoLSkiXSxbMiw0LCJGIiwyXSxbMyw1LCJDbyB2KEYpIl0sWzYsNywiQ292KEYpIl0sWzksMTAsIkNvdigtKSIsMCx7InNob3J0ZW4iOnsic291cmNlIjoyMCwidGFyZ2V0IjoyMH0sImxldmVsIjoxLCJzdHlsZSI6eyJ0YWlsIjp7Im5hbWUiOiJtYXBzIHRvIn19fV1d
|
|
\[\begin{tikzcd}
|
|
{\textbf{biCC}} && {\textbf{biCC}} & \\
|
|
{\mathcal{A}} && {Cov(\mathcal{A})} & {(X,A,f)} \\
|
|
{\mathcal{B}} && {Cov(\mathcal{B})} & {(X, FA, Ff)}
|
|
\arrow["{Cov(-)}", from=1-1, to=1-3]
|
|
\arrow[""{name=0, anchor=center, inner sep=0}, "F"', from=2-1, to=3-1]
|
|
\arrow[""{name=1, anchor=center, inner sep=0}, "{Co v(F)}", from=2-3, to=3-3]
|
|
\arrow["{Cov(F)}", from=2-4, to=3-4]
|
|
\arrow["{Cov(-)}", between={0.2}{0.8}, maps to, from=0, to=1]
|
|
\end{tikzcd}\]
|
|
we can check that the external square commutes using unicity of abstraction so whe check that $Ev_{Set}\Gamma(D)^f \hat{u} \Gamma()$
|
|
\end{proposition}
|
|
|
|
|
|
|
|
\printbibliography
|
|
\end{document} |