added notes
This commit is contained in:
Egbert Rijke
parent
35db866a61
commit
5da0c57835
3 changed files with 1929 additions and 0 deletions
781
Notes/macros.tex
Normal file
781
Notes/macros.tex
Normal file
|
|
@ -0,0 +1,781 @@
|
||||||
|
%%%% MACROS FOR NOTATION %%%%
|
||||||
|
% Use these for any notation where there are multiple options.
|
||||||
|
|
||||||
|
%%% Notes and exercise sections
|
||||||
|
\makeatletter
|
||||||
|
\newcommand{\sectionNotes}{\phantomsection\section*{Notes}\addcontentsline{toc}{section}{Notes}\markright{\textsc{\@chapapp{} \thechapter{} Notes}}}
|
||||||
|
\newcommand{\sectionExercises}[1]{\phantomsection\section*{Exercises}\addcontentsline{toc}{section}{Exercises}\markright{\textsc{\@chapapp{} \thechapter{} Exercises}}}
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
%%% Definitional equality (used infix) %%%
|
||||||
|
\newcommand{\jdeq}{\equiv} % An equality judgment
|
||||||
|
\let\judgeq\jdeq
|
||||||
|
%\newcommand{\defeq}{\coloneqq} % An equality currently being defined
|
||||||
|
\newcommand{\defeq}{\vcentcolon\equiv} % A judgmental equality currently being defined
|
||||||
|
|
||||||
|
%%% Term being defined
|
||||||
|
\newcommand{\define}[1]{\textbf{#1}}
|
||||||
|
|
||||||
|
%%% Vec (for example)
|
||||||
|
|
||||||
|
\newcommand{\Vect}{\ensuremath{\mathsf{Vec}}}
|
||||||
|
\newcommand{\Fin}{\ensuremath{\mathsf{Fin}}}
|
||||||
|
\newcommand{\fmax}{\ensuremath{\mathsf{fmax}}}
|
||||||
|
\newcommand{\seq}[1]{\langle #1\rangle}
|
||||||
|
|
||||||
|
%%% Dependent products %%%
|
||||||
|
\def\prdsym{\textstyle\prod}
|
||||||
|
%% Call the macro like \prd{x,y:A}{p:x=y} with any number of
|
||||||
|
%% arguments. Make sure that whatever comes *after* the call doesn't
|
||||||
|
%% begin with an open-brace, or it will be parsed as another argument.
|
||||||
|
\makeatletter
|
||||||
|
% Currently the macro is configured to produce
|
||||||
|
% {\textstyle\prod}(x:A) \; {\textstyle\prod}(y:B),\
|
||||||
|
% in display-math mode, and
|
||||||
|
% \prod_{(x:A)} \prod_{y:B}
|
||||||
|
% in text-math mode.
|
||||||
|
\def\prd#1{\@ifnextchar\bgroup{\prd@parens{#1}}{\@ifnextchar\sm{\prd@parens{#1}\@eatsm}{\prd@noparens{#1}}}}
|
||||||
|
\def\prd@parens#1{\@ifnextchar\bgroup%
|
||||||
|
{\mathchoice{\@dprd{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}\prd@parens}%
|
||||||
|
{\@ifnextchar\sm%
|
||||||
|
{\mathchoice{\@dprd{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}\@eatsm}%
|
||||||
|
{\mathchoice{\@dprd{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}}}}
|
||||||
|
\def\@eatsm\sm{\sm@parens}
|
||||||
|
\def\prd@noparens#1{\mathchoice{\@dprd@noparens{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}}
|
||||||
|
% Helper macros for three styles
|
||||||
|
\def\lprd#1{\@ifnextchar\bgroup{\@lprd{#1}\lprd}{\@@lprd{#1}}}
|
||||||
|
\def\@lprd#1{\mathchoice{{\textstyle\prod}}{\prod}{\prod}{\prod}({\textstyle #1})\;}
|
||||||
|
\def\@@lprd#1{\mathchoice{{\textstyle\prod}}{\prod}{\prod}{\prod}({\textstyle #1}),\ }
|
||||||
|
\def\tprd#1{\@tprd{#1}\@ifnextchar\bgroup{\tprd}{}}
|
||||||
|
\def\@tprd#1{\mathchoice{{\textstyle\prod_{(#1)}}}{\prod_{(#1)}}{\prod_{(#1)}}{\prod_{(#1)}}}
|
||||||
|
\def\dprd#1{\@dprd{#1}\@ifnextchar\bgroup{\dprd}{}}
|
||||||
|
\def\@dprd#1{\prod_{(#1)}\,}
|
||||||
|
\def\@dprd@noparens#1{\prod_{#1}\,}
|
||||||
|
|
||||||
|
%%% Lambda abstractions.
|
||||||
|
% Each variable being abstracted over is a separate argument. If
|
||||||
|
% there is more than one such argument, they *must* be enclosed in
|
||||||
|
% braces. Arguments can be untyped, as in \lam{x}{y}, or typed with a
|
||||||
|
% colon, as in \lam{x:A}{y:B}. In the latter case, the colons are
|
||||||
|
% automatically noticed and (with current implementation) the space
|
||||||
|
% around the colon is reduced. You can even give more than one variable
|
||||||
|
% the same type, as in \lam{x,y:A}.
|
||||||
|
\def\lam#1{{\lambda}\@lamarg#1:\@endlamarg\@ifnextchar\bgroup{.\,\lam}{.\,}}
|
||||||
|
\def\@lamarg#1:#2\@endlamarg{\if\relax\detokenize{#2}\relax #1\else\@lamvar{\@lameatcolon#2},#1\@endlamvar\fi}
|
||||||
|
\def\@lamvar#1,#2\@endlamvar{(#2\,{:}\,#1)}
|
||||||
|
% \def\@lamvar#1,#2{{#2}^{#1}\@ifnextchar,{.\,{\lambda}\@lamvar{#1}}{\let\@endlamvar\relax}}
|
||||||
|
\def\@lameatcolon#1:{#1}
|
||||||
|
\let\lamt\lam
|
||||||
|
% This version silently eats any typing annotation.
|
||||||
|
\def\lamu#1{{\lambda}\@lamuarg#1:\@endlamuarg\@ifnextchar\bgroup{.\,\lamu}{.\,}}
|
||||||
|
\def\@lamuarg#1:#2\@endlamuarg{#1}
|
||||||
|
|
||||||
|
%%% Dependent products written with \forall, in the same style
|
||||||
|
\def\fall#1{\forall (#1)\@ifnextchar\bgroup{.\,\fall}{.\,}}
|
||||||
|
|
||||||
|
%%% Existential quantifier %%%
|
||||||
|
\def\exis#1{\exists (#1)\@ifnextchar\bgroup{.\,\exis}{.\,}}
|
||||||
|
|
||||||
|
%%% Dependent sums %%%
|
||||||
|
\def\smsym{\textstyle\sum}
|
||||||
|
% Use in the same way as \prd
|
||||||
|
\def\sm#1{\@ifnextchar\bgroup{\sm@parens{#1}}{\@ifnextchar\prd{\sm@parens{#1}\@eatprd}{\sm@noparens{#1}}}}
|
||||||
|
\def\sm@parens#1{\@ifnextchar\bgroup%
|
||||||
|
{\mathchoice{\@dsm{#1}}{\@tsm{#1}}{\@tsm{#1}}{\@tsm{#1}}\sm@parens}%
|
||||||
|
{\@ifnextchar\prd%
|
||||||
|
{\mathchoice{\@dsm{#1}}{\@tsm{#1}}{\@tsm{#1}}{\@tsm{#1}}\@eatprd}%
|
||||||
|
{\mathchoice{\@dsm{#1}}{\@tsm{#1}}{\@tsm{#1}}{\@tsm{#1}}}}}
|
||||||
|
\def\@eatprd\prd{\prd@parens}
|
||||||
|
\def\sm@noparens#1{\mathchoice{\@dsm@noparens{#1}}{\@tsm{#1}}{\@tsm{#1}}{\@tsm{#1}}}
|
||||||
|
\def\lsm#1{\@ifnextchar\bgroup{\@lsm{#1}\lsm}{\@@lsm{#1}}}
|
||||||
|
\def\@lsm#1{\mathchoice{{\textstyle\sum}}{\sum}{\sum}{\sum}({\textstyle #1})\;}
|
||||||
|
\def\@@lsm#1{\mathchoice{{\textstyle\sum}}{\sum}{\sum}{\sum}({\textstyle #1}),\ }
|
||||||
|
\def\tsm#1{\@tsm{#1}\@ifnextchar\bgroup{\tsm}{}}
|
||||||
|
\def\@tsm#1{\mathchoice{{\textstyle\sum_{(#1)}}}{\sum_{(#1)}}{\sum_{(#1)}}{\sum_{(#1)}}}
|
||||||
|
\def\dsm#1{\@dsm{#1}\@ifnextchar\bgroup{\dsm}{}}
|
||||||
|
\def\@dsm#1{\sum_{(#1)}\,}
|
||||||
|
\def\@dsm@noparens#1{\sum_{#1}\,}
|
||||||
|
|
||||||
|
%%% W-types
|
||||||
|
\def\wtypesym{{\mathsf{W}}}
|
||||||
|
\def\wtype#1{\@ifnextchar\bgroup%
|
||||||
|
{\mathchoice{\@twtype{#1}}{\@twtype{#1}}{\@twtype{#1}}{\@twtype{#1}}\wtype}%
|
||||||
|
{\mathchoice{\@twtype{#1}}{\@twtype{#1}}{\@twtype{#1}}{\@twtype{#1}}}}
|
||||||
|
\def\lwtype#1{\@ifnextchar\bgroup{\@lwtype{#1}\lwtype}{\@@lwtype{#1}}}
|
||||||
|
\def\@lwtype#1{\mathchoice{{\textstyle\mathsf{W}}}{\mathsf{W}}{\mathsf{W}}{\mathsf{W}}({\textstyle #1})\;}
|
||||||
|
\def\@@lwtype#1{\mathchoice{{\textstyle\mathsf{W}}}{\mathsf{W}}{\mathsf{W}}{\mathsf{W}}({\textstyle #1}),\ }
|
||||||
|
\def\twtype#1{\@twtype{#1}\@ifnextchar\bgroup{\twtype}{}}
|
||||||
|
\def\@twtype#1{\mathchoice{{\textstyle\mathsf{W}_{(#1)}}}{\mathsf{W}_{(#1)}}{\mathsf{W}_{(#1)}}{\mathsf{W}_{(#1)}}}
|
||||||
|
\def\dwtype#1{\@dwtype{#1}\@ifnextchar\bgroup{\dwtype}{}}
|
||||||
|
\def\@dwtype#1{\mathsf{W}_{(#1)}\,}
|
||||||
|
|
||||||
|
\newcommand{\suppsym}{{\mathsf{sup}}}
|
||||||
|
\newcommand{\supp}{\ensuremath\suppsym\xspace}
|
||||||
|
|
||||||
|
\def\wtypeh#1{\@ifnextchar\bgroup%
|
||||||
|
{\mathchoice{\@lwtypeh{#1}}{\@twtypeh{#1}}{\@twtypeh{#1}}{\@twtypeh{#1}}\wtypeh}%
|
||||||
|
{\mathchoice{\@@lwtypeh{#1}}{\@twtypeh{#1}}{\@twtypeh{#1}}{\@twtypeh{#1}}}}
|
||||||
|
\def\lwtypeh#1{\@ifnextchar\bgroup{\@lwtypeh{#1}\lwtypeh}{\@@lwtypeh{#1}}}
|
||||||
|
\def\@lwtypeh#1{\mathchoice{{\textstyle\mathsf{W}^h}}{\mathsf{W}^h}{\mathsf{W}^h}{\mathsf{W}^h}({\textstyle #1})\;}
|
||||||
|
\def\@@lwtypeh#1{\mathchoice{{\textstyle\mathsf{W}^h}}{\mathsf{W}^h}{\mathsf{W}^h}{\mathsf{W}^h}({\textstyle #1}),\ }
|
||||||
|
\def\twtypeh#1{\@twtypeh{#1}\@ifnextchar\bgroup{\twtypeh}{}}
|
||||||
|
\def\@twtypeh#1{\mathchoice{{\textstyle\mathsf{W}^h_{(#1)}}}{\mathsf{W}^h_{(#1)}}{\mathsf{W}^h_{(#1)}}{\mathsf{W}^h_{(#1)}}}
|
||||||
|
\def\dwtypeh#1{\@dwtypeh{#1}\@ifnextchar\bgroup{\dwtypeh}{}}
|
||||||
|
\def\@dwtypeh#1{\mathsf{W}^h_{(#1)}\,}
|
||||||
|
|
||||||
|
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
% Other notations related to dependent sums
|
||||||
|
\let\setof\Set % from package 'braket', write \setof{ x:A | P(x) }.
|
||||||
|
\newcommand{\pair}{\ensuremath{\mathsf{pair}}\xspace}
|
||||||
|
\newcommand{\tup}[2]{(#1,#2)}
|
||||||
|
\newcommand{\proj}[1]{\ensuremath{\mathsf{pr}_{#1}}\xspace}
|
||||||
|
\newcommand{\fst}{\ensuremath{\proj1}\xspace}
|
||||||
|
\newcommand{\snd}{\ensuremath{\proj2}\xspace}
|
||||||
|
\newcommand{\ac}{\ensuremath{\mathsf{ac}}\xspace} % not needed in symbol index
|
||||||
|
\newcommand{\un}{\ensuremath{\mathsf{upun}}\xspace} % not needed in symbol index, uniqueness principle for unit type
|
||||||
|
|
||||||
|
%%% recursor and induction
|
||||||
|
\newcommand{\rec}[1]{\mathsf{rec}_{#1}}
|
||||||
|
\newcommand{\ind}[1]{\mathsf{ind}_{#1}}
|
||||||
|
\newcommand{\indid}[1]{\ind{=_{#1}}} % (Martin-Lof) path induction principle for identity types
|
||||||
|
\newcommand{\indidb}[1]{\ind{=_{#1}}'} % (Paulin-Mohring) based path induction principle for identity types
|
||||||
|
|
||||||
|
%%% the uniqueness principle for product types, formerly called surjective pairing and named \spr:
|
||||||
|
\newcommand{\uppt}{\ensuremath{\mathsf{uppt}}\xspace}
|
||||||
|
|
||||||
|
% Paths in pairs
|
||||||
|
\newcommand{\pairpath}{\ensuremath{\mathsf{pair}^{\mathord{=}}}\xspace}
|
||||||
|
% \newcommand{\projpath}[1]{\proj{#1}^{\mathord{=}}}
|
||||||
|
\newcommand{\projpath}[1]{\ensuremath{\apfunc{\proj{#1}}}\xspace}
|
||||||
|
|
||||||
|
%%% For quotients %%%
|
||||||
|
%\newcommand{\pairr}[1]{{\langle #1\rangle}}
|
||||||
|
\newcommand{\pairr}[1]{{\mathopen{}(#1)\mathclose{}}}
|
||||||
|
\newcommand{\Pairr}[1]{{\mathopen{}\left(#1\right)\mathclose{}}}
|
||||||
|
|
||||||
|
% \newcommand{\type}{\ensuremath{\mathsf{Type}}} % this command is overridden below, so it's commented out
|
||||||
|
\newcommand{\im}{\ensuremath{\mathsf{im}}} % the image
|
||||||
|
|
||||||
|
%%% 2D path operations
|
||||||
|
\newcommand{\leftwhisker}{\mathbin{{\ct}_{\ell}}}
|
||||||
|
\newcommand{\rightwhisker}{\mathbin{{\ct}_{r}}}
|
||||||
|
\newcommand{\hct}{\star}
|
||||||
|
|
||||||
|
%%% modalities %%%
|
||||||
|
\newcommand{\modal}{\ensuremath{\ocircle}}
|
||||||
|
\let\reflect\modal
|
||||||
|
\newcommand{\modaltype}{\ensuremath{\type_\modal}}
|
||||||
|
% \newcommand{\ism}[1]{\ensuremath{\mathsf{is}_{#1}}}
|
||||||
|
% \newcommand{\ismodal}{\ism{\modal}}
|
||||||
|
% \newcommand{\existsmodal}{\ensuremath{{\exists}_{\modal}}}
|
||||||
|
% \newcommand{\existsmodalunique}{\ensuremath{{\exists!}_{\modal}}}
|
||||||
|
% \newcommand{\modalfunc}{\textsf{\modal-fun}}
|
||||||
|
% \newcommand{\Ecirc}{\ensuremath{\mathsf{E}_\modal}}
|
||||||
|
% \newcommand{\Mcirc}{\ensuremath{\mathsf{M}_\modal}}
|
||||||
|
\newcommand{\mreturn}{\ensuremath{\eta}}
|
||||||
|
\let\project\mreturn
|
||||||
|
%\newcommand{\mbind}[1]{\ensuremath{\hat{#1}}}
|
||||||
|
\newcommand{\ext}{\mathsf{ext}}
|
||||||
|
%\newcommand{\mmap}[1]{\ensuremath{\bar{#1}}}
|
||||||
|
%\newcommand{\mjoin}{\ensuremath{\mreturn^{-1}}}
|
||||||
|
% Subuniverse
|
||||||
|
\renewcommand{\P}{\ensuremath{\type_{P}}\xspace}
|
||||||
|
|
||||||
|
%%% Localizations
|
||||||
|
% \newcommand{\islocal}[1]{\ensuremath{\mathsf{islocal}_{#1}}\xspace}
|
||||||
|
% \newcommand{\loc}[1]{\ensuremath{\mathcal{L}_{#1}}\xspace}
|
||||||
|
|
||||||
|
%%% Identity types %%%
|
||||||
|
\newcommand{\idsym}{{=}}
|
||||||
|
\newcommand{\id}[3][]{\ensuremath{#2 =_{#1} #3}\xspace}
|
||||||
|
\newcommand{\idtype}[3][]{\ensuremath{\mathsf{Id}_{#1}(#2,#3)}\xspace}
|
||||||
|
\newcommand{\idtypevar}[1]{\ensuremath{\mathsf{Id}_{#1}}\xspace}
|
||||||
|
% A propositional equality currently being defined
|
||||||
|
\newcommand{\defid}{\coloneqq}
|
||||||
|
|
||||||
|
%%% Dependent paths
|
||||||
|
\newcommand{\dpath}[4]{#3 =^{#1}_{#2} #4}
|
||||||
|
|
||||||
|
%%% singleton
|
||||||
|
% \newcommand{\sgl}{\ensuremath{\mathsf{sgl}}\xspace}
|
||||||
|
% \newcommand{\sctr}{\ensuremath{\mathsf{sctr}}\xspace}
|
||||||
|
|
||||||
|
%%% Reflexivity terms %%%
|
||||||
|
% \newcommand{\reflsym}{{\mathsf{refl}}}
|
||||||
|
\newcommand{\refl}[1]{\ensuremath{\mathsf{refl}_{#1}}\xspace}
|
||||||
|
|
||||||
|
%%% Path concatenation (used infix, in diagrammatic order) %%%
|
||||||
|
\newcommand{\ct}{%
|
||||||
|
\mathchoice{\mathbin{\raisebox{0.5ex}{$\displaystyle\centerdot$}}}%
|
||||||
|
{\mathbin{\raisebox{0.5ex}{$\centerdot$}}}%
|
||||||
|
{\mathbin{\raisebox{0.25ex}{$\scriptstyle\,\centerdot\,$}}}%
|
||||||
|
{\mathbin{\raisebox{0.1ex}{$\scriptscriptstyle\,\centerdot\,$}}}
|
||||||
|
}
|
||||||
|
|
||||||
|
%%% Path reversal %%%
|
||||||
|
\newcommand{\opp}[1]{\mathord{{#1}^{-1}}}
|
||||||
|
\let\rev\opp
|
||||||
|
|
||||||
|
%%% Transport (covariant) %%%
|
||||||
|
\newcommand{\trans}[2]{\ensuremath{{#1}_{*}\mathopen{}\left({#2}\right)\mathclose{}}\xspace}
|
||||||
|
\let\Trans\trans
|
||||||
|
%\newcommand{\Trans}[2]{\ensuremath{{#1}_{*}\left({#2}\right)}\xspace}
|
||||||
|
\newcommand{\transf}[1]{\ensuremath{{#1}_{*}}\xspace} % Without argument
|
||||||
|
%\newcommand{\transport}[2]{\ensuremath{\mathsf{transport}_{*} \: {#2}\xspace}}
|
||||||
|
\newcommand{\transfib}[3]{\ensuremath{\mathsf{transport}^{#1}(#2,#3)\xspace}}
|
||||||
|
\newcommand{\Transfib}[3]{\ensuremath{\mathsf{transport}^{#1}\Big(#2,\, #3\Big)\xspace}}
|
||||||
|
\newcommand{\transfibf}[1]{\ensuremath{\mathsf{transport}^{#1}\xspace}}
|
||||||
|
|
||||||
|
%%% 2D transport
|
||||||
|
\newcommand{\transtwo}[2]{\ensuremath{\mathsf{transport}^2\mathopen{}\left({#1},{#2}\right)\mathclose{}}\xspace}
|
||||||
|
|
||||||
|
%%% Constant transport
|
||||||
|
\newcommand{\transconst}[3]{\ensuremath{\mathsf{transportconst}}^{#1}_{#2}(#3)\xspace}
|
||||||
|
\newcommand{\transconstf}{\ensuremath{\mathsf{transportconst}}\xspace}
|
||||||
|
|
||||||
|
%%% Map on paths %%%
|
||||||
|
\newcommand{\mapfunc}[1]{\ensuremath{\mathsf{ap}_{#1}}\xspace} % Without argument
|
||||||
|
\newcommand{\map}[2]{\ensuremath{{#1}\mathopen{}\left({#2}\right)\mathclose{}}\xspace}
|
||||||
|
\let\Ap\map
|
||||||
|
%\newcommand{\Ap}[2]{\ensuremath{{#1}\left({#2}\right)}\xspace}
|
||||||
|
\newcommand{\mapdepfunc}[1]{\ensuremath{\mathsf{apd}_{#1}}\xspace} % Without argument
|
||||||
|
% \newcommand{\mapdep}[2]{\ensuremath{{#1}\llparenthesis{#2}\rrparenthesis}\xspace}
|
||||||
|
\newcommand{\mapdep}[2]{\ensuremath{\mapdepfunc{#1}\mathopen{}\left(#2\right)\mathclose{}}\xspace}
|
||||||
|
\let\apfunc\mapfunc
|
||||||
|
\let\ap\map
|
||||||
|
\let\apdfunc\mapdepfunc
|
||||||
|
\let\apd\mapdep
|
||||||
|
|
||||||
|
%%% 2D map on paths
|
||||||
|
\newcommand{\aptwofunc}[1]{\ensuremath{\mathsf{ap}^2_{#1}}\xspace}
|
||||||
|
\newcommand{\aptwo}[2]{\ensuremath{\aptwofunc{#1}\mathopen{}\left({#2}\right)\mathclose{}}\xspace}
|
||||||
|
\newcommand{\apdtwofunc}[1]{\ensuremath{\mathsf{apd}^2_{#1}}\xspace}
|
||||||
|
\newcommand{\apdtwo}[2]{\ensuremath{\apdtwofunc{#1}\mathopen{}\left(#2\right)\mathclose{}}\xspace}
|
||||||
|
|
||||||
|
%%% Identity functions %%%
|
||||||
|
\newcommand{\idfunc}[1][]{\ensuremath{\mathsf{id}_{#1}}\xspace}
|
||||||
|
|
||||||
|
%%% Homotopies (written infix) %%%
|
||||||
|
\newcommand{\htpy}{\sim}
|
||||||
|
|
||||||
|
%%% Other meanings of \sim
|
||||||
|
\newcommand{\bisim}{\sim} % bisimulation
|
||||||
|
\newcommand{\eqr}{\sim} % an equivalence relation
|
||||||
|
|
||||||
|
%%% Equivalence types %%%
|
||||||
|
\newcommand{\eqv}[2]{\ensuremath{#1 \simeq #2}\xspace}
|
||||||
|
\newcommand{\eqvspaced}[2]{\ensuremath{#1 \;\simeq\; #2}\xspace}
|
||||||
|
\newcommand{\eqvsym}{\simeq} % infix symbol
|
||||||
|
\newcommand{\texteqv}[2]{\ensuremath{\mathsf{Equiv}(#1,#2)}\xspace}
|
||||||
|
\newcommand{\isequiv}{\ensuremath{\mathsf{isequiv}}}
|
||||||
|
\newcommand{\qinv}{\ensuremath{\mathsf{qinv}}}
|
||||||
|
\newcommand{\ishae}{\ensuremath{\mathsf{ishae}}}
|
||||||
|
\newcommand{\linv}{\ensuremath{\mathsf{linv}}}
|
||||||
|
\newcommand{\rinv}{\ensuremath{\mathsf{rinv}}}
|
||||||
|
\newcommand{\biinv}{\ensuremath{\mathsf{biinv}}}
|
||||||
|
\newcommand{\lcoh}[3]{\mathsf{lcoh}_{#1}(#2,#3)}
|
||||||
|
\newcommand{\rcoh}[3]{\mathsf{rcoh}_{#1}(#2,#3)}
|
||||||
|
\newcommand{\hfib}[2]{{\mathsf{fib}}_{#1}(#2)}
|
||||||
|
|
||||||
|
%%% Map on total spaces %%%
|
||||||
|
\newcommand{\total}[1]{\ensuremath{\mathsf{total}(#1)}}
|
||||||
|
|
||||||
|
%%% Universe types %%%
|
||||||
|
%\newcommand{\type}{\ensuremath{\mathsf{Type}}\xspace}
|
||||||
|
\newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace}
|
||||||
|
\let\bbU\UU
|
||||||
|
\let\type\UU
|
||||||
|
% Universes of truncated types
|
||||||
|
\newcommand{\typele}[1]{\ensuremath{{#1}\text-\mathsf{Type}}\xspace}
|
||||||
|
\newcommand{\typeleU}[1]{\ensuremath{{#1}\text-\mathsf{Type}_\UU}\xspace}
|
||||||
|
\newcommand{\typelep}[1]{\ensuremath{{(#1)}\text-\mathsf{Type}}\xspace}
|
||||||
|
\newcommand{\typelepU}[1]{\ensuremath{{(#1)}\text-\mathsf{Type}_\UU}\xspace}
|
||||||
|
\let\ntype\typele
|
||||||
|
\let\ntypeU\typeleU
|
||||||
|
\let\ntypep\typelep
|
||||||
|
\let\ntypepU\typelepU
|
||||||
|
\renewcommand{\set}{\ensuremath{\mathsf{Set}}\xspace}
|
||||||
|
\newcommand{\setU}{\ensuremath{\mathsf{Set}_\UU}\xspace}
|
||||||
|
\newcommand{\prop}{\ensuremath{\mathsf{Prop}}\xspace}
|
||||||
|
\newcommand{\propU}{\ensuremath{\mathsf{Prop}_\UU}\xspace}
|
||||||
|
%Pointed types
|
||||||
|
\newcommand{\pointed}[1]{\ensuremath{#1_\bullet}}
|
||||||
|
|
||||||
|
%%% Ordinals and cardinals
|
||||||
|
\newcommand{\card}{\ensuremath{\mathsf{Card}}\xspace}
|
||||||
|
\newcommand{\ord}{\ensuremath{\mathsf{Ord}}\xspace}
|
||||||
|
\newcommand{\ordsl}[2]{{#1}_{/#2}}
|
||||||
|
|
||||||
|
%%% Univalence
|
||||||
|
\newcommand{\ua}{\ensuremath{\mathsf{ua}}\xspace} % the inverse of idtoeqv
|
||||||
|
\newcommand{\idtoeqv}{\ensuremath{\mathsf{idtoeqv}}\xspace}
|
||||||
|
\newcommand{\univalence}{\ensuremath{\mathsf{univalence}}\xspace} % the full axiom
|
||||||
|
|
||||||
|
%%% Truncation levels
|
||||||
|
\newcommand{\iscontr}{\ensuremath{\mathsf{isContr}}}
|
||||||
|
\newcommand{\contr}{\ensuremath{\mathsf{contr}}} % The path to the center of contraction
|
||||||
|
\newcommand{\isset}{\ensuremath{\mathsf{isSet}}}
|
||||||
|
\newcommand{\isprop}{\ensuremath{\mathsf{isProp}}}
|
||||||
|
% h-propositions
|
||||||
|
% \newcommand{\anhprop}{a mere proposition\xspace}
|
||||||
|
% \newcommand{\hprops}{mere propositions\xspace}
|
||||||
|
|
||||||
|
%%% Homotopy fibers %%%
|
||||||
|
%\newcommand{\hfiber}[2]{\ensuremath{\mathsf{hFiber}(#1,#2)}\xspace}
|
||||||
|
\let\hfiber\hfib
|
||||||
|
|
||||||
|
%%% Bracket/squash/truncation types %%%
|
||||||
|
% \newcommand{\brck}[1]{\textsf{mere}(#1)}
|
||||||
|
% \newcommand{\Brck}[1]{\textsf{mere}\Big(#1\Big)}
|
||||||
|
% \newcommand{\trunc}[2]{\tau_{#1}(#2)}
|
||||||
|
% \newcommand{\Trunc}[2]{\tau_{#1}\Big(#2\Big)}
|
||||||
|
% \newcommand{\truncf}[1]{\tau_{#1}}
|
||||||
|
%\newcommand{\trunc}[2]{\Vert #2\Vert_{#1}}
|
||||||
|
\newcommand{\trunc}[2]{\mathopen{}\left\Vert #2\right\Vert_{#1}\mathclose{}}
|
||||||
|
\newcommand{\ttrunc}[2]{\bigl\Vert #2\bigr\Vert_{#1}}
|
||||||
|
\newcommand{\Trunc}[2]{\Bigl\Vert #2\Bigr\Vert_{#1}}
|
||||||
|
\newcommand{\truncf}[1]{\Vert \blank \Vert_{#1}}
|
||||||
|
\newcommand{\tproj}[3][]{\mathopen{}\left|#3\right|_{#2}^{#1}\mathclose{}}
|
||||||
|
\newcommand{\tprojf}[2][]{|\blank|_{#2}^{#1}}
|
||||||
|
\def\pizero{\trunc0}
|
||||||
|
%\newcommand{\brck}[1]{\trunc{-1}{#1}}
|
||||||
|
%\newcommand{\Brck}[1]{\Trunc{-1}{#1}}
|
||||||
|
%\newcommand{\bproj}[1]{\tproj{-1}{#1}}
|
||||||
|
%\newcommand{\bprojf}{\tprojf{-1}}
|
||||||
|
|
||||||
|
\newcommand{\brck}[1]{\trunc{}{#1}}
|
||||||
|
\newcommand{\bbrck}[1]{\ttrunc{}{#1}}
|
||||||
|
\newcommand{\Brck}[1]{\Trunc{}{#1}}
|
||||||
|
\newcommand{\bproj}[1]{\tproj{}{#1}}
|
||||||
|
\newcommand{\bprojf}{\tprojf{}}
|
||||||
|
|
||||||
|
% Big parentheses
|
||||||
|
\newcommand{\Parens}[1]{\Bigl(#1\Bigr)}
|
||||||
|
|
||||||
|
% Projection and extension for truncations
|
||||||
|
\let\extendsmb\ext
|
||||||
|
\newcommand{\extend}[1]{\extendsmb(#1)}
|
||||||
|
|
||||||
|
%
|
||||||
|
%%% The empty type
|
||||||
|
\newcommand{\emptyt}{\ensuremath{\mathbf{0}}\xspace}
|
||||||
|
|
||||||
|
%%% The unit type
|
||||||
|
\newcommand{\unit}{\ensuremath{\mathbf{1}}\xspace}
|
||||||
|
\newcommand{\ttt}{\ensuremath{\star}\xspace}
|
||||||
|
|
||||||
|
%%% The two-element type
|
||||||
|
\newcommand{\bool}{\ensuremath{\mathbf{2}}\xspace}
|
||||||
|
\newcommand{\btrue}{{1_{\bool}}}
|
||||||
|
\newcommand{\bfalse}{{0_{\bool}}}
|
||||||
|
|
||||||
|
%%% Injections into binary sums and pushouts
|
||||||
|
\newcommand{\inlsym}{{\mathsf{inl}}}
|
||||||
|
\newcommand{\inrsym}{{\mathsf{inr}}}
|
||||||
|
\newcommand{\inl}{\ensuremath\inlsym\xspace}
|
||||||
|
\newcommand{\inr}{\ensuremath\inrsym\xspace}
|
||||||
|
|
||||||
|
%%% The segment of the interval
|
||||||
|
\newcommand{\seg}{\ensuremath{\mathsf{seg}}\xspace}
|
||||||
|
|
||||||
|
%%% Free groups
|
||||||
|
\newcommand{\freegroup}[1]{F(#1)}
|
||||||
|
\newcommand{\freegroupx}[1]{F'(#1)} % the "other" free group
|
||||||
|
|
||||||
|
%%% Glue of a pushout
|
||||||
|
\newcommand{\glue}{\mathsf{glue}}
|
||||||
|
|
||||||
|
%%% Circles and spheres
|
||||||
|
\newcommand{\Sn}{\mathbb{S}}
|
||||||
|
\newcommand{\base}{\ensuremath{\mathsf{base}}\xspace}
|
||||||
|
\newcommand{\lloop}{\ensuremath{\mathsf{loop}}\xspace}
|
||||||
|
\newcommand{\surf}{\ensuremath{\mathsf{surf}}\xspace}
|
||||||
|
|
||||||
|
%%% Suspension
|
||||||
|
\newcommand{\susp}{\Sigma}
|
||||||
|
\newcommand{\north}{\mathsf{N}}
|
||||||
|
\newcommand{\south}{\mathsf{S}}
|
||||||
|
\newcommand{\merid}{\mathsf{merid}}
|
||||||
|
|
||||||
|
%%% Blanks (shorthand for lambda abstractions)
|
||||||
|
\newcommand{\blank}{\mathord{\hspace{1pt}\text{--}\hspace{1pt}}}
|
||||||
|
|
||||||
|
%%% Nameless objects
|
||||||
|
\newcommand{\nameless}{\mathord{\hspace{1pt}\underline{\hspace{1ex}}\hspace{1pt}}}
|
||||||
|
|
||||||
|
%%% Some decorations
|
||||||
|
%\newcommand{\bbU}{\ensuremath{\mathbb{U}}\xspace}
|
||||||
|
% \newcommand{\bbB}{\ensuremath{\mathbb{B}}\xspace}
|
||||||
|
\newcommand{\bbP}{\ensuremath{\mathbb{P}}\xspace}
|
||||||
|
|
||||||
|
%%% Some categories
|
||||||
|
\newcommand{\uset}{\ensuremath{\mathcal{S}et}\xspace}
|
||||||
|
\newcommand{\ucat}{\ensuremath{{\mathcal{C}at}}\xspace}
|
||||||
|
\newcommand{\urel}{\ensuremath{\mathcal{R}el}\xspace}
|
||||||
|
\newcommand{\uhilb}{\ensuremath{\mathcal{H}ilb}\xspace}
|
||||||
|
\newcommand{\utype}{\ensuremath{\mathcal{T}\!ype}\xspace}
|
||||||
|
|
||||||
|
% Pullback corner
|
||||||
|
%\newbox\pbbox
|
||||||
|
%\setbox\pbbox=\hbox{\xy \POS(65,0)\ar@{-} (0,0) \ar@{-} (65,65)\endxy}
|
||||||
|
%\def\pb{\save[]+<3.5mm,-3.5mm>*{\copy\pbbox} \restore}
|
||||||
|
|
||||||
|
% Macros for the categories chapter
|
||||||
|
\newcommand{\inv}[1]{{#1}^{-1}}
|
||||||
|
\newcommand{\idtoiso}{\ensuremath{\mathsf{idtoiso}}\xspace}
|
||||||
|
\newcommand{\isotoid}{\ensuremath{\mathsf{isotoid}}\xspace}
|
||||||
|
\newcommand{\op}{^{\mathrm{op}}}
|
||||||
|
\newcommand{\y}{\ensuremath{\mathbf{y}}\xspace}
|
||||||
|
\newcommand{\dgr}[1]{{#1}^{\dagger}}
|
||||||
|
\newcommand{\unitaryiso}{\mathrel{\cong^\dagger}}
|
||||||
|
\newcommand{\cteqv}[2]{\ensuremath{#1 \simeq #2}\xspace}
|
||||||
|
\newcommand{\cteqvsym}{\simeq} % Symbol for equivalence of categories
|
||||||
|
|
||||||
|
%%% Natural numbers
|
||||||
|
\newcommand{\N}{\ensuremath{\mathbb{N}}\xspace}
|
||||||
|
%\newcommand{\N}{\textbf{N}}
|
||||||
|
\let\nat\N
|
||||||
|
\newcommand{\natp}{\ensuremath{\nat'}\xspace} % alternative nat in induction chapter
|
||||||
|
|
||||||
|
\newcommand{\zerop}{\ensuremath{0'}\xspace} % alternative zero in induction chapter
|
||||||
|
\newcommand{\suc}{\mathsf{succ}}
|
||||||
|
\newcommand{\sucp}{\ensuremath{\suc'}\xspace} % alternative suc in induction chapter
|
||||||
|
\newcommand{\add}{\mathsf{add}}
|
||||||
|
\newcommand{\ack}{\mathsf{ack}}
|
||||||
|
\newcommand{\ite}{\mathsf{iter}}
|
||||||
|
\newcommand{\assoc}{\mathsf{assoc}}
|
||||||
|
\newcommand{\dbl}{\ensuremath{\mathsf{double}}}
|
||||||
|
\newcommand{\dblp}{\ensuremath{\dbl'}\xspace} % alternative double in induction chapter
|
||||||
|
|
||||||
|
|
||||||
|
%%% Lists
|
||||||
|
\newcommand{\lst}[1]{\mathsf{List}(#1)}
|
||||||
|
\newcommand{\nil}{\mathsf{nil}}
|
||||||
|
\newcommand{\cons}{\mathsf{cons}}
|
||||||
|
|
||||||
|
%%% Vectors of given length, used in induction chapter
|
||||||
|
\newcommand{\vect}[2]{\ensuremath{\mathsf{Vec}_{#1}(#2)}\xspace}
|
||||||
|
|
||||||
|
%%% Integers
|
||||||
|
\newcommand{\Z}{\ensuremath{\mathbb{Z}}\xspace}
|
||||||
|
\newcommand{\Zsuc}{\mathsf{succ}}
|
||||||
|
\newcommand{\Zpred}{\mathsf{pred}}
|
||||||
|
|
||||||
|
%%% Rationals
|
||||||
|
\newcommand{\Q}{\ensuremath{\mathbb{Q}}\xspace}
|
||||||
|
|
||||||
|
%%% Function extensionality
|
||||||
|
\newcommand{\funext}{\mathsf{funext}}
|
||||||
|
\newcommand{\happly}{\mathsf{happly}}
|
||||||
|
|
||||||
|
%%% A naturality lemma
|
||||||
|
\newcommand{\com}[3]{\mathsf{swap}_{#1,#2}(#3)}
|
||||||
|
|
||||||
|
%%% Code/encode/decode
|
||||||
|
\newcommand{\code}{\ensuremath{\mathsf{code}}\xspace}
|
||||||
|
\newcommand{\encode}{\ensuremath{\mathsf{encode}}\xspace}
|
||||||
|
\newcommand{\decode}{\ensuremath{\mathsf{decode}}\xspace}
|
||||||
|
|
||||||
|
% Function definition with domain and codomain
|
||||||
|
\newcommand{\function}[4]{\left\{\begin{array}{rcl}#1 &
|
||||||
|
\longrightarrow & #2 \\ #3 & \longmapsto & #4 \end{array}\right.}
|
||||||
|
|
||||||
|
%%% Cones and cocones
|
||||||
|
\newcommand{\cone}[2]{\mathsf{cone}_{#1}(#2)}
|
||||||
|
\newcommand{\cocone}[2]{\mathsf{cocone}_{#1}(#2)}
|
||||||
|
% Apply a function to a cocone
|
||||||
|
\newcommand{\composecocone}[2]{#1\circ#2}
|
||||||
|
\newcommand{\composecone}[2]{#2\circ#1}
|
||||||
|
%%% Diagrams
|
||||||
|
\newcommand{\Ddiag}{\mathscr{D}}
|
||||||
|
|
||||||
|
%%% (pointed) mapping spaces
|
||||||
|
\newcommand{\Map}{\mathsf{Map}}
|
||||||
|
|
||||||
|
%%% The interval
|
||||||
|
\newcommand{\interval}{\ensuremath{I}\xspace}
|
||||||
|
\newcommand{\izero}{\ensuremath{0_{\interval}}\xspace}
|
||||||
|
\newcommand{\ione}{\ensuremath{1_{\interval}}\xspace}
|
||||||
|
|
||||||
|
%%% Arrows
|
||||||
|
\newcommand{\epi}{\ensuremath{\twoheadrightarrow}}
|
||||||
|
\newcommand{\mono}{\ensuremath{\rightarrowtail}}
|
||||||
|
|
||||||
|
%%% Sets
|
||||||
|
\newcommand{\bin}{\ensuremath{\mathrel{\widetilde{\in}}}}
|
||||||
|
|
||||||
|
%%% Semigroup structure
|
||||||
|
\newcommand{\semigroupstrsym}{\ensuremath{\mathsf{SemigroupStr}}}
|
||||||
|
\newcommand{\semigroupstr}[1]{\ensuremath{\mathsf{SemigroupStr}}(#1)}
|
||||||
|
\newcommand{\semigroup}[0]{\ensuremath{\mathsf{Semigroup}}}
|
||||||
|
|
||||||
|
%%% Macros for the formal type theory
|
||||||
|
\newcommand{\emptyctx}{\ensuremath{\cdot}}
|
||||||
|
\newcommand{\production}{\vcentcolon\vcentcolon=}
|
||||||
|
\newcommand{\conv}{\downarrow}
|
||||||
|
\newcommand{\ctx}{\ensuremath{\mathsf{ctx}}}
|
||||||
|
\newcommand{\wfctx}[1]{#1\ \ctx}
|
||||||
|
\newcommand{\oftp}[3]{#1 \vdash #2 : #3}
|
||||||
|
\newcommand{\jdeqtp}[4]{#1 \vdash #2 \jdeq #3 : #4}
|
||||||
|
\newcommand{\judg}[2]{#1 \vdash #2}
|
||||||
|
\newcommand{\tmtp}[2]{#1 \mathord{:} #2}
|
||||||
|
|
||||||
|
% rule names
|
||||||
|
\newcommand{\form}{\textsc{form}}
|
||||||
|
\newcommand{\intro}{\textsc{intro}}
|
||||||
|
\newcommand{\elim}{\textsc{elim}}
|
||||||
|
\newcommand{\comp}{\textsc{comp}}
|
||||||
|
\newcommand{\uniq}{\textsc{uniq}}
|
||||||
|
\newcommand{\Weak}{\mathsf{Wkg}}
|
||||||
|
\newcommand{\Vble}{\mathsf{Vble}}
|
||||||
|
\newcommand{\Exch}{\mathsf{Exch}}
|
||||||
|
\newcommand{\Subst}{\mathsf{Subst}}
|
||||||
|
|
||||||
|
%%% Macros for HITs
|
||||||
|
\newcommand{\cc}{\mathsf{c}}
|
||||||
|
\newcommand{\pp}{\mathsf{p}}
|
||||||
|
\newcommand{\cct}{\widetilde{\mathsf{c}}}
|
||||||
|
\newcommand{\ppt}{\widetilde{\mathsf{p}}}
|
||||||
|
\newcommand{\Wtil}{\ensuremath{\widetilde{W}}\xspace}
|
||||||
|
|
||||||
|
%%% Macros for n-types
|
||||||
|
\newcommand{\istype}[1]{\mathsf{is}\mbox{-}{#1}\mbox{-}\mathsf{type}}
|
||||||
|
\newcommand{\nplusone}{\ensuremath{(n+1)}}
|
||||||
|
\newcommand{\nminusone}{\ensuremath{(n-1)}}
|
||||||
|
\newcommand{\fact}{\mathsf{fact}}
|
||||||
|
|
||||||
|
%%% Macros for homotopy
|
||||||
|
\newcommand{\kbar}{\overline{k}} % Used in van Kampen's theorem
|
||||||
|
|
||||||
|
%%% Macros for induction
|
||||||
|
\newcommand{\natw}{\ensuremath{\mathbf{N^w}}\xspace}
|
||||||
|
\newcommand{\zerow}{\ensuremath{0^\mathbf{w}}\xspace}
|
||||||
|
\newcommand{\sucw}{\ensuremath{\mathbf{s^w}}\xspace}
|
||||||
|
\newcommand{\nalg}{\nat\mathsf{Alg}}
|
||||||
|
\newcommand{\nhom}{\nat\mathsf{Hom}}
|
||||||
|
\newcommand{\ishinitw}{\mathsf{isHinit}_{\mathsf{W}}}
|
||||||
|
\newcommand{\ishinitn}{\mathsf{isHinit}_\nat}
|
||||||
|
\newcommand{\w}{\mathsf{W}}
|
||||||
|
\newcommand{\walg}{\w\mathsf{Alg}}
|
||||||
|
\newcommand{\whom}{\w\mathsf{Hom}}
|
||||||
|
|
||||||
|
%%% Macros for real numbers
|
||||||
|
\newcommand{\RC}{\ensuremath{\mathbb{R}_\mathsf{c}}\xspace} % Cauchy
|
||||||
|
\newcommand{\RD}{\ensuremath{\mathbb{R}_\mathsf{d}}\xspace} % Dedekind
|
||||||
|
\newcommand{\R}{\ensuremath{\mathbb{R}}\xspace} % Either
|
||||||
|
\newcommand{\barRD}{\ensuremath{\bar{\mathbb{R}}_\mathsf{d}}\xspace} % Dedekind completion of Dedekind
|
||||||
|
|
||||||
|
\newcommand{\close}[1]{\sim_{#1}} % Relation of closeness
|
||||||
|
\newcommand{\closesym}{\mathord\sim}
|
||||||
|
\newcommand{\rclim}{\mathsf{lim}} % HIT constructor for Cauchy reals
|
||||||
|
\newcommand{\rcrat}{\mathsf{rat}} % Embedding of rationals into Cauchy reals
|
||||||
|
\newcommand{\rceq}{\mathsf{eq}_{\RC}} % HIT path constructor
|
||||||
|
\newcommand{\CAP}{\mathcal{C}} % The type of Cauchy approximations
|
||||||
|
\newcommand{\Qp}{\Q_{+}}
|
||||||
|
\newcommand{\apart}{\mathrel{\#}} % apartness
|
||||||
|
\newcommand{\dcut}{\mathsf{isCut}} % Dedekind cut
|
||||||
|
\newcommand{\cover}{\triangleleft} % inductive cover
|
||||||
|
\newcommand{\intfam}[3]{(#2, \lam{#1} #3)} % family of rational intervals
|
||||||
|
|
||||||
|
% Macros for the Cauchy reals construction
|
||||||
|
\newcommand{\bsim}{\frown}
|
||||||
|
\newcommand{\bbsim}{\smile}
|
||||||
|
|
||||||
|
\newcommand{\hapx}{\diamondsuit\approx}
|
||||||
|
\newcommand{\hapname}{\diamondsuit}
|
||||||
|
\newcommand{\hapxb}{\heartsuit\approx}
|
||||||
|
\newcommand{\hapbname}{\heartsuit}
|
||||||
|
\newcommand{\tap}[1]{\bullet\approx_{#1}\triangle}
|
||||||
|
\newcommand{\tapname}{\triangle}
|
||||||
|
\newcommand{\tapb}[1]{\bullet\approx_{#1}\square}
|
||||||
|
\newcommand{\tapbname}{\square}
|
||||||
|
|
||||||
|
%%% Macros for surreals
|
||||||
|
\newcommand{\NO}{\ensuremath{\mathsf{No}}\xspace}
|
||||||
|
\newcommand{\surr}[2]{\{\,#1\,\big|\,#2\,\}}
|
||||||
|
\newcommand{\LL}{\mathcal{L}}
|
||||||
|
\newcommand{\RR}{\mathcal{R}}
|
||||||
|
\newcommand{\noeq}{\mathsf{eq}_{\NO}} % HIT path constructor
|
||||||
|
|
||||||
|
\newcommand{\ble}{\trianglelefteqslant}
|
||||||
|
\newcommand{\blt}{\vartriangleleft}
|
||||||
|
\newcommand{\bble}{\sqsubseteq}
|
||||||
|
\newcommand{\bblt}{\sqsubset}
|
||||||
|
|
||||||
|
\newcommand{\hle}{\diamondsuit\preceq}
|
||||||
|
\newcommand{\hlt}{\diamondsuit\prec}
|
||||||
|
\newcommand{\hlname}{\diamondsuit}
|
||||||
|
\newcommand{\hleb}{\heartsuit\preceq}
|
||||||
|
\newcommand{\hltb}{\heartsuit\prec}
|
||||||
|
\newcommand{\hlbname}{\heartsuit}
|
||||||
|
% \newcommand{\tle}{(\bullet\preceq\triangle)}
|
||||||
|
% \newcommand{\tlt}{(\bullet\prec\triangle)}
|
||||||
|
\newcommand{\tle}{\triangle\preceq}
|
||||||
|
\newcommand{\tlt}{\triangle\prec}
|
||||||
|
\newcommand{\tlname}{\triangle}
|
||||||
|
% \newcommand{\tleb}{(\bullet\preceq\square)}
|
||||||
|
% \newcommand{\tltb}{(\bullet\prec\square)}
|
||||||
|
\newcommand{\tleb}{\square\preceq}
|
||||||
|
\newcommand{\tltb}{\square\prec}
|
||||||
|
\newcommand{\tlbname}{\square}
|
||||||
|
|
||||||
|
%%% Macros for set theory
|
||||||
|
\newcommand{\vset}{\mathsf{set}} % point constructor for cummulative hierarchy V
|
||||||
|
\def\cd{\tproj0}
|
||||||
|
\newcommand{\inj}{\ensuremath{\mathsf{inj}}} % type of injections
|
||||||
|
\newcommand{\acc}{\ensuremath{\mathsf{acc}}} % accessibility
|
||||||
|
|
||||||
|
\newcommand{\atMostOne}{\mathsf{atMostOne}}
|
||||||
|
|
||||||
|
\newcommand{\power}[1]{\mathcal{P}(#1)} % power set
|
||||||
|
\newcommand{\powerp}[1]{\mathcal{P}_+(#1)} % inhabited power set
|
||||||
|
|
||||||
|
%%%% THEOREM ENVIRONMENTS %%%%
|
||||||
|
|
||||||
|
% Hyperref includes the command \autoref{...} which is like \ref{...}
|
||||||
|
% except that it automatically inserts the type of the thing you're
|
||||||
|
% referring to, e.g. it produces "Theorem 3.8" instead of just "3.8"
|
||||||
|
% (and makes the whole thing a hyperlink). This saves a slight amount
|
||||||
|
% of typing, but more importantly it means that if you decide later on
|
||||||
|
% that 3.8 should be a Lemma or a Definition instead of a Theorem, you
|
||||||
|
% don't have to change the name in all the places you referred to it.
|
||||||
|
|
||||||
|
% The following hack improves on this by using the same counter for
|
||||||
|
% all theorem-type environments, so that after Theorem 1.1 comes
|
||||||
|
% Corollary 1.2 rather than Corollary 1.1. This makes it much easier
|
||||||
|
% for the reader to find a particular theorem when flipping through
|
||||||
|
% the document.
|
||||||
|
\makeatletter
|
||||||
|
\def\defthm#1#2#3{%
|
||||||
|
%% Ensure all theorem types are numbered with the same counter
|
||||||
|
\newaliascnt{#1}{thm}
|
||||||
|
\newtheorem{#1}[#1]{#2}
|
||||||
|
\aliascntresetthe{#1}
|
||||||
|
%% This command tells cleveref's \cref what to call things
|
||||||
|
\crefname{#1}{#2}{#3}}
|
||||||
|
|
||||||
|
% Now define a bunch of theorem-type environments.
|
||||||
|
\newtheorem{thm}{Theorem}[section]
|
||||||
|
\crefname{thm}{Theorem}{Theorems}
|
||||||
|
%\defthm{prop}{Proposition} % Probably we shouldn't use "Proposition" in this way
|
||||||
|
\defthm{cor}{Corollary}{Corollaries}
|
||||||
|
\defthm{lem}{Lemma}{Lemmas}
|
||||||
|
\defthm{axiom}{Axiom}{Axioms}
|
||||||
|
% Since definitions and theorems in type theory are synonymous, should
|
||||||
|
% we actually use the same theoremstyle for them?
|
||||||
|
\theoremstyle{definition}
|
||||||
|
\defthm{defn}{Definition}{Definitions}
|
||||||
|
\theoremstyle{remark}
|
||||||
|
\defthm{rmk}{Remark}{Remarks}
|
||||||
|
\defthm{eg}{Example}{Examples}
|
||||||
|
\defthm{egs}{Examples}{Examples}
|
||||||
|
\defthm{notes}{Notes}{Notes}
|
||||||
|
% Number exercises within chapters, with their own counter.
|
||||||
|
%\newtheorem{ex}{Exercise}[chapter]
|
||||||
|
%\crefname{ex}{Exercise}{Exercises}
|
||||||
|
|
||||||
|
% Display format for sections
|
||||||
|
\crefformat{section}{\S#2#1#3}
|
||||||
|
\Crefformat{section}{Section~#2#1#3}
|
||||||
|
\crefrangeformat{section}{\S\S#3#1#4--#5#2#6}
|
||||||
|
\Crefrangeformat{section}{Sections~#3#1#4--#5#2#6}
|
||||||
|
\crefmultiformat{section}{\S\S#2#1#3}{ and~#2#1#3}{, #2#1#3}{ and~#2#1#3}
|
||||||
|
\Crefmultiformat{section}{Sections~#2#1#3}{ and~#2#1#3}{, #2#1#3}{ and~#2#1#3}
|
||||||
|
\crefrangemultiformat{section}{\S\S#3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}{, #3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}
|
||||||
|
\Crefrangemultiformat{section}{Sections~#3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}{, #3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}
|
||||||
|
|
||||||
|
% Display format for appendices
|
||||||
|
\crefformat{appendix}{Appendix~#2#1#3}
|
||||||
|
\Crefformat{appendix}{Appendix~#2#1#3}
|
||||||
|
\crefrangeformat{appendix}{Appendices~#3#1#4--#5#2#6}
|
||||||
|
\Crefrangeformat{appendix}{Appendices~#3#1#4--#5#2#6}
|
||||||
|
\crefmultiformat{appendix}{Appendices~#2#1#3}{ and~#2#1#3}{, #2#1#3}{ and~#2#1#3}
|
||||||
|
\Crefmultiformat{appendix}{Appendices~#2#1#3}{ and~#2#1#3}{, #2#1#3}{ and~#2#1#3}
|
||||||
|
\crefrangemultiformat{appendix}{Appendices~#3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}{, #3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}
|
||||||
|
\Crefrangemultiformat{appendix}{Appendices~#3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}{, #3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}
|
||||||
|
|
||||||
|
\crefname{part}{Part}{Parts}
|
||||||
|
|
||||||
|
% Number subsubsections
|
||||||
|
\setcounter{secnumdepth}{5}
|
||||||
|
|
||||||
|
% Display format for figures
|
||||||
|
\crefname{figure}{Figure}{Figures}
|
||||||
|
|
||||||
|
% Use cleveref instead of hyperref's \autoref
|
||||||
|
\let\autoref\cref
|
||||||
|
|
||||||
|
|
||||||
|
%%%% EQUATION NUMBERING %%%%
|
||||||
|
|
||||||
|
% The following hack uses the single theorem counter to number
|
||||||
|
% equations as well, so that we don't have both Theorem 1.1 and
|
||||||
|
% equation (1.1).
|
||||||
|
\let\c@equation\c@thm
|
||||||
|
\numberwithin{equation}{section}
|
||||||
|
|
||||||
|
|
||||||
|
%%%% ENUMERATE NUMBERING %%%%
|
||||||
|
|
||||||
|
% Number the first level of enumerates as (i), (ii), ...
|
||||||
|
\renewcommand{\theenumi}{(\roman{enumi})}
|
||||||
|
\renewcommand{\labelenumi}{\theenumi}
|
||||||
|
|
||||||
|
|
||||||
|
%%%% MARGINS %%%%
|
||||||
|
|
||||||
|
% This is a matter of personal preference, but I think the left
|
||||||
|
% margins on enumerates and itemizes are too wide.
|
||||||
|
\setitemize[1]{leftmargin=2em}
|
||||||
|
\setenumerate[1]{leftmargin=*}
|
||||||
|
|
||||||
|
% Likewise that they are too spaced out.
|
||||||
|
\setitemize[1]{itemsep=-0.2em}
|
||||||
|
\setenumerate[1]{itemsep=-0.2em}
|
||||||
|
|
||||||
|
%%% Notes %%%
|
||||||
|
\def\noteson{%
|
||||||
|
\gdef\note##1{\mbox{}\marginpar{\color{blue}\textasteriskcentered\ ##1}}}
|
||||||
|
\gdef\notesoff{\gdef\note##1{\null}}
|
||||||
|
\noteson
|
||||||
|
|
||||||
|
\newcommand{\Coq}{\textsc{Coq}\xspace}
|
||||||
|
\newcommand{\Agda}{\textsc{Agda}\xspace}
|
||||||
|
\newcommand{\NuPRL}{\textsc{NuPRL}\xspace}
|
||||||
|
|
||||||
|
%%%% CITATIONS %%%%
|
||||||
|
|
||||||
|
% \let \cite \citep
|
||||||
|
|
||||||
|
%%%% INDEX %%%%
|
||||||
|
|
||||||
|
\newcommand{\footstyle}[1]{{\hyperpage{#1}}n} % If you index something that is in a footnote
|
||||||
|
\newcommand{\defstyle}[1]{\textbf{\hyperpage{#1}}} % Style for pageref to a definition
|
||||||
|
|
||||||
|
\newcommand{\indexdef}[1]{\index{#1|defstyle}} % Index a definition
|
||||||
|
\newcommand{\indexfoot}[1]{\index{#1|footstyle}} % Index a term in a footnote
|
||||||
|
\newcommand{\indexsee}[2]{\index{#1|see{#2}}} % Index "see also"
|
||||||
|
|
||||||
|
|
||||||
|
%%%% Standard phrasing or spelling of common phrases %%%%
|
||||||
|
|
||||||
|
\newcommand{\ZF}{Zermelo--Fraenkel}
|
||||||
|
\newcommand{\CZF}{Constructive \ZF{} Set Theory}
|
||||||
|
|
||||||
|
\newcommand{\LEM}[1]{\ensuremath{\mathsf{LEM}_{#1}}\xspace}
|
||||||
|
\newcommand{\choice}[1]{\ensuremath{\mathsf{AC}_{#1}}\xspace}
|
||||||
|
|
||||||
|
%%%% MISC %%%%
|
||||||
|
|
||||||
|
\newcommand{\mentalpause}{\medskip} % Use for "mental" pause, instead of \smallskip or \medskip
|
||||||
|
|
||||||
|
%% Use \symlabel instead of \label to mark a pageref that you need in the index of symbols
|
||||||
|
\newcounter{symindex}
|
||||||
|
\newcommand{\symlabel}[1]{\refstepcounter{symindex}\label{#1}}
|
||||||
|
|
||||||
|
% Local Variables:
|
||||||
|
% mode: latex
|
||||||
|
% TeX-master: "hott-online"
|
||||||
|
% End:
|
||||||
640
Notes/notes.tex
Normal file
640
Notes/notes.tex
Normal file
|
|
@ -0,0 +1,640 @@
|
||||||
|
\documentclass{article}
|
||||||
|
|
||||||
|
\input{preamble-articles}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% We define a command \@ifnextcharamong accepting an arbitrary number of
|
||||||
|
%%%% arguments. The first is what it should do if a match is found, the second
|
||||||
|
%%%% contains what it should do when no match is found; all the other arguments
|
||||||
|
%%%% are the things it tries to find as the next character.
|
||||||
|
%%%%
|
||||||
|
%%%% For example \@ifnextcharamong{#1}{#2}{*}{\bgroup} expands #1 if the next
|
||||||
|
%%%% character is a * or a \bgroup and it expands #2 otherwise.
|
||||||
|
|
||||||
|
\makeatletter
|
||||||
|
\newcommand{\@ifnextcharamong}[2]
|
||||||
|
{\@ifnextchar\bgroup{\@@ifnextchar{#1}{\@@ifnextcharamong{#1}{#2}}}{#2}}
|
||||||
|
\newcommand{\@@ifnextchar}[3]{\@ifnextchar{#3}{#1}{#2}}
|
||||||
|
\newcommand{\@@ifnextcharamong}[3]{\@ifnextcharamong{#1}{#2}}
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
\newcommand{\ucomp}[1]{\hat{#1}}
|
||||||
|
\newcommand{\finset}[1]{{[#1]}}
|
||||||
|
|
||||||
|
\makeatletter
|
||||||
|
\newcommand{\higherequifibsf}{\mathcal}
|
||||||
|
\newcommand{\higherequifib}[2]{\higherequifibsf{#1}(#2)}
|
||||||
|
\newcommand{\underlyinggraph}[1]{U(#1)}
|
||||||
|
\newcommand{\theequifib}[1]{{\def\higherequifibsf{}#1}}
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
\newcommand{\loopspace}[2][]{\typefont{\Omega}^{#1}(#2)}
|
||||||
|
\newcommand{\join}[2]{{#1}*{#2}}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
\title{Notes on algebraic topology}
|
||||||
|
\date{\today}
|
||||||
|
|
||||||
|
\begin{document}
|
||||||
|
|
||||||
|
\maketitle
|
||||||
|
|
||||||
|
\tableofcontents
|
||||||
|
|
||||||
|
\part{Spectral sequences}
|
||||||
|
\section{Background}
|
||||||
|
\begin{defn}
|
||||||
|
A graded $R$-module $M$ is an $R$-module which decomposes as a direct
|
||||||
|
sum
|
||||||
|
\begin{equation*}
|
||||||
|
\bigoplus_{p\in\Z} F_p M
|
||||||
|
\end{equation*}
|
||||||
|
of $R$-modules. A graded $R$-homomorphism $h:M\to N$ is an $R$-homomorphism which
|
||||||
|
decomposes into $h_p:F_pM\to F_pN$.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{lem}
|
||||||
|
Suppose $M$ and $N$ are graded $R$-modules. Then $M\otimes N$ is a graded
|
||||||
|
$R$-module by
|
||||||
|
\begin{equation*}
|
||||||
|
(M\otimes_R N)_i\defeq \bigoplus_{p+q=i} F_pM\otimes_R F_qN.
|
||||||
|
\end{equation*}
|
||||||
|
\end{lem}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
A graded algebra is a graded $R$-module $M$ for which there are linear mappings
|
||||||
|
$\varphi_{p,q}:F_pM\otimes_R F_qM\to F_{p+q}M$, i.e.~a graded $R$-homomorphism
|
||||||
|
$\varphi:M\otimes M\to M$, which is associative in the sense
|
||||||
|
that the diagram
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
M\otimes M\otimes M \arrow[r,"\varphi\otimes 1"] \arrow[d,swap,"1\otimes\varphi"] &
|
||||||
|
M\otimes M \arrow[d,"\varphi"] \\ M\otimes M \arrow[r,swap,"\varphi"] & M
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
commutes.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{eg}
|
||||||
|
Polynomials with coefficients in $R$ forms a graded algebra. Moreover, in the
|
||||||
|
polynomial ring $R[X]$, we find that $G_pR[X]\defeq F_pR[X]/F_{p-1}R[X]\cong R$.
|
||||||
|
Since those are free modules, we have that $R[X]\cong \bigoplus_p G_pR[X]$.
|
||||||
|
\end{eg}
|
||||||
|
|
||||||
|
\section{Spectral sequences}
|
||||||
|
|
||||||
|
\subsection{Motivation from the long exact sequence of a pair}
|
||||||
|
|
||||||
|
Recall that a pair of spaces $(X,A)$ induces a long exact sequence of homology
|
||||||
|
groups
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
\cdots \arrow[r,"\partial_{n+1}"]
|
||||||
|
& H_n(A) \arrow[r,"i_n"]
|
||||||
|
& H_n(X) \arrow[r,"j_n"]
|
||||||
|
& H_n(X,A) \arrow[r,"\partial_n"]
|
||||||
|
& H_{n-1}(A) \arrow[r,"i_{n-1}"]
|
||||||
|
& \cdots
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
from the short exact sequence
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
0 \arrow[r] & C_\ast(A) \arrow[r] & C_\ast(X) \arrow[r] & C_\ast(X,A) \arrow[r] & 0
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
of chain complexes, by means of the snake lemma. This long exact sequence helps
|
||||||
|
us to compute $H_n(X)$ in terms of $H_n(A)$ and $H_n(X,A)$, which may be easier
|
||||||
|
to determine. For instance, from the long exact sequence we obtain the short
|
||||||
|
exact sequence
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
0 \arrow[r] & \mathrm{coker}(\partial_{n+1}) \arrow[r] & H_n(X) \arrow[r] & \mathrm{ker}(\partial_n) \arrow[r] & 0
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
and hence we have determined that $H_n(X)$ can be obtained as some element of the
|
||||||
|
group $\mathrm{Ext}(\mathrm{coker}(\partial_{n+1}),\mathrm{ker}(\partial_n))$.
|
||||||
|
In other words, $H_n(X)$ is a particular solution to an extension problem.
|
||||||
|
|
||||||
|
Note also that the long exact sequence of relative homology groups can be
|
||||||
|
presented as an exact triangle of graded $R$-homomorphisms:
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}[column sep=0em]
|
||||||
|
\bigoplus_n H_n(C_\ast(A))
|
||||||
|
\arrow[rr,"i"] & & \bigoplus_n H_n(C_\ast(X)) \arrow[dl,"j"] \\
|
||||||
|
& \bigoplus_n H_n(C_\ast(X,A)) \arrow[ul,"\partial"]
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
|
||||||
|
The first idea of spectral sequences is to generalize the long exact sequence
|
||||||
|
of homology obtained from a pair of spaces, to an algebraic gadget obtained from
|
||||||
|
a filtration on a space, and mimic the derivation of determining the homology
|
||||||
|
group as a solution to an extension problem.
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
A filtration of a space X consists of a sequence
|
||||||
|
\begin{equation*}
|
||||||
|
\cdots\subseteq X_p\subseteq X_{p+1}\subseteq\cdots
|
||||||
|
\end{equation*}
|
||||||
|
such that $X=\bigcup_p X_p$ and $\bigcap_p X_p=\varnothing$. A filtration of $X$ is said to be bounded, if
|
||||||
|
$X_p=\varnothing$ for $p$ sufficiently small, and $X_p=X$ for $X$ sufficiently
|
||||||
|
large.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
An important class of filtered spaces is that of CW-complexes, where the filtration
|
||||||
|
$X_p$ of $X$ is given by the $p$-skeleton of $X$. Another case is where
|
||||||
|
$X_p\defeq\varnothing$ for $p<0$, $X_0\defeq A$ and $X_p\defeq X$ for $p>0$; here
|
||||||
|
we recover the old theory of the topological pair.
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
Given a space $X$ with a filtration, we can form the staircase diagram
|
||||||
|
\begin{footnotesize}
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
& \vdots \arrow[d] & & \vdots \arrow[d] \\
|
||||||
|
\cdots \arrow[r]
|
||||||
|
& H_{n+1}(X_p) \arrow[r] \arrow[d]
|
||||||
|
& H_{n+1}(X_p,X_{p-1}) \arrow[r]
|
||||||
|
& H_n(X_{p-1}) \arrow[r] \arrow[d]
|
||||||
|
& H_n(X_{p-1},X_{p-2}) \arrow[r]
|
||||||
|
& \cdots \\
|
||||||
|
\cdots \arrow[r]
|
||||||
|
& H_{n+1}(X_{p+1}) \arrow[r] \arrow[d]
|
||||||
|
& H_{n+1}(X_{p+1},X_{p}) \arrow[r]
|
||||||
|
& H_n(X_{p}) \arrow[r] \arrow[d]
|
||||||
|
& H_n(X_{p},X_{p-1}) \arrow[r]
|
||||||
|
& \cdots \\
|
||||||
|
& \vdots & & \vdots
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}%
|
||||||
|
\end{footnotesize}%
|
||||||
|
in which the familiar long exact sequence of the pairs $(X_p,X_{p-1})$ run
|
||||||
|
down like a staircase.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
Let $X$ be a space with a filtration. Then we obtain the exact couple
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
A \arrow[rr,"i"] & & A \arrow[dl,"j"] \\
|
||||||
|
& E \arrow[ul,"\partial"]
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
in which $A\defeq\bigoplus_{p,n} H_n(X_p)$, and $E\defeq\bigoplus_{p,n}H_n(X_p,X_{p-1})$.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
We can come to such an exact couple from any filtered chain complex, which is
|
||||||
|
what we turn our attention to before continuing.
|
||||||
|
|
||||||
|
\subsection{The spectral sequence of a filtered complex}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
A filtration of an $R$-module $M$ consists of a sequence
|
||||||
|
\begin{equation*}
|
||||||
|
\cdots\subseteq F_pM\subseteq F_{p+1}M\subseteq\cdots
|
||||||
|
\end{equation*}
|
||||||
|
of $R$-submodules of $M$, such that $M=\bigcup_p F_pM$ and $\bigcap_p F_pM=0$.
|
||||||
|
A filtration of $R$ is said to be bounded if $F_pM=0$ for $p$ sufficiently
|
||||||
|
small and $F_pM=M$ for $p$ sufficiently large.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
Let $\{M,F_pM\}$ be a graded $R$-module. The associated graded module is defined
|
||||||
|
by $G_p M\defeq F_pM/F_{p-1}M$. We obtain a short exact sequence
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
0 \arrow[r] & F_{p-1}M \arrow[r] & F_pM \arrow[r] & G_pM \arrow[r] & 0.
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{rmk}
|
||||||
|
It would be nice if $F_pM\cong F_{p-1}M\oplus G_pM$, so that we can write
|
||||||
|
$M\cong\bigoplus_p G_pM$. Under what condition does this hold? This holds if
|
||||||
|
each $G_pM$ is a projective $R$-module, so under what conditions is this true?
|
||||||
|
\end{rmk}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
A filtered chain complex is a chain complex $(C_\ast,\partial)$ together with a
|
||||||
|
filtration $\{F_pC_i\}$ of each $C_i$, such that the differential preserves the
|
||||||
|
filtration, i.e.~$\partial(F_pC_i)\subseteq F_p C_{i-1}$.
|
||||||
|
|
||||||
|
A filtration of a chain complex is said to be bounded if it is bounded in each
|
||||||
|
dimension.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
Let $(F_pC_\ast,\partial)$ be a filtered chain complex. We have again our
|
||||||
|
short exact sequence
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
0 \arrow[r] & F_{p-1} C_\ast \arrow[r] & F_p C_\ast \arrow[r] & G_p C_\ast \arrow[r] & 0
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
of chain complexes. This also gives us the long exact sequence on homology,
|
||||||
|
which we may express conveniently as the exact couple
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}[column sep=0em]
|
||||||
|
\bigoplus_{p,q} H_{p+q}(F_pC_\ast) \arrow[rr,"i"] & & \bigoplus_{p,q} H_{p+q}(F_pC_\ast) \arrow[dl,"j"] \\
|
||||||
|
& \bigoplus_{p,q} H_{p+q}(G_p C_\ast) \arrow[ul,"k"]
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
consisting of graded $R$-homomorphisms (of which $k$ shifts in degree).
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
Consider an exact couple, i.e.~a commutative triangle
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
A \arrow[rr,"i"] & & A \arrow[dl,"j"] \\ & E \arrow[ul,"k"]
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
of $R$-modules, which is exact at every vertex. Taking $\partial^0\defeq j\circ k$,
|
||||||
|
we see that $(\partial^0)^2=0$ by exactness. We may now form the derived exact couple
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}[column sep=0]
|
||||||
|
\mathrm{im}(i) \arrow[rr,"i'"] & & \mathrm{im}(i) \arrow[dl,"j'"] \\
|
||||||
|
& \frac{\mathrm{ker}(\partial)}{\mathrm{im}(\partial)} \arrow[ul,"k'"]
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
where
|
||||||
|
\begin{align*}
|
||||||
|
i'(i(a)) & \defeq i(i(a)) \\
|
||||||
|
j'(i(a)) & \defeq [j(a)] \\
|
||||||
|
k'([e]) & \defeq k(e)
|
||||||
|
\end{align*}
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{rmk}
|
||||||
|
Since quotients commute with direct sums (both are colimits), it follows that
|
||||||
|
\begin{equation*}
|
||||||
|
E'\defeq \frac{\mathrm{ker}(\partial)}{\mathrm{im}(\partial)}
|
||||||
|
\cong
|
||||||
|
\bigoplus_{p,q} \frac{\mathrm{ker}(\partial^0_{p,q})}{\mathrm{im}(\partial^0_{p,q+1})}
|
||||||
|
\end{equation*}
|
||||||
|
is a graded $R$-module. In other words, $E'$ is a direct sum of the homology
|
||||||
|
groups of the $p$-indexed family of chain complexes
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
\cdots \arrow[r] & E_{p,q}^0 \arrow[r,"{\partial^0_{p,q}}"] & E_{p,q-1}^0 \arrow[r] & \cdots
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
It follows that $i'$, $j'$ and $k'$ are graded
|
||||||
|
whenever $i$, $j$ and $k$ are, where $k'$ shifts down in dimension the same way
|
||||||
|
$k$ does.
|
||||||
|
\end{rmk}
|
||||||
|
|
||||||
|
\begin{comment}
|
||||||
|
\begin{defn}
|
||||||
|
We define
|
||||||
|
\begin{equation*}
|
||||||
|
E_{p,q}^0\defeq G_pC_{p+q}\defeq F_pC_{p+1}/F_{p-1}C_{p+q},
|
||||||
|
\end{equation*}
|
||||||
|
|
||||||
|
Since the differential preserves the filtration, we obtain from the differentials
|
||||||
|
well-defined $R$-homomorphisms functioning as the boundary maps in the chain complex
|
||||||
|
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
The homology groups
|
||||||
|
\begin{equation*}
|
||||||
|
E^1_{p,q}\defeq \mathrm{ker}(\partial^0_{p,q})/\mathrm{im}(\partial^0_{p,q+1})
|
||||||
|
\end{equation*}
|
||||||
|
form again a chain complex, with boundary maps $\partial^1_{p,q}:E^1_{p,q}\to
|
||||||
|
E^1_{p,q-1}$. Thus, this process may be repeated indefinitely.
|
||||||
|
\end{defn}
|
||||||
|
\end{comment}
|
||||||
|
|
||||||
|
\begin{comment}
|
||||||
|
\begin{lem}
|
||||||
|
Let $(C_\ast,\partial)$ be a filtered chain complex. Then there is a filtration
|
||||||
|
on the homology of $C_\ast$, given by
|
||||||
|
\begin{equation*}
|
||||||
|
F_pH_i(C_\ast)\defeq\{\alpha\in H_i(C_\ast)\mid \exists_{(x\in F_p C_i)}\,\alpha=[x]\}.
|
||||||
|
\end{equation*}
|
||||||
|
\end{lem}
|
||||||
|
\end{comment}
|
||||||
|
|
||||||
|
\subsection{Convergent spectral sequences}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
A spectral sequence consists of
|
||||||
|
\begin{enumerate}
|
||||||
|
\item An $R$-module $E^r_{p,q}$ for each $p,q\in\Z$ and each $r\geq 0$.
|
||||||
|
\item Differentials $\partial_r:E^r_{p,q}\to E^r_{p-r,q+r-1}$ such that
|
||||||
|
$\partial_r^2=0$ and $E^{r+1}$ is the homology of $(E^r,\partial_r)$
|
||||||
|
\end{enumerate}
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
A spectral sequence $\{E^r,\partial_r\}$ of $R$-modules is said to converge
|
||||||
|
if for every $p,q\in\Z$, one has $\partial_r=0:E^r_{p,q}\to E^r_{p-r,q+r-1}$
|
||||||
|
for $r$ sufficiently large.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{rmk}
|
||||||
|
If a spectral sequence $\{E^r,\partial_r\}$ converges, then the $R$-module
|
||||||
|
$E^r_{p,q}$ is independent of $r$ for sufficiently large $r$.
|
||||||
|
\end{rmk}
|
||||||
|
|
||||||
|
\begin{thm}
|
||||||
|
Let $(F_pC_\ast,\partial)$ be a filtered complex. Then we obtain a spectral
|
||||||
|
sequence $(E^r_{p,q},\partial^r)$ defined for $r\geq 0$, with
|
||||||
|
\begin{equation*}
|
||||||
|
E^1_{p,q}\defeq H_{p+q}(G_pC_\ast).
|
||||||
|
\end{equation*}
|
||||||
|
This is the spectral sequence of filtered complexes.
|
||||||
|
\end{thm}
|
||||||
|
|
||||||
|
\begin{thm}
|
||||||
|
If $(F_pC_\ast,\partial)$ is a bounded filtered complex, then the spectral
|
||||||
|
sequence converges to
|
||||||
|
\begin{equation*}
|
||||||
|
E^\infty_{p,q}\defeq G_pH_{p+q}(C_\ast).
|
||||||
|
\end{equation*}
|
||||||
|
\end{thm}
|
||||||
|
|
||||||
|
Let $X$ be a filtered space, and let our goal be to compute the $n$-th (co)homology
|
||||||
|
group $H_n(X)$. In general, this might be a complicated task. However, it might
|
||||||
|
be easier to compute the homologies of the subcomplex $C_\ast(X_p)$, and the quotient
|
||||||
|
complex $C_\ast(X)/C_\ast(X_p)$. From this, we obtain a short exact sequence
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
0 \arrow[r]
|
||||||
|
& \mathrm{coker}(\delta) \arrow[r]
|
||||||
|
& H_\ast(X) \arrow[r]
|
||||||
|
& \mathrm{ker}(\delta) \arrow[r]
|
||||||
|
& 0
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
|
||||||
|
\subsection{The Serre spectral sequence}
|
||||||
|
|
||||||
|
The Serre spectral sequence relates the homology of a Serre fibration to the
|
||||||
|
homology of the fibers and the base. Thus, in some cases one can compute the
|
||||||
|
homology of the fibration in terms of the homology of the fibers and the base.
|
||||||
|
|
||||||
|
Let $\pi : X\to B$ be a fibration, with $B$ a path-connected CW-complex, and we
|
||||||
|
filter $X$ by the subspaces $X_p\defeq \pi^{-1}(B_p)$, in which $B_p$ is the
|
||||||
|
$p$-skeleton of $B$.
|
||||||
|
|
||||||
|
\begin{lem}
|
||||||
|
The spectral sequence for homology with coefficients in $G$ associated to this
|
||||||
|
filtration of $X$ converges to $H_\ast(X;G)$.
|
||||||
|
\end{lem}
|
||||||
|
|
||||||
|
\begin{thm}
|
||||||
|
Let $F\to X\to B$ be a fibration with $B$ path-connected. If $\pi_1(B)$ acts
|
||||||
|
trivially on $H_\ast(F;G)$, then there is a spectral sequence $\{E^r_{p,q},\partial_r\}$
|
||||||
|
with:
|
||||||
|
\begin{enumerate}
|
||||||
|
%\item $\partial_r : E^r_{p,q}\to E^r_{p-r,q+r-1}$ and $E^{r+1}_{p,q}=\mathrm{ker}\,d_r/\mathrm{im}\,dr$.
|
||||||
|
\item the stable terms $E^\infty_{p,n-p}$ are isomorphic to $F^p_n/F^{p-1}_n$ in
|
||||||
|
a filtration $0\subseteq F^0_n\subseteq\cdots\subseteq F^n_n=H_n(X;G)$ of ...
|
||||||
|
\item $E^2_{p,q}\cong H_p(B;H_q(F;G))$.
|
||||||
|
\end{enumerate}
|
||||||
|
\end{thm}
|
||||||
|
|
||||||
|
\part{K-theory}
|
||||||
|
|
||||||
|
\section{Vector bundles}
|
||||||
|
|
||||||
|
\subsection{Basic spaces}
|
||||||
|
\begin{defn}
|
||||||
|
The \define{$n$-sphere} $\Sn^n$ is the subspace of $\R^{n+1}$ consisting of unit vectors.
|
||||||
|
The \define{real projective $n$-space} $\R P^n$ is the space of lines in
|
||||||
|
$\R^{n+1}$ through the origin. Equivalently, we may regard $\R P^n$ as the quotient
|
||||||
|
space of $\Sn^n$ in which the antipodal pairs of points are identified. Notice
|
||||||
|
that $\R P^1\approx \Sn^1$.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
For each $n$, we may include the $n$-sphere $\Sn^n$ into $\Sn^{n+1}$ by mapping
|
||||||
|
it into the equator. These inclusions induce inclusions $\R P^n\to \R P^{n+1}$.
|
||||||
|
We define $\R P^\infty$ to be the sequential colimit of $\R P^n$.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\subsection{Definition and basic properties}
|
||||||
|
\begin{defn}
|
||||||
|
An \define{$n$-dimensional vector bundle} is a map $p:E\to B$ together with a
|
||||||
|
real vector space structure on $p^{-1}(b)$ for each $b\in B$, satisfying the
|
||||||
|
\define{local triviality condition}, which says that there is an open cover
|
||||||
|
$\mathcal{C}$ of $B$, with homeomorphisms $h_U:p^{-1}(U)\to U\times\mathbb{R}^n$
|
||||||
|
for each $U\in\mathcal{C}$, which maps $p^{-1}(b)$ to $\{b\}\times\mathbb{R}^n$
|
||||||
|
for each $b\in U$.
|
||||||
|
|
||||||
|
The functions $h_U$ are also called \define{local trivializations}. Given a
|
||||||
|
vector bundle $p:E\to B$, the space $B$ is called the \define{base space}, the
|
||||||
|
space $E$ is called the \define{total space}, and the spaces $p^{-1}(b)$ are
|
||||||
|
called the \define{fibers}. A $1$-dimensional
|
||||||
|
vector bundle is also called a \define{line bundle}.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
An \define{isomorphism of vector bundles} from $p:E\to B$ to $p':E'\to B$
|
||||||
|
consists of a map $h:E\to E'$ satisfying $p'\circ h=p$,
|
||||||
|
which induces a linear isomorphism
|
||||||
|
$p^{-1}(b)\to p'^{-1}(b)$ between each of the fibers.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{lem}
|
||||||
|
If $h:E\to E'$ is an isomorphism of vector bundles, then the underlying map
|
||||||
|
of type $E\to E'$ is a homeomorphism.
|
||||||
|
\end{lem}
|
||||||
|
|
||||||
|
\begin{proof}
|
||||||
|
Suppose $h:E\to E'$ induces isomorphisms $p^{-1}(b)\to p'^{-1}(b)$ for each
|
||||||
|
$b\in B$. Then, for each $x\in E'$ we have an isomorphism from
|
||||||
|
$p^{-1}(p'(x))$ to $p'^{-1}(p'(x))$. Since $x\in p'^{-1}(p'(x))$, we find
|
||||||
|
an element $y\in p^{-1}(p'(x))\subseteq E$. Thus, $h$ is surjective. Now suppose
|
||||||
|
that $x,x'\in E$ are two elements for which $h(x)=h(x')$. Since $p'\circ h=p$,
|
||||||
|
it follows that $x'\in p^{-1}(x)$. Now, the fact that $h$ induces an isomorphism
|
||||||
|
between fibers implies that $x=x'$.
|
||||||
|
|
||||||
|
Thus, $h$ has an inverse function $k:E'\to E$, and we need to show that this
|
||||||
|
function is continuous. It suffices to show that $k|_U$ is continuous for each
|
||||||
|
$U$ on which $p'$ is trivial. Let $x\in B$, and compose the map
|
||||||
|
$h_U:p^{-1}(U)\to p'^{-1}(U)$ with its local trivializations. Thus, we obtain
|
||||||
|
a map $g_U:U\times\R^n\to U\times \R^n$, mapping $(x,y)$ to $(x,A(y))$, where
|
||||||
|
$A$ is a linear isomorphism.
|
||||||
|
\end{proof}
|
||||||
|
|
||||||
|
In the following definition, we give a vector bundle by a gluing construction.
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
Consider a space $B$, and an open cover $\mathcal{C}$ which is closed under
|
||||||
|
finite intersections. Then $\mathcal{C}$ may be considered a poset ordered by
|
||||||
|
inclusion.
|
||||||
|
|
||||||
|
A \define{collection of gluing functions} consists of a continuous choice of linear
|
||||||
|
isomorphisms $g_{U,V}:U\cap V\to GL_n(\R)$ satisfying the \define{cocycle
|
||||||
|
condition}
|
||||||
|
\begin{equation*}
|
||||||
|
g_{V,W}\circ g_{U,V}=g_{U,W}
|
||||||
|
\end{equation*}
|
||||||
|
on $U\cap V\cap W$, for every
|
||||||
|
$U,V,W\in\mathcal{C}$. Such a collection of gluing functions determines a functor
|
||||||
|
$\mathcal{C}\to\mathbf{Top}$, which is given on points by $U\mapsto U\times\R^n$,
|
||||||
|
and on morphisms by $(x,v)\mapsto(x,A(v))$, for each $U\subseteq V$ determining
|
||||||
|
a linear isomorphism $A$.
|
||||||
|
|
||||||
|
The colimit of this functor is the total space of a vector bundle.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{eg}
|
||||||
|
There are lots of examples of vector bundles:
|
||||||
|
\begin{enumerate}
|
||||||
|
\item The \define{$n$-dimensional trivial bundle} over $B$ is defined to be
|
||||||
|
$\proj1:B\times\mathbb{R}^n\to B$. So the trivial bundle is the one which is
|
||||||
|
\emph{globally} trivial. We will write the $n$-dimensional trivial bundle over
|
||||||
|
$B$ as $\epsilon^n\to B$.
|
||||||
|
\item The circle may be regarded as the quotient of $[0,1]$ modulo the end points.
|
||||||
|
The \define{Mobius bundle} is the line bundle over $\Sn^1$ to have total space
|
||||||
|
$E\defeq [0,1]\times\R$, with the identifications $(0,t)\sim(1,-t)$.
|
||||||
|
\item The \define{tangent bundle} of the unit sphere $\Sn^n$, viewed as a subspace of
|
||||||
|
$\R^{n+1}$, is defined to be the subspace $E\defeq\{(x,v)\in\Sn^n\times\R^{n+1}
|
||||||
|
\mid x\perp v\}$ of $\R^{2n+2}$, which projects onto $\Sn^n$.
|
||||||
|
|
||||||
|
The $n$-sphere is covered by $2n+2$ open hemispheres, centering at $\pm e_i$,
|
||||||
|
where $e_i\in\R^{n+1}$ is a basis vector.
|
||||||
|
\item The \define{normal bundle} of the unit sphere $\Sn^n$ is the line bundle
|
||||||
|
with $E$ consisting of pairs $(x,v)\in\Sn^n\times\R^{n+1}$ such that $v=tx$ for
|
||||||
|
some $t\in\R$. \emph{The normal bundle on $\Sn^n$ is isomorphic to the trivial line
|
||||||
|
bundle $\Sn^n\times\R\to\Sn^n$.}
|
||||||
|
\item The \define{canonical line bundle} $p:E\to \R P^n$ has as its total space
|
||||||
|
the subspace $E\subseteq \R P^{n+1}\times\R ^{n+1}$ consisting of pairs
|
||||||
|
$(l,v)$ with $v\in l$. \emph{The M\"obius line bundle is isomorphic to the
|
||||||
|
canonical line bundle on $\Sn^1$.}
|
||||||
|
\item The inclusions $\R P^n\subseteq \R P^{n+1}$ induce inclusions of the
|
||||||
|
canonical line bundles. The sequential colimit of the canonical line bundles
|
||||||
|
produces the canonical line bundle on $\R P^\infty$.
|
||||||
|
\end{enumerate}
|
||||||
|
\end{eg}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
Given two vector bundles $p:E\to B$ and $p':E'\to B$ over the same base space
|
||||||
|
$B$, we obtain a vector bundle $p\oplus p': E\oplus E'\to B$, fitting in the
|
||||||
|
pullback square
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
E\oplus E' \arrow[r] \arrow[d] \arrow[dr,"{p\oplus p'}" description ] & E' \arrow[d,"{p'}"] \\
|
||||||
|
E \arrow[r,swap,"p"] & B
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{eg}
|
||||||
|
\begin{enumerate}
|
||||||
|
\item The direct sum of the tangent and normal bundles on $\Sn^n$ is the trivial
|
||||||
|
bundle $\Sn^n\times\R^{n+1}$.
|
||||||
|
\end{enumerate}
|
||||||
|
\end{eg}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
Let $p:E\to B$ and $p':E'\to B$ be two vector bundles over the same space $B$,
|
||||||
|
and choose an open cover $\mathcal{C}$ such that both $E$ and $E'$ are locally
|
||||||
|
trivial with respect to $\mathcal{C}$. We define $E\otimes E'$ by gluing.
|
||||||
|
|
||||||
|
Then we can define, for each $U,V\in\mathcal{C}$ satisfying $U\subseteq V$, we
|
||||||
|
have linear isomorphisms $g_{U,V}(x):\R^n\to\R^n$ and $g'_{U,V}(x):\R^m\to\R^m$,
|
||||||
|
induced by the local trivializations of $E$ and $E'$ respectively. These give
|
||||||
|
gluing functions $g_{U,V}(x)\otimes g'_{U,V}(x):\R^n\otimes\R^m\to\R^n\otimes\R^m$
|
||||||
|
for each $x\in U$, and these gluing functions satisfy the cocycle condition.
|
||||||
|
|
||||||
|
Thus, we obtain a vector bundle $E\otimes E'$ from these gluing functions.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{lem}
|
||||||
|
The tensor product of vector bundles over a fixed base space is commutative,
|
||||||
|
associative, it has an identity element (the trivial bundle), and it is
|
||||||
|
distributive with respect to direct sum.
|
||||||
|
\end{lem}
|
||||||
|
|
||||||
|
Change of base $f:B'\to B$ turns a vector bundle $E$ over $B$ to a vector
|
||||||
|
bundle $f^\ast(E)$ over $B'$.
|
||||||
|
|
||||||
|
\begin{lem}
|
||||||
|
For any two vector bundles $E$ and $E'$ over $B$, and any $f:B'\to B$, we have
|
||||||
|
natural isomorphisms $f^\ast(E\oplus E')\approx f^\ast(E)\oplus f^\ast(E')$, and
|
||||||
|
$f^\ast(E\otimes E')\approx f^\ast(E)\otimes f^\ast(E')$. Moreover, if $f$
|
||||||
|
is homotopic to $g$, then $f^\ast=g^\ast$.
|
||||||
|
\end{lem}
|
||||||
|
|
||||||
|
\subsection{K-theory}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
Two vector bundles $E\to B$ and $E'\to B$ are callec \define{stably isomorphic},
|
||||||
|
if there is an $n$ for which $E\oplus\epsilon^n\approx E'\oplus\epsilon^n$, and
|
||||||
|
we write $E\approx_s E'$ if $E$ and $E'$ are stably isomorphic. Also,
|
||||||
|
we will define the relation $E\sim E'$ if there are $m$ and $n$ such that
|
||||||
|
$E\oplus\epsilon^m\approx E'\oplus^n$.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
\begin{lem}
|
||||||
|
The direct sum preserves both $\approx_s$ and $\sim$. Moreover, if $B$ is compact,
|
||||||
|
then the set of ${\sim}$-equivalence classes of vector bundles forms an abelian
|
||||||
|
group, called $\tilde{K}(B)$. If $B$ is pointed, then the tensor product turns
|
||||||
|
$\tilde{K}(B)$ into a ring.
|
||||||
|
\end{lem}
|
||||||
|
|
||||||
|
\begin{lem}
|
||||||
|
The direct sum satisfies the cancellation property with respect to $\approx_s$,
|
||||||
|
i.e.~we have that $E\oplus E'\approx_s E\oplus E''$ implies $E'\oplus E''$.
|
||||||
|
Thus, if we define two pairs $(E,F)$ and $(E',F')$ to be equivalent to each
|
||||||
|
other whenever $E\oplus F'=E'\oplus F$, we obtain an abelian group $K(B)$ for
|
||||||
|
any compact space $B$. The tensor product turns $K(B)$ into a ring.
|
||||||
|
\end{lem}
|
||||||
|
|
||||||
|
\begin{lem}
|
||||||
|
We have a ring isomorphism
|
||||||
|
\begin{equation*}
|
||||||
|
K(B)\approx \tilde{K}(B)\oplus\Z.
|
||||||
|
\end{equation*}
|
||||||
|
\end{lem}
|
||||||
|
|
||||||
|
Both $K$ and $\tilde{K}$ are contravariant functors.
|
||||||
|
|
||||||
|
\begin{lem}
|
||||||
|
If $X$ is compact Hausdorff and $A\subseteq X$ is a closed subspace, then the
|
||||||
|
inclusion and quotient maps $A\stackrel{i}{\to}X\stackrel{q}{\to}X/A$ induces
|
||||||
|
an sequence
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}
|
||||||
|
\tilde{K}(X/A) \arrow[r,"q^\ast"] & \tilde{K}(X) \arrow[r,"i^\ast"] & \tilde{K}(A)
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
which is exact at $\tilde{K}(X)$.
|
||||||
|
\end{lem}
|
||||||
|
|
||||||
|
\begin{lem}
|
||||||
|
If $A$ is contractible, the quotient map $q:X\to X/A$ induces a bijection
|
||||||
|
$q^\ast:\mathrm{Vect}^n(X/A)\to\mathrm{Vect}^n(X)$.
|
||||||
|
\end{lem}
|
||||||
|
|
||||||
|
Apparently, this gives a long exact sequence of $\tilde{K}$-groups:
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}[column sep=small]
|
||||||
|
\cdots\arrow[r] & \tilde{K}(\Sn(X)) \arrow[r] & \tilde{K}(\Sn(A)) \arrow[r]
|
||||||
|
& \tilde{K}(X/A) \arrow[r] & \tilde{K}(X) \arrow[r] & \tilde{K}(A).
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
Still considering pointed spaces, we may consider the long exact sequence of the pair $(X\times Y,
|
||||||
|
X\vee Y)$. Recall that $(X\times Y)/(X\vee Y)$ is the smash product
|
||||||
|
$X\wedge Y$, i.e.~the smash product is the pushout of $\unit\leftarrow
|
||||||
|
X\vee Y\rightarrow X\times Y$. The long exact sequence of the pair
|
||||||
|
$(X\times Y,X\vee Y)$ looks as follows:
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{tikzcd}[column sep=.8em]
|
||||||
|
\cdots\arrow[r] & \tilde{K}(\Sn(X\times Y)) \arrow[r] & \tilde{K}(\Sn(X\vee Y)) \arrow[r]
|
||||||
|
& \tilde{K}(X\wedge Y) \arrow[r] & \tilde{K}(X\times Y) \arrow[r] & \tilde{K}(X\vee Y).
|
||||||
|
\end{tikzcd}
|
||||||
|
\end{equation*}
|
||||||
|
|
||||||
|
\subsection{Bott periodicity}
|
||||||
|
|
||||||
|
\begin{defn}
|
||||||
|
We define an \define{external product} $\mu:K(X)\otimes K(Y)\to K(X\times Y)$,
|
||||||
|
by $\mu(a\otimes b)\defeq \proj1^\ast(a)\cdot\proj2^\ast(b)$.
|
||||||
|
\end{defn}
|
||||||
|
|
||||||
|
|
||||||
|
\end{document}
|
||||||
508
Notes/preamble-articles.tex
Normal file
508
Notes/preamble-articles.tex
Normal file
|
|
@ -0,0 +1,508 @@
|
||||||
|
% for type setting urls
|
||||||
|
\usepackage[hyphens]{url} % This package has to be loaded *before* hyperref
|
||||||
|
\usepackage[pagebackref,colorlinks,citecolor=darkgreen,linkcolor=darkgreen,unicode]{hyperref}
|
||||||
|
\usepackage[english]{babel}
|
||||||
|
|
||||||
|
%%% Because Germans have umlauts and Slavs have even stranger ways of mangling letters
|
||||||
|
\usepackage[utf8]{inputenc}
|
||||||
|
|
||||||
|
%%% Multi-Columns for long lists of names
|
||||||
|
\usepackage{multicol}
|
||||||
|
|
||||||
|
%%% Set the fonts
|
||||||
|
\usepackage{mathpazo}
|
||||||
|
\usepackage[scaled=0.95]{helvet}
|
||||||
|
\usepackage{courier}
|
||||||
|
\linespread{1.05} % Palatino looks better with this
|
||||||
|
|
||||||
|
\usepackage{graphicx}
|
||||||
|
\usepackage{comment}
|
||||||
|
|
||||||
|
%\usepackage{wallpaper} % For the background image on the cover page
|
||||||
|
%\usepackage{geometry} % For the cover page
|
||||||
|
\usepackage{fancyhdr} % To set headers and footers
|
||||||
|
|
||||||
|
\usepackage{ifthen}
|
||||||
|
\usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym}
|
||||||
|
\usepackage{enumitem,mathtools,xspace,xcolor}
|
||||||
|
\definecolor{darkgreen}{rgb}{0,0.45,0}
|
||||||
|
\usepackage{aliascnt}
|
||||||
|
\usepackage[capitalize]{cleveref}
|
||||||
|
%\usepackage[all,2cell]{xy}
|
||||||
|
%\UseAllTwocells
|
||||||
|
% \usepackage{natbib}
|
||||||
|
\usepackage{braket} % used for \setof{ ... } macro
|
||||||
|
\usepackage{tikz-cd}
|
||||||
|
\usepackage{tikz}
|
||||||
|
\usetikzlibrary{decorations.pathmorphing}
|
||||||
|
\usepackage[inference]{semantic}
|
||||||
|
\usepackage{booktabs}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%% To include references in TOC we should use this package rather than a hack.
|
||||||
|
\usepackage{tocbibind}
|
||||||
|
%\usepackage{etoolbox} % get \apptocmd
|
||||||
|
%\apptocmd{\thebibliography}{\addcontentsline{toc}{section}{References}}{}{} % tell bibliography to get itself into the table of contents
|
||||||
|
|
||||||
|
|
||||||
|
\begin{comment}
|
||||||
|
%%%% Header and footers
|
||||||
|
\pagestyle{fancyplain}
|
||||||
|
\setlength{\headheight}{15pt}
|
||||||
|
\renewcommand{\chaptermark}[1]{\markboth{\textsc{Chapter \thechapter. #1}}{}}
|
||||||
|
\renewcommand{\sectionmark}[1]{\markright{\textsc{\thesection\ #1}}}
|
||||||
|
\end{comment}
|
||||||
|
|
||||||
|
% TOC depth
|
||||||
|
\setcounter{tocdepth}{2}
|
||||||
|
|
||||||
|
\lhead[\fancyplain{}{{\thepage}}]%
|
||||||
|
{\fancyplain{}{\nouppercase{\rightmark}}}
|
||||||
|
\rhead[\fancyplain{}{\nouppercase{\leftmark}}]%
|
||||||
|
{\fancyplain{}{\thepage}}
|
||||||
|
\cfoot{\textsc{\footnotesize [Draft of \today]}}
|
||||||
|
\lfoot[]{}
|
||||||
|
\rfoot[]{}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% We mostly use the macros of the book, to keep notations
|
||||||
|
%%%% and conventions the same. Recall that when the macros file
|
||||||
|
%%%% is updated, we need to comment the lines containing the
|
||||||
|
%%%% string `[chapter]` since our article is not a book.
|
||||||
|
%%%%
|
||||||
|
%%%% Instructions for updating the macros.tex file:
|
||||||
|
%%%% - fetch the latest macros.tex file from the HoTT/book git repository.
|
||||||
|
%%%% - comment all lines containing "[chapter]" because this is not a book.
|
||||||
|
%%%% - comment the definition of pbcorner because the xypic package is not used.
|
||||||
|
%%%%
|
||||||
|
\input{macros}
|
||||||
|
|
||||||
|
\newcommand{\idsymbin}{=}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% Our commands which are not part of the macros.tex file.
|
||||||
|
%%%% We should keep these commands separate, because we will
|
||||||
|
%%%% update the macros.tex following the updates of the book.
|
||||||
|
|
||||||
|
%%%% First we redefine the \id, \eqv and \ct commands so that they accept an
|
||||||
|
%%%% arbitrary number of arguments. This is useful when writing longer strings
|
||||||
|
%%%% of equalities or equivalences.
|
||||||
|
|
||||||
|
\makeatletter
|
||||||
|
|
||||||
|
\renewcommand{\id}[3][]{
|
||||||
|
\@ifnextchar\bgroup
|
||||||
|
{#2 \mathbin{\idsym_{#1}} \id[#1]{#3}}
|
||||||
|
{#2 \mathbin{\idsym_{#1}} #3}
|
||||||
|
}
|
||||||
|
|
||||||
|
\renewcommand{\eqv}[2]{
|
||||||
|
\@ifnextchar\bgroup
|
||||||
|
{#1 \eqvsym \eqv{#2}}
|
||||||
|
{#1 \eqvsym #2}
|
||||||
|
}
|
||||||
|
|
||||||
|
\newcommand{\ctsym}{%
|
||||||
|
\mathchoice{\mathbin{\raisebox{0.5ex}{$\displaystyle\centerdot$}}}%
|
||||||
|
{\mathbin{\raisebox{0.5ex}{$\centerdot$}}}%
|
||||||
|
{\mathbin{\raisebox{0.25ex}{$\scriptstyle\,\centerdot\,$}}}%
|
||||||
|
{\mathbin{\raisebox{0.1ex}{$\scriptscriptstyle\,\centerdot\,$}}}
|
||||||
|
}
|
||||||
|
|
||||||
|
\renewcommand{\ct}[3][]{
|
||||||
|
\@ifnextchar\bgroup
|
||||||
|
{#2 \mathbin{\ctsym_{#1}} \ct[#1]{#3}}
|
||||||
|
{#2 \mathbin{\ctsym_{#1}} #3}
|
||||||
|
}
|
||||||
|
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
%%%% We always use textstyle products and sums...
|
||||||
|
%\renewcommand{\prd}{\tprd}
|
||||||
|
%\renewcommand{\sm}{\tsm}
|
||||||
|
\makeatletter
|
||||||
|
\renewcommand{\@dprd}{\@tprd}
|
||||||
|
\renewcommand{\@dsm}{\@tsm}
|
||||||
|
\renewcommand{\@dprd@noparens}{\@tprd}
|
||||||
|
\renewcommand{\@dsm@noparens}{\@tsm}
|
||||||
|
|
||||||
|
%%%% ...with a bit more spacing
|
||||||
|
\renewcommand{\@tprd}[1]{\mathchoice{{\textstyle\prod_{(#1)}\,}}{\prod_{(#1)}\,}{\prod_{(#1)}\,}{\prod_{(#1)}\,}}
|
||||||
|
\renewcommand{\@tsm}[1]{\mathchoice{{\textstyle\sum_{(#1)}\,}}{\sum_{(#1)}\,}{\sum_{(#1)}\,}{\sum_{(#1)}\,}}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% We adjust the \prd command so that implicit arguments become possible.
|
||||||
|
%%%%
|
||||||
|
%%%% First, we have the following switch. Set it to true if implicit arguments
|
||||||
|
%%%% are desired, or to false if not. Note turning off implicit arguments
|
||||||
|
%%%% might render some parts of the text harder to comprehend, since in the
|
||||||
|
%%%% text might appear $f(x)$ where we would have $f(i,x)$ without implicit
|
||||||
|
%%%% arguments.
|
||||||
|
|
||||||
|
\newcommand{\implicitargumentson}{\boolean{true}}
|
||||||
|
|
||||||
|
%%%% If one wants to use implicit arguments in the notation for product types,
|
||||||
|
%%%% a * has to be put before the argument that has to be implicit.
|
||||||
|
%%%% For example: in $\prd{x:A}*{y:B}{u:P(y)}Q(x,y,u)$, the argument y is
|
||||||
|
%%%% implicit. Any of the arguments can be made implicit this way.
|
||||||
|
|
||||||
|
%%%% First of all, we should make the command \prd search not only for a
|
||||||
|
%%%% brace, but also for a star. We introduce an auxiliary command that
|
||||||
|
%%%% determines whether the next character is a star or brace.
|
||||||
|
\newcommand{\@ifnextchar@starorbrace}[2]
|
||||||
|
% {\@ifnextcharamong{#1}{#2}{*}{\bgroup};}
|
||||||
|
{\@ifnextchar*{#1}{\@ifnextchar\bgroup{#1}{#2}}}
|
||||||
|
|
||||||
|
%%%% When encountering the \prd command, latex should determine whether it
|
||||||
|
%%%% should print implicit argument brackets or not. So the first branching
|
||||||
|
%%%% happens right here.
|
||||||
|
\renewcommand{\prd}{\@ifnextchar*{\@iprd}{\@prd}}
|
||||||
|
|
||||||
|
\newcommand{\@prd}[1]
|
||||||
|
{\@ifnextchar@starorbrace
|
||||||
|
{\prd@parens{#1}}
|
||||||
|
{\@ifnextchar\sm{\prd@parens{#1}\@eatsm}{\prd@noparens{#1}}}}
|
||||||
|
\newcommand{\@prd@parens}{\@ifnextchar*{\@iprd}{\prd@parens}}
|
||||||
|
\renewcommand{\prd@parens}[1]
|
||||||
|
{\@ifnextchar@starorbrace
|
||||||
|
{\@theprd{#1}\@prd@parens}
|
||||||
|
{\@ifnextchar\sm{\@theprd{#1}\@eatsm}{\@theprd{#1}}}}
|
||||||
|
\newcommand{\@theprd}[1]
|
||||||
|
{\mathchoice{\@dprd{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}}
|
||||||
|
\renewcommand{\dprd}[1]{\@dprd{#1}\@ifnextchar@starorbrace{\dprd}{}}
|
||||||
|
\renewcommand{\tprd}[1]{\@tprd{#1}\@ifnextchar@starorbrace{\tprd}{}}
|
||||||
|
|
||||||
|
%%%% Here we tell the actual symbols to be printed.
|
||||||
|
\newcommand{\@theiprd}[1]{\mathchoice{\@diprd{#1}}{\@tiprd{#1}}{\@tiprd{#1}}{\@tiprd{#1}}}
|
||||||
|
\newcommand{\@iprd}[2]{\@ifnextchar@starorbrace%
|
||||||
|
{\@theiprd{#2}\@prd@parens}%
|
||||||
|
{\@ifnextchar\sm%
|
||||||
|
{\@theiprd{#2}\@eatsm}%
|
||||||
|
{\@theiprd{#2}}}}
|
||||||
|
\def\@tiprd#1{
|
||||||
|
\ifthenelse{\implicitargumentson}
|
||||||
|
{\@@tiprd{#1}\@ifnextchar\bgroup{\@tiprd}{}}
|
||||||
|
{\@tprd{#1}}}
|
||||||
|
\def\@@tiprd#1{\mathchoice{{\textstyle\prod_{\{#1\}}\,}}{\prod_{\{#1\}}\,}{\prod_{\{#1\}}\,}{\prod_{\{#1\}}\,}}
|
||||||
|
\def\@diprd{
|
||||||
|
\ifthenelse{\implicitargumentson}
|
||||||
|
{\@tiprd}
|
||||||
|
{\@tprd}}
|
||||||
|
|
||||||
|
|
||||||
|
%%%% And finally we need to redefine \@eatprd so that implicit arguments also
|
||||||
|
%%%% works in the scope of a dependent sum.
|
||||||
|
\def\@eatprd\prd{\@prd@parens}
|
||||||
|
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% Redefining the quantifiers, so that some of the longer
|
||||||
|
%%%% formulas appear one a single line without problems
|
||||||
|
|
||||||
|
%%% Dependent products written with \forall, in the same style
|
||||||
|
\makeatletter
|
||||||
|
\def\tfall#1{\forall_{(#1)}\@ifnextchar\bgroup{\,\tfall}{\,}}
|
||||||
|
\renewcommand{\fall}{\tfall}
|
||||||
|
|
||||||
|
%%% Existential quantifier %%%
|
||||||
|
\def\texis#1{\exists_{(#1)}\@ifnextchar\bgroup{\,\texis}{\,}}
|
||||||
|
\renewcommand{\exis}{\texis}
|
||||||
|
|
||||||
|
%%% Unique existence %%%
|
||||||
|
\def\uexis#1{\exists!_{(#1)}\@ifnextchar\bgroup{\,\uexis}{\,}}
|
||||||
|
\makeatother
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
|
||||||
|
%%%% Introducing logical usage of fonts.
|
||||||
|
\newcommand{\modelfont}{\mathit} % use 'mf' in command to indicate model font
|
||||||
|
\newcommand{\typefont}{\mathsf} % use 'tf' in command to indicate type font
|
||||||
|
\newcommand{\catfont}{\mathrm} % use 'cf' in command to indicate cat font
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% Some macros of the book are redefined.
|
||||||
|
|
||||||
|
\renewcommand{\UU}{\typefont{U}}
|
||||||
|
\renewcommand{\isequiv}{\typefont{isEquiv}}
|
||||||
|
\renewcommand{\happly}{\typefont{hApply}}
|
||||||
|
\renewcommand{\pairr}[1]{{\mathopen{}\langle #1\rangle\mathclose{}}}
|
||||||
|
\renewcommand{\type}{\typefont{Type}}
|
||||||
|
\renewcommand{\op}[1]{{{#1}^\typefont{op}}}
|
||||||
|
\renewcommand{\susp}{\typefont{\Sigma}}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% The following is a big unorganized list of new macros that we use in the
|
||||||
|
%%%% notes.
|
||||||
|
|
||||||
|
\newcommand{\mfM}{\modelfont{M}}
|
||||||
|
\newcommand{\mfN}{\modelfont{N}}
|
||||||
|
\newcommand{\tfctx}{\typefont{ctx}}
|
||||||
|
\newcommand{\mftypfunc}[1]{{\modelfont{typ}^{#1}}}
|
||||||
|
\newcommand{\mftyp}[2]{{\mftypfunc{#1}(#2)}}
|
||||||
|
\newcommand{\tftypfunc}[1]{{\typefont{typ}^{#1}}}
|
||||||
|
\newcommand{\tftyp}[2]{{\tftypfunc{#1}(#2)}}
|
||||||
|
\newcommand{\hfibfunc}[1]{\typefont{fib}_{#1}}
|
||||||
|
\newcommand{\mappingcone}[1]{\mathcal{C}_{#1}}
|
||||||
|
\newcommand{\equifib}{\typefont{equiFib}}
|
||||||
|
\newcommand{\tfcolim}{\typefont{colim}}
|
||||||
|
\newcommand{\tflim}{\typefont{lim}}
|
||||||
|
\newcommand{\tfdiag}{\typefont{diag}}
|
||||||
|
\newcommand{\tfGraph}{\typefont{Graph}}
|
||||||
|
\newcommand{\mfGraph}{\modelfont{Graph}}
|
||||||
|
\newcommand{\unitGraph}{\unit^\mfGraph}
|
||||||
|
\newcommand{\UUGraph}{\UU^\mfGraph}
|
||||||
|
\newcommand{\tfrGraph}{\typefont{rGraph}}
|
||||||
|
\newcommand{\mfrGraph}{\modelfont{rGraph}}
|
||||||
|
\newcommand{\isfunction}{\typefont{isFunction}}
|
||||||
|
\newcommand{\tfconst}{\typefont{const}}
|
||||||
|
\newcommand{\conemap}{\typefont{coneMap}}
|
||||||
|
\newcommand{\coconemap}{\typefont{coconeMap}}
|
||||||
|
\newcommand{\tflimits}{\typefont{limits}}
|
||||||
|
\newcommand{\tfcolimits}{\typefont{colimits}}
|
||||||
|
\newcommand{\islimiting}{\typefont{isLimiting}}
|
||||||
|
\newcommand{\iscolimiting}{\typefont{isColimiting}}
|
||||||
|
\newcommand{\islimit}{\typefont{isLimit}}
|
||||||
|
\newcommand{\iscolimit}{\typefont{iscolimit}}
|
||||||
|
\newcommand{\pbcone}{\typefont{cone_{pb}}}
|
||||||
|
\newcommand{\tfinj}{\typefont{inj}}
|
||||||
|
\newcommand{\tfsurj}{\typefont{surj}}
|
||||||
|
\newcommand{\tfepi}{\typefont{epi}}
|
||||||
|
\newcommand{\tftop}{\typefont{top}}
|
||||||
|
\newcommand{\sbrck}[1]{\Vert #1\Vert}
|
||||||
|
\newcommand{\strunc}[2]{\Vert #2\Vert_{#1}}
|
||||||
|
\newcommand{\gobjclass}{{\typefont{U}^\mfGraph}}
|
||||||
|
\newcommand{\gcharmap}{\typefont{fib}}
|
||||||
|
\newcommand{\diagclass}{\typefont{T}}
|
||||||
|
\newcommand{\opdiagclass}{\op{\diagclass}}
|
||||||
|
\newcommand{\equifibclass}{\diagclass^{\eqv{}{}}}
|
||||||
|
\newcommand{\universe}{\typefont{U}}
|
||||||
|
\newcommand{\catid}[1]{{\catfont{id}_{#1}}}
|
||||||
|
\newcommand{\isleftfib}{\typefont{isLeftFib}}
|
||||||
|
\newcommand{\isrightfib}{\typefont{isRightFib}}
|
||||||
|
\newcommand{\leftLiftings}{\typefont{leftLiftings}}
|
||||||
|
\newcommand{\rightLiftings}{\typefont{rightLiftings}}
|
||||||
|
\newcommand{\psh}{\typefont{Psh}}
|
||||||
|
\newcommand{\rgclass}{\typefont{\Omega^{RG}}}
|
||||||
|
\newcommand{\terms}[2][]{\lfloor #2 \rfloor^{#1}}
|
||||||
|
\newcommand{\grconstr}[2]
|
||||||
|
{\mathchoice % max size is textstyle size.
|
||||||
|
{{\textstyle \int_{#1}}#2}%
|
||||||
|
{\int_{#1}#2}%
|
||||||
|
{\int_{#1}#2}%
|
||||||
|
{\int_{#1}#2}}
|
||||||
|
\newcommand{\ctxhom}[3][]{\typefont{hom}_{#1}(#2,#3)}
|
||||||
|
\newcommand{\graphcharmapfunc}[1]{\gcharmap_{#1}}
|
||||||
|
\newcommand{\graphcharmap}[2][]{\graphcharmapfunc{#1}(#2)}
|
||||||
|
\newcommand{\tfexp}[1]{\typefont{exp}_{#1}}
|
||||||
|
\newcommand{\tffamfunc}{\typefont{fam}}
|
||||||
|
\newcommand{\tffam}[1]{\tffamfunc(#1)}
|
||||||
|
\newcommand{\tfev}{\typefont{ev}}
|
||||||
|
\newcommand{\tfcomp}{\typefont{comp}}
|
||||||
|
\newcommand{\isDec}[1]{\typefont{isDecidable}(#1)}
|
||||||
|
\newcommand{\smal}{\mathcal{S}}
|
||||||
|
\renewcommand{\modal}{{\ensuremath{\ocircle}}}
|
||||||
|
\newcommand{\eqrel}{\typefont{EqRel}}
|
||||||
|
\newcommand{\piw}{\ensuremath{\Pi\typefont{W}}} %% to be used in conjunction with -pretopos.
|
||||||
|
\renewcommand{\sslash}{/\!\!/}
|
||||||
|
\newcommand{\mprd}[2]{\Pi(#1,#2)}
|
||||||
|
\newcommand{\msm}[2]{\Sigma(#1,#2)}
|
||||||
|
\newcommand{\midt}[1]{\idvartype_#1}
|
||||||
|
\newcommand{\reflf}[1]{\typefont{refl}^{#1}}
|
||||||
|
\newcommand{\tfJ}{\typefont{J}}
|
||||||
|
\newcommand{\tftrans}{\typefont{trans}}
|
||||||
|
|
||||||
|
\newcommand{\tfT}{\typefont{T}}
|
||||||
|
\newcommand{\reflsym}{{\mathsf{refl}}}
|
||||||
|
\newcommand{\strans}[2]{\ensuremath{{#1}_{*}({#2})}}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% JUDGMENTS
|
||||||
|
%%%%
|
||||||
|
%%%% Below we define several commands for the judgments of type theory. There
|
||||||
|
%%%% are commands
|
||||||
|
%%%% * \jctx for the judgment that something is a context.
|
||||||
|
%%%% * \jctxeq for the judgment that two contexts are the same
|
||||||
|
%%%% * \jtype for the judgment that something is a type in a context
|
||||||
|
%%%% * \jtypeeq for the judgment that two types in the same context are the same
|
||||||
|
%%%% * \jterm for the judgment that something is a term of a type in a context
|
||||||
|
%%%% * \jtermeq for the judgment that two terms of the same type are the same
|
||||||
|
|
||||||
|
\makeatletter
|
||||||
|
\newcommand{\jctx}{\@ifnextchar*{\@jctxAlignTrue}{\@jctxAlignFalse}}
|
||||||
|
\newcommand{\@jctxAlignTrue}[2]{& \vdash #2~ctx}
|
||||||
|
\newcommand{\@jctxAlignFalse}[1]{\vdash #1~ctx}
|
||||||
|
|
||||||
|
\newcommand{\jtype}{\@ifnextchar*{\@jtypeAlignTrue}{\@jtypeAlignFalse}}
|
||||||
|
\newcommand{\@jtypeAlignFalse}[2]{#1\vdash #2~type}
|
||||||
|
\newcommand{\@jtypeAlignTrue}[3]{#2 & \vdash #3~type}
|
||||||
|
|
||||||
|
\newcommand{\jtermc}{\@ifnextchar*{\@jtermcAlignTrue}{\@jtermcAlignFalse}}
|
||||||
|
\newcommand{\@jtermcAlignTrue}[3]{ & \vdash #3:#2}
|
||||||
|
\newcommand{\@jtermcAlignFalse}[2]{\vdash #2:#1}
|
||||||
|
|
||||||
|
\newcommand{\jtermt}{\@ifnextchar*{\@jtermtAlignTrue}{\@jtermtAlignFalse}}
|
||||||
|
\newcommand{\@jtermtAlignTrue}[4]{#2 & \vdash #4:#3}
|
||||||
|
\newcommand{\@jtermtAlignFalse}[3]{#1 \vdash #3:#2}
|
||||||
|
|
||||||
|
\newcommand{\jctxeq}{\@ifnextchar*{\@jctxeqAlignTrue}{\@jctxeqAlignFalse}}
|
||||||
|
\newcommand{\@jctxeqAlignTrue}[3]{& \vdash #2\jdeq #3~ctx}
|
||||||
|
\newcommand{\@jctxeqAlignFalse}[2]{\vdash #1\jdeq #2~ctx}
|
||||||
|
|
||||||
|
\newcommand{\jtypeeq}{\@ifnextchar*{\@jtypeeqAlignTrue}{\@jtypeeqAlignFalse}}
|
||||||
|
\newcommand{\@jtypeeqAlignTrue}[4]{#2 & \vdash #3\jdeq #4~type}
|
||||||
|
\newcommand{\@jtypeeqAlignFalse}[3]{#1\vdash #2\jdeq #3~type}
|
||||||
|
|
||||||
|
\newcommand{\jtermceq}{\@ifnextchar*{\@jtermceqAlignTrue}{\@jtermceqAlignFalse}}
|
||||||
|
\newcommand{\@jtermceqAlignTrue}[4]{& \vdash #3\jdeq #4:#2}
|
||||||
|
\newcommand{\@jtermceqAlignFalse}[3]{\vdash #2\jdeq #3:#1}
|
||||||
|
|
||||||
|
\newcommand{\jtermteq}{\@ifnextchar*{\@jtermteqAlignTrue}{\@jtermteqAlignFalse}}
|
||||||
|
\newcommand{\@jtermteqAlignTrue}[5]{#2 & \vdash #4\jdeq #5:#3}
|
||||||
|
\newcommand{\@jtermteqAlignFalse}[4]{#1\vdash #3\jdeq #4:#2}
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% Often we shall need to display lists of inference rules. This environment
|
||||||
|
%%%% adjusts the array environment so that there is enough vertical space
|
||||||
|
%%%% between two inference rules
|
||||||
|
%%%%
|
||||||
|
%%%% bug: there's two much space above the array.
|
||||||
|
|
||||||
|
\newenvironment{infarray}[1]{\begingroup\renewcommand*{\arraystretch}{3}
|
||||||
|
\begin{equation*}
|
||||||
|
\begin{array}{#1}}{
|
||||||
|
\end{array}
|
||||||
|
\end{equation*}
|
||||||
|
\endgroup}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% CONTEXT EXTENSION
|
||||||
|
%%%%
|
||||||
|
%%%% explicit context extension notation which we will use only rarely
|
||||||
|
|
||||||
|
\newcommand{\tfext}{\typefont{ext}}
|
||||||
|
|
||||||
|
%%%% The context extension command.
|
||||||
|
%%%%
|
||||||
|
%%%% To get a feeling of how the command works, here are a few examples.
|
||||||
|
%%%% \ctxext{A}{B} will print A.B
|
||||||
|
%%%% \ctxext{{A}{B}}{C} will print (A.B).C
|
||||||
|
%%%% \ctxext{{{A}{B}}{C}}{{D}{E}} will print ((A.B).C).(D.E)
|
||||||
|
|
||||||
|
\makeatletter
|
||||||
|
\newcommand{\ctxext}[2]{\@ctxext@ctx #1.\@ctxext@type #2}
|
||||||
|
\newcommand{\@ctxext}{\@ifnextchar\bgroup{\@@ctxext}{}}
|
||||||
|
\newcommand{\@ctxext@ctx}{\@ifnextchar\ctxext{\@ctxext@nested}{\@ifnextchar\ctxwk{\@ctxwk@nested}{\@ctxext}}}
|
||||||
|
\newcommand{\@ctxext@type}{\@ifnextchar\ctxext{\@ctxext@nested}{\@ifnextchar\subst{\@subst@nested}{\@ctxext}}}
|
||||||
|
\newcommand{\@@ctxext}[1]{\@ifnextchar\bgroup{\@ctxext@parens{#1}}{#1}}
|
||||||
|
\newcommand{\@ctxext@parens}[2]{(\ctxext{#1}{#2})}
|
||||||
|
\newcommand{\@ctxext@nested}[3]{\@ctxext@parens{#2}{#3}}
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% SUBSTITUTION
|
||||||
|
|
||||||
|
\newcommand{\tfsubst}{\typefont{subst}}
|
||||||
|
|
||||||
|
%%%% The substitution command will act the following way
|
||||||
|
%%%%
|
||||||
|
%%%% \subst{x}{P} will print P[x]
|
||||||
|
%%%% \subst{x}{{f}{Q}} will print Q[f][x]
|
||||||
|
%%%% \subst{{x}{f}}{{x}{Q}} will print Q[x][f[x]]
|
||||||
|
|
||||||
|
\makeatletter
|
||||||
|
\newcommand{\subst}[2]{\@subst@type #2[\@subst@term #1]}
|
||||||
|
\newcommand{\@subst}{\@ifnextchar\bgroup{\@@subst}{}}
|
||||||
|
\newcommand{\@@subst}[1]{\@ifnextchar\bgroup{\subst{#1}}{#1}}
|
||||||
|
\newcommand{\@subst@term}{\@subst}
|
||||||
|
\newcommand{\@subst@type}{\@ifnextchar\ctxext{\@ctxext@nested}{\@ifnextchar\ctxwk{\@ctxwk@nested}{\@subst}}}
|
||||||
|
\newcommand{\@subst@nested}[3]{\@subst@parens{#2}{#3}}
|
||||||
|
\newcommand{\@subst@parens}[2]{(\subst{#1}{#2})}
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% WEAKENING
|
||||||
|
|
||||||
|
\newcommand{\tfwk}{\typefont{wk}}
|
||||||
|
|
||||||
|
%%%% The weakening command is very much like the substitution command.
|
||||||
|
|
||||||
|
\makeatletter
|
||||||
|
\newcommand{\ctxwk}[2]{\langle\@ctxwk@act #1\rangle\@ctxwk@pass #2}
|
||||||
|
\newcommand{\@ctxwk}{\@ifnextchar\bgroup{\@@ctxwk}{}}
|
||||||
|
\newcommand{\@@ctxwk}[1]{\@ifnextchar\bgroup{\ctxwk{#1}}{#1}}
|
||||||
|
\newcommand{\@ctxwk@act}{\@ctxwk}
|
||||||
|
\newcommand{\@ctxwk@pass}{\@ifnextchar\ctxext{\@ctxext@nested}{\@ifnextchar\subst{\@subst@nested}{\@ctxwk}}}
|
||||||
|
\newcommand{\@ctxwk@parens}[2]{(\ctxwk{#1}{#2})}
|
||||||
|
\newcommand{\@ctxwk@nested}[3]{\@ctxwk@parens{#2}{#3}}
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% When investigation pointed structures we use the \pt macro.
|
||||||
|
|
||||||
|
\makeatletter
|
||||||
|
\newcommand{\pt}[1][]{*_{
|
||||||
|
\@ifnextchar\undergraph{\@undergraph@nested}
|
||||||
|
{\@ifnextchar\underovergraph{\@underovergraph@nested}{}}#1}}
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% OPERATIONS ON GRAPHS
|
||||||
|
%%%%
|
||||||
|
%%%% First of all, each graph has a type of vertices and a type of edges. The
|
||||||
|
%%%% type of vertices of a graph $\Gamma$ is denoted by $\pts{\Gamma}$;
|
||||||
|
%%%% and likewise for the type of edges.
|
||||||
|
|
||||||
|
\makeatletter
|
||||||
|
\newcommand{\pts}[1]{{\@graphop@nested{#1}}_{0}}
|
||||||
|
\newcommand{\edg}[1]{{\@graphop@nested{#1}}_{1}}
|
||||||
|
\newcommand{\@graphop@nested}[1]
|
||||||
|
{\@ifnextchar\ctxext{\@ctxext@nested}
|
||||||
|
{\@ifnextchar\undergraph{\@undergraph@nested}
|
||||||
|
{\@ifnextchar\underovergraph{\@underovergraph@nested}{}}}
|
||||||
|
#1}
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
%%%% The following operations of \undergraph and \underovergraph are used to
|
||||||
|
%%%% define the free category and the free groupoid of a graph, respectively
|
||||||
|
|
||||||
|
\makeatletter
|
||||||
|
\newcommand{\@undergraphtest}[2]{\@ifnextchar({#1}{#2}}
|
||||||
|
\newcommand{\undergraph}[2]{\@undergraphtest{\@undergraph@parens{#1}{#2}}{\@undergraph{#1}{#2}}}
|
||||||
|
\newcommand{\@undergraph}[2]{{#2/#1}}
|
||||||
|
\newcommand{\@undergraph@nested}[3]{\@undergraph@parens{#2}{#3}}
|
||||||
|
\newcommand{\@undergraph@parens}[2]{(\@undergraph{#1}{#2})}
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
\makeatletter
|
||||||
|
\newcommand{\underovergraph}[2]{\@underovergraphtest{\@underovergraph@parens{#1}{#2}}{\@underovergraph{#1}{#2}}}
|
||||||
|
\newcommand{\@underovergraph}[2]{{#2}\,{\parallel}\,{#1}}
|
||||||
|
\newcommand{\@underovergraphtest}{\@undergraphtest}
|
||||||
|
\newcommand{\@underovergraph@parens}[2]{(\@underovergraph{#1}{#2})}
|
||||||
|
\newcommand{\@underovergraph@nested}[3]{\@underovergraph@parens{#2}{#3}}
|
||||||
|
\makeatother
|
||||||
|
|
||||||
|
\newcommand{\graphid}[1]{\mathrm{id}_{#1}}
|
||||||
|
\newcommand{\freecat}[1]{\mathcal{C}(#1)}
|
||||||
|
\newcommand{\freegrpd}[1]{\mathcal{G}(#1)}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%% Some tikz macros to typeset diagrams uniformly.
|
||||||
|
|
||||||
|
\tikzset{patharrow/.style={double,double equal sign distance,-,font=\scriptsize}}
|
||||||
|
\tikzset{description/.style={fill=white,inner sep=2pt}}
|
||||||
|
|
||||||
|
%% Used for extra wide diagrams, e.g. when the label is too large otherwise.
|
||||||
|
\tikzset{commutative diagrams/column sep/Huge/.initial=18ex}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% New theorem environment for conjectures.
|
||||||
|
|
||||||
|
\defthm{conj}{Conjecture}{Conjectures}
|
||||||
|
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||||
|
%%%% The following environment for desiderata should not be there. It is better
|
||||||
|
%%%% to use the issue tracker for desiderata.
|
||||||
|
|
||||||
|
\newenvironment{desiderata}{\begingroup\color{blue}\textbf{Desiderata.}}
|
||||||
|
{\endgroup}
|
||||||
Loading…
Reference in a new issue