generated from nerf/texTemplate
handed in version (minus signature and burocracy stuff)
This commit is contained in:
parent
666b13385c
commit
88b294c767
13 changed files with 768 additions and 299 deletions
2
.gitignore
vendored
2
.gitignore
vendored
|
|
@ -308,6 +308,6 @@ TSWLatexianTemp*
|
||||||
|
|
||||||
# Nix buid output
|
# Nix buid output
|
||||||
/result
|
/result
|
||||||
|
/src/Unterschrift_dennis.png
|
||||||
# language correction
|
# language correction
|
||||||
.aspell.*
|
.aspell.*
|
||||||
|
|
|
||||||
14
src/Main.tex
14
src/Main.tex
|
|
@ -5,7 +5,7 @@
|
||||||
\Subject{see title}
|
\Subject{see title}
|
||||||
\Keywords{keyword}
|
\Keywords{keyword}
|
||||||
\end{filecontents*}
|
\end{filecontents*}
|
||||||
\documentclass[DIV=calc,fontsize=12pt,draft=true]{scrartcl}
|
\documentclass[DIV=calc,fontsize=12pt]{scrartcl}
|
||||||
\usepackage[a-2b,mathxmp]{pdfx}[2018/12/22]
|
\usepackage[a-2b,mathxmp]{pdfx}[2018/12/22]
|
||||||
%\usepackage{pdfmanagement-testphase}
|
%\usepackage{pdfmanagement-testphase}
|
||||||
%\DeclareDocumentMetadata{
|
%\DeclareDocumentMetadata{
|
||||||
|
|
@ -71,6 +71,7 @@
|
||||||
\newtheorem{notation}[theorem]{Notation}
|
\newtheorem{notation}[theorem]{Notation}
|
||||||
\theoremstyle{remark}
|
\theoremstyle{remark}
|
||||||
\newtheorem{remark}[theorem]{Remark}
|
\newtheorem{remark}[theorem]{Remark}
|
||||||
|
\newtheorem*{remark*}{Remark}
|
||||||
|
|
||||||
\newcommand*{\fancyrefthmlabelprefix}{thm}
|
\newcommand*{\fancyrefthmlabelprefix}{thm}
|
||||||
\newcommand*{\fancyreflemlabelprefix}{lem}
|
\newcommand*{\fancyreflemlabelprefix}{lem}
|
||||||
|
|
@ -175,16 +176,21 @@
|
||||||
|
|
||||||
|
|
||||||
% \AtBeginDocument{\DeclareMathSymbol{→}{\mathbin}{symbols}{"21}} % I don't know why this does not work
|
% \AtBeginDocument{\DeclareMathSymbol{→}{\mathbin}{symbols}{"21}} % I don't know why this does not work
|
||||||
\title{A uniform equivariant model for cubical Type Theory}
|
\title{A Uniform Equivariant Model for Cubical Type Theory}
|
||||||
\author{Dennis Frieberg}
|
\author{Dennis Frieberg}
|
||||||
\date{\today}
|
\date{2024-08-09}
|
||||||
\begin{document}
|
\begin{document}
|
||||||
\maketitle
|
\maketitle
|
||||||
|
\newpage
|
||||||
|
% \subfile{Preliminaries/erklaerung}
|
||||||
|
\newpage
|
||||||
\tableofcontents
|
\tableofcontents
|
||||||
\newpage
|
\newpage
|
||||||
|
\subfile{Preliminaries/Introduction}
|
||||||
|
\newpage
|
||||||
\subfile{Preliminaries/Preliminaries}
|
\subfile{Preliminaries/Preliminaries}
|
||||||
|
\newpage
|
||||||
\subfile{main/Mainpart}
|
\subfile{main/Mainpart}
|
||||||
\listoftodos
|
|
||||||
% \printindex
|
% \printindex
|
||||||
\printbibliography
|
\printbibliography
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -5,7 +5,7 @@
|
||||||
\newcommand*{\LF}{\ensuremath{\mathrm{L}}\xspace}
|
\newcommand*{\LF}{\ensuremath{\mathrm{L}}\xspace}
|
||||||
\newcommand*{\RF}{\ensuremath{\mathrm{R}}\xspace}
|
\newcommand*{\RF}{\ensuremath{\mathrm{R}}\xspace}
|
||||||
\renewcommand*{\d}{\ensuremath{\mathbf{d}}\xspace}
|
\renewcommand*{\d}{\ensuremath{\mathbf{d}}\xspace}
|
||||||
\section{Algebraic Weak Factorization Systems}
|
\subsection{Algebraic Weak Factorization Systems}
|
||||||
In this section, we will revisit the basic ideas of algebraic weak factorization systems (awfs).
|
In this section, we will revisit the basic ideas of algebraic weak factorization systems (awfs).
|
||||||
We won't use them much explicitly through this paper, but we need one major result about them.
|
We won't use them much explicitly through this paper, but we need one major result about them.
|
||||||
Also, while we don't talk about them explicitly, their ideas permeate through most of the arguments.
|
Also, while we don't talk about them explicitly, their ideas permeate through most of the arguments.
|
||||||
|
|
|
||||||
|
|
@ -8,15 +8,15 @@
|
||||||
%TODO connections
|
%TODO connections
|
||||||
|
|
||||||
The first question we need to answer, what site to consider. In the simplicial world there is more
|
The first question we need to answer, what site to consider. In the simplicial world there is more
|
||||||
or less a consesus, what exactly the site should be. In the cubical world there are multiple models
|
or less a consensus, what exactly the site should be. In the cubical world there are multiple models
|
||||||
with slightly different sites. Our main protagonist will be the cartesian model, but we will also
|
with slightly different sites. Our main protagonist will be the Cartesian model, but we will also
|
||||||
need to introduce the Dedekind model, as it will appear in an argument later. For a comperative
|
need to introduce the Dedekind model, as it will appear in an argument later. For a comparative
|
||||||
analysis we direct the reader to \cite{cavalloUnifyingCubicalModels2016} and \cite{ABCHFL}.
|
analysis we direct the reader to \cite{cavalloUnifyingCubicalModels2016} and \cite{ABCHFL}.
|
||||||
|
|
||||||
\subsubsection{Cartesian cubes}
|
\subsubsection{Cartesian cubes}
|
||||||
|
|
||||||
The most uniform description is probably in form of Lawvere theories,
|
The most uniform description is probably in form of Lawvere theories,
|
||||||
but our site has a more direct description \cite{mathematicalsciencesresearchinstitutemsriEquivariantUniformKan2020}.
|
but our site has a more direct description \cite{riehlVid}.
|
||||||
|
|
||||||
\begin{definition}
|
\begin{definition}
|
||||||
Let \(\mathrm{FinSet}\) be the category whose objects are the subsets of \(ℕ\), of the form \(\{0,..,n\}\), for some
|
Let \(\mathrm{FinSet}\) be the category whose objects are the subsets of \(ℕ\), of the form \(\{0,..,n\}\), for some
|
||||||
|
|
@ -25,13 +25,13 @@ but our site has a more direct description \cite{mathematicalsciencesresearchins
|
||||||
|
|
||||||
\begin{remark}
|
\begin{remark}
|
||||||
Up to equivalence this is the category of finite sets. Choosing a skeleton will circumvent later size issues, but
|
Up to equivalence this is the category of finite sets. Choosing a skeleton will circumvent later size issues, but
|
||||||
for convenience we will pretend that these are finite sets and not always reindex our sets to have an initial segment
|
for convenience we will pretend that these are finite sets and not always re-index our sets to have an initial segment
|
||||||
of \(ℕ\).
|
of \(ℕ\).
|
||||||
\end{remark}
|
\end{remark}
|
||||||
|
|
||||||
\begin{definition}\label{def:cartCubeSet}
|
\begin{definition}\label{def:cartCubeSet}
|
||||||
Let \( □ ≔ {\mathrm{FinSet}\rlap{\raisebox{0.75ex}{\rotatebox{90}{*}}}\raisebox{-0.3ex}{\rotatebox{90}{*}}}^\mathsf{op}\)
|
Let \( □ ≔ {\mathrm{FinSet}\rlap{\raisebox{0.75ex}{\rotatebox{90}{*}}}\raisebox{-0.3ex}{\rotatebox{90}{*}}}^\mathsf{op}\)
|
||||||
the opposite category of double-pointed finite sets.
|
be the opposite category of double-pointed finite sets.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
An alternative definition would be
|
An alternative definition would be
|
||||||
|
|
@ -41,13 +41,13 @@ An alternative definition would be
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
\begin{remark}
|
\begin{remark}
|
||||||
As in light of \fref{def:cartCubeSet} and \fref{def:cartCubeTheory} we sometimes talk about morphisms
|
In light of \cref{def:cartCubeSet} and \cref{def:cartCubeTheory} we sometimes talk about morphisms
|
||||||
as functions \(X + 2 → Y + 2\) preserving both points in \(2\) or equivalently ordinary functions \(X → Y+2\).
|
as functions \(X + 2 → Y + 2\) preserving both points in \(2\) or equivalently ordinary functions \(X → Y+2\).
|
||||||
\end{remark}
|
\end{remark}
|
||||||
|
|
||||||
We will now spend some time exploring, why this might be viewed as the cube category.
|
We will now spend some time exploring, why this might be viewed as the cube category.
|
||||||
We write \(\{⊥|a,b,c|⊤\}\) for double pointed finite sets, where \(⊥\) and \(⊤\) are the
|
We write \(\{⊥|a,b,c|⊤\}\) for double pointed finite sets, where \(⊥\) and \(⊤\) are the
|
||||||
two distunguished points. A cube of dimension \(n\) is now interpreted as such a set
|
two distinguished points. A cube of dimension \(n\) is now interpreted as such a set
|
||||||
with \(n+2\) (\(n\) without the distinguished points) many elements. We think of these
|
with \(n+2\) (\(n\) without the distinguished points) many elements. We think of these
|
||||||
as dimension variables. We could for example think about the zero dimensional cube
|
as dimension variables. We could for example think about the zero dimensional cube
|
||||||
(a point) \(\{⊥|⊤\}\) and the 2 dimensional cube (a square) \(\{⊥|a,b|⊤\}\).
|
(a point) \(\{⊥|⊤\}\) and the 2 dimensional cube (a square) \(\{⊥|a,b|⊤\}\).
|
||||||
|
|
@ -57,13 +57,13 @@ also exactly what we get, a fitting map in \( \FinSetOp \) corresponds to a func
|
||||||
In the other direction we have four maps. These encode the corners. For example the corner “\((⊥,⊥)\)”
|
In the other direction we have four maps. These encode the corners. For example the corner “\((⊥,⊥)\)”
|
||||||
gets encode by sending \(a\) and \(b\) to \(⊥\).
|
gets encode by sending \(a\) and \(b\) to \(⊥\).
|
||||||
|
|
||||||
Lets increase the dimensions a bit and look at the maps from a 1 dimensional cube (a line segment)
|
Let us increase the dimensions a bit and look at the maps from a 1 dimensional cube (a line segment)
|
||||||
\(\{⊥|x|⊤\}\}\) into the square. These correspond to functions from \(\{a,b\} → \{⊥,x,⊤\}\). We
|
\(\{⊥|x|⊤\}\}\) into the square. These correspond to functions from \(\{a,b\} → \{⊥,x,⊤\}\). We
|
||||||
can think of this as a dimensional description of a line in a square. We have 2 dimensions in which
|
can think of this as a dimensional description of a line in a square. We have 2 dimensions in which
|
||||||
the line can move \(a\) and \(b\). And in this two dimennsions the line can either be constant (sending
|
the line can move \(a\) and \(b\). And in these two dimensions the line can either be constant (sending
|
||||||
this dimension to \(⊥\) or \(⊤\), or can advance along its dimension (sending the dimension to \(x\)).
|
this dimension to \(⊥\) or \(⊤\), or can advance along its dimension (sending the dimension to \(x\)).
|
||||||
So we get the degenerate corner points (as lines), by sending both of \(a\) and \(b\) to \(⊥\) or \(⊤\).
|
So we get the degenerate corner points (as lines), by sending both \(a\) and \(b\) to \(⊥\) or \(⊤\).
|
||||||
We get the for sides of the square by sending one of \(a\) or \(b\) to \(⊥\) or \(⊤\). The two sides
|
We get the four sides of the square by sending one of \(a\) or \(b\) to \(⊥\) or \(⊤\). The two sides
|
||||||
that run along the dimension \(a\) send \(a\) to \(x\).
|
that run along the dimension \(a\) send \(a\) to \(x\).
|
||||||
One function is left, sending both \(a\) and \(b\) to \(x\). This is the line that advances in both
|
One function is left, sending both \(a\) and \(b\) to \(x\). This is the line that advances in both
|
||||||
dimensions. Or in other words the diagonal.
|
dimensions. Or in other words the diagonal.
|
||||||
|
|
@ -73,7 +73,7 @@ dimensions. Or in other words the diagonal.
|
||||||
important later.
|
important later.
|
||||||
\end{remark}
|
\end{remark}
|
||||||
|
|
||||||
As we will need some of these element througout the document again we will give them names.
|
As we will need some of these element throughout the document again we will give them names.
|
||||||
\begin{definition}[Notation for cubes]\label{def:cubeNotation}
|
\begin{definition}[Notation for cubes]\label{def:cubeNotation}
|
||||||
We call:
|
We call:
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
|
|
@ -87,14 +87,14 @@ As we will need some of these element througout the document again we will give
|
||||||
\begin{figure}
|
\begin{figure}
|
||||||
\centering
|
\centering
|
||||||
\includesvg[inkscapearea=nocrop,inkscapedpi=500]{figures/square_example_picture.svg}
|
\includesvg[inkscapearea=nocrop,inkscapedpi=500]{figures/square_example_picture.svg}
|
||||||
\caption{A square with some lines maped into it}
|
\caption{A square with some lines mapped into it}
|
||||||
\todo[inline]{fix 0 to \(⊥\) and same for 1}
|
\todo[inline]{fix 0 to \(⊥\) and same for 1}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
|
|
||||||
Also while \(□\) is not a strict Reedy-category (as \(Δ\) is) it is almost, namely an Eilenberg-Zilber category.
|
Also while \(□\) is not a strict Reedy-category (as \(Δ\) is) it almost is, more precisely it is an Eilenberg-Zilber category.
|
||||||
So most of Reedy theory from the simplicial case can be salvaged. This will play an integral part in the
|
Most of Reedy theory from the simplicial case can be salvaged. This will play an integral part in the
|
||||||
prove that our model structure on \□ is equivalent to spaces.
|
proof that our model structure on \□ is equivalent to spaces.
|
||||||
|
|
||||||
\begin{definition}[generalized Reedy-category] %TODO add cite nlab
|
\begin{definition}[generalized Reedy-category] %TODO add cite nlab
|
||||||
A \emph{generalized Reedy category} is a category \C together with two
|
A \emph{generalized Reedy category} is a category \C together with two
|
||||||
|
|
@ -105,13 +105,13 @@ prove that our model structure on \□ is equivalent to spaces.
|
||||||
\item every non-isomorphism in \(\C_-\) lowers degree,
|
\item every non-isomorphism in \(\C_-\) lowers degree,
|
||||||
\item every isomorphism in \C preserves degree,
|
\item every isomorphism in \C preserves degree,
|
||||||
\item \(\C_+ ∩ \C_-\) is the core of \C
|
\item \(\C_+ ∩ \C_-\) is the core of \C
|
||||||
\item every morphism factors as a mapn in \(\C_-\) followed by a map in \(\C_+\), uniquely up
|
\item every morphism factors as a map in \(\C_-\) followed by a map in \(\C_+\), uniquely up
|
||||||
to isomorphism
|
to isomorphism
|
||||||
\item if \(f ∈ \C_-\) and \(θ\) is an isomorphism such that \(θf = f\), then \(θ = \id\)
|
\item if \(f ∈ \C_-\) and \(θ\) is an isomorphism such that \(θf = f\), then \(θ = \id\)
|
||||||
\end{enumerate}
|
\end{enumerate}
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
Which will be an important concept later, but in our special case we can do even better
|
This will be an important concept later, but in our special case we can do even better
|
||||||
|
|
||||||
\begin{definition}[Eilenberg-Zilber category] %TODO add cite nlab
|
\begin{definition}[Eilenberg-Zilber category] %TODO add cite nlab
|
||||||
An \emph{Eilenberg-Zilber category} or short \emph{EZ-category} is a small category \C
|
An \emph{Eilenberg-Zilber category} or short \emph{EZ-category} is a small category \C
|
||||||
|
|
@ -129,7 +129,15 @@ Which will be an important concept later, but in our special case we can do even
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
\begin{remark}
|
\begin{remark}
|
||||||
Cleary every EZ-category is a generalized Reedy category
|
Clearly every EZ-category is a generalized Reedy category
|
||||||
|
\end{remark}
|
||||||
|
|
||||||
|
\begin{remark}
|
||||||
|
A lot of homotopical construction one knows from Reedy categories can be carried out with EZ-categories.
|
||||||
|
A word of caution: if we try to do the usual Reedy style decomposition of a presheaf into
|
||||||
|
a cell-complex, such that the attached cells are boundary inclusions in the representables, we will fail.
|
||||||
|
Instead we need to consider all quotients of boundary inclusions in quotients of representables.
|
||||||
|
For more details see \cites{riehlTheoryPracticeReedy2014}{shulmanREEDYCATEGORIESTHEIR}{campionCubicalSitesEilenbergZilber2023}.
|
||||||
\end{remark}
|
\end{remark}
|
||||||
|
|
||||||
|
|
||||||
|
|
@ -149,7 +157,7 @@ Before we give a proof we will give a technical lemma about absolute pushouts of
|
||||||
be a diagram in a category \C of split epis such that, \(bc' = d_1'd_2\). Then it is already a pushout square.
|
be a diagram in a category \C of split epis such that, \(bc' = d_1'd_2\). Then it is already a pushout square.
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
We look at an arbitrary cocone
|
We look at an arbitrary co-cone
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
\begin{tikzcd}
|
\begin{tikzcd}
|
||||||
A \arrow[r, two heads, "b"] \arrow[d, two heads, "c"] & B \arrow[d, "e_1"] \\
|
A \arrow[r, two heads, "b"] \arrow[d, two heads, "c"] & B \arrow[d, "e_1"] \\
|
||||||
|
|
@ -164,10 +172,10 @@ Before we give a proof we will give a technical lemma about absolute pushouts of
|
||||||
C \arrow[r, "e_2"] & E
|
C \arrow[r, "e_2"] & E
|
||||||
\end{tikzcd}
|
\end{tikzcd}
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
We get our candidate map from \(e_1d_1' : D → E\). We need to show that it commuts with \(e_1\) and \(d_1\) as well as
|
We get our candidate map from \(e_1d_1' : D → E\). We need to show that it commutes with \(e_1\) and \(d_1\) as well as
|
||||||
\(e_2\) and \(d_2\). The second case \(e_1d_1'd_2 = e_2\) is directly obvious from the diagram.
|
\(e_2\) and \(d_2\). The second case \(e_1d_1'd_2 = e_2\) is immediately obvious from the diagram.
|
||||||
To check that \(e_1d_1'd_1 = e_1\) it is enough to check that \(be_1d_1'd_1 = be_1\), as \(b\) is epic. Which is a
|
To check that \(e_1d_1'd_1 = e_1\) it is enough to check that \(be_1d_1'd_1 = be_1\), as \(b\) is epic. Which is a
|
||||||
straight forward diagramm chase, if one adds all the undrawn arrwos to the diagram above. Since \(d_1\), are epic \(e_1d'_1\) is unique in fulfilling already one of the two conditions.
|
straight forward diagram chase, if one adds all the not drawn arrows to the diagram above. Since \(d_1\) are epic, \(e_1d'_1\) is unique in fulfilling already one of the two conditions.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
\begin{remark}
|
\begin{remark}
|
||||||
|
|
@ -186,23 +194,23 @@ As we will use the following statement multiple times in the proof we put it int
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Let \(f\) be an epi in \(□\). It is thus a monomorphism in \(\FinSet\). We construct a retraction
|
Let \(f\) be an epi in \(□\). It is thus a monomorphism in \(\FinSet\). We construct a retraction
|
||||||
\(g\) (that will be a split in \(□\)). Let \(g(x)\) by the unique pre image of \(f\) if it is not empty. If it is empty we choose
|
\(g\) that will be a split in \(□\). Let \(g(x)\) by the unique pre-image of \(f\) if it is not empty. If it is empty we choose
|
||||||
any element (for example \(⊥\)). It is trivial to verify that this is a retraction. And as \(f\) needs to
|
any element (for example \(⊥\)). It is trivial to verify that this is a retraction. As \(f\) needs to
|
||||||
preserve the destinguished points, \(g\) does to.
|
preserve the distinguished points, \(g\) does too.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
\begin{proof}[Proof of theorem \ref{thm:CisEZ}]
|
\begin{proof}[Proof of \cref{thm:CisEZ}]
|
||||||
Property \ref{EZ:1} follows from basic facts about surjectivity and injectivity between finite sets.
|
Property \ref{EZ:1} follows from basic facts about surjectivity and injectivity between finite sets.
|
||||||
Property \ref{EZ:2} needs us to find a (epi,mono) factorization in \(\FinSet\). This factorization
|
Property \ref{EZ:2} needs us to find a (epi,mono) factorization in \(\FinSet\). This factorization
|
||||||
can be obtained in the same way one would obtain it \(\Set\), by factoring an morphism through its image.
|
can be obtained in the same way one would obtain it \(\Set\), by factoring an morphism through its image.
|
||||||
It is straight forward to verify, that the distinguished points are preserved by those maps. And the
|
It is straight forward to verify, that the distinguished points are preserved by those maps. And the
|
||||||
that the epi (in \(□\)) splits follows from \ref{EZ:split}.
|
fact that the epi (in \(□\)) splits follows from \cref{EZ:split}.
|
||||||
|
|
||||||
For property \ref{EZ:3}, we only need find a pushout and splits of the form described in \ref{absolutePushout}.
|
For property \ref{EZ:3}, we only need find a pushout and splits of the form described in \cref{absolutePushout}.
|
||||||
So let \(c : A → C\) and \(b : A → B\) spilt epis. We will do this by
|
So let \(c : A → C\) and \(b : A → B\) split epis. We will do this by
|
||||||
constructing the dual digram in \(\FinSet\). We will keep the names for the morphisms. As pullbacks over non-empty diagrams
|
constructing the dual diagram in \(\FinSet\). We will keep the names for the morphisms. As pullbacks over nonempty diagrams
|
||||||
work in \(\FinSet\) like in \(\Set\) we can construct a pullback. Now we must construct the
|
work in \(\FinSet\) like in \(\Set\) we can construct a pullback. Now we must construct the
|
||||||
dotted arrows that satisfy the dual properties of lemma \ref{absolutePushout}.
|
dashed arrows that satisfy the dual properties of \cref{absolutePushout}.
|
||||||
|
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
\begin{tikzcd}
|
\begin{tikzcd}
|
||||||
|
|
@ -214,7 +222,7 @@ As we will use the following statement multiple times in the proof we put it int
|
||||||
their image to \(0\).
|
their image to \(0\).
|
||||||
We will show the required commutativity by case distinction
|
We will show the required commutativity by case distinction
|
||||||
Let \(x ∈ C\). Note that \(x ∈ \im c^*b\) if and only if \(c(x) ∈ \im b\) as this is a pullback diagram. Thus it is
|
Let \(x ∈ C\). Note that \(x ∈ \im c^*b\) if and only if \(c(x) ∈ \im b\) as this is a pullback diagram. Thus it is
|
||||||
immediatly clear that if \(x\) is not contained in \(\im c^*b\) that \((b^*c)(c^*b)'(x) = 0 = b'c(x)\). Let us turn to
|
immediately clear that if \(x\) is not contained in \(\im c^*b\) that \((b^*c)(c^*b)'(x) = 0 = b'c(x)\). Let us turn to
|
||||||
the case that \(x ∈ \im c^*b \). As restricted to those \(x\) the map \(c^*b\) is surjective it suffices to check
|
the case that \(x ∈ \im c^*b \). As restricted to those \(x\) the map \(c^*b\) is surjective it suffices to check
|
||||||
\( b'c(c^*b) = (b^*c)(c^*b)'(c^*b) \).
|
\( b'c(c^*b) = (b^*c)(c^*b)'(c^*b) \).
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
|
|
@ -222,27 +230,31 @@ As we will use the following statement multiple times in the proof we put it int
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
|
|
||||||
|
|
||||||
Thus the corresponding diagram in \(□\) fulfills the requirements of lemma \ref{absolutePushout}, and is thus
|
Therefore the corresponding diagram in \(□\) fulfills the requirements of \cref{absolutePushout}, and is thus
|
||||||
an absolute pushout square.
|
an absolute pushout square.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
Next we start looking at the presheaf topos on our cube category \(\hat{□}\).
|
Next we start looking at the presheaf topos on our cube category \(\□\).
|
||||||
We will recall some important concepts, and give some construtcion, that we will
|
We will recall some important concepts and give some constructions, that we will
|
||||||
use later. Also we introduce some notation.
|
use later. We also introduce some notation.
|
||||||
|
|
||||||
\begin{definition}[Notation for Cubical Sets]\label{def:notationCubeSets}
|
\begin{definition}[Notation for Cubical Sets]\label{def:notationCubeSets}
|
||||||
We fix the following notations for Cartesian cubical sets:
|
We fix the following notations for Cartesian cubical sets:
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item \(* ≔ \Yo{[0]}\)
|
\item \(* ≔ \Yo{[0]}\)
|
||||||
\item \(\I ≔ \Yo{[1]}\)
|
\item \(\I ≔ \Yo{[1]}\)
|
||||||
\item \(δ_k ≔ \Yo \mathrm{d}_k\)
|
\item \(δ_k ≔ \Yo \mathrm{d}_k\) with \(k ∈ \{0,1\}\)
|
||||||
|
\item \(δ ≔ ⟨\id_{\I},\id_{\I}⟩ : \I → \I × \I\)
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
|
|
||||||
\subsubsection{Dedekind cubes}
|
\subsubsection{Dedekind cubes}
|
||||||
We will also encounter the so called Dedekind cubes. There are also multiple ways to look at them. We will present
|
We will also encounter the so-called Dedekind cubes. As they are not in the focus
|
||||||
multiple definitions, but skip the equivalence proofs as they don't bear much inside into the subject.
|
of this discussion, we give the needed definitions, but omit most of the proofs of their
|
||||||
|
properties.
|
||||||
|
There are also multiple ways to look at them. We will present
|
||||||
|
multiple definitions, but skip the equivalence proofs as they don't bear much insight into the subject.
|
||||||
|
|
||||||
\begin{definition}\leavevmode
|
\begin{definition}\leavevmode
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
|
|
@ -260,22 +272,21 @@ multiple definitions, but skip the equivalence proofs as they don't bear much in
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
Unraveling this definition gives us a quite similar description to our description of Cartesian cubes.
|
Unraveling this definition gives us a quite similar description to our description of Cartesian cubes.
|
||||||
Let \(F\) be the functor that assigns to a set its free lattice. We have then as objects
|
Let \(F\) be the functor that assigns to a set its free lattice. We then have as objects
|
||||||
natural numbers (or up to equivalence finite sets). And again we will write elements of these as lower
|
natural numbers (or up to equivalence finite sets). And again we will write elements of these as lower
|
||||||
roman letters instead of natural numbers to keep the confusion between sets and their elements minimal.
|
roman letters instead of natural numbers to keep the confusion between sets and their elements minimal.
|
||||||
A morphism \(m → n\) is a function
|
A morphism \(m → n\) is a function
|
||||||
from \(n → F(m)\). This adds a few more degeneracy maps, but the general geometric intuition stays the
|
from \(n → F(m)\). This adds a few more degeneracy maps, but the general geometric intuition stays the
|
||||||
same. The elments of of an object are dimensions, and maps do give us for every dimension in the target
|
same. The elements of an object are dimensions, and maps do give us for every dimension in the target
|
||||||
a term, that describes the behaiviour of our domain in that particular direction. If we look at an
|
a term, that describes the behavior of our domain in that particular direction. If we look at an
|
||||||
example again one might ask what the difference is, between the new degeneracies map from a square
|
example again one might ask what the difference is, between the new degeneracies map from a square
|
||||||
to the interval in comparison to the old one. We can view these as degenrate squares where we map the top
|
to the interval in comparison to the old one. We can view these as degenerate squares where we map the top
|
||||||
and right (or bottom and left) side along the interval and the other to sides to \(⊥\) (or \(⊤\)).
|
and right (or bottom and left) side along the interval and the other to sides to \(⊥\) (or \(⊤\)).
|
||||||
This wasn't possible before and will make a drastic difference once we start considiring filling and
|
This wasn't possible before and will make a drastic difference once we start considering lifting problems.
|
||||||
composition problems.
|
|
||||||
|
|
||||||
\begin{figure}
|
\begin{figure}
|
||||||
\missingfigure{draw pictures for this}
|
\missingfigure{draw pictures for this}
|
||||||
\caption{A squre degenrated with a connection. The upper and right side are equal while the left and bottom side is degenrated to point.}
|
\caption{A square degenerated with a connection. The upper and right side are equal while the left and bottom side is degenerated to point.}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
\todo{add figure for \(2→2\) degeneracy map}
|
\todo{add figure for \(2→2\) degeneracy map}
|
||||||
|
|
@ -284,11 +295,11 @@ composition problems.
|
||||||
The Dedekind cubes are an EZ-category
|
The Dedekind cubes are an EZ-category
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
\begin{proof}[Proof sketch:]
|
\begin{proof}[Proof sketch:]
|
||||||
This can be proven by an analog argument as \fref{thm:CisEZ}
|
This can be proven by an analogous argument as \fref{thm:CisEZ}
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
If it is clear from the context we will use the notation from \fref{def:cubeNotation} and \fref{def:notationCubeSets} for
|
If it is clear from the context we will use the notation from \fref{def:cubeNotation} and \fref{def:notationCubeSets} for
|
||||||
the anologous objects of the Dedekind cubes.
|
the analogous objects of the Dedekind cubes.
|
||||||
|
|
||||||
\todo{think about if I want to write down the proof}
|
\todo{think about if I want to write down the proof}
|
||||||
|
|
||||||
|
|
|
||||||
66
src/Preliminaries/Introduction.tex
Normal file
66
src/Preliminaries/Introduction.tex
Normal file
|
|
@ -0,0 +1,66 @@
|
||||||
|
\documentclass[../Main.tex]{subfiles}
|
||||||
|
\begin{document}
|
||||||
|
\section{Introduction}
|
||||||
|
In recent years there has been a rise in interest in homotopy type theory, a form of dependent type theory
|
||||||
|
that treats identities as homotopies between the relevant objects. Notably there is an axiom
|
||||||
|
that establishes an equivalence between homotopy equivalences of two types and identities between
|
||||||
|
these types. The model structure that was built by Voevodsky to prove consistency of these axioms, is
|
||||||
|
built on simplicial sets, and the well known Kan-Quillen model structure\cite{kapulkinSimplicialModelUnivalent2021}.
|
||||||
|
One might even say that this is not only a homotopical version of type theory, but the language of
|
||||||
|
homotopy types. This aligns very well with interpretation, types are interpreted as fibrations.
|
||||||
|
But from a constructive view point this was not satisfying as parts of the interpretation were based
|
||||||
|
on classical logic. A bit later it was shown that this model inherently needs some classical principles
|
||||||
|
\cite{bezemNonConstructivityKanSimplicial2015}.
|
||||||
|
|
||||||
|
One of the approaches to get a constructive model was to go over to cubical models, the first of these
|
||||||
|
is due to Bezem, Coquand, and Huber \cite{bezemModelTypeTheory2014}. From there different variants
|
||||||
|
of cubical models where considered \cites{CCHM,angiuliCartesianCubicalComputational2018a,coquandHigherInductiveTypes2018}
|
||||||
|
one of them the Cartesian cubes \cite{awodeyCubicalModelHomotopy2018}. These are all different model
|
||||||
|
construction with slightly different attached type theories. There happened a lot of work to unify
|
||||||
|
some of these constructions \cite{ABCHFL}.
|
||||||
|
|
||||||
|
It is not at all clear that these give rise to model structures, but also not very surprising considering
|
||||||
|
the languages from which these are build try to capture homotopical notions. Now one might ask if
|
||||||
|
these induced homotopy theories are again equivalent to the original Kan-Quillen model structure.
|
||||||
|
For this we have a multiple negative results. These results are not well documented and the
|
||||||
|
reference I could find is on this mailing list \cite{QuillenModelStructure}. For the model structure
|
||||||
|
induced on the Dedekind cubes this question remains an open. The equivariant model structure on Cartesian
|
||||||
|
cubes discussed in this thesis is the
|
||||||
|
first construction for which this equivalence is known. A little later Cavallo and Sattler found
|
||||||
|
that the in the case with only one connection the equivalence to spaces can also be shown
|
||||||
|
\cite{cavalloRelativeEleganceCartesian2022}.
|
||||||
|
|
||||||
|
This thesis gives a proof that the uniform equivariant model of cubical type theory is equivalent to spaces.
|
||||||
|
This model came out of the joint work of Awodey, Cavallo, Coquand, Riehl, and Sattler. The thesis
|
||||||
|
is split in three parts, the first part are short introductions to topics of category theory
|
||||||
|
that one might not be familiar with. The reader acquainted with these might safely skip them.
|
||||||
|
The second part introduces the main object, the topos \(\□\), and the equivariant premodel structure on it.
|
||||||
|
It then continues by constructing universes for those fibrations, and uses them to prove that the premodel
|
||||||
|
structure is indeed a model structure. The third part shows the equivalence of this model structure to spaces.
|
||||||
|
|
||||||
|
In section two we first describe the site and afterwards the equivariant premodel structure.
|
||||||
|
We spend then most of the section with the construction of fibrant universes. This mostly follows
|
||||||
|
\cite{awodeyCartesianCubicalModel2023}. The main idea of this argument is to internalize
|
||||||
|
the structure of the algebraic factorization system, attached to the fibrations. These
|
||||||
|
are called classifying types. These can then be used to extract
|
||||||
|
universes from Hofmann-Streicher universes.
|
||||||
|
|
||||||
|
In section three we show equivalence to spaces and follow the argument sketched in
|
||||||
|
\cite{riehlVid}. To compare the simplex category \(Δ\) to the Cartesian cubes \(□\), we
|
||||||
|
pass through the Dedekind cubes. We establish a pair of left Quillen functors that
|
||||||
|
induce an equivalence of the desired homotopy categories. An important fragment of the
|
||||||
|
proof was laid out in \cite{sattlerIdempotentCompletionCubes2019}.
|
||||||
|
|
||||||
|
When this project started there was no written account on this model, and I tried to remedy
|
||||||
|
this fact.
|
||||||
|
So the content is mainly based on a talk given by Riehl \cite{riehlVid}, the account about
|
||||||
|
premodel structures in \cite[Section 3]{cavalloRelativeEleganceCartesian2022}, and universe
|
||||||
|
construction techniques from \cite{awodeyCartesianCubicalModel2023}. Shortly before this project
|
||||||
|
was finished, an extensive written report on this subject was released by the original creators
|
||||||
|
of this model structure \cite{solution}. I changed some formulations in the universe construction
|
||||||
|
to highlight the similarities in the argument. For example there are now explicit mentions
|
||||||
|
of cubical species in the argument. We also verify an older argument for the equivalence to
|
||||||
|
spaces that is no longer present in \cite{solution} in this form.
|
||||||
|
|
||||||
|
|
||||||
|
\end{document}
|
||||||
|
|
@ -1,16 +1,16 @@
|
||||||
\documentclass[../Main.tex]{subfiles}
|
\documentclass[../Main.tex]{subfiles}
|
||||||
\begin{document}
|
\begin{document}
|
||||||
\section{Leibniz Construction}
|
\section{Leibniz Construction}
|
||||||
We will see use a well know construction in homotopy theory, to
|
We will use a well-know construction in homotopy theory to
|
||||||
elegantly construct a lot of interesting objects, the Leibniz construction.
|
elegantly construct a lot of interesting objects, the Leibniz construction.
|
||||||
This section will mostly give a definition and some examples to get familiar with this construction.
|
This section will mostly give a definition and some examples to get familiar with this construction.
|
||||||
If the reader is already familiar with it, they might skip this section without any problems.
|
If the reader is already familiar with it, they might skip this section without any problems.
|
||||||
We start by giving the definition.
|
We start by giving the definition.
|
||||||
\begin{definition}[Leibniz Construction]
|
\begin{definition}[Leibniz Construction]
|
||||||
Let \(\A\), \(\B\) and \(\C\) be categories and \(\C\) has finite pushouts. Let \(⊗ : \A × \B → \C \) be a bifunctor.
|
Let \(\A\), \(\B\) and \(\C\) be categories and \(\C\) have finite pushouts. Let \(⊗ : \A × \B → \C \) be a bifunctor.
|
||||||
Then we define the \emph{Leibniz Construction} \(\⊗ : \arr{\A} × \arr{\B} → \arr{\C}\) to be the functor
|
Then we define the \emph{Leibniz Construction} \(\⊗ : \arr{\A} × \arr{\B} → \arr{\C}\) to be the functor
|
||||||
that sends \(f : A → A' \) in \(\A\) and
|
that sends \(f : A → A' \) in \(\A\) and
|
||||||
\( g : B → B' \) in \(\B\), to \( f \⊗ g \) as defined as in the following diagram.
|
\( g : B → B' \) in \(\B\), to \( f \⊗ g \) as defined via the following diagram.
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
\begin{tikzcd}
|
\begin{tikzcd}
|
||||||
A ⊗ B \arrow[r, "f ⊗ \id"] \arrow[d, "\id ⊗ g"] \arrow[dr, phantom, "\ulcorner", very near end] & A' ⊗ \mathrlap{B} \phantom{A'} \arrow[ddr, bend left, "\id ⊗ g"] \arrow[d] & \\
|
A ⊗ B \arrow[r, "f ⊗ \id"] \arrow[d, "\id ⊗ g"] \arrow[dr, phantom, "\ulcorner", very near end] & A' ⊗ \mathrlap{B} \phantom{A'} \arrow[ddr, bend left, "\id ⊗ g"] \arrow[d] & \\
|
||||||
|
|
@ -18,16 +18,16 @@ We start by giving the definition.
|
||||||
& & A' ⊗ B'
|
& & A' ⊗ B'
|
||||||
\end{tikzcd}
|
\end{tikzcd}
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
If \(⊗\) is the tensor functor of a monoidal category we also call it the \emph{Leibniz product} or \emph{pushout-product}. If \(⊗\) is
|
If \(⊗\) is the tensor functor of a monoidal category, we also call it the \emph{Leibniz product} or \emph{pushout-product}. If \(⊗\) is
|
||||||
the functor application functor we also call it the \emph{Leibniz application}.
|
the functor application functor, we also call it the \emph{Leibniz application}.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
The following examples are true for any category of nice spaces, we will state them for simplicial sets as the reader is probably
|
The following examples are true for any category of nice spaces. We will state them for simplicial sets as the reader is probably
|
||||||
familiar with them.
|
familiar with them.
|
||||||
|
|
||||||
\begin{example}\label{ex:leib:prism}
|
\begin{example}\label{a}
|
||||||
Let \(δ_k : * → Δ^1\) for \(k ∈ {0,1}\) be one of the endpoint inclusions into the interval and \(i : \∂ Δ^n → Δ^n\) the boundary
|
Let \(δ_k : * → Δ^1\) for \(k ∈ \{0,1\}\) be one of the endpoint inclusions into the interval and \(i : \∂ Δ^n → Δ^n\) the boundary
|
||||||
inclusion of the \(n\)-simplex, then \(δ_k \× i\) is the inclusion of a prism without its interior and one cap, into the prism.
|
inclusion of the \(n\)-simplex. Then \(δ_k \× i\) is the inclusion of a prism without its interior and one cap into the prism.
|
||||||
\end{example}
|
\end{example}
|
||||||
This gives us a description of a possible set of generating trivial cofibrations. This will be an ongoing theme.
|
This gives us a description of a possible set of generating trivial cofibrations. This will be an ongoing theme.
|
||||||
We can even observe something stronger. If we would replace the boundary inclusion
|
We can even observe something stronger. If we would replace the boundary inclusion
|
||||||
|
|
@ -39,15 +39,14 @@ without a cap and its interior into the cylinder.
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
\begin{observation}
|
\begin{observation}
|
||||||
If \(f\) and \(g\) are cofibrations then \(f \× g\) is too. If one of them is a trivial cofibration then so is \(f \× g\).
|
If \(f\) and \(g\) are cofibrations then \(f \× g\) is too. If \(f\) or \(g\) is a trivial cofibration, then so is \(f \× g\).
|
||||||
\end{observation}
|
\end{observation}
|
||||||
This has far reaching consequences, and one can define the notion of a monoidal model category where this are one of the axioms
|
This has far reaching consequences and one can define the notion of a monoidal model category where this one of the axioms
|
||||||
for the tensor functor. This axioms basically states that the tensor product behaves homotopicaly. For more
|
for the tensor functor. This axiom basically states that the tensor product behaves homotopicaly. For more
|
||||||
detail see \cite{hoveyModelCategories2007}. We are not going to need much of this theory explicitly. But it is worthy to note
|
detail see \cite{hoveyModelCategories2007}. We are not going to need much of this theory explicitly. But it is worthy noting
|
||||||
that all examples of model categories that we are going to encouter are of this form.
|
that all examples of model categories that we are going to encounter are of this form.
|
||||||
|
|
||||||
|
We will also encounter basically the same construction as \ref{a} in another way. We can also get the Cylinder object
|
||||||
We will also encouter the basically same construction as \cref{ex:leib:prism} in another way. We can also get the Cylinder object
|
|
||||||
functorialy in \Δ, such that the cap inclusions are natural transformations.
|
functorialy in \Δ, such that the cap inclusions are natural transformations.
|
||||||
We can also get the inclusion the Leibniz product produces in a natural manner via the Leibniz application.
|
We can also get the inclusion the Leibniz product produces in a natural manner via the Leibniz application.
|
||||||
|
|
||||||
|
|
@ -56,7 +55,7 @@ We can also get the inclusion the Leibniz product produces in a natural manner
|
||||||
\( F @ x ≔ F(x)\) the functor application functor. Let \(\I × (−)\) be the functor that sends \(X\) to its cylinder object (also known as the
|
\( F @ x ≔ F(x)\) the functor application functor. Let \(\I × (−)\) be the functor that sends \(X\) to its cylinder object (also known as the
|
||||||
product with the interval).
|
product with the interval).
|
||||||
Let be one of the inclusions \( δ_k : \Id → \I ⊗ (−) \), the natural transformation that embeds the space in one of the cylinder caps.
|
Let be one of the inclusions \( δ_k : \Id → \I ⊗ (−) \), the natural transformation that embeds the space in one of the cylinder caps.
|
||||||
Let \( \∂ X → X \) be the boundery inclusion of \(X\).
|
Let \( \∂ X → X \) be the boundary inclusion of \(X\).
|
||||||
Then \( δ_k \widehat{@} (∂X → X) \) is the filling of a cylinder with one base surface of shape \(X\).
|
Then \( δ_k \widehat{@} (∂X → X) \) is the filling of a cylinder with one base surface of shape \(X\).
|
||||||
\end{example}
|
\end{example}
|
||||||
This kind of construction will later play an important role in the construction of our desired model categories.
|
This kind of construction will later play an important role in the construction of our desired model categories.
|
||||||
|
|
@ -64,13 +63,13 @@ And as we will constructions like this more often we add a bit of notation for i
|
||||||
|
|
||||||
\begin{notation}
|
\begin{notation}
|
||||||
Let \(⊗ : \A × \B → \C\) be a bifunctor, \(A\) be an object of \A, \(F : \B → \C\) be a functor , and let \(η : F ⇒ A ⊗ (−)\)
|
Let \(⊗ : \A × \B → \C\) be a bifunctor, \(A\) be an object of \A, \(F : \B → \C\) be a functor , and let \(η : F ⇒ A ⊗ (−)\)
|
||||||
be a nutral transformation. We write \(η \⊗ (−) ≔ (η ⊗ (−)) \widehat{@} (−)\).
|
be a natural transformation. We write \(η \⊗ (−) ≔ (η ⊗ (−)) \widehat{@} (−)\).
|
||||||
\end{notation}
|
\end{notation}
|
||||||
|
|
||||||
Here is a property that we will exploit fairly often.
|
Here is a property that we will exploit fairly often.
|
||||||
\begin{proposition}\label{rem:leibniz:adhesive}
|
\begin{proposition}\label{rem:leibniz:adhesive}
|
||||||
Since every topos is adhesive \cite{lackAdhesiveQuasiadhesiveCategories2005}, the pushout-product and the
|
Since every topos is adhesive \cite{lackAdhesiveQuasiadhesiveCategories2005}, the pushout-product and the
|
||||||
Leibniz application of \(A × (−)\), are stable under monomorhpisms in every topos.
|
Leibniz application of \(A × (−)\), are stable under monomorphisms in every topos.
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
|
|
||||||
The Leibniz construction has a dual construction, the Leibniz pullback construction
|
The Leibniz construction has a dual construction, the Leibniz pullback construction
|
||||||
|
|
@ -106,11 +105,11 @@ The Leibniz construction has a dual construction, the Leibniz pullback construct
|
||||||
Analog to the notation above we introduce the following notation
|
Analog to the notation above we introduce the following notation
|
||||||
\begin{notation}
|
\begin{notation}
|
||||||
Let \(⊗ : \A × \B → \C\) be a bifunctor, \(A\) be an object of \A, \(F : \B → \C\) be a functor , and let \(η : F ⇒ A ⊗ (−)\)
|
Let \(⊗ : \A × \B → \C\) be a bifunctor, \(A\) be an object of \A, \(F : \B → \C\) be a functor , and let \(η : F ⇒ A ⊗ (−)\)
|
||||||
be a nutral transformation. We write \(η \widehat⊗ (−) ≔ (η ⊗ (−)) \widehat{@} (−)\). As it is common in the literature we
|
be a natural transformation. We write \(η \widehat⊗ (−) ≔ (η ⊗ (−)) \widehat{@} (−)\). As it is common in the literature we
|
||||||
also write for the special case \(A⊗ (−) = (−)^A\), the following \(η ⇒ (−) ≔ η \widecheck⊗ (−)\).
|
also write for the special case \(A⊗ (−) = (−)^A\), the following \(η ⇒ (−) ≔ η \widecheck⊗ (−)\).
|
||||||
\end{notation}
|
\end{notation}
|
||||||
|
|
||||||
Dualy to our observation above it will be a theme that the pullback-power sends fibrations to trivial fibrations.
|
Dual to our observation above it will be a theme that the pullback-power sends fibrations to trivial fibrations.
|
||||||
Or more formally:
|
Or more formally:
|
||||||
\begin{lemma}[{\cite[Lemma 4.10]{riehlTheoryPracticeReedy2014}}]
|
\begin{lemma}[{\cite[Lemma 4.10]{riehlTheoryPracticeReedy2014}}]
|
||||||
There is an adjunction \({η \× (−) ⊣ η ⇒ (−)}\), between the pushout-product and the pullback-power.
|
There is an adjunction \({η \× (−) ⊣ η ⇒ (−)}\), between the pushout-product and the pullback-power.
|
||||||
|
|
@ -123,7 +122,7 @@ Or more formally:
|
||||||
between cofibrations and trivial fibrations, to lifting problems between trivial cofibrations and fibrations.
|
between cofibrations and trivial fibrations, to lifting problems between trivial cofibrations and fibrations.
|
||||||
\end{remark}
|
\end{remark}
|
||||||
|
|
||||||
We will also encouter another form of Leibniz application, which has at first glance not to do alot with homotopy. On
|
We will also encounter another form of Leibniz application, which has at first glance not to do a lot with homotopy. On
|
||||||
the other hand one might read this as, getting the component of an natural transformation is some sort of a homotopic construction.
|
the other hand one might read this as, getting the component of an natural transformation is some sort of a homotopic construction.
|
||||||
\begin{lemma}
|
\begin{lemma}
|
||||||
Let \(F,G : A → B \) and \(η : F ⇒ G\) be a natural transformation, and \A has an initial object \(∅\). Let
|
Let \(F,G : A → B \) and \(η : F ⇒ G\) be a natural transformation, and \A has an initial object \(∅\). Let
|
||||||
|
|
@ -131,13 +130,13 @@ the other hand one might read this as, getting the component of an natural trans
|
||||||
We write \(∅ → X\) for the unique map with the same type. Then we get \(η \at (∅ → X) = η_X\).
|
We write \(∅ → X\) for the unique map with the same type. Then we get \(η \at (∅ → X) = η_X\).
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
We will draw the diagram from the definiton
|
We will draw the diagram from the definition
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
F (∅) \arrow[r, "F(∅ → X)"] \arrow[d, "η_∅"] \arrow[dr, phantom, "\ulcorner", very near end] & F(X) \arrow[ddr, bend left, "η_X"] \arrow[d] & \\
|
F (∅) \arrow[r, "F(∅ → X)"] \arrow[d, "η_∅"] \arrow[dr, phantom, "\ulcorner", very near end] & F(X) \arrow[ddr, bend left, "η_X"] \arrow[d] & \\
|
||||||
G(∅) \arrow[drr, bend right, "G(∅ → X)"'] \arrow[r] & G(∅) ∐\limits_{F(∅)} \mathrlap{F(X)} \phantom{G(∅)} \arrow[dr, dashed ,"η \widehat{@} (∅ → X)" description] & \\
|
G(∅) \arrow[drr, bend right, "G(∅ → X)"'] \arrow[r] & G(∅) ∐\limits_{F(∅)} \mathrlap{F(X)} \phantom{G(∅)} \arrow[dr, dashed ,"η \widehat{@} (∅ → X)" description] & \\
|
||||||
& & G(X)
|
& & G(X)
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
If we substitude \(F(\emptyset)\) and \(G(∅)\) with \(∅\) the claim directly follows.
|
If we substitute \(F(\emptyset)\) and \(G(∅)\) with \(∅\) the claim directly follows.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
% TODO Left adjoint
|
% TODO Left adjoint
|
||||||
|
|
||||||
|
|
|
||||||
143
src/Preliminaries/MWE.tex
Normal file
143
src/Preliminaries/MWE.tex
Normal file
|
|
@ -0,0 +1,143 @@
|
||||||
|
\documentclass[../Main.tex]{subfiles}
|
||||||
|
\begin{document}
|
||||||
|
\subsection{Leibniz Construction}
|
||||||
|
We will use a well-know construction in homotopy theory to
|
||||||
|
elegantly construct a lot of interesting objects, the Leibniz construction.
|
||||||
|
This section will mostly give a definition and some examples to get familiar with this construction.
|
||||||
|
If the reader is already familiar with it, they might skip this section without any problems.
|
||||||
|
We start by giving the definition.
|
||||||
|
\begin{definition}[Leibniz Construction]
|
||||||
|
Let \(\A\), \(\B\) and \(\C\) be categories and \(\C\) have finite pushouts. Let \(⊗ : \A × \B → \C \) be a bifunctor.
|
||||||
|
Then we define the \emph{Leibniz Construction} \(\⊗ : \arr{\A} × \arr{\B} → \arr{\C}\) to be the functor
|
||||||
|
that sends \(f : A → A' \) in \(\A\) and
|
||||||
|
\( g : B → B' \) in \(\B\), to \( f \⊗ g \) as defined via the following diagram.
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
A ⊗ B \arrow[r, "f ⊗ \id"] \arrow[d, "\id ⊗ g"] \arrow[dr, phantom, "\ulcorner", very near end] & A' ⊗ \mathrlap{B} \phantom{A'} \arrow[ddr, bend left, "\id ⊗ g"] \arrow[d] & \\
|
||||||
|
\phantom{B'} \mathllap{A} ⊗ B' \arrow[drr, bend right, "f ⊗ \id"] \arrow[r] & A ⊗ B' ∐\limits_{A ⊗ B} A' ⊗ B \arrow[dr, dashed ,"f \⊗ g"] & \\
|
||||||
|
& & A' ⊗ B'
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
If \(⊗\) is the tensor functor of a monoidal category, we also call it the \emph{Leibniz product} or \emph{pushout-product}. If \(⊗\) is
|
||||||
|
the functor application functor, we also call it the \emph{Leibniz application}.
|
||||||
|
\end{definition}
|
||||||
|
|
||||||
|
The following examples are true for any category of nice spaces. We will state them for simplicial sets as the reader is probably
|
||||||
|
familiar with them.
|
||||||
|
|
||||||
|
\begin{example}\label{a}
|
||||||
|
Let \(δ_k : * → Δ^1\) for \(k ∈ \{0,1\}\) be one of the endpoint inclusions into the interval and \(i : \∂ Δ^n → Δ^n\) the boundary
|
||||||
|
inclusion of the \(n\)-simplex. Then \(δ_k \× i\) is the inclusion of a prism without its interior and one cap into the prism.
|
||||||
|
\end{example}
|
||||||
|
This gives us a description of a possible set of generating trivial cofibrations. This will be an ongoing theme.
|
||||||
|
We can even observe something stronger. If we would replace the boundary inclusion
|
||||||
|
of the \(n\)-simplex with the boundary inclusion of an arbitrary space \(X\). We get the inclusion of the cylinder object of \(X\)
|
||||||
|
without a cap and its interior into the cylinder.
|
||||||
|
%\begin{figure}
|
||||||
|
% \missingfigure{cylinder inclusion as pushout product}
|
||||||
|
% \caption{cylinder inclusion as Leibniz product}
|
||||||
|
%\end{figure}
|
||||||
|
|
||||||
|
\begin{observation}
|
||||||
|
If \(f\) and \(g\) are cofibrations then \(f \× g\) is too. If \(f\) or \(g\) is a trivial cofibration, then so is \(f \× g\).
|
||||||
|
\end{observation}
|
||||||
|
This has far reaching consequences and one can define the notion of a monoidal model category where this one of the axioms
|
||||||
|
for the tensor functor. This axiom basically states that the tensor product behaves homotopicaly. For more
|
||||||
|
detail see \cite{hoveyModelCategories2007}. We are not going to need much of this theory explicitly. But it is worthy noting
|
||||||
|
that all examples of model categories that we are going to encounter are of this form.
|
||||||
|
|
||||||
|
We will also encounter basically the same construction as \cref{a} in another way. We can get the Cylinder object
|
||||||
|
functorialy in \Δ, such that the cap inclusions are natural transformations.
|
||||||
|
The inclusion the Leibniz product produces the inclusion in a natural manner via the Leibniz application.
|
||||||
|
|
||||||
|
\begin{example}\label{ex:leib:functorialCylinder}
|
||||||
|
Let the functor application functor \( @ : \C^{\C} × \C → \C \) defined as
|
||||||
|
\( F @ x ≔ F(x)\). Let \(\I × (−)\) be the functor that sends \(X\) to its cylinder object (also known as the
|
||||||
|
product with the interval).
|
||||||
|
Let \( δ_k : \Id → \I ⊗ (−) \) be one of the, the natural transformation that embeds the space in one of the cylinder caps.
|
||||||
|
Let \( \∂ X → X \) be the boundary inclusion of \(X\).
|
||||||
|
Then \( δ_k \widehat{@} (∂X → X) \) is the filling of a cylinder with one base surface of shape \(X\).
|
||||||
|
\end{example}
|
||||||
|
This kind of construction will later play an important role in the construction of our desired model categories.
|
||||||
|
And as we will use constructions like this more often we add a bit of notation for it.
|
||||||
|
|
||||||
|
\begin{notation}
|
||||||
|
Let \(⊗ : \A × \B → \C\) be a bifunctor, \(A\) an object of \A, \(F : \B → \C\) a functor, and \(η : F ⇒ A ⊗ (−)\)
|
||||||
|
a natural transformation. We write \(η \⊗ (−) ≔ (η ⊗ (−)) \widehat{@} (−)\).
|
||||||
|
\end{notation}
|
||||||
|
|
||||||
|
Here is a property that we will exploit fairly often.
|
||||||
|
\begin{proposition}\label{rem:leibniz:adhesive}
|
||||||
|
Since every topos is adhesive \cite{lackAdhesiveQuasiadhesiveCategories2005}, monomorphisms are stable under the pushout-product and the
|
||||||
|
Leibniz application of \(A × (−)\) in every topos.
|
||||||
|
\end{proposition}
|
||||||
|
|
||||||
|
The Leibniz construction has a dual construction, the Leibniz pullback construction.
|
||||||
|
\begin{definition}[Leibniz pullback Construction]
|
||||||
|
Let \(\A\), \(\B\) and \(\C\) be categories and \(\C\) have finite pullbacks. Let \(⊗ : \A × \B → \C \) be a bifunctor.
|
||||||
|
Then we define the \emph{Leibniz pullback construction} \(\widecheck{⊗ }: \arr{\A} × \arr{\B} → \arr{\C}\) to be the functor
|
||||||
|
that sends \(f : A → A' \) in \(\A\) and
|
||||||
|
\( g : B → B' \) in \(\B\) to \( f \widecheck{⊗} g \) as defined by the following diagram.
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
A ⊗ B
|
||||||
|
\arrow[rrd, "f ⊗ \id",bend left]
|
||||||
|
\arrow[ddr, "\id ⊗ g",bend right]
|
||||||
|
\arrow[rd, "", dashed]
|
||||||
|
& &
|
||||||
|
\\
|
||||||
|
{} & A ⊗ B' \displaystyle\prod_{A'⊗B'} A'⊗ B
|
||||||
|
\arrow[d]
|
||||||
|
\arrow[r]
|
||||||
|
\pb
|
||||||
|
& A' ⊗ \mathrlap{B} \phantom{A'}
|
||||||
|
\arrow[d, "\id ⊗ g"]
|
||||||
|
\\
|
||||||
|
{}
|
||||||
|
& \phantom{B'} \mathllap{A} ⊗ B'
|
||||||
|
\arrow[r, "f ⊗ \id"]
|
||||||
|
& A' ⊗ B'
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
If \(⊗\) is the exponential functor, we also call it the \emph{Leibniz pullback Hom}, \emph{pullback-power} or \emph{pullback-hom}.
|
||||||
|
If \(⊗\) is the functor application functor we also call it the \emph{Leibniz pullback application}.
|
||||||
|
\end{definition}
|
||||||
|
Analog to the notation above we introduce the following notation
|
||||||
|
\begin{notation}
|
||||||
|
Let \(⊗ : \A × \B → \C\) be a bifunctor, \(A\) be an object of \A, \(F : \B → \C\) be a functor , and let \(η : F ⇒ A ⊗ (−)\)
|
||||||
|
be a natural transformation. We write \(η \widehat⊗ (−) ≔ (η ⊗ (−)) \widehat{@} (−)\). As it is common in the literature, we
|
||||||
|
also write the following for the special case \(A⊗ (−) = (−)^A\), \(η ⇒ (−) ≔ η \widecheck⊗ (−)\).
|
||||||
|
\end{notation}
|
||||||
|
|
||||||
|
Dual to our observation above it will be a theme that the pullback-power sends fibrations to trivial fibrations.
|
||||||
|
Or more formally:
|
||||||
|
\begin{lemma}[{\cite[Lemma 4.10]{riehlTheoryPracticeReedy2014}}]
|
||||||
|
There is an adjunction \({η \× (−) ⊣ η ⇒ (−)}\) between the pushout-product and the pullback-power.
|
||||||
|
\end{lemma}
|
||||||
|
\begin{remark}
|
||||||
|
This holds in much more generality, for details see \cite[Lemma 2.1.15]{solution}.
|
||||||
|
\end{remark}
|
||||||
|
\begin{remark}
|
||||||
|
Our main application of this lemma will be that it gives us the ability to transpose lifting problems
|
||||||
|
between cofibrations and trivial fibrations, to lifting problems between trivial cofibrations and fibrations.
|
||||||
|
\end{remark}
|
||||||
|
|
||||||
|
We will encounter another form of Leibniz application, which at first glance does not has a lot to do with homotopy. Though,
|
||||||
|
one might read this as getting the component of a natural transformation some sort of a homotopic construction.
|
||||||
|
\begin{lemma}\label{leibnizNatural}
|
||||||
|
Let \(F,G : A → B \) be functors, \(η : F ⇒ G\) a natural transformation, and \A have an initial object \(∅\). Let
|
||||||
|
\(F\) and \(G\) preserve the initial object.
|
||||||
|
We write \(∅ → X\) for the unique map. Then we get \(η \at (∅ → X) = η_X\).
|
||||||
|
\end{lemma}
|
||||||
|
\begin{proof}
|
||||||
|
We will draw the diagram from the definition
|
||||||
|
\begin{eqcd*}
|
||||||
|
F (∅) \arrow[r, "F(∅ → X)"] \arrow[d, "η_∅"] \arrow[dr, phantom, "\ulcorner", very near end] & F(X) \arrow[ddr, bend left, "η_X"] \arrow[d] & \\
|
||||||
|
G(∅) \arrow[drr, bend right, "G(∅ → X)"'] \arrow[r] & G(∅) ∐\limits_{F(∅)} \mathrlap{F(X)} \phantom{G(∅)} \arrow[dr, dashed ,"η \widehat{@} (∅ → X)" description] & \\
|
||||||
|
& & G(X)
|
||||||
|
\end{eqcd*}
|
||||||
|
If we substitute \(F(\emptyset)\) and \(G(∅)\) with \(∅\) the claim directly follows.
|
||||||
|
\end{proof}
|
||||||
|
% TODO Left adjoint
|
||||||
|
|
||||||
|
\end{document}
|
||||||
|
|
@ -8,8 +8,8 @@
|
||||||
% Then cubical sets
|
% Then cubical sets
|
||||||
|
|
||||||
\subsection{Equivariant Cartesian Cubes}
|
\subsection{Equivariant Cartesian Cubes}
|
||||||
We now presenting our, main star, the equivariant model structure on cubical sets.
|
We now present our, main object of study, the equivariant model structure on cubical sets.
|
||||||
We will give a description of the two involved factorization systems and then follow
|
We will give a description of the two factorization systems involved and then follow
|
||||||
an argument from \cite{cavalloRelativeEleganceCartesian2022}, to show that it is indeed
|
an argument from \cite{cavalloRelativeEleganceCartesian2022}, to show that it is indeed
|
||||||
a model structure. The model structure as well as the presentation is taken from
|
a model structure. The model structure as well as the presentation is taken from
|
||||||
\cite{riehlVid}. This
|
\cite{riehlVid}. This
|
||||||
|
|
@ -23,16 +23,35 @@ contractible, while in spaces it is. The idea is to correct this defect, by maki
|
||||||
of the point a trivial cofibration. This is archived by forcing an extra property onto
|
of the point a trivial cofibration. This is archived by forcing an extra property onto
|
||||||
the fibrations.
|
the fibrations.
|
||||||
|
|
||||||
\begin{equation*}
|
\begin{equation*}\label{Leibniz:Ex:OpenBox}
|
||||||
\begin{tikzcd}[column sep=large, row sep=large]
|
\begin{tikzcd}[column sep=large, row sep=large]
|
||||||
* \arrow[r,"\id"] \arrow[d,tail,"f"] & * \arrow[d,tail,"σf"'] \arrow[r] & * \arrow[d,tail] \arrow[r,"β"] & X \arrow[d,"f"] \\
|
*
|
||||||
\I^2 \arrow[r,"σ"', shift right=0.7ex] \arrow[r,"\id", shift left=0.7ex] \arrow[urrr, dashed, ,near end, "{j(αe,β)}"'] & \I^2 \arrow[urr, dashed, "{j(αeσ,β)}"] \arrow[r, "e"] & Q \arrow[r,"α"] & Y
|
\arrow[r,"\id"]
|
||||||
|
\arrow[d,tail,"f"]
|
||||||
|
& *
|
||||||
|
\arrow[d,tail,"σf"']
|
||||||
|
\arrow[r]
|
||||||
|
& *
|
||||||
|
\arrow[d,tail]
|
||||||
|
\arrow[r,"β"] & X
|
||||||
|
\arrow[d,"f"]
|
||||||
|
\\
|
||||||
|
\I^2
|
||||||
|
\arrow[r,"σ"', shift right=0.7ex]
|
||||||
|
\arrow[r,"\id", shift left=0.7ex]
|
||||||
|
\arrow[urrr, dashed, ,near end, "{j(αe,β)}"']
|
||||||
|
& \I^2
|
||||||
|
\arrow[urr, dashed, "{j(αeσ,β)}"]
|
||||||
|
\arrow[r, "e"]
|
||||||
|
& Q
|
||||||
|
\arrow[r,"α"]
|
||||||
|
& Y
|
||||||
\end{tikzcd}
|
\end{tikzcd}
|
||||||
\end{equation*} % Fix twist of suboject
|
\end{equation*} % Fix twist of suboject
|
||||||
|
|
||||||
Here \(σ\) is the map that swaps the dimensions and \(e\) is the coequalizer map. The hope would be, that
|
Here \(σ\) is the map that swaps the dimensions and \(e\) is the coequalizer map. The hope would be, that
|
||||||
the coequalizer, would now present a lift for the right most lifting problem. But in general that
|
the coequalizer would now present a lift for the right most lifting problem. But in general that
|
||||||
does not hold, the lifts have neither to commute with \(σ\) nor with \(\id\). The path forward
|
does not hold, the lifts neither have to commute with \(σ\) nor with \(\id\). The path forward
|
||||||
will be to restrict the fibrations to have the desired property.
|
will be to restrict the fibrations to have the desired property.
|
||||||
%
|
%
|
||||||
|
|
||||||
|
|
@ -101,13 +120,14 @@ will be to restrict the fibrations to have the desired property.
|
||||||
|
|
||||||
|
|
||||||
\subsubsection{Cofibrations and trivial fibrations}
|
\subsubsection{Cofibrations and trivial fibrations}
|
||||||
The short way of specifying this weak factorization system, is by saying
|
The short way of specifying this weak factorization system is by saying
|
||||||
the cofibrations are the monomorphisms. Another, longer way, but for the further development more
|
the cofibrations are the monomorphisms. Another, longer way, but for the further development more
|
||||||
enlightening is by formulating this as a uniform lifting properties.
|
enlightening, is formulating this as a uniform lifting property.
|
||||||
It is also not equivalent from the viewpoint of an awfs, as this definition has extra conditions on the
|
It is also not equivalent from the viewpoint of an awfs, as this definition has extra conditions on the
|
||||||
chosen lifts.
|
chosen lifts.
|
||||||
The condition to have uniform lifts, comes from \cite{CCHM} and generalized in \cite{gambinoFrobeniusConditionRight2017} . This requirement is motivated to have
|
The condition to have uniform lifts comes from \cite{CCHM} and is generalized in \cite{gambinoFrobeniusConditionRight2017} . This requirement is motivated to have
|
||||||
constructive interpretation of Cubical type theory\todo{see ctt intro chapter when it is done}. As we don't focus on the type theoretic interpretation, but on the model structure we won't
|
constructive interpretation of Cubical type theory\todo{see ctt intro chapter when it is done}. As we don't focus on the
|
||||||
|
type theoretic interpretation but on the model structure, we won't
|
||||||
explore this further.
|
explore this further.
|
||||||
|
|
||||||
\begin{definition}
|
\begin{definition}
|
||||||
|
|
@ -117,27 +137,27 @@ explore this further.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
\begin{definition}
|
\begin{definition}
|
||||||
The category of \emph{uniform generating cofibrations} has as object monomorphisms into a cube \(C ↣ \I^n\) of arbitrary dimension, and
|
The category of \emph{uniform generating cofibrations} has as objects monomorphisms into a cube \(C ↣ \I^n\) of arbitrary dimension, and
|
||||||
as morphism Cartesian squares between those.
|
as morphism Cartesian squares between those.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
\begin{definition}
|
\begin{definition}
|
||||||
A \emph{uniform trivial fibration} is a right map with respect to the inclusion functor from the category of uniform generation cofibrations
|
A \emph{uniform trivial fibration} is a right map with respect to the inclusion functor from the category of uniform generation cofibrations
|
||||||
into \(\□^→\)
|
into \(\□^→\).
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
From this it is not immediately clear that the left maps are all monomorphisms, but it follows from
|
From this, it is not immediately clear that the left maps are all monomorphisms, but it follows from
|
||||||
\cite[Proposition 7.5]{gambinoFrobeniusConditionRight2017}.
|
\cite[Proposition 7.5]{gambinoFrobeniusConditionRight2017}.
|
||||||
By Garners small object argument \cref{awfs:smallObject}, this gives rise to an awfs which we call \((\TCF,\FF)\) and an underlying wfs
|
By Garners small object argument \cref{awfs:smallObject}, this gives rise to an awfs, which we call \((\TCF,\FF)\), and an underlying wfs,
|
||||||
that we call \((\C_t,\F)\)
|
that we call \((\C_t,\F)\).
|
||||||
\subsubsection{Trivial cofibrations and fibrations}
|
\subsubsection{Trivial Cofibrations and Fibrations}
|
||||||
|
|
||||||
As we sketched above, the strategy will be to make more maps trivial cofibrations. This is done
|
As sketched above, the strategy will be to make more maps trivial cofibrations. This is done
|
||||||
by making it harder to be a fibration. Before we give the definition in full generality, we
|
by making it harder to be a fibration. Before we give the definition in full generality, we
|
||||||
need to address which coequalizer we talk about precisely.
|
need to address which coequalizer we talk about precisely.
|
||||||
|
|
||||||
Of course doing this only in the 2 dimensional case is not enough. For this we need to say what
|
Of course, doing this only in the 2 dimensional case is not enough. For this, we need to say what
|
||||||
the “swap” maps are. What these should do is permuting the dimensions. So let \(Σ_k\) be the symmetric group
|
the “swap” maps are. What these should do, is permuting the dimensions. So let \(Σ_k\) be the symmetric group
|
||||||
on \(k\) elements. For every \(σ' ∈ Σ_k\), we get a map from \( σ : \I^k → \I^k \), by \((π_{σ'(1)}, … , π_{σ'(k)})\),
|
on \(k\) elements. For every \(σ' ∈ Σ_k\), we get a map from \( σ : \I^k → \I^k \), by \((π_{σ'(1)}, … , π_{σ'(k)})\),
|
||||||
where \(π_l : \I^k → \I \) is the \(l\)-th projection. Also if we have a sub-cube \(f : \I^n \rightarrowtail \I^k\),
|
where \(π_l : \I^k → \I \) is the \(l\)-th projection. Also if we have a sub-cube \(f : \I^n \rightarrowtail \I^k\),
|
||||||
we get a pullback square of the following form
|
we get a pullback square of the following form
|
||||||
|
|
@ -148,14 +168,20 @@ we get a pullback square of the following form
|
||||||
\end{tikzcd}
|
\end{tikzcd}
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
whose right arrow we call \(σf\).
|
whose right arrow we call \(σf\).
|
||||||
%
|
|
||||||
Now we describe our generating trivial cofibrations. We remember example \cref{Leibniz:Ex:OpenBox}. We would
|
Now we describe our generating trivial cofibrations. We recall example \cref{Leibniz:Ex:OpenBox}. We would
|
||||||
like to do the same here, but a bit more general.
|
like to do the same here, but a bit more general.
|
||||||
|
%
|
||||||
|
There is also another problem we didn't talked about yet. In \(\mathbf{Top}\), if we start with a compact space \(X\),
|
||||||
|
and let \(∂X → X\) be its boundary inclusion. We can then not only lift against the cylinder filling problem with the
|
||||||
|
cap at the bottom \(δ_0 \⊗ (∂X → X)\), or the at the top \(δ_0 \⊗ (∂X → X)\), but at every point in the interval.
|
||||||
|
Even more we can prove the existence of a lift leaving the point as a variable. In \(\mathbf{Top}\), \Δ, and \dcSet
|
||||||
|
this follows automatically from the endpoint liftings. In the absence of connections this is not true. So we need
|
||||||
|
to accomedate for that and make this part of our generating trivial cofibrations.
|
||||||
|
|
||||||
|
To solve this problem we are going for box-fillings in the context of a cube. The definition of those will be very similar
|
||||||
Instead we are going for box-fillings in the context of a cube. The definition of those will be very similar
|
we will just work in the slice over a cube \(\I^k\). We do the pushout-product in the slice, and
|
||||||
we will just work in the slice over a cube \(I^k\). We do the Pushout-product in the slice, and
|
forget the slice, to get a map in \(\□\).
|
||||||
forget the slice to get a map in \(\□\).
|
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
\begin{tikzcd}
|
\begin{tikzcd}
|
||||||
\left(\faktor{\□}{\I^k} \right) ^{→} × \left(\faktor{\□}{\I^k}\right)^{→} \arrow[r,"\hat{×}_{\I^k}"] & \left(\faktor{\□}{\I^k}\right)^→ \arrow[r,"\textrm{forget}"] & \□^→
|
\left(\faktor{\□}{\I^k} \right) ^{→} × \left(\faktor{\□}{\I^k}\right)^{→} \arrow[r,"\hat{×}_{\I^k}"] & \left(\faktor{\□}{\I^k}\right)^→ \arrow[r,"\textrm{forget}"] & \□^→
|
||||||
|
|
@ -164,13 +190,13 @@ forget the slice to get a map in \(\□\).
|
||||||
|
|
||||||
What do we change by working in the slice?
|
What do we change by working in the slice?
|
||||||
For intuition let us first look at the case
|
For intuition let us first look at the case
|
||||||
with a one dimensional context. The point in in this context is the terminal object in \(\faktor{\□}{\I}\).
|
with a one dimensional context. The point in this context is the terminal object in \(\faktor{\□}{\I}\).
|
||||||
The interval in this cube category could be described as the pullback, of the interval in \(\□ = \faktor{\□}{\I^0}\)
|
The interval in this cube category could be described as the pullback, of the interval in \(\□ = \faktor{\□}{\I^0}\),
|
||||||
along the unique map \(\I → \I^0\), or in simpler words it is the left projection \(π_l : \I × \I → \I\).
|
along the unique map \(\I → \I^0\), or in simpler words it is the left projection \(π_l : \I × \I → \I\).
|
||||||
Let us now look what maps we have from the point into the interval \(\id_\I → π_l \). We get the two
|
Let us now look what maps we have from the point into the interval \(\id_\I → π_l \). We get the two
|
||||||
endpoint maps we expected, as \(⟨\id, 0⟩ \) and \(⟨\id, 1⟩\), but in this context we get an additional map,
|
endpoint maps we expected, as \(⟨\id, 0⟩ \) and \(⟨\id, 1⟩\), but in this context we get an additional map,
|
||||||
namely \(⟨\id, \id⟩\). If we would forget the context again (aka being in the slice), this is the diagonal of the square. From
|
namely \(⟨\id, \id⟩\). If we would forget the context again (aka, being in the slice), this is the diagonal of the square. From
|
||||||
a type theoretic perspective this is really not surprising. Here it amounts to the question, how many different terms
|
a type theoretic perspective, this is not really surprising. Here it amounts to the question, how many different terms
|
||||||
of type \(\I\) can be produced. In an empty context the answer is two.
|
of type \(\I\) can be produced. In an empty context the answer is two.
|
||||||
\begin{align*}
|
\begin{align*}
|
||||||
⊢ 0 : \I && ⊢ 1 : \I
|
⊢ 0 : \I && ⊢ 1 : \I
|
||||||
|
|
@ -179,20 +205,19 @@ But in the context of \(\I\), the answer is three.
|
||||||
\begin{align*}
|
\begin{align*}
|
||||||
i:\I ⊢ 0 : \I && i:\I ⊢ 1 : \I && i:\I ⊢ i : \I
|
i:\I ⊢ 0 : \I && i:\I ⊢ 1 : \I && i:\I ⊢ i : \I
|
||||||
\end{align*}
|
\end{align*}
|
||||||
Like the type theory suggest we can think of this, as an generic element of the interval. That this
|
Like the type theory suggest, we can think of this, as generic element of the interval. That this
|
||||||
element is different from both closed points, is what differentiates the interval from the
|
element that ranges across the interval.
|
||||||
coproduct of two points. In the type theoretic world we want something that is called a composition structure, and these
|
As we sketched above we want to be able to fill at the point \(i : \I\) as well,
|
||||||
should also work
|
this amounts to being able to have a cube filling property along those diagonals,
|
||||||
along those diagonals, this amounts to be able to have be able to have a cube filling property along those diagonals,
|
or in other words we want them to be trivial cofibrations too. The earliest mention of the idea that I am aware of, is
|
||||||
or in other words we want them to be trivial cofibrations too. The earliest mention of the idea the I am aware of is
|
this short note \cite{coquandVariationCubicalSets2014}, for a discussion see for example \cites{ABCHFL}{awodeyCartesianCubicalModel2023}.
|
||||||
this short note \cite{coquandVariationCubicalSets2014}, for a discussion see for example \cite{angiuliSyntaxModelsCartesian2021}.
|
|
||||||
|
|
||||||
The generalization of the boundary inclusion is straight forward. We just take any cube over \(\I^k\)
|
The generalization of the boundary inclusion is straight forward. We just take any cube over \(\I^k\)
|
||||||
\(ζ : \I^n → \I^k\) and a monomorphism \(c : C → \I^n\), this also induces an object in the slice by composition.
|
\(ζ : \I^n → \I^k\) and a monomorphism \(c : C ↣ \I^n\), this also induces an object in the slice by composition.
|
||||||
Notice that we did not require that \( n ≥ k\).
|
Notice that we did not require that \( n ≥ k\).
|
||||||
If we pack all of this into a definition we get.
|
If we pack all of this into a definition we get the following.
|
||||||
\begin{definition}\label{def:modelStructure:generatingTrivialCofibration}
|
\begin{definition}\label{def:modelStructure:generatingTrivialCofibration}
|
||||||
Let \(ζ : \I^n → \I^k\) be a cube over \(\I^k\) and \(c : C → \I^n\) monic. A map of the form
|
Let \(ζ : \I^n → \I^k\) be a cube over \(\I^k\) and \(c : C ↣ \I^n\) monic. A map of the form
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
\begin{tikzcd}
|
\begin{tikzcd}
|
||||||
C \arrow[r,"c", tail] \arrow[dr] & \I^n \arrow[d,"ζ"] \arrow[dr,phantom, "\hat{×}_{\I^k}"] & \I^k \arrow[d,"\id"] \arrow[r,"{⟨\id,l⟩}"] & \I^k × \I^m \arrow[dl,"π_l"] \\
|
C \arrow[r,"c", tail] \arrow[dr] & \I^n \arrow[d,"ζ"] \arrow[dr,phantom, "\hat{×}_{\I^k}"] & \I^k \arrow[d,"\id"] \arrow[r,"{⟨\id,l⟩}"] & \I^k × \I^m \arrow[dl,"π_l"] \\
|
||||||
|
|
@ -208,7 +233,7 @@ If we pack all of this into a definition we get.
|
||||||
\caption{An example construction of a trivial cofibration}
|
\caption{An example construction of a trivial cofibration}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
|
|
||||||
We now want to define our fibrations as the uniform equivariant right lifting maps. To do this we need to define what this
|
We now want to define our fibrations as the uniform equivariant right lifting maps. To do this, we need to define what this
|
||||||
actually means. Uniformity wants a choice of lifts that agree with pullback squares between (trivial) cofibrations. %TODO move the uniformity section upwards
|
actually means. Uniformity wants a choice of lifts that agree with pullback squares between (trivial) cofibrations. %TODO move the uniformity section upwards
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
\begin{tikzcd}[column sep=large]
|
\begin{tikzcd}[column sep=large]
|
||||||
|
|
@ -217,7 +242,7 @@ actually means. Uniformity wants a choice of lifts that agree with pullback squa
|
||||||
\end{tikzcd}
|
\end{tikzcd}
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
The uniformity condition wants that the triangle containing both chosen lifts commutes, or as an equation \(j(x,y)b = j(ax,yb)\).
|
The uniformity condition wants that the triangle containing both chosen lifts commutes, or as an equation \(j(x,y)b = j(ax,yb)\).
|
||||||
We now need to combine the uniformity and the equivariance condition. As the pushout-product is functorial it is enough to
|
We now need to combine the uniformity and the equivariance condition. As the pushout-product is functorial, it is enough to
|
||||||
describe these conditions between the building blocks of our trivial cofibration and apply the pushout-product again.
|
describe these conditions between the building blocks of our trivial cofibration and apply the pushout-product again.
|
||||||
Again we will do this in a slice and forget the slice afterwards.
|
Again we will do this in a slice and forget the slice afterwards.
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
|
|
@ -238,8 +263,11 @@ Again we will do this in a slice and forget the slice afterwards.
|
||||||
\right)
|
\right)
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
Notice that we understand the vertical morphisms as objects of \(\□^→\) and the horizontal ones as morphism in \(\□^→\).
|
Notice that we understand the vertical morphisms as objects of \(\□^→\) and the horizontal ones as morphism in \(\□^→\).
|
||||||
Also notice, that the left diagram is a square for which we use in our uniformity condition and the right one captures
|
Also notice that the left diagram is a square which captures our uniformity condition and the right one captures
|
||||||
equivariance. And notice that the pushout-product of the columns yield trivial cofibrations. We will denote the resulting
|
equivariance. This is interesting, because this means that uniformity is a condition that can be stated on the base
|
||||||
|
of the filling, while equivariance is a condition on the cylinder walls, that are now multi dimensional.
|
||||||
|
In other words we added a group action on the products of intervals.
|
||||||
|
Also notice that the pushout-product of the columns yield trivial cofibrations. We will denote the resulting
|
||||||
commutative square as
|
commutative square as
|
||||||
\begin{equation}\label{devilSquare}
|
\begin{equation}\label{devilSquare}
|
||||||
\begin{tikzcd}[column sep=large]
|
\begin{tikzcd}[column sep=large]
|
||||||
|
|
@ -250,37 +278,48 @@ commutative square as
|
||||||
Now we can finally give the definition of uniform equivariant fibrations.
|
Now we can finally give the definition of uniform equivariant fibrations.
|
||||||
|
|
||||||
\begin{definition}
|
\begin{definition}
|
||||||
The category of \emph{generating uniform equivariant trivial cofibrations} has as object
|
The category of \emph{generating uniform equivariant trivial cofibrations} has as objects
|
||||||
generating cofibrations and as morphism squares of the shape defined in \cref{devilSquare}
|
generating cofibrations and as morphism squares of the shape defined in \cref{devilSquare}
|
||||||
above.
|
above.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
\begin{definition}
|
\begin{definition}
|
||||||
A \emph{uniform equivariant fibration} is right map with respect to the inclusion functor of the category of generating
|
A \emph{uniform equivariant fibration} is a right map with respect to the inclusion functor of the category of generating
|
||||||
uniform equivariant trivial cofibrations into \(\□^→\).
|
uniform equivariant trivial cofibrations into \(\□^→\).
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
|
\begin{remark}
|
||||||
|
This gives us directly that all quotients of representables are contractible, because it is now part of the
|
||||||
|
definition that the point inclusion is a weak equivalence.
|
||||||
|
\end{remark}
|
||||||
|
|
||||||
|
\begin{remark}\label{rem:modelStructure:checkov}
|
||||||
|
There are more ways to state the equivariance property. This one follows closely \cite{riehlVid}.
|
||||||
|
We could also passed to a category of group actions on \□ and defined uniform fibrations in a naive way in that
|
||||||
|
category. This construction will show up later \cref{rem:modelStructure:speciesPremodelSrtucture},
|
||||||
|
also see \cite[Section 4 \& 5]{solution} for more details.
|
||||||
|
\end{remark}
|
||||||
|
|
||||||
\begin{notation}
|
\begin{notation}
|
||||||
By \cref{awfs:smallObject} these categories of maps form an awfs. We call it \((\TCF,\FF)\) and the underlying wfs
|
By \cref{awfs:smallObject} these categories of maps form an awfs. We denote it by \((\TCF,\FF)\) and the underlying wfs
|
||||||
\((\Ct,\F)\)
|
\((\Ct,\F)\)
|
||||||
\end{notation}
|
\end{notation}
|
||||||
|
|
||||||
\subsubsection{The Premodel Structure of Equivariant Cubical Sets}
|
\subsubsection{The Premodel Structure of Equivariant Cubical Sets}
|
||||||
On our way to show that this is a model structure, we will use the theory of premodel structures
|
On our way to show that this is a model structure, we will use the theory of premodel structures
|
||||||
\cites{bartonModel2CategoryEnriched2019}[section 3]{cavalloRelativeEleganceCartesian2022}[section 3]{solution}{sattlerCYLINDRICALMODELSTRUCTURES}.
|
\cites{bartonModel2CategoryEnriched2019}[section 3]{cavalloRelativeEleganceCartesian2022}[section 3]{solution}{sattlerCYLINDRICALMODELSTRUCTURES}.
|
||||||
\todo{if there is time (there probably won't be) include the premodel theory and explain}
|
|
||||||
|
|
||||||
\begin{definition}[{\cites{bartonModel2CategoryEnriched2019}[def. 3.1.1]{cavalloRelativeEleganceCartesian2022}}]\label{def:preModelStructure}
|
\begin{definition}[{\cites{bartonModel2CategoryEnriched2019}[def. 3.1.1]{cavalloRelativeEleganceCartesian2022}}]\label{def:preModelStructure}
|
||||||
A \emph{premodel Structure} on a finitely co-complete and complete category \M consists of two weak factorization systems
|
A \emph{premodel Structure} on a finitely co-complete and complete category \M consists of two weak factorization systems
|
||||||
\((C,F_t)\) (the \emph{cofibrations} and \emph{trivial fibrations}) and \((C_t, F)\) (the \emph{trivial cofibrations} and \emph{fibrations})
|
\((C,F_t)\) (the \emph{cofibrations} and \emph{trivial fibrations}) and \((C_t, F)\) (the \emph{trivial cofibrations} and \emph{fibrations})
|
||||||
on \M such that \(C_t ⊆ C\) (or equivalently \(F_t ⊆ F\) ).
|
on \M, such that \(C_t ⊆ C\) (or equivalently \(F_t ⊆ F\) ).
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
\begin{remark}
|
\begin{remark}
|
||||||
This structure ascend to all slices and is created by the corresponding forgetful functor. This should not be surprising, as model
|
This structure ascends to all slices and is created by the corresponding forgetful functor. This should not be surprising, as model
|
||||||
structures do the same.
|
structures do the same.
|
||||||
\end{remark}
|
\end{remark}
|
||||||
|
|
||||||
As all trivial cofibrations are monomorphisms, we get immediately that the two defined factorization systems above form a
|
As all trivial cofibrations are monomorphisms, we immediately get that the two defined factorization systems above form a
|
||||||
premodel structure. Every premodel structure comes equipped with a notion of weak equivalences.
|
premodel structure. Every premodel structure comes equipped with a notion of weak equivalences.
|
||||||
|
|
||||||
\begin{definition}[{\cite[Definition 3.1.3]{cavalloRelativeEleganceCartesian2022}}]
|
\begin{definition}[{\cite[Definition 3.1.3]{cavalloRelativeEleganceCartesian2022}}]
|
||||||
|
|
@ -291,12 +330,12 @@ premodel structure. Every premodel structure comes equipped with a notion of wea
|
||||||
|
|
||||||
What is missing, is that these equivalences actually satisfy the 2-out-of-3 condition.
|
What is missing, is that these equivalences actually satisfy the 2-out-of-3 condition.
|
||||||
The machinery of premodel structures gives us a nice condition to check if we are actually dealing with a model structure.
|
The machinery of premodel structures gives us a nice condition to check if we are actually dealing with a model structure.
|
||||||
But first we investigate a bit more structure our premodel structure possesses
|
But first, we investigate a bit more structure of our premodel structure.
|
||||||
|
|
||||||
|
|
||||||
\begin{definition}[{\cite[Definition 3.2.1]{cavalloRelativeEleganceCartesian2022}}]
|
\begin{definition}[{\cite[Definition 3.2.1]{cavalloRelativeEleganceCartesian2022}}]
|
||||||
A \emph{functorial cylinder} on a category \(E\) is a functor \(\I⊗(−) : E → E\) equipped with endpoint and contraction
|
A \emph{functorial cylinder} on a category \(E\) is a functor \(\I⊗(−) : E → E\) equipped with endpoint and contraction
|
||||||
transformations fitting in a diagram as shown:
|
transformations. Fitting in a diagram as shown:
|
||||||
\begin{eqcd*}[column sep = large, row sep=large]
|
\begin{eqcd*}[column sep = large, row sep=large]
|
||||||
\Id
|
\Id
|
||||||
\arrow[r,"δ_0⊗(−)", dashed]
|
\arrow[r,"δ_0⊗(−)", dashed]
|
||||||
|
|
@ -311,32 +350,48 @@ But first we investigate a bit more structure our premodel structure possesses
|
||||||
& \Id
|
& \Id
|
||||||
&
|
&
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
An \emph{adjoint functorial cylinder} is a functorial cylinder such that \(I ⊗ (−)\) is a left adjoint.
|
An \emph{adjoint functorial cylinder} is a functorial cylinder such that \(\I ⊗ (−)\) is a left adjoint.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
\todo{mention \(ε\) in cubical set notation}
|
\todo{mention \(ε\) in cubical set notation}
|
||||||
We can see immediately that the functor \(\I × (−)\) the product with the interval is a functorial cylinder,
|
We can see immediately that the functor \(\I × (−)\), the product with the interval, is a functorial cylinder,
|
||||||
and by \□ being a presheaf topos even an adjoint functorial cylinder. But for now it is not at all clear
|
and by \□ being a presheaf topos even an adjoint functorial cylinder. But for now it is not at all clear
|
||||||
that this functor is relevant in a homotopical sense. This is captured by the next definition.
|
that this functor is relevant in a homotopical sense. This is captured by the next definition.
|
||||||
|
|
||||||
\begin{definition}[{\cite[Definition 3.2.5]{cavalloRelativeEleganceCartesian2022}}]
|
\begin{definition}[{\cite[Definition 3.2.5]{cavalloRelativeEleganceCartesian2022}}]
|
||||||
|
We write \(∂ = [δ_0, δ_1] : \Id + \Id ⇒ \I ⊗ (−)\) for the inclusion of both endpoints.
|
||||||
A \emph{cylindrical} premodel structure on a category E consists of a premodel structure
|
A \emph{cylindrical} premodel structure on a category E consists of a premodel structure
|
||||||
and adjoint functorial cylinder on E that are compatible in the following sense:
|
and an adjoint functorial cylinder on E that are compatible in the following sense:
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item \(∂ \⊗ (−)\) preserves cofibrations and trivial cofibrations;
|
\item \(∂ \⊗ (−)\) preserves cofibrations and trivial cofibrations,
|
||||||
\item \(δ_k \⊗ (−)\) sends cofibrations to trivial cofibrations for \(k ∈ \{0, 1\}\).
|
\item \(δ_k \⊗ (−)\) sends cofibrations to trivial cofibrations for \(k ∈ \{0, 1\}\).
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
\end{definition}\todo{clean up and explain}
|
\end{definition}\todo{clean up and explain}
|
||||||
\todo{mention adhesiveness in Leibniz product chapter}
|
\todo{mention adhesiveness in Leibniz product chapter}
|
||||||
|
|
||||||
These properties are verified quickly, the map \(∂ : 1 + 1 → \I\) is monic and thus
|
These properties are verified quickly, the map \(∂ : 1 + 1 → \I\) is monic and thus
|
||||||
it follows from \cref{TODO}. We check the second property on generating cofibrations\todo{is this enough?},
|
it follows from \cref{rem:leibniz:adhesive}. We check the second property on generating cofibrations\todo{is this enough?},
|
||||||
plugging in the definition of our functorial cylinder we see that this is by definition
|
Plugging in the definition of our functorial cylinder, we see that this is by definition
|
||||||
a trivial cofibration if set \(k = 0\) and \(m = 1\) in \cref{def:modelStructure:generatingTrivialCofibration}.
|
a trivial cofibration if we set \(k = 0\) and \(m = 1\) in \cref{def:modelStructure:generatingTrivialCofibration}.
|
||||||
|
There is also an even stronger notion.
|
||||||
|
|
||||||
|
\begin{definition}[{\cite[compare][]{hazratpour2categoricalProofFrobenius2024}}]
|
||||||
|
We say a premodel structure is \emph{generated by an interval},
|
||||||
|
if we have an interval object \(\I\), the functorial cylinder is given by \(\I \⊗ (−)\), we have
|
||||||
|
a generic point of the interval \(δ = ⟨\id,\id⟩: \I → \I⊗ \I\) as a map in the slice over \I,
|
||||||
|
and a map is a fibration if and only if \(δ ⇒ f\) a trivial fibration.
|
||||||
|
\end{definition}
|
||||||
|
|
||||||
|
Sadly our premodel structure is not generated by \(\I\). But the appropriate premodel structure
|
||||||
|
of group actions on \□ is, see \cref{rem:modelStructure:speciesPremodelSrtucture}, and for more details
|
||||||
|
\cite[Section 4]{solution}.
|
||||||
|
|
||||||
|
The theory of premodel structures also gives a criterea to determine if a premodel structure
|
||||||
|
actually induces a model structure.
|
||||||
\begin{definition}[{\cite[Definition 3.3.3]{cavalloRelativeEleganceCartesian2022}}]
|
\begin{definition}[{\cite[Definition 3.3.3]{cavalloRelativeEleganceCartesian2022}}]
|
||||||
We say a premodel category \M has the fibration extension property when for any fibration
|
We say a premodel category \M has the fibration extension propertyi, when for any fibration
|
||||||
\(f : Y → X\) and trivial cofibration \(m : X → X′\), there exists a fibration \(f' : Y' → X'\) whose base change along \(m\) is
|
\(f : Y → X\) and trivial cofibration \(m : X → X′\), there exists a fibration \(f' : Y' → X'\),
|
||||||
|
whose base change along \(m\) is
|
||||||
\(f\):
|
\(f\):
|
||||||
\begin{eqcd*}[row sep=large, column sep=large]
|
\begin{eqcd*}[row sep=large, column sep=large]
|
||||||
Y \arrow[r,dashed] \arrow[d,"f"] \pb & Y' \arrow[d,dashed, "f'"] \\
|
Y \arrow[r,dashed] \arrow[d,"f"] \pb & Y' \arrow[d,dashed, "f'"] \\
|
||||||
|
|
@ -346,15 +401,15 @@ a trivial cofibration if set \(k = 0\) and \(m = 1\) in \cref{def:modelStructure
|
||||||
|
|
||||||
\begin{theorem}[{\cite[Theorem 3.3.5]{cavalloRelativeEleganceCartesian2022}}]\label{thm:premodelIsModel} \todo{if this gets longer expanded give it its own section}
|
\begin{theorem}[{\cite[Theorem 3.3.5]{cavalloRelativeEleganceCartesian2022}}]\label{thm:premodelIsModel} \todo{if this gets longer expanded give it its own section}
|
||||||
Let \(\M\) be a cylindrical premodel category in which
|
Let \(\M\) be a cylindrical premodel category in which
|
||||||
\begin{enumerate}
|
\begin{itemize}
|
||||||
\item all objects are cofibrant;
|
\item all objects are cofibrant;
|
||||||
\item the fibration extension property is satisfied.
|
\item the fibration extension property is satisfied.
|
||||||
\end{enumerate}
|
\end{itemize}
|
||||||
Then the premodel structure on \(\M\) defines a model structure.
|
Then the premodel structure on \(\M\) defines a model structure.
|
||||||
\end{theorem}
|
\end{theorem}
|
||||||
|
|
||||||
The first item is fast verified, as all monomorphisms are cofibrations.\todo{make a small lemma to prove it (closure properties got you covered)}
|
The first item is fast verified, as all monomorphisms are cofibrations.\todo{make a small lemma to prove it (closure properties got you covered)}
|
||||||
The second condition we won't show directly. We will get for free if we construct universes, which we want to do anyway.
|
The second condition we won't show directly. We will get it for free if we construct universes, which we want to do anyway.
|
||||||
Before we construct universes we will first talk about another property that follows from general
|
Before we construct universes we will first talk about another property that follows from general
|
||||||
pre model structure theory. This property relates back to type theory, as it is the categorical side of
|
pre model structure theory. This property relates back to type theory, as it is the categorical side of
|
||||||
glue types. These keep track of type extension and are used to prove univalence. We will use it later to show
|
glue types. These keep track of type extension and are used to prove univalence. We will use it later to show
|
||||||
|
|
@ -364,7 +419,7 @@ In categorical terms it says the following.
|
||||||
\begin{definition}[{\cite{sattlerEquivalenceExtensionProperty2017}}]
|
\begin{definition}[{\cite{sattlerEquivalenceExtensionProperty2017}}]
|
||||||
A cylindrical premodel structure has the equivalence extension
|
A cylindrical premodel structure has the equivalence extension
|
||||||
property when any weak equivalence \(e\) over an object \(A\) can be extended along any cofibration
|
property when any weak equivalence \(e\) over an object \(A\) can be extended along any cofibration
|
||||||
\(i : A → B\) to a weak equivalence \(f\) over \(B\) with a specified codomain extending that of the original map:
|
\(i : A ↣ B\) to a weak equivalence \(f\) over \(B\) with a specified codomain extending that of the original map:
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
X_0
|
X_0
|
||||||
\arrow[rr,dotted]
|
\arrow[rr,dotted]
|
||||||
|
|
@ -385,7 +440,7 @@ In categorical terms it says the following.
|
||||||
\\
|
\\
|
||||||
{}
|
{}
|
||||||
& A
|
& A
|
||||||
\arrow[rr,"i"]
|
\arrow[rr,"i",tail]
|
||||||
& & B
|
& & B
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
In a setting such as a presheaf topos where we have universe levels,
|
In a setting such as a presheaf topos where we have universe levels,
|
||||||
|
|
@ -394,32 +449,32 @@ In categorical terms it says the following.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
We could have equivalently used \cite[Proposition 5.1]{sattlerEquivalenceExtensionProperty2017},
|
We could have equivalently used \cite[Proposition 5.1]{sattlerEquivalenceExtensionProperty2017},
|
||||||
but this version aligns more direct with the data that we are given.
|
or \cite[Section 7]{awodeyCartesianCubicalModel2023}.
|
||||||
|
This version aligns more direct with the data that we are given.
|
||||||
\begin{theorem}[{\cite[Theorem 3.3.3]{solution}}]\label{thm:modelStructure:equivalenceExtension}
|
\begin{theorem}[{\cite[Theorem 3.3.3]{solution}}]\label{thm:modelStructure:equivalenceExtension}
|
||||||
Let \(E\) be a locally Cartesian closed category with a cylindrical premodel
|
Let \(E\) be a locally Cartesian closed category with a cylindrical premodel
|
||||||
structure in which the cofibrations are the monomorphisms, and these are stable under
|
structure in which the cofibrations are the monomorphisms, and these are stable under
|
||||||
pushout-products in all slices. Then the equivalence extension property holds in \(E\).
|
pushout-products in all slices. Then the equivalence extension property holds in \(E\).
|
||||||
\end{theorem}
|
\end{theorem}
|
||||||
The pushout product claim is verified by \cref{TODO}\todo{adhesive note in Leibniz chapter}
|
The pushout product claim is verified by \cref{rem:leibniz:adhesive}, and as every topos is cartesian closed,
|
||||||
|
we can apply the theorem.
|
||||||
|
|
||||||
\subsubsection{Universes for Fibrations}
|
\subsubsection{Universes for Fibrations}
|
||||||
In this section we will change notation between commutative diagrams and the internal language of our presheaf.
|
|
||||||
As these tools can get quite technical and tedious to verify, we will only present the idea how these constructions
|
As these tools can get quite technical and tedious to verify, we will only present the idea how these constructions
|
||||||
work and refer for the technical details to the source material.
|
work and refer for the technical details to the source material.
|
||||||
|
|
||||||
The general construction of these universes follow mostly the same idea. We lift a Grothendieck universe from \Set to
|
The general construction of these universes follows mostly the same idea. We lift a Grothendieck universe from \Set to
|
||||||
the desired presheaf category, obtaining a Hofmann-Streicher universe \cite{hofmannLiftingGrothendieckUniverses1997},
|
the desired presheaf category, obtaining a Hofmann-Streicher universe \cite{hofmannLiftingGrothendieckUniverses1997},
|
||||||
classifying small maps.
|
classifying small maps.
|
||||||
This works in general for any presheaf topos over a small site. Afterwards we restrict this universe to only small fibrations.
|
This works in general for any presheaf topos over a small site. Afterwards, we restrict this universe to only small fibrations.
|
||||||
We are then faced with a challenge, we need to prove that the resulting classifier is itself a fibration. In some cases
|
We are then faced with a challenge, we need to prove that the resulting classifier is itself a fibration. In some cases
|
||||||
this can be made easier or avoided by stating this construction in a specific way.
|
this can be made easier or avoided by stating this construction in a specific way.
|
||||||
|
|
||||||
For example by the arguments in \cite[Section 7]{awodeyHofmannStreicherUniverses2023} it suffices to construct \emph{classifying types}.
|
For example by the arguments in \cite[Section 7]{awodeyHofmannStreicherUniverses2023} it suffices to construct \emph{classifying types}.
|
||||||
\begin{definition}\label{def:modelStructure:classifyingType}
|
\begin{definition}\label{def:modelStructure:classifyingType}
|
||||||
A \emph{classifying type} for an awfs is a construction \(\Fib\) such that for every object \(X\)
|
A \emph{classifying type} for an awfs is a construction \emph{\(\Fib\)} such that for every object \(X\)
|
||||||
and every morphism \(f : A → X\) there is a map \({\Fib(f) : \Fib(A) → X}\) and the section are in correspondence with
|
and every morphism \(f : A → X\), there is a map \({\Fib(f) : \Fib(A) → X}\) and the sections are in correspondence with
|
||||||
\(\mathrm{R}\)-algebra structures on \(f\).
|
\(\mathrm{R}\)-algebra structures on \(f\).
|
||||||
Given a map \(g : Y → X\) then \(\Fib\) is stable under
|
Given a map \(g : Y → X\), then \(\Fib\) is stable under
|
||||||
pullbacks along \(g\).
|
pullbacks along \(g\).
|
||||||
\begin{eqcd*}[row sep=large]
|
\begin{eqcd*}[row sep=large]
|
||||||
g^*A
|
g^*A
|
||||||
|
|
@ -441,18 +496,18 @@ For example by the arguments in \cite[Section 7]{awodeyHofmannStreicherUniverses
|
||||||
\arrow[u, "\Fib(f)"']
|
\arrow[u, "\Fib(f)"']
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
\end{definition}
|
\end{definition}
|
||||||
If the wfs, for that we try to classify the right maps, is functorial we might think of this as an internalization
|
\begin{remark*}
|
||||||
of the \(\R\)-algebra structures on \(f\).
|
We might think of this as an internalization
|
||||||
|
of the \(\mathrm{R}\)-algebra structures on \(f\).
|
||||||
We will first construct classifying types, after that we construct universes from it.
|
\end{remark*}
|
||||||
|
|
||||||
In preparation of the fibrant case we will first classify the trivial fibrations.
|
In preparation of the fibrant case we will first classify the trivial fibrations.
|
||||||
We don't have any equivariance condition on them, and thus they are the same as in \cite[Section 2]{awodeyCartesianCubicalModel2023},
|
We don't have any equivariance condition on them,thus they are the same as in \cite[Section 2]{awodeyCartesianCubicalModel2023},
|
||||||
when we assume \(Φ = Ω\).
|
when if we assume \(Φ = Ω\).
|
||||||
|
|
||||||
Let us first think about the easiest case where the domain of the trivial fibration is the terminal.
|
Let us first think about the easiest case where the domain of the trivial fibration is the terminal.
|
||||||
We should ask us what are the \TFF-algebra structures\todo{introduce notion above}. These are intuitively
|
We should ask, what the \TFF-algebra structures are. These are
|
||||||
choice functions of uniform liftings against cofibrations. So let us think about them first. If we picture
|
choice functions of uniform liftings against cofibrations. So let us consider them first. If we picture
|
||||||
a lifting problem,
|
a lifting problem,
|
||||||
\begin{eqcd}\label{diag:liftProbTerminal}
|
\begin{eqcd}\label{diag:liftProbTerminal}
|
||||||
A \arrow[d, tail] \arrow[r] & X \arrow[d] \\
|
A \arrow[d, tail] \arrow[r] & X \arrow[d] \\
|
||||||
|
|
@ -460,29 +515,29 @@ a lifting problem,
|
||||||
\end{eqcd}
|
\end{eqcd}
|
||||||
we might think of this as a filling porblem of some shape \(A\) in \(X\) to some shape \(C\) in \(X\).
|
we might think of this as a filling porblem of some shape \(A\) in \(X\) to some shape \(C\) in \(X\).
|
||||||
Or in other words as a complition of a partial map\footnote{Recall that a partial map \(C → X\) is a span \(C \leftarrow A → X\),
|
Or in other words as a complition of a partial map\footnote{Recall that a partial map \(C → X\) is a span \(C \leftarrow A → X\),
|
||||||
where the left map is a monomorphism.} from \(C → X\). We can classify these these by the partial map classifier,
|
where the left map is a monomorphism.} from \(C → X\). We can classify these by the partial map classifier,
|
||||||
given by \(X^+ ≔ Σ_{φ:Ω}X^{[φ]}\)\todo{give a reference}. This is gives us an object \(X^+\) (technicaly equipped with a map into the terminal)
|
given by \(X^+ ≔ Σ_{φ:Ω}X^{[φ]}\) \cite{gambinoPolynomialFunctorsPolynomial2013}. This gives us an object \(X^+\) (technicaly equipped with a map into the terminal)
|
||||||
and a monomrphism \( η_X : X → X^+\) such that for evey partial map \(C → X\) there is a unique map \(a: C → X^+\) completing
|
and a monomrphism \( η_X : X ↣ X^+\) such that for every partial map \(C → X\) there is a unique map \(a: C → X^+\), completing
|
||||||
the following pullback square.
|
the following pullback square.
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
A \arrow[d, tail] \arrow[r] \pb & X \arrow[d,"η_X"] \\
|
A \arrow[d, tail] \arrow[r] \pb & X \arrow[d,"η_X"] \\
|
||||||
C \arrow[r, "a"] & X^+
|
C \arrow[r, "a"] & X^+
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
This makes \((−)^+\) into a pointed endofunctor, and with little surprise are the \(+\)-algebras in correspondence with
|
This makes \((−)^+\) into a pointed endofunctor, and with little surprise the \(+\)-algebras are in correspondence with
|
||||||
the \TFF-algebras.
|
the \TFF-algebras.
|
||||||
|
|
||||||
\begin{proposition}[{\cite[Proposition 15]{awodeyCartesianCubicalModel2023}}]
|
\begin{proposition}[{\cite[Proposition 15]{awodeyCartesianCubicalModel2023}}]
|
||||||
The algebras of the pointed endofunctor \((−)^+\) are in correspondence to the algebras of the pointed endofunctor \TFF
|
The algebras of the pointed endofunctor \((−)^+\) are in correspondence to the algebras of the pointed endofunctor \TFF
|
||||||
with codomain \(*\).
|
with codomain \(*\).
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
\begin{proof}[Proofsketch:]
|
\begin{proof}[Proof sketch:]
|
||||||
A \(+\)-algebra is an object \(X\) together with a morphism \(α : X^+ → X\) such that \(α η_x = \id\).
|
A \(+\)-algebra is an object \(X\) together with a morphism \(α : X^+ → X\) such that \(α η_x = \id\).
|
||||||
Take some lifting problem like \cref{diag:liftProbTerminal}, define the chosen map to be \(αa\). If we
|
Take some lifting problem like \cref{diag:liftProbTerminal}, define the chosen map to be \(αa\). If we
|
||||||
are given a chosen lift, we compose it with \(η_X\) to retrieve \(a\).
|
are given a chosen lift, we compose it with \(η_X\) to retrieve \(a\).
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
The benefit of \((−)^+\)-algebras is, that they are morphisms in \□ rather than in \(\□^→\).
|
The benefit of \((−)^+\)-algebras is, that they are morphisms in \□ rather than in \(\□^→\).
|
||||||
We can interalize the condition to be a \((−)^+\)-algebra by means of the internal \(\Hom\).
|
We can internalize the condition to be a \((−)^+\)-algebra by means of the internal \(\Hom\).
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
+\textrm{-Alg}(X)
|
+\textrm{-Alg}(X)
|
||||||
\arrow[d]
|
\arrow[d]
|
||||||
|
|
@ -495,11 +550,11 @@ We can interalize the condition to be a \((−)^+\)-algebra by means of the inte
|
||||||
\arrow[r,"λ\id_X"]
|
\arrow[r,"λ\id_X"]
|
||||||
& {[X,X]}
|
& {[X,X]}
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
It is immediatly clear that a sections of the left map correspond to the desired \(+\)-algebra structure.
|
It is immediatly clear that a section of the left map correspond to the desired \(+\)-algebra structure.
|
||||||
|
|
||||||
If we want to archive the same with a trivial fibration that has arbitrary codomain \(Y\), we might just move
|
If we want to archive the same with a trivial fibration that has arbitrary codomain \(Y\), we might just move
|
||||||
to the slice topos \(\faktor{\□}{Y}\), there such a map becomes again a map into the terminal.
|
to the slice topos \(\faktor{\□}{Y}\), there a map to \(Y\) map becomes again a map into the terminal.
|
||||||
To not be confused we will call the partial map classification functor in
|
To not be confused we will denote the partial map classification functor in
|
||||||
the slice over \(Y\) by the name \((−)^{+Y}\). The algebras will be called relative \(+\)-algberas.
|
the slice over \(Y\) by the name \((−)^{+Y}\). The algebras will be called relative \(+\)-algberas.
|
||||||
We have even more luck and this functor commutes with the pullback
|
We have even more luck and this functor commutes with the pullback
|
||||||
functor \(\□ → \faktor{\□}{Y}\),
|
functor \(\□ → \faktor{\□}{Y}\),
|
||||||
|
|
@ -515,51 +570,55 @@ functor \(\□ → \faktor{\□}{Y}\),
|
||||||
\arrow[u,"Y^*"]
|
\arrow[u,"Y^*"]
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
which allows us to compute it fiberwise \cite[Proposition 12]{awodeyCartesianCubicalModel2023}. This allows us to write
|
which allows us to compute it fiberwise \cite[Proposition 12]{awodeyCartesianCubicalModel2023}. This allows us to write
|
||||||
\((A)^{+Y} = Σ_{y:Y}A_y^+\), where \(A_y\) is the fiber of \(A\) at \(y\). We will still continue to write \(+\)-Alg, when
|
\((A)^{+Y} = Σ_{y:Y}A_y^+\), where \(A_y\) is the fiber of \(A\) at \(y\). We will still continue to write \(+\)-Alg, if
|
||||||
there is no confusion.
|
there is no ambiguity.
|
||||||
As all the involved functors \((−)^+\), pullbacks and exponentials are pullback stable so is \(+\)-Alg. Wich lets us conlude
|
As all the involved functors \((−)^+\), pullbacks and exponentials are pullback stable so is \(+\)-Alg. This lets us conlude
|
||||||
the following.
|
the following.
|
||||||
\begin{proposition}
|
\begin{proposition}
|
||||||
\(+\)-Alg is a classifying type for trivial cofibrations.
|
\(+\)-Alg is a classifying type for trivial cofibrations.
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
|
|
||||||
|
|
||||||
We will move down a very similar path as \cite{awodeyCartesianCubicalModel2023}, but need to keep track of the group
|
We will move down a very similar path as \cite{awodeyCartesianCubicalModel2023} but need to keep track of the group
|
||||||
actions of the symmetric groups on representables.
|
actions of the symmetric groups on representables.
|
||||||
For this we will pass to a category that \cite{solution} calls cubical species. The argument in essence will be very similar
|
For this, we will pass to a category that \cite{solution} calls cubical species. The argument in essence will be very similar
|
||||||
to the argument there, though in a different language.
|
to the argument there, though in a different language.
|
||||||
|
|
||||||
\begin{definition}[compare {\cite[Section 4]{solution}}]
|
\begin{definition}[compare {\cite[Section 4]{solution}}]
|
||||||
By abuse of notation we will say \(Σ_k\) to be the one object groupoid induced by the symmetric group \(Σ_k\).
|
By abuse of notation we will say \(Σ_k\) to be the one object groupoid induced by the symmetric group \(Σ_k\).
|
||||||
Let \(Σ ≔ ∐_{k ∈ ℕ} Σ_k\), we define \(\□^Σ\) to be the category of \emph{cubical species}. For a cubical
|
Let \(Σ ≔ ∐_{k ∈ ℕ} Σ_k\). We define \(\□^Σ\) to be the category of \emph{cubical species}. For a cubical
|
||||||
species \(A\) we write \(A_k\) for the cubical set in the image of \(Σ_k\).
|
species \(A\) we write \(A_k\) for the cubical set in the image of \(Σ_k\).
|
||||||
\end{definition}
|
\end{definition}
|
||||||
\begin{remark}
|
\begin{remark}
|
||||||
\(\□^Σ\) is a presheaf topos.
|
\(\□^Σ\) is a presheaf topos, regarded as \(\Set^{Σ × \FinSet}\).
|
||||||
\end{remark}
|
\end{remark}
|
||||||
\begin{remark}
|
\begin{remark}
|
||||||
\cite{solution} excludes the case for \(k = 0\), because they want to exhibit a model category on cubical species.
|
\cite{solution} excludes the case for \(k = 0\), because they want to exhibit a model category on cubical species.
|
||||||
For the construction on cubical Sets this makes no difference compare \cite[Remark 4.3.17]{solution}.
|
For the construction on cubical Sets this makes no difference, compare \cite[Remark 4.3.17]{solution}.
|
||||||
\end{remark}
|
\end{remark}
|
||||||
|
|
||||||
We need to define our equivalent of an interval, and the generic point inclusion. Recall that a functor from a group
|
We need to define the interval, and the generic point inclusion. Recall that a functor from a group
|
||||||
into a category is the same as choosing an object of that category together with a group action on it.
|
into a category is the same as choosing an object of that category together with a group action on it.
|
||||||
\begin{definition}[{\cite[Example 4.3.5]{solution}}]
|
\begin{definition}[{\cite[Example 4.3.5]{solution}}]
|
||||||
Let \(\mathrm{I} : Σ → \□\) be the functor that sends \(Σ_k\) to \(\I^k\) together with the group action that freely
|
Let \(\mathrm{I} : Σ → \□\) be the functor that sends \(Σ_k\) to \(\I^k\) together with the group action that freely
|
||||||
permutates the dimensions.
|
permutates the dimensions. Spelled out this means the if \(\I^k\) is represented by \(A = \{⊥|x_1,…,x_k |⊤\}\), then
|
||||||
|
an element \(σ ∈ Σ_k\) is send to the automorphism \(A ↦ \{⊥|x_{σ(1)},…,x_{σ(k)}|⊤\}\).
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
\begin{remark}
|
||||||
|
This is exactly the same group action we want our liftings be equivariant under, compare \cref{rem:modelStructure:checkov}.
|
||||||
|
\end{remark}
|
||||||
\begin{remark}[{\cite[Lemma 4.2.7]{solution}}]
|
\begin{remark}[{\cite[Lemma 4.2.7]{solution}}]
|
||||||
The interval \(\mathrm{I}\) is tiny.
|
The interval \(\mathrm{I}\) is tiny.
|
||||||
\end{remark}
|
\end{remark}
|
||||||
|
|
||||||
\begin{definition}[{\cite[Definition 4.3.3]{solution}}]
|
\begin{definition}[{\cite[Definition 4.3.3]{solution}}]
|
||||||
The diagonal \(δ : \mathrm{I} → \mathrm{I} × \mathrm{I}\) as a map in the slice \(\faktor{\□^Σ}{\mathrm{I}}\) is called
|
The diagonal \(δ : \mathrm{I} → \mathrm{I} × \mathrm{I}\) as a map in the slice \(\faktor{\□^Σ}{\mathrm{I}}\) is called
|
||||||
the generic point.
|
the \emph{generic point of \(\mathrm{I}\)}.
|
||||||
\end{definition}
|
\end{definition}
|
||||||
\begin{remark}\label{rem:modelStructure:cubicalSpeciesPremodelStructure}
|
\begin{remark}\label{rem:modelStructure:cubicalSpeciesPremodelStructure}
|
||||||
Our classifcation induce a premodle structure on cubical species, where the cofibrations are all monomorhpisms,
|
Our classifcation induce a premodle structure on cubical species, where the cofibrations are all monomorhpisms,
|
||||||
the trivial fibrations are classified by relative \(+\)-algebras and the fibrations are those maps such that their pullback
|
the trivial fibrations are classified by relative \(+\)-algebras and the fibrations are those maps such that their pullback
|
||||||
to the slice over \(\mathrm{I}\) are getting send
|
to the slice over \(\mathrm{I}\) are getting sent
|
||||||
to a trivial fibration by \(δ ⇒ (−)\). Premodel structures in this way are called \emph{generated by \(\mathrm{I}\)}.
|
to a trivial fibration by \(δ ⇒ (−)\). Premodel structures in this way are called \emph{generated by \(\mathrm{I}\)}.
|
||||||
\end{remark}
|
\end{remark}
|
||||||
\begin{remark}\label{rem:modelStructure:speciesPremodelSrtucture}
|
\begin{remark}\label{rem:modelStructure:speciesPremodelSrtucture}
|
||||||
|
|
@ -578,8 +637,7 @@ stable along right maps, for both factorization systems.
|
||||||
|
|
||||||
\begin{theorem}[{\cites[§5]{awodeyCartesianCubicalModel2023}{hazratpour2categoricalProofFrobenius2024}[Proposition 3.4.2]{solution}}]
|
\begin{theorem}[{\cites[§5]{awodeyCartesianCubicalModel2023}{hazratpour2categoricalProofFrobenius2024}[Proposition 3.4.2]{solution}}]
|
||||||
Let \(E\) be a locally cartesian closed category with a premodel structure in which the cofibrations are the monomorphisms.
|
Let \(E\) be a locally cartesian closed category with a premodel structure in which the cofibrations are the monomorphisms.
|
||||||
Suppose there is an object \(I\) such that a map is a fibration just when the Leibniz exponential of its pullback
|
Suppose it is generated by an interval,
|
||||||
to the slice over \(I\) by the diagonal \(δ : I → I × I\) is a trivial fibration in the slice premodel structure,
|
|
||||||
then the premodel structure satisfies the Frobenius condition.
|
then the premodel structure satisfies the Frobenius condition.
|
||||||
\end{theorem}
|
\end{theorem}
|
||||||
|
|
||||||
|
|
@ -590,11 +648,11 @@ stable along right maps, for both factorization systems.
|
||||||
% componentwise fibrations. But because we passed to \(\□^Σ\), the classifying type will have group actions on
|
% componentwise fibrations. But because we passed to \(\□^Σ\), the classifying type will have group actions on
|
||||||
% every level, and we need to restrict to those, that are invariant under those group actions.
|
% every level, and we need to restrict to those, that are invariant under those group actions.
|
||||||
|
|
||||||
The main idea to continue classifying uniform fibrations from here on out is quite simple. As being a uniform fibration is
|
The main idea to continue classifying uniform fibrations in \(\□^Σ\), from here on out is quite simple. As being a uniform fibration is
|
||||||
equivalent by being send to a trivial fibration by the right adjoint of the leibniz applicationfunctor of the interval,
|
equivalent by being send to a trivial fibration by the right adjoint of the Leibniz application functor of the interval,
|
||||||
we get that a \(+\)-algebra structure on \(δ ⇒ f\)\todo{write the right thing here}
|
we get that a \(+\)-algebra structure on \(δ ⇒ f\)
|
||||||
is equivalent to a \FF-algebra structure on \(f\). This must then
|
is equivalent to an \FF-algebra structure on \(f\). This must then
|
||||||
be reformulated, to get the desired map. This reformulation is quite tedious and so we will refer
|
be reformulated to get the desired map. This reformulation is quite tedious and so we will refer
|
||||||
for the details to
|
for the details to
|
||||||
\cite[The classifying types of unbiased fibration structures]{awodeyCartesianCubicalModel2023}.
|
\cite[The classifying types of unbiased fibration structures]{awodeyCartesianCubicalModel2023}.
|
||||||
In the source this takes place in \□, but it only makes use of the features we already established for \(\□^Σ\).
|
In the source this takes place in \□, but it only makes use of the features we already established for \(\□^Σ\).
|
||||||
|
|
@ -602,23 +660,23 @@ An important detail
|
||||||
to this procedure is, that in order to get the resulting classifying type pullback stable, this argument uses that
|
to this procedure is, that in order to get the resulting classifying type pullback stable, this argument uses that
|
||||||
the interval is tiny.
|
the interval is tiny.
|
||||||
|
|
||||||
We get a pullback stable construction \(\Fib^Σ(f)\)\footnote{this can be made into a classifying type for some
|
We get a pullback stable construction \(\Fib^Σ(f)\),
|
||||||
awfs compare \cite[Section 4.]{solution}}\todo{this footnote 2 is bad, but how to make different}
|
|
||||||
whose sections now correspond componentwise to \FF-algebra structures, that are equivariant with respect
|
whose sections now correspond componentwise to \FF-algebra structures, that are equivariant with respect
|
||||||
to the group action of \(Σ^k\).
|
to the group action of \(Σ^k\).\footnote{This can be made into a classifying type for some
|
||||||
|
awfs compare \cite[Section 4.]{solution}.}
|
||||||
|
|
||||||
We now going to extract the classifying type for equivariant cubical fibrations. For this we need to relate cubical sets
|
We are now going to extract the classifying type for equivariant cubical fibrations. For this we need to relate cubical sets
|
||||||
and cubical species. There exists the constant diagram functor \(Δ\) that sends a cubical set to the constant cubical species.
|
and cubical species. There exists the constant diagram functor \(Δ\) that sends a cubical set to the constant cubical species.
|
||||||
|
|
||||||
|
|
||||||
Since \□ is complete this functor has a right adjoint\footnote{and also a left adjoint as \□ is co-complete}
|
Since \□ is complete this functor has a right adjoint\footnote{and also a left adjoint as \□ is co-complete.}
|
||||||
\(Γ\) compare \cite[Section 5.1]{solution}, which is given by
|
\(Γ\) compare \cite[Section 5.1]{solution}, which is given by
|
||||||
|
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
Γ(A) ≔ ∏\limits_{k∈ℕ}(A_k)^{Σ_k}
|
Γ(A) ≔ ∏\limits_{k∈ℕ}(A_k)^{Σ_k}
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
|
|
||||||
where \((A_k)^Σ_k\) is the cubical set of \(Σ_k\) fixed points. It is not hard to see that this is indeed
|
where \((A_k)^Σ_k\) is the cubical set of \(Σ_k\) fixed points. It is not hard to see, that this is indeed
|
||||||
the right adjoint functor.
|
the right adjoint functor.
|
||||||
|
|
||||||
\begin{proposition}
|
\begin{proposition}
|
||||||
|
|
@ -627,15 +685,18 @@ the right adjoint functor.
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
We need to show
|
We need to show
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
\Hom_{\□^Σ}(Δ(A),B) = \Hom_{\□}\left(A,∏\limits_{k∈ℕ}(B_k)^{Σ_k}\right) \text{.}
|
\Hom_{\□^Σ}(Δ(A),B) = \Hom_{\□}\left(A,∏\limits_{k∈ℕ}(B_k)^{Σ_k}\right)
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
But this is immediatly clear, on the right hand side we have componentwise equivariant natural translations
|
But this is immediatly clear: on the right hand side, we have componentwise equivariant natural translations
|
||||||
from \(Δ(A)_k = A\) to \(B_k\). They can only be valued in the fixed points in \(B_k\) as \(Δ(A)_k\) carries the
|
from \(Δ(A)_k = A\) to \(B_k\). They can only be valued in the fixed points in \(B_k\) as \(Δ(A)_k\) carries the
|
||||||
trivial group action. A map on the right side is also a collection of natural transformations from \(A\) to
|
trivial group action. A map on the right side is also a collection of natural transformations from \(A\) to
|
||||||
the fixed points of \(B_k\).
|
the fixed points of \(B_k\).
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
We get now that an \FF-algebra on \(f : A → B\) structure corresponds to a section
|
As the sections of the classifying types in \(\□^Σ\), correspond componentwise to choice
|
||||||
|
functions of lifts in \(\□\), for different dimensional box fillings, and they are
|
||||||
|
equivariant by virtue of being a morphism in \(\□^Σ\),
|
||||||
|
we get now that an \FF-algebra on \(f : A → B\) structure corresponds to a section.
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
{} & \mathrm{Fib}^{Σ_k}(Δ(A))
|
{} & \mathrm{Fib}^{Σ_k}(Δ(A))
|
||||||
\arrow[d,"\mathrm{Fib}^{Σ_k}(Δ(f))"]
|
\arrow[d,"\mathrm{Fib}^{Σ_k}(Δ(f))"]
|
||||||
|
|
@ -643,7 +704,7 @@ We get now that an \FF-algebra on \(f : A → B\) structure corresponds to a sec
|
||||||
\arrow[ru, dashed]
|
\arrow[ru, dashed]
|
||||||
& Δ(B)
|
& Δ(B)
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
By adjointness we can transpose this lift to a lift in cubical sets, and by pulling back
|
By adjointness, we can transpose this lift to a lift in cubical sets, and by pulling back
|
||||||
along the adjunction unit to splits of a map over \(B\) (compare \cite[Lemma 5.3.3,2.1.16]{solution}).
|
along the adjunction unit to splits of a map over \(B\) (compare \cite[Lemma 5.3.3,2.1.16]{solution}).
|
||||||
\begin{eqcd*}[row sep=large]
|
\begin{eqcd*}[row sep=large]
|
||||||
\mathrm{Fib}(B)
|
\mathrm{Fib}(B)
|
||||||
|
|
@ -659,7 +720,7 @@ along the adjunction unit to splits of a map over \(B\) (compare \cite[Lemma 5.3
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
|
|
||||||
\begin{remark}
|
\begin{remark}
|
||||||
From this discussion it is also clear that \(f\) is a fibration in \□, if and only if \(Δ(f)\) is
|
From this discussion it is also clear that \(f\) is a equivariant fibration in \□, if and only if \(Δ(f)\) is
|
||||||
a fibration in \(\□^Σ\).
|
a fibration in \(\□^Σ\).
|
||||||
\end{remark}
|
\end{remark}
|
||||||
|
|
||||||
|
|
@ -668,13 +729,13 @@ This is mainly taken from \cite[Section 7]{awodeyHofmannStreicherUniverses2023}.
|
||||||
One might hope that we can construct a universal fibration, in the sense that every fibration
|
One might hope that we can construct a universal fibration, in the sense that every fibration
|
||||||
is a pullback of this universal fibration. This can not happen for size reasons. We will do
|
is a pullback of this universal fibration. This can not happen for size reasons. We will do
|
||||||
the next best thing and construct a universe for big enough kardinals \(κ\). Because
|
the next best thing and construct a universe for big enough kardinals \(κ\). Because
|
||||||
our set theory has Grothendieck universes this will give us universes for \(κ\) small fibrations.
|
our set theory has Grothendieck universes, this will give us enough universes to classify all fibrations.
|
||||||
|
|
||||||
To start we will call our Hofmann-Streicher, or \(κ\)-small map classifier, \({p : \dot{\mathcal{V}}_κ → \mathcal{V}_κ}\).
|
To start we will call our Hofmann-Streicher, or \(κ\)-small map classifier \({p : \dot{\mathcal{V}}_κ → \mathcal{V}_κ}\).
|
||||||
|
|
||||||
\begin{theorem}[{\cite[Proposition 10]{awodeyHofmannStreicherUniverses2023}}]
|
\begin{theorem}[{\cite[Proposition 10]{awodeyHofmannStreicherUniverses2023}}]
|
||||||
For a large enough \(κ\), there is a universe for \(κ\)-small fibrant maps, in the sense that there is
|
For a large enough \(κ\), there is a universe for \(κ\)-small fibrant maps, in the sense that there is
|
||||||
a small fibration \(π : \dot{\mathcal{U}}_κ → \mathcal{U}_κ\) such that every small fibration \(f : A → X\), is
|
a small fibration \(π : \dot{\mathcal{U}}_κ → \mathcal{U}_κ\) such that every small fibration \(f : A → X\) is
|
||||||
a pullback of it along a connonical classifying map \(a\)
|
a pullback of it along a connonical classifying map \(a\)
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
A
|
A
|
||||||
|
|
@ -705,7 +766,7 @@ and building the following pullback.
|
||||||
\arrow[r,"\mathrm{Fib}(p)"]
|
\arrow[r,"\mathrm{Fib}(p)"]
|
||||||
& \mathcal{V}
|
& \mathcal{V}
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
To see this is a fibration we will exhibit we exhibit a split of the classifying type of \(π_κ\).
|
To see that this is a fibration, we will exhibit we exhibit a split of the classifying type of \(π_κ\).
|
||||||
As the classifying type is pullback stable we get the following diagram
|
As the classifying type is pullback stable we get the following diagram
|
||||||
\begin{eqcd*}[]
|
\begin{eqcd*}[]
|
||||||
\dot{\mathcal{U}}_κ
|
\dot{\mathcal{U}}_κ
|
||||||
|
|
@ -727,8 +788,8 @@ As the classifying type is pullback stable we get the following diagram
|
||||||
\arrow[u,"\mathrm{Fib}(p)"]
|
\arrow[u,"\mathrm{Fib}(p)"]
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
The lower pullback square is a pullback of \(\Fib(p)\) along itself. This map has a split, namely the diagonal.
|
The lower pullback square is a pullback of \(\Fib(p)\) along itself. This map has a split, namely the diagonal.
|
||||||
To show that this classifies small fibrations, let us consider a small fibration \(f : A → X\).
|
To show that this classifies small fibrations, we consider a small fibration \(f : A → X\).
|
||||||
Because it is a small map we get it as a pull back along a cannonical map \(a : X → \mathcal{V}\).
|
Because it is a small map we get it as a pull back along a canonical map \(a : X → \mathcal{V}\).
|
||||||
\begin{eqcd*}[row sep=small, column sep=small]
|
\begin{eqcd*}[row sep=small, column sep=small]
|
||||||
{}
|
{}
|
||||||
& {}
|
& {}
|
||||||
|
|
@ -778,16 +839,18 @@ As \(f\) is a fibration, we get a split \(s\) of the fibration structure. And so
|
||||||
\arrow[r]
|
\arrow[r]
|
||||||
& X
|
& X
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
Note that if either projection is a trivial fibration, then both are.
|
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
\begin{remark*}
|
||||||
|
Note that if either projection is a trivial fibration, then both are.
|
||||||
|
\end{remark*}
|
||||||
|
|
||||||
\begin{lemma}[{\cite[Lemma 95]{awodeyCartesianCubicalModel2023}}]\label{lem:modelStructure:weakProposition}
|
\begin{lemma}[{\cite[Lemma 95]{awodeyCartesianCubicalModel2023}}]\label{lem:modelStructure:weakProposition}
|
||||||
For any \(A → X\), the classifying type \(\TFib(A) → X\) is a weak proposition. Moreover, the same is true for \(\Fib(A) → X\).
|
For any \(A → X\), the classifying type \(\TFib(A) → X\) is a weak proposition. Moreover, the same is true for \(\Fib(A) → X\).
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
We again will give the proofidea, sort out the differences for the equivariant case and refer the reader to the
|
We again will discuss the proof idea, sort out the differences for the equivariant case and refer to the
|
||||||
source material for the technical details.
|
source material for the technical details.
|
||||||
\begin{proof}[Proofsketch:]
|
\begin{proof}[Proof sketch:]
|
||||||
We first prove the case for \(\TFib\) and afterwards reduce the case the \Fib case to it.
|
We first prove the case for \(\TFib\) and afterwards reduce the \Fib case to it.
|
||||||
We first note that if a map \(A → X\) is a trivial fibration, so is \(\TFib(A) → X\). This is
|
We first note that if a map \(A → X\) is a trivial fibration, so is \(\TFib(A) → X\). This is
|
||||||
because if we expand the definition and look at the \(+\)-algebra structure, the map \(η_x : X → X^+\)
|
because if we expand the definition and look at the \(+\)-algebra structure, the map \(η_x : X → X^+\)
|
||||||
is always monic.
|
is always monic.
|
||||||
|
|
@ -811,25 +874,26 @@ source material for the technical details.
|
||||||
& & |[alias=X]| X
|
& & |[alias=X]| X
|
||||||
\arrow[from=A,to=X,crossing over, "f" near start]
|
\arrow[from=A,to=X,crossing over, "f" near start]
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
Since \(\TFib\) is stable under pullback we hav that \( \TFib(\TFib(A) ×_X A) \) is isomporhic to
|
Since \(\TFib\) is stable under pullback we have that \( \TFib(\TFib(A) ×_X A) \) is isomorphic to
|
||||||
\( \TFib(A) ×_X \TFib(A) \), and since the latter has a canonical section \(\TFib(A) ×_X A → \TFib(A) ×_X \TFib(A)\),
|
\( \TFib(A) ×_X \TFib(A) \), and since the latter has a canonical section \({\TFib(A) ×_X A} → {\TFib(A) ×_X \TFib(A)}\).
|
||||||
the \(\TFib(A) ×_X A\) is a trivial fibration over \(\TFib(A)\). By our note above we see that also \( \TFib(A) ×_X \TFib(A)\) is
|
Therefore \(\TFib(A) ×_X A\) is a trivial fibration over \(\TFib(A)\). By previous consideration, we see that also \( \TFib(A) ×_X \TFib(A)\) is
|
||||||
a trivial fibration over \(\TFib(A)\).
|
a trivial fibration over \(\TFib(A)\).
|
||||||
|
|
||||||
For \Fib we trace now through the whole construction process, and reduce it to the case above. For the technical details
|
For \Fib, we now trace through the whole construction process, and reduce it to the case above. For the technical details,
|
||||||
we refer to the source material. For our deviation in the construction we need a few additional properties. Namely
|
we refer to the source material. For our deviation in the construction, we need a few additional properties. Namely
|
||||||
the constant diagram functor preserves monomorhpisms, which is obviously true, and that taking exponentials with the
|
the constant diagram functor preserves monomorhpisms, which is obviously true, and that taking exponentials with the
|
||||||
interval in cubical species preserves monomorhpisms. As \(Σ\) has only endomorphisms, this reduces again
|
interval in cubical species preserves monomorhpisms. As \(Σ\) has only endomorphisms, this reduces again
|
||||||
to a componentwise check in \□, where we already know it by \cref{TODO}.\todo{show this}
|
to a componentwise check in \□, where we see this easily being true for the interval, and the rest follows from \(□\) being
|
||||||
|
closed under products.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
\begin{remark}
|
\begin{remark}
|
||||||
The source has an additional condition, that in our setting is true.
|
The source has an additional condition, that in our setting is true.
|
||||||
\end{remark}
|
\end{remark}
|
||||||
|
|
||||||
\begin{lemma}[{\cite[Lemma 96]{awodeyCartesianCubicalModel2023}}]
|
\begin{lemma}[{\cite[Lemma 96]{awodeyCartesianCubicalModel2023}}]
|
||||||
The univeres \(\mathcal{U}_κ\) satisfies \emph{realignment} in the following senes.
|
The univeres \(\mathcal{U}_κ\) satisfies \emph{realignment} in the following sense.
|
||||||
Given a \(κ\)-small fibration \(g : A → X\) and a cofibration \(c : C → X\), let \(f_c : C → \mathcal{U}_κ\) classify the pullback
|
Given a \(κ\)-small fibration \(g : A → X\) and a cofibration \(c : C ↣ X\), let \(f_c : C → \mathcal{U}_κ\) classify the pullback
|
||||||
\(c^∗A → C\). Then there is a classifying map \(f : X ↣ \mathcal{U}_κ\) for \(A\) with \(f c = f_c\).
|
\(c^∗A → C\). Then there is a classifying map \(f : X →\mathcal{U}_κ\) for \(A\) with \(f c = f_c\).
|
||||||
\begin{eqcd*}[row sep = small, column sep = small]
|
\begin{eqcd*}[row sep = small, column sep = small]
|
||||||
c^*F
|
c^*F
|
||||||
\arrow[rr]
|
\arrow[rr]
|
||||||
|
|
@ -857,7 +921,7 @@ source material for the technical details.
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
|
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
First, we extend this diagram by the small map classifier and, by realignment for HS-Universes \cref{TODO}\todo{make a lemma, or cite}
|
First, we extend this diagram by the small map classifier and by realignment for HS-Universes \cite[Proposition 6]{awodeyHofmannStreicherUniverses2023},
|
||||||
we get an extension \(f_0\).
|
we get an extension \(f_0\).
|
||||||
\begin{eqcd*}[row sep = small, column sep = small]
|
\begin{eqcd*}[row sep = small, column sep = small]
|
||||||
c^*F
|
c^*F
|
||||||
|
|
@ -926,7 +990,7 @@ source material for the technical details.
|
||||||
\arrow[r]
|
\arrow[r]
|
||||||
& \V
|
& \V
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
By \cref{lem:modelStructure:weakProposition} \(\Fib(\Vd) = \U → \V\) is a weak proposition, this means
|
By \cref{lem:modelStructure:weakProposition}, \(\Fib(\Vd) = \U → \V\) is a weak proposition, this means
|
||||||
\(π_1\) is a trivial fibration and we get a lift \(f_2 : X → \U ×_{\V} \U\), by normal lifting properties.
|
\(π_1\) is a trivial fibration and we get a lift \(f_2 : X → \U ×_{\V} \U\), by normal lifting properties.
|
||||||
Taking \(f ≔ π_2 f_2\) gives another classifying map for the fibration structure, for which
|
Taking \(f ≔ π_2 f_2\) gives another classifying map for the fibration structure, for which
|
||||||
\(fc=f_c\) as required.
|
\(fc=f_c\) as required.
|
||||||
|
|
@ -962,8 +1026,7 @@ source material for the technical details.
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
\todo{in leibniz chapter introduce \(δ ⇒ f\) in the slice}
|
Let us write out \(δ ⇒ f\). \todo{introduce notation for generic point}
|
||||||
Let us write out \(δ ⇒ f\).
|
|
||||||
\[δ ⇒ f = ⟨f^\mathrm{I} × \id_\mathrm{I}, ⟨\mathsf{ev}, p_2⟩⟩: Y^\mathrm{I} × \mathrm{I} → (X^\mathrm{I} × \mathrm{I}) ×_{X×\mathrm{I}} (Y × \mathrm{I})\]
|
\[δ ⇒ f = ⟨f^\mathrm{I} × \id_\mathrm{I}, ⟨\mathsf{ev}, p_2⟩⟩: Y^\mathrm{I} × \mathrm{I} → (X^\mathrm{I} × \mathrm{I}) ×_{X×\mathrm{I}} (Y × \mathrm{I})\]
|
||||||
We interpolate the above pullback square with another one.
|
We interpolate the above pullback square with another one.
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
|
|
@ -988,7 +1051,7 @@ source material for the technical details.
|
||||||
\(Y' \simeq (X^\mathrm{I} × \mathrm{I}) ×_{X×\mathrm{I}} (Y × \mathrm{I})\) and \(δ ⇒ f \simeq u\).
|
\(Y' \simeq (X^\mathrm{I} × \mathrm{I}) ×_{X×\mathrm{I}} (Y × \mathrm{I})\) and \(δ ⇒ f \simeq u\).
|
||||||
\end{proof}
|
\end{proof}
|
||||||
\begin{corollary}[{\cite[Corollary 27]{awodeyCartesianCubicalModel2023}}]\label{cor:27}
|
\begin{corollary}[{\cite[Corollary 27]{awodeyCartesianCubicalModel2023}}]\label{cor:27}
|
||||||
An \(X\) in \(\□^Σ\) is fibrant if and only if the canonical map \(u\) to the pullback, in the following diagram
|
\(X\) in \(\□^Σ\) is fibrant if and only if the canonical map \(u\) to the pullback, in the following diagram
|
||||||
is a trivial fibration.
|
is a trivial fibration.
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
X^{\mathrm{I}} × \mathrm{I}
|
X^{\mathrm{I}} × \mathrm{I}
|
||||||
|
|
@ -1095,7 +1158,7 @@ source material for the technical details.
|
||||||
& & Z × \mathrm{I}
|
& & Z × \mathrm{I}
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
This is exactly the definition of pushout product so we have \(d = c \× δ\), which is a trivial cofibration.
|
This is exactly the definition of pushout product so we have \(d = c \× δ\), which is a trivial cofibration.
|
||||||
And as \(\□^Σ\) has the equivalence extension property \cref{rem:modelStructure:cubicalSpeciesEquivalenceExtension},
|
And as \(\□^Σ\) has the equivalence extension property, see \cref{rem:modelStructure:cubicalSpeciesEquivalenceExtension},
|
||||||
we can extend \([a,b]\) to the desired map in \cref{eq:modelStructure:mapEq}, and with this we get our desired lift.
|
we can extend \([a,b]\) to the desired map in \cref{eq:modelStructure:mapEq}, and with this we get our desired lift.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
|
|
@ -1104,24 +1167,22 @@ source material for the technical details.
|
||||||
|
|
||||||
\todo{introduce Leibniz pullback exponential}
|
\todo{introduce Leibniz pullback exponential}
|
||||||
\todo{introduced (unbiased) uniform fibrations and how they behave with leibniz constructions}
|
\todo{introduced (unbiased) uniform fibrations and how they behave with leibniz constructions}
|
||||||
\todo{hate my life}
|
|
||||||
|
|
||||||
\subsubsection{From Premodel Structure to Model Structure}
|
\subsubsection{From Premodel Structure to Model Structure}
|
||||||
From here on we assume our constructed universe is fibrant. \todo{hopefully we can get rid of this}
|
|
||||||
We are now ready to verify the last precondition of \cref{thm:premodelIsModel}.
|
We are now ready to verify the last precondition of \cref{thm:premodelIsModel}.
|
||||||
|
|
||||||
\begin{proposition}
|
\begin{proposition}
|
||||||
Fibrant universes imply the fibrant extension property.
|
Fibrant universes with realignment imply the fibrant extension property.
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Let \(f : A → X\) be a fibration and \(m : X → Y\) be a cofibration. Let \(κ\) be large enough so that
|
Let \(f : A → X\) be a fibration and \(m : X ↣ Y\) be a cofibration. Let \(κ\) be large enough so that
|
||||||
\(f\) is \(κ\)-small. We can classify \(f\) by a map \(a : X → \U\) and get the following diagram in the base.
|
\(f\) is \(κ\)-small. We can classify \(f\) by a map \(a : X → \U\) and get the following diagram in the base.
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
X \arrow[r,"a"] \arrow[d,"m"] & \U \arrow[d] \\
|
X \arrow[r,"a"] \arrow[d,"m",tail] & \U \arrow[d] \\
|
||||||
X' \arrow[r] \arrow[ru, dashed,"a'"] & *
|
Y \arrow[r] \arrow[ru, dashed,"a'"] & *
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
As \U is fibrant this gives us a lift \(a'\). We can then get the required fibration by pulling
|
As \U is fibrant, this gives us a lift \(a'\). We can then get the required fibration by pulling
|
||||||
back \(π_κ\) along \(a'\).
|
back \(π_κ\) along \(a'\)
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
A
|
A
|
||||||
\arrow[rr]
|
\arrow[rr]
|
||||||
|
|
@ -1146,19 +1207,19 @@ We are now ready to verify the last precondition of \cref{thm:premodelIsModel}.
|
||||||
&
|
&
|
||||||
\arrow[from=F, to=X, crossing over, dashed]
|
\arrow[from=F, to=X, crossing over, dashed]
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
Making the required diagram a pullback, by the double pullback lemma.
|
making the required diagram a pullback, by the double pullback lemma.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
\subsection{Dedekind Cubes}
|
\subsection{Dedekind Cubes}
|
||||||
We will also need a description of the model structure on the Dedekind cubes. It is similar in construction, we just
|
We will also need a description of the model structure on the Dedekind cubes.
|
||||||
don't need explicit equivariance. It turns out that in the presence of connections we get equivariance for free
|
As it is not our main focus of this thesis, we will describe the premodel structure
|
||||||
\cite[Remark 4.2.26]{cavalloRelativeEleganceCartesian2022}. While the argument that this modelstructure indeed is a
|
and give some hints how to go from there, but don't carry out the whole universe construction.
|
||||||
model structure constructing univalent universes is somewhat easier, as we can extract it from an internal description
|
It turns out that in the presence of connections we get liftings of a general point and equivariance for free
|
||||||
in the presheaf topos, by using strategies from \cite{LOPS}. As we only need this model structure for a later argument
|
\cite[Remark 4.2.26 \& Corollary 4.2.24]{cavalloRelativeEleganceCartesian2022}. While the argument that this modelstructure indeed is a
|
||||||
we will not present all the arguments here.
|
model structure constructing universes is somewhat easier, as we can extract it from an internal description
|
||||||
|
in the presheaf topos, by using strategies from \cite{LOPS}.
|
||||||
|
|
||||||
Characterizing cofibrations and trivial fibrations will done as above.
|
Characterizing cofibrations and trivial fibrations will done as above.
|
||||||
|
|
||||||
\begin{definition}
|
\begin{definition}
|
||||||
A \emph{generating cofibration} is a monomorphism into a cube \(c : C ↣ \I^n\)
|
A \emph{generating cofibration} is a monomorphism into a cube \(c : C ↣ \I^n\)
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
@ -1170,7 +1231,7 @@ Characterizing cofibrations and trivial fibrations will done as above.
|
||||||
It will be usefull for our later development, to give a characterization in the internal language of the presheaf topos
|
It will be usefull for our later development, to give a characterization in the internal language of the presheaf topos
|
||||||
\(\□_{∧∨}\). For more details on the interpretation of the internal semantics of cubical sets see \cite{awodeyKripkeJoyalForcingType2021}.
|
\(\□_{∧∨}\). For more details on the interpretation of the internal semantics of cubical sets see \cite{awodeyKripkeJoyalForcingType2021}.
|
||||||
For the this style of modeling cubical type thoery inside of topoi see \cite{ortonAxiomsModellingCubical2018}.
|
For the this style of modeling cubical type thoery inside of topoi see \cite{ortonAxiomsModellingCubical2018}.
|
||||||
We will first give the characterization, then try to give some intuition why it makes sense and afterwards give a prove.
|
We will first give the characterization, then try to give some intuition why it makes sense.
|
||||||
|
|
||||||
|
|
||||||
\begin{equation}\label{eq:TFib}
|
\begin{equation}\label{eq:TFib}
|
||||||
|
|
@ -1201,15 +1262,14 @@ does not appear explicitly in this description, but happens automatically as pul
|
||||||
interpretation of substitutions, and the type thoeretic rules around substitution already imply a uniform
|
interpretation of substitutions, and the type thoeretic rules around substitution already imply a uniform
|
||||||
choice of our lifts.
|
choice of our lifts.
|
||||||
|
|
||||||
\todo{give a proof or get rid of the claim that we do}
|
We can also give an anolog description of fibrations. As we do not need to think about equivariance,
|
||||||
|
or the generic point the descriptions
|
||||||
We can also give an anolog description of fibrations. As we do not need to think about equivariance the descriptions
|
|
||||||
gets a bit less involved but stays basically the same.
|
gets a bit less involved but stays basically the same.
|
||||||
|
|
||||||
\begin{definition}
|
\begin{definition}
|
||||||
Let \(c : C ↣ \I^n\) be monic a \emph{generating trivial cofibration} is a map of the form
|
Let \(c : C ↣ \I^n\) be monic a \emph{generating trivial cofibration} is a map of the form
|
||||||
\( c \× δ_k\)
|
\( c \× δ_k\)
|
||||||
\end{definition}
|
\end{definition} \todo{introduce \(δ\) and \(δ_k in cubicals\)}
|
||||||
|
|
||||||
\begin{definition}
|
\begin{definition}
|
||||||
A \emph{uniform fibration} is a uniform right lifting map against generating trivial cofibrations.
|
A \emph{uniform fibration} is a uniform right lifting map against generating trivial cofibrations.
|
||||||
|
|
@ -1219,9 +1279,46 @@ gets a bit less involved but stays basically the same.
|
||||||
The uniform fibrations of \(□_{∧∨}\) are equivariant.
|
The uniform fibrations of \(□_{∧∨}\) are equivariant.
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
|
|
||||||
|
There is an analog internal description to the trivial fibration case, just a bit more involved. For details
|
||||||
|
see \cites[Section 5]{ortonAxiomsModellingCubical2018}, the very short version of this is, that we can
|
||||||
|
describe the the classifying type directly in the internal language of the topos, having a specific form,
|
||||||
|
\[
|
||||||
|
\mathrm{isFib} (A) ≔ (p : \I → Γ) → \mathrm{Comp}\,(A ◦ p)
|
||||||
|
\]
|
||||||
|
where \(\mathrm{Comp}\) is some term, for the details see \cite[Eq 5.10]{ortonAxiomsModellingCubical2018}.
|
||||||
|
Terms of this type correspond to terms of \(\mathrm{Comp}\,(A ◦ p)\) in the context of \(Γ^\I\).
|
||||||
|
We can then extract the classifying types back out of it by means of the right adjoint of \((−)^\I ⊣ \sqrt{−}\).
|
||||||
|
Transposing
|
||||||
|
\begin{eqcd*}
|
||||||
|
Γ^{\I}
|
||||||
|
\arrow[r,dashed]
|
||||||
|
\arrow[dr,"\id"]
|
||||||
|
& Σ p : Γ^{\I}, \mathrm{Comp}\,(A◦p)
|
||||||
|
\arrow[d,"p_1"]
|
||||||
|
\\
|
||||||
|
{}
|
||||||
|
& Γ^{\I}
|
||||||
|
\end{eqcd*}
|
||||||
|
to
|
||||||
|
\begin{eqcd*}
|
||||||
|
Γ
|
||||||
|
\arrow[r, dashed]
|
||||||
|
\arrow[rr,dashed, bend left=15]
|
||||||
|
\arrow[dr,"\id"]
|
||||||
|
& \Fib(A)
|
||||||
|
\arrow[r]
|
||||||
|
\pb
|
||||||
|
\arrow[d]
|
||||||
|
& \sqrt{Σ p : Γ^{\I}, \mathrm{Comp}\,(A◦p)}
|
||||||
|
\arrow[d,"\sqrt{p_1}"]
|
||||||
|
\\
|
||||||
|
{}
|
||||||
|
& Γ \arrow[r,"η"]
|
||||||
|
& \sqrt{Γ^{\I}}
|
||||||
|
\end{eqcd*}
|
||||||
|
It might look like we had won exactly nothing, but that isn't true. If we plug in for the type \(A\) over \(Γ\) our
|
||||||
|
Hofmann-Streicher universe, this will directly extract us a universe for fibrations. For details on this
|
||||||
|
procedure see \cite[Theorem 5.2]{LOPS}.
|
||||||
% % \subsubsubsection{Internal description}
|
% % \subsubsubsection{Internal description}
|
||||||
% For our further development we also want an internal description of our fibrations. This turns out to be more tricky then
|
% For our further development we also want an internal description of our fibrations. This turns out to be more tricky then
|
||||||
% the trivial fibration variant for multiple reasons. The first is, that trivial cofibrations are harder to describe then
|
% the trivial fibration variant for multiple reasons. The first is, that trivial cofibrations are harder to describe then
|
||||||
|
|
|
||||||
|
|
@ -9,7 +9,9 @@
|
||||||
|
|
||||||
|
|
||||||
% \subfile{Model_Categories}
|
% \subfile{Model_Categories}
|
||||||
\subfile{Leibniz_Construction}
|
\section{Preliminaries}
|
||||||
|
\subfile{Algebraic_Weak_Factorization_System}
|
||||||
|
\subfile{MWE}
|
||||||
\subfile{Cubical_Set}
|
\subfile{Cubical_Set}
|
||||||
\subfile{Model_Structure}
|
\subfile{Model_Structure}
|
||||||
% \subfile{Reedy_Categories}
|
% \subfile{Reedy_Categories}
|
||||||
|
|
|
||||||
26
src/Preliminaries/erklaerung.tex
Normal file
26
src/Preliminaries/erklaerung.tex
Normal file
|
|
@ -0,0 +1,26 @@
|
||||||
|
% Keine Kopf-/Fußzeile auf dieser Seite
|
||||||
|
\documentclass[../Main.tex]{subfiles}
|
||||||
|
\begin{document}
|
||||||
|
\thispagestyle{empty}
|
||||||
|
|
||||||
|
%\vspace*{4cm}
|
||||||
|
|
||||||
|
|
||||||
|
\section*{Thesis Statement pursuant to \S22 paragraph 7 of APB TU Darmstadt}
|
||||||
|
|
||||||
|
I herewith formally declare that I, Dennis Frieberg, have written the submitted thesis independently pursuant to \S 22 paragraph 7 of APB TU Darmstadt without any outside support and using only the quoted literature and other sources. I did not use any outside support except for the quoted literature and other sources mentioned in the paper. I have clearly marked and separately listed in the text the literature used literally or in terms of content and all other sources I used for the preparation of this academic work. This also applies to sources or aids from the Internet.
|
||||||
|
This thesis has not been handed in or published before in the same or similar form.
|
||||||
|
|
||||||
|
I am aware, that in case of an attempt at deception based on plagiarism (\S38 Abs. 2 APB), the thesis would be graded with 5,0 and counted as one failed examination attempt. The thesis may only be repeated once.
|
||||||
|
|
||||||
|
\vspace{20pt}
|
||||||
|
|
||||||
|
\noindent
|
||||||
|
Darmstadt, 9.8.2024\vspace{30pt}
|
||||||
|
|
||||||
|
% Unterschrift (handgeschrieben)
|
||||||
|
|
||||||
|
\noindent
|
||||||
|
Signature of author \\
|
||||||
|
\includegraphics[scale=0.15]{../Unterschrift_dennis.png}
|
||||||
|
\end{document}
|
||||||
|
|
@ -7,18 +7,18 @@ For this section we fix the following notation. We write \(n\) for a set with ca
|
||||||
and identify \(2\) with the set \(\{⊥,⊤\}\). We write \([n]\) for the well ordered sets
|
and identify \(2\) with the set \(\{⊥,⊤\}\). We write \([n]\) for the well ordered sets
|
||||||
\(\{0,…,n\}\).
|
\(\{0,…,n\}\).
|
||||||
|
|
||||||
We would love to compare the model categories on \(\□\) and \(\Δ\). For this we want at least
|
We would love to compare the model categories on \(\□\) and \(\Δ\). For this, we want at least
|
||||||
an adjoint pair between those. If we somehow could get a functor on the site level, we could
|
an adjoint pair between those. If we somehow could get a functor on the site level, we could
|
||||||
get an adjoint triple. But there is no immediate obvious functor to do the job.
|
get an adjoint triple. But there is no immediate obvious functor to do the job.
|
||||||
The usual trick would be to go look at the idempotent completions of these categories. These
|
The usual trick would be to go look at the idempotent completions of these categories. These
|
||||||
usually have :w
|
usually have
|
||||||
more objects and are sometimes more suitable as the codomain of a functor, while
|
more objects and are sometimes more suitable as the codomain of a functor, while
|
||||||
the presheaf category stays the same (up to equivalence).
|
the presheaf category stays the same (up to equivalence).
|
||||||
For example, the idempotent completion of \dCube is the category \FL of finite lattices and
|
For example, the idempotent completion of \dCube is the category \FL of finite lattices and
|
||||||
monotone maps \cites{streicherSimplicialSetsCubical2021}{sattlerIdempotentCompletionCubes2019}.
|
monotone maps \cites{streicherSimplicialSetsCubical2021}{sattlerIdempotentCompletionCubes2019}.
|
||||||
So we have automatically \(\widehat{\FL} = \dcSet\),
|
So we have automatically \(\widehat{\FL} = \dcSet\),
|
||||||
and there is an obvious inclusion \(i: Δ → \FL\). Sadly for us \(□\) is already idempotent complete.
|
and there is an obvious inclusion \(i: Δ → \FL\). Sadly for us, \(□\) is already idempotent complete.
|
||||||
To get around this issue we can embed \(j: □ → \dCube → \FL\), and get into the following situation.
|
To get around this issue, we can embed \(j: □ → \dCube → \FL\), and get into the following situation.
|
||||||
|
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
\begin{tikzcd}[column sep=large]
|
\begin{tikzcd}[column sep=large]
|
||||||
|
|
@ -39,14 +39,14 @@ We can also define \(j\) explicitly like this:
|
||||||
\end{definition} \todo{\printline move this somewhere sane}
|
\end{definition} \todo{\printline move this somewhere sane}
|
||||||
|
|
||||||
\begin{definition}\label{def:j}
|
\begin{definition}\label{def:j}
|
||||||
Let \(j : □ → \FL\) the functor given by the following data:
|
Let \(j : □ → \FL\) be the functor given by the following data:
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item On objects: \(f(\{⊥|x_1…x_n|⊤\}) ≔ 𝟚^n\) \todo{\printline use \(⊥⊤\) notation in introduction chapter}
|
\item On objects: \(f(\{⊥|x_1…x_n|⊤\}) ≔ 𝟚^n\) \todo{\printline use \(⊥⊤\) notation in introduction chapter}
|
||||||
\item On morphisms: \(j(f)(g)(x) ≔ \begin{cases}g(f(x)) & f(x) \notin 𝟚 \\ f(x) & f(x) ∈ 𝟚\end{cases}\)
|
\item On morphisms: \(j(f)(g)(x) ≔ \begin{cases}g(f(x)) & f(x) \notin 𝟚 \\ f(x) & f(x) ∈ 𝟚\end{cases}\)
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
\end{definition}
|
\end{definition}
|
||||||
|
|
||||||
In \cite{riehlVid} it is claimed that \(i^*j_!\) is the triangulation functor and \(j^*i_!\) a
|
In \cite{riehlVid}, it is claimed that \(i^*j_!\) is the triangulation functor and \(j^*i_!\) a
|
||||||
left Quillen homotopy inverse. In the mean time Reid Barton observed in an yet unpublished paper,
|
left Quillen homotopy inverse. In the mean time Reid Barton observed in an yet unpublished paper,
|
||||||
\todo{\printline how to cite this? claimed in \cite{solution}}
|
\todo{\printline how to cite this? claimed in \cite{solution}}
|
||||||
that this triangulation can be described by a single functor on the level of sites \(Δ → □\). One
|
that this triangulation can be described by a single functor on the level of sites \(Δ → □\). One
|
||||||
|
|
@ -60,16 +60,16 @@ We are going to verify the original argument. To give an overview of the necessa
|
||||||
\end{enumerate}
|
\end{enumerate}
|
||||||
|
|
||||||
Before we jump into the formal proofs we like to get some intuition for the four functors of interest.
|
Before we jump into the formal proofs we like to get some intuition for the four functors of interest.
|
||||||
The category \FL has the luxury as containing
|
The category \FL has the luxury of containing
|
||||||
both \(Δ\) as the well orderings and \dCube as \(𝟚^n\). As \FL is the idempotent completion of \dCube,
|
both \(Δ\) as the well orderings and \dCube as \(𝟚^n\). As \FL is the idempotent completion of \dCube,
|
||||||
we also know that a presheaf on \FL is completely determined by its behavior on \dCube. The two functors
|
we also know that a presheaf on \FL is completely determined by its behavior on \dCube. The two functors
|
||||||
\(i^*\) and \(j^*\) are just the restrictions, and we can also understand \(i_!\) and \(j_!\) geometrically.
|
\(i^*\) and \(j^*\) are just the restrictions, and we can also understand \(i_!\) and \(j_!\) geometrically.
|
||||||
Let \(F ∈ \Δ\), then \(F(x) = i_!(F)(i(x))\). The interesting question is what does \(i_!\) define
|
Let \(F ∈ \Δ\), then \(F(x) = i_!(F)(i(x))\). The interesting question is: what does \(i_!\) define
|
||||||
on cubes (aka \(\Yo 𝟚^n\)) and \(j_!\) on simplicials (aka \(\Yo [n]\)). \(j_!\) will basically triangulate the cube (see \cref{prop:triangulation}),
|
on cubes (aka \(\Yo 𝟚^n\)) and \(j_!\) on simplicials (aka \(\Yo [n]\)). \(j_!\) will basically triangulate the cube (see \cref{prop:triangulation}),
|
||||||
while \(i_!\) will add just all possible cubes that are degenerated to simplicials.
|
while \(i_!\) will add just all possible cubes that are degenerated to simplicials.
|
||||||
|
|
||||||
To understand \(i^*\) a bit better we might take a look how things that are defined on \(𝟚^n\) extend to simplicials.
|
To understand \(i^*\) a bit better we might take a look how things that are defined on \(𝟚^n\) and extend this to simplicials.
|
||||||
For this we need to exhibit \([n]\) as a retract of \(𝟚^n\). For this we define two maps.
|
For this, we need to exhibit \([n]\) as a retract of \(𝟚^n\). To do this we define two maps.
|
||||||
\begin{definition}
|
\begin{definition}
|
||||||
Let
|
Let
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
|
|
@ -97,7 +97,7 @@ in \Set.
|
||||||
\(j_!(\I^n) = \Yo 𝟚^n\)
|
\(j_!(\I^n) = \Yo 𝟚^n\)
|
||||||
\end{proposition} \todo{\printline move to a sane place}
|
\end{proposition} \todo{\printline move to a sane place}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
We have that \(\Hom(j_!(\I^n),B) = \Hom(\I^n,j^*(B))\). And we get
|
We have that \(\Hom(j_!(\I^n),B) = \Hom(\I^n,j^*(B))\) and we get
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
\Hom(\Yo 𝟚^n, B) = B(𝟚^n) = B(j(n)) = \Hom(\I^n,j^*B)\text{.}
|
\Hom(\Yo 𝟚^n, B) = B(𝟚^n) = B(j(n)) = \Hom(\I^n,j^*B)\text{.}
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
|
|
@ -107,7 +107,7 @@ in \Set.
|
||||||
\subsection{\(i_!\) and \(i^*\) are left Quillen functors}
|
\subsection{\(i_!\) and \(i^*\) are left Quillen functors}
|
||||||
We need to show that \(i_!\) and \(i^*\) preserve cofibrations (or
|
We need to show that \(i_!\) and \(i^*\) preserve cofibrations (or
|
||||||
in other words monomorphisms) and trivial cofibrations. The hard
|
in other words monomorphisms) and trivial cofibrations. The hard
|
||||||
part will be to show that \(i_!\) preserves monomorphisms and we will do that last.
|
part will be to show that \(i_!\) preserves monomorphisms which we will do at the end.
|
||||||
|
|
||||||
\begin{lemma}\label{lem:restrictionPreserveMonos}
|
\begin{lemma}\label{lem:restrictionPreserveMonos}
|
||||||
Let \(F: \A → \B\) be a functor, then the restriction functor \(F^* : \hat{\B} → \hat{\A}\) preserves monomorphisms.
|
Let \(F: \A → \B\) be a functor, then the restriction functor \(F^* : \hat{\B} → \hat{\A}\) preserves monomorphisms.
|
||||||
|
|
@ -121,7 +121,7 @@ Let \(F: \A → \B\) be a functor, then the restriction functor \(F^* : \hat{\B}
|
||||||
\(i^*\) preserves monomorphisms.
|
\(i^*\) preserves monomorphisms.
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Directly by \cref{lem:restrictionPreserveMonos}.
|
Follows directly by \cref{lem:restrictionPreserveMonos}.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
\begin{proposition}\label{prop:i*preservesTrivialCofib}
|
\begin{proposition}\label{prop:i*preservesTrivialCofib}
|
||||||
|
|
@ -157,7 +157,7 @@ Note that a repetition of this argument is also good to check if we actually nee
|
||||||
or if we can do with just an Eilenberg-Zilber category.
|
or if we can do with just an Eilenberg-Zilber category.
|
||||||
|
|
||||||
\begin{lemma}[{\cite[lem 3.4]{sattlerIdempotentCompletionCubes2019}}]\label{lem:idemLemma3.4}
|
\begin{lemma}[{\cite[lem 3.4]{sattlerIdempotentCompletionCubes2019}}]\label{lem:idemLemma3.4}
|
||||||
Let \C be an Eilenberg-Zilber category. Assume \C as pullbacks along face maps.
|
Let \C be an Eilenberg-Zilber category. Assume \C has pullbacks along face maps.
|
||||||
The functor \(\colim : \hat{\C} → \Set\) preserves monomorphisms.
|
The functor \(\colim : \hat{\C} → \Set\) preserves monomorphisms.
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{remark}
|
\begin{remark}
|
||||||
|
|
@ -195,7 +195,7 @@ in \cite{pareAbsoluteColimits1971}.
|
||||||
or the symmetric situation where \(B\) and \(C\) are interchanged.
|
or the symmetric situation where \(B\) and \(C\) are interchanged.
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Let us assume first we have given all the data above (and WLOG \(B\) and \(C\) are not interchanged), and let
|
First let us assume we have given all the data above (and WLOG \(B\) and \(C\) are not interchanged), and let
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
A \arrow[r, "p" ] \arrow[d, "q" ] & B \arrow[d, "b"] \\
|
A \arrow[r, "p" ] \arrow[d, "q" ] & B \arrow[d, "b"] \\
|
||||||
C \arrow[r, "c"] & X
|
C \arrow[r, "c"] & X
|
||||||
|
|
@ -203,7 +203,7 @@ in \cite{pareAbsoluteColimits1971}.
|
||||||
be a commutative square. As all this data gets preserved by any functor we only need to prove that such a diagram
|
be a commutative square. As all this data gets preserved by any functor we only need to prove that such a diagram
|
||||||
is already a pushout. We now need to find a \(x : P → X\) that witnesses \(P\) as a pushout.
|
is already a pushout. We now need to find a \(x : P → X\) that witnesses \(P\) as a pushout.
|
||||||
Since \(m\) splits, \(x\) will be unique automatically. We define \(x ≔ bu\). We now need to check
|
Since \(m\) splits, \(x\) will be unique automatically. We define \(x ≔ bu\). We now need to check
|
||||||
if it makes the both evident triangles commute. We do this by chasing though all the data we have been given.
|
if it makes both evident triangles commute. We do this by chasing through all the data we have been given.
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
xm = bum = bqr_k = cqr_k = cqs_k = bps_k = bqr_{k-1} = … = bps_1 = b
|
xm = bum = bqr_k = cqr_k = cqs_k = bps_k = bqr_{k-1} = … = bps_1 = b
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
|
|
@ -220,7 +220,7 @@ in \cite{pareAbsoluteColimits1971}.
|
||||||
\end{eqcd*}
|
\end{eqcd*}
|
||||||
That means we have a surjection from \(\Hom(P,B) + \Hom(P,C) → \Hom(P,P)\).
|
That means we have a surjection from \(\Hom(P,B) + \Hom(P,C) → \Hom(P,P)\).
|
||||||
A preimage of \(\id_P\) under this surjection is a morphism \(u\) for that either \(mu = \id_P\)
|
A preimage of \(\id_P\) under this surjection is a morphism \(u\) for that either \(mu = \id_P\)
|
||||||
or \(nu = \id_P\) holds. We assume WLOG the first case.
|
or \(nu = \id_P\) holds. WLOG we assume the first case.
|
||||||
|
|
||||||
To get \(r_1,…,r_k\) and \(s_1,…,s_k\) that relate \(\id_B\) and \(um\), we look at the image under the
|
To get \(r_1,…,r_k\) and \(s_1,…,s_k\) that relate \(\id_B\) and \(um\), we look at the image under the
|
||||||
\(\Hom(B,−)\) functor.
|
\(\Hom(B,−)\) functor.
|
||||||
|
|
@ -247,7 +247,7 @@ in \cite{pareAbsoluteColimits1971}.
|
||||||
|
|
||||||
To be able to lift this structure, we make sure we can lift commuting triangles first.
|
To be able to lift this structure, we make sure we can lift commuting triangles first.
|
||||||
\begin{lemma}\label{lem:gfibliftcommute}
|
\begin{lemma}\label{lem:gfibliftcommute}
|
||||||
Let \(F : Q → \C\) be a discrete Grothendieck fibration, \(f: A → B\) be a morphism in \(Q\), and
|
Let \(F : Q → \C\) be a discrete Grothendieck fibration, \(f: A → B\) be a morphism in \(Q\),
|
||||||
\(g : C → F(B)\) and \(h : F(A) → C\) such that \(gh = F(f)\). We can lift \(g\) and \(h\) to form
|
\(g : C → F(B)\) and \(h : F(A) → C\) such that \(gh = F(f)\). We can lift \(g\) and \(h\) to form
|
||||||
a commutative diagram in \(Q\).
|
a commutative diagram in \(Q\).
|
||||||
\begin{eqcd*}[column sep=small]
|
\begin{eqcd*}[column sep=small]
|
||||||
|
|
@ -275,7 +275,7 @@ To be able to lift this structure, we make sure we can lift commuting triangles
|
||||||
|
|
||||||
Given some monomorphism \(f : A ↣B\) in \(Q\) and two morphisms \(g,h : C → \p(A)\) in \C, such that \(\p(f)h = \p(f)g \),
|
Given some monomorphism \(f : A ↣B\) in \(Q\) and two morphisms \(g,h : C → \p(A)\) in \C, such that \(\p(f)h = \p(f)g \),
|
||||||
we can lift \(g\) and \(h\) to \(g' : C' → A\) and \(h' : C' → A\). By \cref{lem:gfibliftcommute}, we have \(fg' = fh'\) and
|
we can lift \(g\) and \(h\) to \(g' : C' → A\) and \(h' : C' → A\). By \cref{lem:gfibliftcommute}, we have \(fg' = fh'\) and
|
||||||
thus \(g' = h'\). We get directly \( g = \p(g') = \p(h') = h\) and thus \(\p(f)\) is monic.
|
thus \(g' = h'\). We directly get \( g = \p(g') = \p(h') = h\) and thus \(\p(f)\) is monic.
|
||||||
|
|
||||||
Assume we have a map \(f\) in \(Q\) such that \(\p(f)\) has a (one sided) inverse. By \cref{lem:gfibliftcommute}, the lift
|
Assume we have a map \(f\) in \(Q\) such that \(\p(f)\) has a (one sided) inverse. By \cref{lem:gfibliftcommute}, the lift
|
||||||
of that (one sided) inverse is also a (one sided) inverse of \(f\).
|
of that (one sided) inverse is also a (one sided) inverse of \(f\).
|
||||||
|
|
@ -345,13 +345,13 @@ To be able to lift this structure, we make sure we can lift commuting triangles
|
||||||
& \C &
|
& \C &
|
||||||
\end{tikzcd}
|
\end{tikzcd}
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
That \(\colim\) sends \(f\) to a monomorphism,
|
The fact that \(\colim\) sends \(f\) to a monomorphism,
|
||||||
is equivalent to the statement that \(F\) is monic on connected components. That follows directly from the explicit construction
|
is equivalent to the statement that \(F\) is monic on connected components. That follows directly from the explicit construction
|
||||||
of colimits in \(\Set\). Also \(F\) gets to be a discrete Grothendieck fibration on its own. We can lift the Eilenberg-Zilber
|
of colimits in \(\Set\). Also \(F\) gets to be a discrete Grothendieck fibration on its own. We can lift the Eilenberg-Zilber
|
||||||
structure to \(Q\) by \cref{lem:liftEZFib}.
|
structure to \(Q\) by \cref{lem:liftEZFib}.
|
||||||
|
|
||||||
So now let \(S\) and \(T\) be be objects of \(P\) such that \(F(S)\) and \(F(T)\) lie in the same connected component of \(Q\).
|
So now let \(S\) and \(T\) be be objects of \(P\) such that \(F(S)\) and \(F(T)\) lie in the same connected component of \(Q\).
|
||||||
This means there is a zigzag connecting \(F(S)\) and \(F(T)\). We can normalize this to a span. To see this, we are going
|
This means that there is a zigzag connecting \(F(S)\) and \(F(T)\). We can normalize this to a span. To see this, we are going
|
||||||
to show how to turn a cospan into a span of morphisms. So let \( f : D → B\) and \( g : E → B \) be a cospan. Because of the Eilenberg-Zilber
|
to show how to turn a cospan into a span of morphisms. So let \( f : D → B\) and \( g : E → B \) be a cospan. Because of the Eilenberg-Zilber
|
||||||
structure, we can factor those into a degeneracy followed by a face map. Lets call them \(f_d\), \(f_f\), \(g_d\) and \(g_f\).
|
structure, we can factor those into a degeneracy followed by a face map. Lets call them \(f_d\), \(f_f\), \(g_d\) and \(g_f\).
|
||||||
\begin{eqcd*}[column sep=small]
|
\begin{eqcd*}[column sep=small]
|
||||||
|
|
@ -373,8 +373,8 @@ structures. Sadly this does not work well for Eilenberg-Zilber categories. So we
|
||||||
category.
|
category.
|
||||||
\end{lemma}
|
\end{lemma}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
First we need to define a degree function \(\d: \Obj (\B) → ℕ\), let \(\d'\) be the degree function from the elegant Reedy structure
|
First we need to define a degree function \(\d: \Obj (\B) → ℕ\). Let \(\d'\) be the degree function from the elegant Reedy structure.
|
||||||
we can then define \(\d ≔ \d'p\). We define the degeneracies and faces, as being degeneracies and faces under \(p\).
|
We can then define \(\d ≔ \d'p\). We define the degeneracies and faces, as being degeneracies and faces under \(p\).
|
||||||
Here we would already get a problem with EZ-categories as we might have maps that are monic in \(B ↓ i\), but not in \B.
|
Here we would already get a problem with EZ-categories as we might have maps that are monic in \(B ↓ i\), but not in \B.
|
||||||
|
|
||||||
As a next step we need to construct the desired factorization into a degeneracy and a face map. So we take
|
As a next step we need to construct the desired factorization into a degeneracy and a face map. So we take
|
||||||
|
|
@ -401,7 +401,7 @@ structures. Sadly this does not work well for Eilenberg-Zilber categories. So we
|
||||||
Usually this situation is given, if \A has pullbacks along a class of maps and \(i\) preserves them.
|
Usually this situation is given, if \A has pullbacks along a class of maps and \(i\) preserves them.
|
||||||
\end{remark}
|
\end{remark}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
So consider a span of maps in \(B ↓ i\). That fulfills the conditions of this lemma.
|
So consider a span of maps in \(B ↓ i\), that fulfills the conditions of this lemma.
|
||||||
If we unravel this, we get the following diagram:
|
If we unravel this, we get the following diagram:
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
{} & B \arrow[rdd, "ϕ'", bend left] \arrow[ldd, "ϕ"', bend right] & \\
|
{} & B \arrow[rdd, "ϕ'", bend left] \arrow[ldd, "ϕ"', bend right] & \\
|
||||||
|
|
@ -430,7 +430,7 @@ structures. Sadly this does not work well for Eilenberg-Zilber categories. So we
|
||||||
that degeneracies are split in \cref{lem:liftEZFib}.
|
that degeneracies are split in \cref{lem:liftEZFib}.
|
||||||
\end{remark}
|
\end{remark}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
We only need to show that \(i_!\) preserves monomorphisms component wise, giving us a functor from \(\hat{\A} → \Set\) for every
|
We only need to show that \(i_!\) preserves monomorphisms componentwise, giving us a functor from \(\hat{\A} → \Set\) for every
|
||||||
object in \( B ∈\B\). This functor can be written as
|
object in \( B ∈\B\). This functor can be written as
|
||||||
\begin{eqcd*}
|
\begin{eqcd*}
|
||||||
\hat{\A} \arrow[r,"p^*"] & \widehat{B ↓ i} \arrow[r,"\colim"] & \Set
|
\hat{\A} \arrow[r,"p^*"] & \widehat{B ↓ i} \arrow[r,"\colim"] & \Set
|
||||||
|
|
@ -490,7 +490,7 @@ So let us start with \(j^*\) again.
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
Preservation of uniform fibrations is clear, as every lifting problem against a generating trivial cofibration factors
|
Preservation of uniform fibrations is clear, as every lifting problem against a generating trivial cofibration factors
|
||||||
throug the image of a trivial cofibration under \(j^*\). As \(j^*\) preserves coequalizer the equivariance follows
|
throug the image of a trivial cofibration under \(j^*\). As \(j^*\) preserves coequalizer the equivariance follows
|
||||||
from the equivariance of the model category on \dcSet, which follows from the presence of (at least one connection).
|
from the equivariance of the model category on \dcSet, which follows from the presence of (at least one) connection.
|
||||||
\end{proof}\todo{define uniform fibrations without equivariance}\todo{make a lemma that \dcSet is equivariant even if we just cite this from the relative elegance paper}
|
\end{proof}\todo{define uniform fibrations without equivariance}\todo{make a lemma that \dcSet is equivariant even if we just cite this from the relative elegance paper}
|
||||||
|
|
||||||
We want to recap the general proof idea that \(i_!\) preserved monos. We can test being a monomorphism component wise and can write the
|
We want to recap the general proof idea that \(i_!\) preserved monos. We can test being a monomorphism component wise and can write the
|
||||||
|
|
@ -499,8 +499,8 @@ That the colimit preserves monomorphisms is equivalent to a condition of connec
|
||||||
of elements. We can only lift morphisms backwards along discrete Grothendieck fibrations, but we are faced
|
of elements. We can only lift morphisms backwards along discrete Grothendieck fibrations, but we are faced
|
||||||
with zigzags. To remedy this we want to lift a strong enough pullback property to turn these zigzags into spans.
|
with zigzags. To remedy this we want to lift a strong enough pullback property to turn these zigzags into spans.
|
||||||
|
|
||||||
This strategy will be the same for \(j_!\). Sadly we couldn't get arbitrary Eilenberg-Zilber structures to lift, so
|
The strategy will be the same for \(j_!\). Sadly we couldn't get arbitrary Eilenberg-Zilber structures to lift, so
|
||||||
we will need a slightly different attack point.
|
we will need a slightly different point of attack.
|
||||||
|
|
||||||
We first observe that \(□\) has a lot more pullbacks then \(Δ\). While \(Δ\) has only “non-empty” pullbacks of face maps,
|
We first observe that \(□\) has a lot more pullbacks then \(Δ\). While \(Δ\) has only “non-empty” pullbacks of face maps,
|
||||||
\(□\) has all “non-empty" pullbacks. This elevates us from the necessity to lift the Eilenberg-Zilber structure to \(B ↓ i\).
|
\(□\) has all “non-empty" pullbacks. This elevates us from the necessity to lift the Eilenberg-Zilber structure to \(B ↓ i\).
|
||||||
|
|
@ -533,11 +533,7 @@ Let \C be a category. Assume \C has pullbacks, then the functor \(\colim : \hat{
|
||||||
consequence of \cref{commaPullback}.
|
consequence of \cref{commaPullback}.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
And we arrive at the conclusion we wanted to get to:
|
Finally we arrive at the conclusion we wanted to get to:
|
||||||
\begin{lemma}
|
|
||||||
Let \(F: \A → \B\) be a functor, then the restriction functor \(F^* : \hat{\B} → \hat{\A}\) preserves monomorphisms.
|
|
||||||
\end{lemma}
|
|
||||||
|
|
||||||
\begin{proposition}\label{prop:j!preservesMonos}
|
\begin{proposition}\label{prop:j!preservesMonos}
|
||||||
\(j_! : \widehat{\FL} → \□\) preserves monomorphisms.
|
\(j_! : \widehat{\FL} → \□\) preserves monomorphisms.
|
||||||
\end{proposition}
|
\end{proposition}
|
||||||
|
|
@ -553,7 +549,7 @@ And we arrive at the conclusion we wanted to get to:
|
||||||
where we identify \(f\) and \(g\) with functions \(m → n + 2\).
|
where we identify \(f\) and \(g\) with functions \(m → n + 2\).
|
||||||
We note that equalizers, if they exist in \FL, are constructed the same way as in \Set.
|
We note that equalizers, if they exist in \FL, are constructed the same way as in \Set.
|
||||||
If we apply this to our diagram, we can see that this construction can't create something empty,
|
If we apply this to our diagram, we can see that this construction can't create something empty,
|
||||||
as both maps needs to preserve elements from \(B\).
|
as both maps need to preserve elements from \(B\).
|
||||||
We would like to complete the diagram in the following way
|
We would like to complete the diagram in the following way
|
||||||
%\begin{eqcd*}[column sep=large]
|
%\begin{eqcd*}[column sep=large]
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
|
|
@ -568,7 +564,7 @@ And we arrive at the conclusion we wanted to get to:
|
||||||
\(f\) and \(g\). We will now argue that our equalizer would be empty if this quotient identifies
|
\(f\) and \(g\). We will now argue that our equalizer would be empty if this quotient identifies
|
||||||
\(⊤\) and \(⊥\).
|
\(⊤\) and \(⊥\).
|
||||||
|
|
||||||
We assume that indeed the relation identifies \(⊥\) and \(⊤\), let \(h ∈ 𝟚^n\) such that \(j(f)(h) = j(g)(h)\).
|
We assume that indeed the relation identifies \(⊥\) and \(⊤\). Let \(h ∈ 𝟚^n\) such that \(j(f)(h) = j(g)(h)\).
|
||||||
Because \(⊥\) and \(⊤\) are being identified, there exists two finite sequence of elements \(x_i\) and \(y_i\) in \(m\), such that
|
Because \(⊥\) and \(⊤\) are being identified, there exists two finite sequence of elements \(x_i\) and \(y_i\) in \(m\), such that
|
||||||
there exists a \(k\) and
|
there exists a \(k\) and
|
||||||
(WLOG) \(f(x_1) = ⊥\), \(g(x_i) = f(y_i)\), \(g(y_i) = f(x_{i+1})\) and \(g(y_k) = ⊤\).
|
(WLOG) \(f(x_1) = ⊥\), \(g(x_i) = f(y_i)\), \(g(y_i) = f(x_{i+1})\) and \(g(y_k) = ⊤\).
|
||||||
|
|
@ -587,8 +583,8 @@ And we arrive at the conclusion we wanted to get to:
|
||||||
h': l → 𝟚 && \text{by} && h'(x) ≔ h(z) & & \text{where} && z ∈ e^{-1}(x)\text{.}
|
h': l → 𝟚 && \text{by} && h'(x) ≔ h(z) & & \text{where} && z ∈ e^{-1}(x)\text{.}
|
||||||
\end{align*}
|
\end{align*}
|
||||||
For this definition to make sense we need to argue that the choice of \(z\) does not matter.
|
For this definition to make sense we need to argue that the choice of \(z\) does not matter.
|
||||||
So let \(z\) and \(z'\) be both element of \(e^{-1}(x)\). Like above that means there are
|
So let \(z\) and \(z'\) be both element of \(e^{-1}(x)\). Like above, that means there are
|
||||||
two sequences \(x_i\) and \(y_i\) like above, just that \(f(x_1) = z\) and \(g(y_k) = z'\), instead
|
two sequences \(x_i\) and \(y_i\), just that \(f(x_1) = z\) and \(g(y_k) = z'\), instead
|
||||||
of \(⊥\) and \(⊤\).
|
of \(⊥\) and \(⊤\).
|
||||||
And like above we get
|
And like above we get
|
||||||
\begin{align*}
|
\begin{align*}
|
||||||
|
|
@ -622,7 +618,7 @@ and that is indeed the case.
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
As \T is the unique cocontinuous functor that extends the product preserving functor from \□ to \Δ that sends the interval
|
As \T is the unique cocontinuous functor that extends the product preserving functor from \□ to \Δ that sends the interval
|
||||||
to the interval, we only need to show these conditions. \(i^*j_!\) is cocontinuous as it is the composition of two left
|
to the interval, we only need to show these conditions. \(i^*j_!\) is cocontinuous as it is the composition of two left
|
||||||
adjoints. We need to show that this functor is product preserving on representables. But by Yoneda and \cref{prop:j_!Nothing}
|
adjoints. We need to show that this functor is product preserving on representables. But by Yoneda and \cref{prop:j_!Nothing} we have
|
||||||
\begin{equation*}
|
\begin{equation*}
|
||||||
j_!(\I^n × \I^m) = j_!(\I^{n+m}) = \Yo 𝟚^{n+m} = \Yo 𝟚^n × \Yo 𝟚^m = j_!(\I^n) × j_!(\I^m)
|
j_!(\I^n × \I^m) = j_!(\I^{n+m}) = \Yo 𝟚^{n+m} = \Yo 𝟚^n × \Yo 𝟚^m = j_!(\I^n) × j_!(\I^m)
|
||||||
\end{equation*}
|
\end{equation*}
|
||||||
|
|
@ -640,9 +636,9 @@ and that is indeed the case.
|
||||||
Intuitively the reason for this is that we can't map a square with one side degenerated to a triangle into the representable
|
Intuitively the reason for this is that we can't map a square with one side degenerated to a triangle into the representable
|
||||||
square in \□. But we have a lot of ways to map a triangle into a triangulated square in \Δ.
|
square in \□. But we have a lot of ways to map a triangle into a triangulated square in \Δ.
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
By the Yoneda lemma and that \(j^*i_!\) is the triangulation functor, a map on the right-hand side corresponds to a
|
By the Yoneda lemma, and that \(j^*i_!\) is the triangulation functor, a map on the right-hand side corresponds to a
|
||||||
pair of monotone maps \([2] → [1]\). There are 16 of such pairs. On the left we can use \cref{prop:j_!Nothing},
|
pair of monotone maps \([2] → [1]\). There are 16 of such pairs. On the left we can use \cref{prop:j_!Nothing},
|
||||||
and expanding the definition to get \(\Hom_{\□}(\Hom_{\FL}(j(-),[2]),\Hom_{□}(-,2))\). Lets take such a transformation
|
and expanding the definition we get \(\Hom_{\□}(\Hom_{\FL}(j(-),[2]),\Hom_{□}(-,2))\). Lets take such a transformation
|
||||||
and call it \(η\). \(η_0\) gives rise to a map \(f : [2] → 𝟚^2\). \(η_1\) witnesses that \(f\) is indeed monotone, by
|
and call it \(η\). \(η_0\) gives rise to a map \(f : [2] → 𝟚^2\). \(η_1\) witnesses that \(f\) is indeed monotone, by
|
||||||
composing with face maps. And \(η_2\) rules out all injective maps, as for them always exactly 2 faces agree and
|
composing with face maps. And \(η_2\) rules out all injective maps, as for them always exactly 2 faces agree and
|
||||||
\(\I^2(2)\) does not contain such faces. There are only 9 such maps, which is an upper bound for the possible number of
|
\(\I^2(2)\) does not contain such faces. There are only 9 such maps, which is an upper bound for the possible number of
|
||||||
|
|
@ -661,7 +657,7 @@ first we don't run into that problem.
|
||||||
As \(j^*i_!\) is the triangulation functor, the left-hand side becomes \(\Hom_{\Δ}(Δ^1 × Δ^1,Δ^1 × Δ^1)\).
|
As \(j^*i_!\) is the triangulation functor, the left-hand side becomes \(\Hom_{\Δ}(Δ^1 × Δ^1,Δ^1 × Δ^1)\).
|
||||||
We can write \( Δ^1 × Δ^1 \) as a pushout of two copies of \(Δ^1\) joint by an edge.
|
We can write \( Δ^1 × Δ^1 \) as a pushout of two copies of \(Δ^1\) joint by an edge.
|
||||||
As \(i_!\) is cocontinuous, we can construct this pushout in \FL. By this and \cref{prop:i_!Nothing}, we
|
As \(i_!\) is cocontinuous, we can construct this pushout in \FL. By this and \cref{prop:i_!Nothing}, we
|
||||||
get a colimit of two representables there. Unraveling these definition it is a straightforward exercise
|
get a colimit of two representables there. Unraveling these definitions it is a straightforward exercise
|
||||||
to verify that the set of on the left-hand side has more elements.
|
to verify that the set of on the left-hand side has more elements.
|
||||||
\end{proof}
|
\end{proof}
|
||||||
|
|
||||||
|
|
@ -703,7 +699,7 @@ contractible.
|
||||||
are weak equivalences, then all components of \(α\) are weak equivalences.
|
are weak equivalences, then all components of \(α\) are weak equivalences.
|
||||||
\end{corollary}
|
\end{corollary}
|
||||||
\begin{proof}
|
\begin{proof}
|
||||||
By \cref{test}\todo{In Leibniz construction chapter make this an example} we can write the the part of \(α\) at \(X\) as a
|
By \cref{leibnizNatural} we can write the the part of \(α\) at \(X\) as a
|
||||||
Leibniz application with the monomorphism \(∅ → X\). We can use both lemmas from above to show that \(α\) gets send by all
|
Leibniz application with the monomorphism \(∅ → X\). We can use both lemmas from above to show that \(α\) gets send by all
|
||||||
of those maps to a weak equivalence. By \cref{lem:Eilenberg-ZilberMonosCreated} the monomorphisms in \(\Set^{\A^\op}\) are generated by
|
of those maps to a weak equivalence. By \cref{lem:Eilenberg-ZilberMonosCreated} the monomorphisms in \(\Set^{\A^\op}\) are generated by
|
||||||
morphisms \(∅ → \faktor{\Yo a}{H}\) under some closure properties. By assumption, morphisms of that form are sent to weak equivalences
|
morphisms \(∅ → \faktor{\Yo a}{H}\) under some closure properties. By assumption, morphisms of that form are sent to weak equivalences
|
||||||
|
|
@ -745,8 +741,8 @@ contractible.
|
||||||
|
|
||||||
To show that these induce an equivalence between the homotopy categories we must show that we have a zigzag of
|
To show that these induce an equivalence between the homotopy categories we must show that we have a zigzag of
|
||||||
natural transformations between \(i^*j_!j^*i_!\) and the identity functor such that every natural transformation
|
natural transformations between \(i^*j_!j^*i_!\) and the identity functor such that every natural transformation
|
||||||
is valued in weak equivalences, and likewise for \(j^*i_!i^*j_!\). We will call \(η^i\) and \(ε^i\) the unit and counit
|
is valued in weak equivalences, and likewise for \(j^*i_!i^*j_!\). We will denote \(η^i\) and \(ε^i\) the unit and counit
|
||||||
of the adjunction \(i_! ⊣ i^*\). Likewise \(η^j\) and \(ε^j\) for the adjunction \(j_! ⊣ j^*\).
|
of the adjunction \(i_! ⊣ i^*\). Likewise we denote \(η^j\) and \(ε^j\) for the adjunction \(j_! ⊣ j^*\).
|
||||||
We can construct these as follows
|
We can construct these as follows
|
||||||
\begin{eqcd*}[column sep=large, row sep=large,execute at end picture={\draw[decorate,decoration={brace,mirror,amplitude=4.5}] (sBrcs.south) to (eBrcs.south);}]
|
\begin{eqcd*}[column sep=large, row sep=large,execute at end picture={\draw[decorate,decoration={brace,mirror,amplitude=4.5}] (sBrcs.south) to (eBrcs.south);}]
|
||||||
\Δ \arrow[r,"i_!", ""'{name=i!s}] & |[alias=sBrcs]| \dcSet \arrow[r,"j^*"] \arrow[d,phantom,"⊛"] \arrow[rr,bend right=20,phantom , ""'{name=cc}] & \□ \arrow[r,"j_!"] & |[alias=eBrcs]| \dcSet \arrow[r,"i^*", ""'{name=i*s}] \arrow[d,phantom,"⊛"] & \Δ \\
|
\Δ \arrow[r,"i_!", ""'{name=i!s}] & |[alias=sBrcs]| \dcSet \arrow[r,"j^*"] \arrow[d,phantom,"⊛"] \arrow[rr,bend right=20,phantom , ""'{name=cc}] & \□ \arrow[r,"j_!"] & |[alias=eBrcs]| \dcSet \arrow[r,"i^*", ""'{name=i*s}] \arrow[d,phantom,"⊛"] & \Δ \\
|
||||||
|
|
|
||||||
123
src/resource.bib
123
src/resource.bib
|
|
@ -1097,3 +1097,126 @@
|
||||||
keywords = {18N45 18N40 03B38 55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic},
|
keywords = {18N45 18N40 03B38 55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory,Mathematics - Logic},
|
||||||
file = {/home/nerf/Zotero/storage/ISNC6YKS/Hazratpour and Riehl - 2024 - A 2-categorical proof of Frobenius for fibrations .pdf;/home/nerf/Zotero/storage/BIR588ML/2210.html}
|
file = {/home/nerf/Zotero/storage/ISNC6YKS/Hazratpour and Riehl - 2024 - A 2-categorical proof of Frobenius for fibrations .pdf;/home/nerf/Zotero/storage/BIR588ML/2210.html}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@online{campionCubicalSitesEilenbergZilber2023,
|
||||||
|
title = {Cubical Sites as {{Eilenberg-Zilber}} Categories},
|
||||||
|
author = {Campion, Timothy},
|
||||||
|
date = {2023-03-10},
|
||||||
|
eprint = {2303.06206},
|
||||||
|
eprinttype = {arXiv},
|
||||||
|
eprintclass = {math},
|
||||||
|
doi = {10.48550/arXiv.2303.06206},
|
||||||
|
url = {http://arxiv.org/abs/2303.06206},
|
||||||
|
urldate = {2024-08-09},
|
||||||
|
abstract = {We show that various cube categories (without diagonals, but with symmetries / connections / reversals) are Eilenberg-Zilber categories. This generalizes a result of Isaacson for one particular cubical site. Our method does not involve direct verification of any absolute pushout diagrams. While we are at it, we record some folklore descriptions of cube categories with diagonals and determine exactly which of these are EZ categories. Beforehand, we develop some general theory of Eilenberg-Zilber categories. We show that a mild generalization of the EZ categories of Berger and Moerdijk are in fact characterized (among a broad class of ``generalized Reedy categories") by the satisfaction of the Eilenberg-Zilber lemma, generalizing a theorem of Bergner and Rezk in the strict Reedy case. We also introduce a mild strengthening of Cisinski's notion of a \textbackslash emph\{cat\textbackslash 'egorie squelettique\}, and show that any such category satisfies the Eilenberg-Zilber lemma. It is this tool which allows us to avoid checking absolute pushouts by hand.},
|
||||||
|
pubstate = {prepublished},
|
||||||
|
keywords = {55U35,Mathematics - Algebraic Topology,Mathematics - Category Theory},
|
||||||
|
file = {/home/nerf/Zotero/storage/DUJL6DRG/Campion - 2023 - Cubical sites as Eilenberg-Zilber categories.pdf;/home/nerf/Zotero/storage/2QSTN5BN/2303.html}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{kapulkinSimplicialModelUnivalent2021,
|
||||||
|
title = {The Simplicial Model of {{Univalent Foundations}} (after {{Voevodsky}})},
|
||||||
|
author = {Kapulkin, Krzysztof and Lumsdaine, Peter LeFanu},
|
||||||
|
date = {2021-03-08},
|
||||||
|
journaltitle = {Journal of the European Mathematical Society},
|
||||||
|
volume = {23},
|
||||||
|
number = {6},
|
||||||
|
pages = {2071--2126},
|
||||||
|
issn = {1435-9855},
|
||||||
|
doi = {10.4171/jems/1050},
|
||||||
|
url = {https://ems.press/journals/jems/articles/274693},
|
||||||
|
urldate = {2024-08-09},
|
||||||
|
abstract = {Krzysztof Kapulkin, Peter LeFanu Lumsdaine},
|
||||||
|
langid = {english},
|
||||||
|
file = {/home/nerf/Zotero/storage/NNLS3E7X/Kapulkin and Lumsdaine - 2021 - The simplicial model of Univalent Foundations (aft.pdf}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{bezemNonConstructivityKanSimplicial2015,
|
||||||
|
title = {Non-{{Constructivity}} in {{Kan Simplicial Sets}}},
|
||||||
|
booktitle = {{{DROPS-IDN}}/v2/Document/10.4230/{{LIPIcs}}.{{TLCA}}.2015.92},
|
||||||
|
author = {Bezem, Marc and Coquand, Thierry and Parmann, Erik},
|
||||||
|
date = {2015},
|
||||||
|
publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
|
||||||
|
doi = {10.4230/LIPIcs.TLCA.2015.92},
|
||||||
|
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.92},
|
||||||
|
urldate = {2024-08-09},
|
||||||
|
abstract = {We give an analysis of the non-constructivity of the following basic result: if X and Y are simplicial sets and Y has the Kan extension property, then Y\textasciicircum X also has the Kan extension property. By means of Kripke countermodels we show that even simple consequences of this basic result, such as edge reversal and edge composition, are not constructively provable. We also show that our unprovability argument will have to be refined if one strengthens the usual formulation of the Kan extension property to one with explicit horn-filler operations.},
|
||||||
|
eventtitle = {13th {{International Conference}} on {{Typed Lambda Calculi}} and {{Applications}} ({{TLCA}} 2015)},
|
||||||
|
langid = {english},
|
||||||
|
file = {/home/nerf/Zotero/storage/36F474PT/Bezem et al. - 2015 - Non-Constructivity in Kan Simplicial Sets.pdf}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{bezemModelTypeTheory2014a,
|
||||||
|
title = {A {{Model}} of {{Type Theory}} in {{Cubical Sets}}},
|
||||||
|
booktitle = {{{DROPS-IDN}}/v2/Document/10.4230/{{LIPIcs}}.{{TYPES}}.2013.107},
|
||||||
|
author = {Bezem, Marc and Coquand, Thierry and Huber, Simon},
|
||||||
|
date = {2014},
|
||||||
|
publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
|
||||||
|
doi = {10.4230/LIPIcs.TYPES.2013.107},
|
||||||
|
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2013.107},
|
||||||
|
urldate = {2024-08-09},
|
||||||
|
abstract = {We present a model of type theory with dependent product, sum, and identity, in cubical sets. We describe a universe and explain how to transform an equivalence between two types into an equality. We also explain how to model propositional truncation and the circle. While not expressed internally in type theory, the model is expressed in a constructive metalogic. Thus it is a step towards a computational interpretation of Voevodsky's Univalence Axiom.},
|
||||||
|
eventtitle = {19th {{International Conference}} on {{Types}} for {{Proofs}} and {{Programs}} ({{TYPES}} 2013)},
|
||||||
|
langid = {english},
|
||||||
|
file = {/home/nerf/Zotero/storage/4QVQJ2J4/Bezem et al. - 2014 - A Model of Type Theory in Cubical Sets.pdf}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{angiuliCartesianCubicalComputational2018a,
|
||||||
|
title = {Cartesian {{Cubical Computational Type Theory}}: {{Constructive Reasoning}} with {{Paths}} and {{Equalities}}},
|
||||||
|
shorttitle = {Cartesian {{Cubical Computational Type Theory}}},
|
||||||
|
booktitle = {{{DROPS-IDN}}/v2/Document/10.4230/{{LIPIcs}}.{{CSL}}.2018.6},
|
||||||
|
author = {Angiuli, Carlo and Hou (Favonia), Kuen-Bang and Harper, Robert},
|
||||||
|
date = {2018},
|
||||||
|
publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
|
||||||
|
doi = {10.4230/LIPIcs.CSL.2018.6},
|
||||||
|
url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.6},
|
||||||
|
urldate = {2024-08-09},
|
||||||
|
abstract = {We present a dependent type theory organized around a Cartesian notion of cubes (with faces, degeneracies, and diagonals), supporting both fibrant and non-fibrant types. The fibrant fragment validates Voevodsky's univalence axiom and includes a circle type, while the non-fibrant fragment includes exact (strict) equality types satisfying equality reflection. Our type theory is defined by a semantics in cubical partial equivalence relations, and is the first two-level type theory to satisfy the canonicity property: all closed terms of boolean type evaluate to either true or false.},
|
||||||
|
eventtitle = {27th {{EACSL Annual Conference}} on {{Computer Science Logic}} ({{CSL}} 2018)},
|
||||||
|
langid = {english},
|
||||||
|
file = {/home/nerf/Zotero/storage/ITQAFSAQ/Angiuli et al. - 2018 - Cartesian Cubical Computational Type Theory Const.pdf}
|
||||||
|
}
|
||||||
|
|
||||||
|
@inproceedings{coquandHigherInductiveTypes2018,
|
||||||
|
title = {On {{Higher Inductive Types}} in {{Cubical Type Theory}}},
|
||||||
|
booktitle = {Proceedings of the 33rd {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}}},
|
||||||
|
author = {Coquand, Thierry and Huber, Simon and Mörtberg, Anders},
|
||||||
|
date = {2018-07-09},
|
||||||
|
series = {{{LICS}} '18},
|
||||||
|
pages = {255--264},
|
||||||
|
publisher = {Association for Computing Machinery},
|
||||||
|
location = {New York, NY, USA},
|
||||||
|
doi = {10.1145/3209108.3209197},
|
||||||
|
url = {https://dl.acm.org/doi/10.1145/3209108.3209197},
|
||||||
|
urldate = {2024-08-09},
|
||||||
|
abstract = {Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions, truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers.},
|
||||||
|
isbn = {978-1-4503-5583-4},
|
||||||
|
file = {/home/nerf/Zotero/storage/ZTLQNGHG/Coquand et al. - 2018 - On Higher Inductive Types in Cubical Type Theory.pdf}
|
||||||
|
}
|
||||||
|
|
||||||
|
@article{awodeyCubicalModelHomotopy2018,
|
||||||
|
title = {A Cubical Model of Homotopy Type Theory},
|
||||||
|
author = {Awodey, Steve},
|
||||||
|
date = {2018-12-01},
|
||||||
|
journaltitle = {Annals of Pure and Applied Logic},
|
||||||
|
shortjournal = {Annals of Pure and Applied Logic},
|
||||||
|
series = {Logic {{Colloquium}} 2015},
|
||||||
|
volume = {169},
|
||||||
|
number = {12},
|
||||||
|
pages = {1270--1294},
|
||||||
|
issn = {0168-0072},
|
||||||
|
doi = {10.1016/j.apal.2018.08.002},
|
||||||
|
url = {https://www.sciencedirect.com/science/article/pii/S0168007218300861},
|
||||||
|
urldate = {2024-08-09},
|
||||||
|
abstract = {We construct an algebraic weak factorization system (L,R) on the category of cartesian cubical sets, in which the canonical path object factorization A→AI→A×A, induced by the 1-cube I, is an (L,R)-factorization for any R-object A.},
|
||||||
|
keywords = {Algebraic weak factorization system,Homotopy type theory,Identity type,Martin-Löf type theory,Path object},
|
||||||
|
file = {/home/nerf/Zotero/storage/BSTEHCTN/Awodey - 2018 - A cubical model of homotopy type theory.pdf;/home/nerf/Zotero/storage/IF3X3VCQ/S0168007218300861.html}
|
||||||
|
}
|
||||||
|
|
||||||
|
@online{QuillenModelStructure,
|
||||||
|
title = {Quillen Model Structure},
|
||||||
|
url = {https://groups.google.com/g/homotopytypetheory/c/RQkLWZ_83kQ},
|
||||||
|
urldate = {2024-08-09},
|
||||||
|
shorthand = {Mail},
|
||||||
|
file = {/home/nerf/Zotero/storage/69U872ED/RQkLWZ_83kQ.html}
|
||||||
|
}
|
||||||
|
|
|
||||||
|
|
@ -1 +1 @@
|
||||||
/nix/store/vi5k8nsgp9knk76bri7p6nr1la5fa4mn-output.pdf
|
/nix/store/7g9d5mh042bhznbcfh25ki95c39pnz83-output.pdf
|
||||||
Loading…
Reference in a new issue