-
Notifications
You must be signed in to change notification settings - Fork 3
/
notes.tex
15290 lines (13425 loc) · 779 KB
/
notes.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\documentclass[10pt,reqno,a4paper]{amsbook}
\usepackage{etex}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{etoolbox,chngcntr}
\usepackage{amsmath,amsthm,amssymb,array,stmaryrd,color,graphicx,mathtools,multirow,setspace}
\usepackage{soul}\setul{0.3ex}{}
\usepackage{bussproofs}
\usepackage{xspace}
\usepackage{longtable}
\usepackage{booktabs}
\usepackage[protrusion=true,expansion=true]{microtype}
\usepackage[bookmarksdepth=2,pdfencoding=auto]{hyperref}
%\addtolength{\oddsidemargin}{7mm}
%\addtolength{\evensidemargin}{-7mm}
% Hack to load extpfeil from https://tex.stackexchange.com/a/297109/32372
\expandafter\def\csname [email protected]\endcsname
{only,shortleftarrow,shortrightarrow}
\usepackage{extpfeil}
\newextarrow{\xbigtoto}{{20}{20}{20}{20}}
{\bigRelbar\bigRelbar{\bigtwoarrowsleft\rightarrow\rightarrow}}
\usepackage[all]{xy}
\usepackage{tikz}
\usetikzlibrary{calc,shapes.callouts,shapes.arrows,matrix,patterns}
\newcommand{\hcancel}[5]{%
\tikz[baseline=(tocancel.base)]{
\node[inner sep=0pt,outer sep=0pt] (tocancel) {#1};
\draw[red, line width=0.3mm] ($(tocancel.south west)+(#2,#3)$) -- ($(tocancel.north east)+(#4,#5)$);
}%
}
\usepackage[natbib=true,style=numeric,maxnames=10]{biblatex}
\usepackage[babel]{csquotes}
\bibliography{bibliography}
\theoremstyle{definition}
\newtheorem{defn}{Definition}[section]
\newtheorem{ex}[defn]{Example}
\theoremstyle{plain}
\newtheorem{prop}[defn]{Proposition}
\newtheorem{cor}[defn]{Corollary}
\newtheorem{lemma}[defn]{Lemma}
\newtheorem{thm}[defn]{Theorem}
\newtheorem{scholium}[defn]{Scholium}
\theoremstyle{remark}
\newtheorem{rem}[defn]{Remark}
\newtheorem{question}[defn]{Question}
\newtheorem{speculation}[defn]{Speculation}
\newtheorem{caveat}[defn]{Caveat}
\newtheorem{conjecture}[defn]{Conjecture}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\FF}{\mathbb{F}}
\renewcommand{\AA}{\mathbb{A}}
\newcommand{\A}{\mathcal{A}}
\newcommand{\B}{\mathcal{B}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\G}{\mathcal{G}}
\let\acuteH\H
\newcommand{\konig}{K\acuteH onig}
\renewcommand{\H}{\mathcal{H}}
\renewcommand{\O}{\mathcal{O}}
\newcommand{\K}{\mathcal{K}}
\newcommand{\N}{\mathcal{N}}
\newcommand{\M}{\mathcal{M}}
\renewcommand{\L}{\mathcal{L}}
\renewcommand{\P}{\mathcal{P}}
\newcommand{\R}{\mathcal{R}}
\newcommand{\T}{\mathcal{T}}
\newcommand{\I}{\mathcal{I}}
\newcommand{\J}{\mathcal{J}}
\renewcommand{\S}{\mathcal{S}}
\newcommand{\U}{\mathcal{U}}
\newcommand{\V}{\mathcal{V}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\PP}{\mathbb{P}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\CC}{\mathbb{C}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\GG}{\mathbb{G}}
\newcommand{\TT}{\mathbb{T}}
\newcommand{\aaa}{\mathfrak{a}}
\newcommand{\bbb}{\mathfrak{b}}
\newcommand{\ccc}{\mathfrak{c}}
\newcommand{\ppp}{\mathfrak{p}}
\newcommand{\qqq}{\mathfrak{q}}
\newcommand{\mmm}{\mathfrak{m}}
\newcommand{\nnn}{\mathfrak{n}}
\newcommand{\Hom}{\mathrm{Hom}}
\newcommand{\HOM}{\mathcal{H}\mathrm{om}}
\newcommand{\EXT}{\mathcal{E}\mathrm{xt}}
\newcommand{\TOR}{\mathcal{T}\mathrm{or}}
\newcommand{\Ind}{\mathrm{Ind}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\GL}{\mathrm{GL}}
\newcommand{\placeholder}{\underline{\quad}}
\let\oldul\ul
\renewcommand{\ul}[1]{\text{\oldul{$#1$}}}
\newcommand{\Set}{\mathrm{Set}}
\newcommand{\Grp}{\mathrm{Grp}}
\newcommand{\Vect}{\mathrm{Vect}}
\newcommand{\Sh}{\mathrm{Sh}}
\newcommand{\PSh}{\mathrm{PSh}}
\newcommand{\Zar}{\mathrm{Zar}}
\newcommand{\Et}{\mathrm{\acute{E}t}}
\newcommand{\fppf}{\mathrm{fppf}}
\newcommand{\ph}{\mathrm{ph}}
\newcommand{\surj}{\mathrm{surj}}
\newcommand{\Sch}{\mathrm{Sch}}
\newcommand{\Aff}{\mathrm{Aff}}
\newcommand{\Mod}{\mathrm{Mod}}
\newcommand{\Alg}{\mathrm{Alg}}
\newcommand{\Ring}{\mathrm{Ring}}
\newcommand{\LocRing}{\mathrm{LocRing}}
\newcommand{\RL}{\mathrm{RL}}
\newcommand{\LRL}{\mathrm{LRL}}
\newcommand{\LRS}{\mathrm{LRS}}
\newcommand{\LRT}{\mathrm{LRT}}
\newcommand{\RT}{\mathrm{RT}}
\newcommand{\pt}{\mathrm{pt}}
\newcommand{\tors}{\mathrm{tors}}
\newcommand{\lfp}{\mathrm{lfp}}
\newcommand{\fp}{\mathrm{fp}}
\DeclareMathOperator{\Spec}{Spec}
\DeclareMathOperator{\Proj}{Proj}
\newcommand{\QcohSpec}[2]{\mathrm{Spec}^{\mathrm{qcoh}}_{#1}{#2}}
\newcommand{\RelSpec}{\operatorname{\ul{\mathrm{Spec}}}}
\newcommand{\RelProj}{\operatorname{\ul{\mathrm{Proj}}}}
\newcommand{\op}{\mathrm{op}}
\DeclareMathOperator*{\colim}{colim}
\DeclareMathOperator{\rank}{rank}
\DeclareMathOperator{\Ann}{Ann}
\DeclareMathOperator{\Int}{int}
\DeclareMathOperator{\Clos}{cl}
\DeclareMathOperator{\Kernel}{ker}
\DeclareMathOperator{\cok}{cok}
\DeclareMathOperator{\im}{im}
\DeclareMathOperator{\supp}{supp}
\newcommand{\Ass}{\mathrm{Ass}}
\newcommand{\Sym}{\mathrm{Sym}}
\newcommand{\Gr}{\mathrm{Gr}}
\newcommand{\Open}{\T}
\newcommand{\?}{\,{:}\,}
\newcommand{\hg}{\mathbin{:}} % homogeneous coordinates
\renewcommand{\_}{\mathpunct{.}\,}
\newcommand{\speak}[1]{\ulcorner\text{\textnormal{#1}}\urcorner}
\newcommand{\Ll}{\vcentcolon\Longleftrightarrow}
\newcommand{\notat}[1]{{!#1}}
\newcommand{\lra}{\longrightarrow}
\newcommand{\lhra}{\ensuremath{\lhook\joinrel\relbar\joinrel\rightarrow}}
\newcommand{\hra}{\hookrightarrow}
\newcommand{\brak}[1]{{\llbracket{#1}\rrbracket}}
\newcommand{\sdense}{{\widehat\Box}}
\newcommand{\sdenseother}{\Box}
\newcommand{\ie}{i.\,e.\@\xspace}
\newcommand{\eg}{e.\,g.\@\xspace}
\newcommand{\vs}{vs.\@\xspace}
\newcommand{\resp}{resp.\@\xspace}
\newcommand{\inv}{inv.\@}
\newcommand{\notnot}{\emph{not~not}\xspace}
\newcommand{\affl}{\ensuremath{{\ul{\AA}^1_S}}\xspace}
\newcommand{\afflx}{\ensuremath{{\ul{\AA}^1_X}}\xspace}
\newcommand{\afflt}{\ensuremath{{\ul{\AA}^1_T}}\xspace}
\newcommand{\afflvi}{\ensuremath{{\ul{\AA}^1_{V_i}}}\xspace}
\newcommand{\affla}{\ensuremath{{\ul{\AA}^1_{\Spec A}}}\xspace}
\newcommand{\afflz}{\ensuremath{{\ul{\AA}^1_{\Spec Z}}}\xspace}
\newcommand{\xra}{\xrightarrow}
\newcommand{\stacksproject}[1]{\cite[{\href{https://stacks.math.columbia.edu/tag/#1}{Tag~#1}}]{stacks-project}}
\newcommand{\apart}{\mathrel{\#}}
\newcommand{\fieldext}{\mathrel{|}}
\newcommand{\effective}{ef{}fective\xspace}
\newenvironment{indentblock}{%
\list{}{\leftmargin\leftmargin}%
\item\relax
}{%
\endlist
}
\newcommand{\XXX}[1]{\textbf{XXX: #1}}
\newcommand{\XXXh}[1]{}
\newcommand{\defeq}{\vcentcolon=}
\newcommand{\defequiv}{\vcentcolon\equiv}
\newcommand{\seq}[1]{\mathrel{\vdash\!\!\!_{#1}}}
\definecolor{gray}{rgb}{0.7,0.7,0.7}
\title{Using the internal language of toposes in algebraic geometry}
\author{Ingo Blechschmidt}
\email{[email protected]}
\makeatletter
\counterwithout{section}{chapter}
\counterwithout{footnote}{chapter}
\counterwithout{table}{chapter}
\counterwithout{figure}{chapter}
\patchcmd{\@thm}{\let\thm@indent\indent}{\let\thm@indent\noindent}{}{}
\patchcmd{\@thm}{\thm@headfont{\scshape}}{\thm@headfont{\bfseries}}{}{}
\patchcmd{\@makechapterhead}{\chaptername}{Part}{}{}
\patchcmd{\@chapter}{\chaptername}{Part}{}{}
\patchcmd{\@schapter}{\chaptername}{Part}{}{}
\addto\captionsenglish{\renewcommand\chaptername{Part}}
\def\l@section{\@tocline{1}{0pt}{1pc}{}{}} % \bfseries}}
\def\l@chapter{\@tocline{-1}{12pt}{0pt}{}{\bfseries}}
\renewcommand\thechapter{\Roman{chapter}}
\newcommand{\nocontentsline}[3]{}
\newcommand{\tocless}[1]{\let\addcontentsline=\nocontentsline}
\normalparindent=12pt
\parindent=\normalparindent
\renewenvironment{proof}[1][\proofname]{\par
\pushQED{\qed}%
\normalfont \topsep6\p@\@plus6\p@\relax
\trivlist
\item[\hskip\labelsep
\itshape
#1\@addpunct{.}]\ignorespaces
}{%
\popQED\endtrivlist\@endpefalse
}
\let\@afterindenttrue\@afterindentfalse
\def\subsection{\@startsection{subsection}{2}%
{0pt}{.5\linespacing\@plus.7\linespacing}{-.5em}%
{\normalfont\bfseries}}
\makeatother
\begin{document}
\newcommand{\HRule}{\rule{\linewidth}{.6pt}}
\begin{center}
\thispagestyle{empty}
\
\bigskip\bigskip
\HRule \\[0.4cm]
{\huge \bfseries Using the internal language of toposes \\ in algebraic geometry\par}\vspace{0.4cm}
\HRule
\bigskip\bigskip\bigskip\bigskip
\Large
Dissertation
\smallskip
zur Erlangung des akademischen Grades
\bigskip\bigskip
Dr.~rer.~nat.
\bigskip\bigskip
eingereicht an der
\bigskip\bigskip
Mathematisch-Naturwissenschaftlich-Technischen Fakultät
\smallskip
der Universität Augsburg
\bigskip\bigskip
von
\bigskip\bigskip
{\large Ingo Blechschmidt}
\bigskip\bigskip
\bigskip\bigskip
\bigskip\bigskip
\bigskip\bigskip
\bigskip\bigskip
\bigskip\bigskip
\bigskip\bigskip
\includegraphics[width=0.4\textwidth]{images/logo-uni-augsburg}
\bigskip\bigskip
\bigskip\bigskip
Juni 2017
\end{center}
\newpage
\vspace*{54em}
\begin{tabbing}
External reviewers:\quad \= \kill
Supervisor: \> Marc Nieper-Wißkirchen, University of Augsburg \\
\\
External reviewers: \> Thierry Coquand, University of Gothenburg \\
\> Frank Herrlich, Karlsruhe Institute of Technology \\
\\
Oral examination: \> October 16th, 2017
\end{tabbing}
{\tocless
\chapter*{Abstract}
Any scheme has its associated little and big Zariski toposes. These toposes
support an internal mathematical language which closely resembles the usual
formal language of mathematics, but is ``local on the base scheme'': For
example, from the internal perspective, the structure sheaf looks like an
ordinary local ring (instead of a sheaf of rings with local stalks) and vector
bundles look like ordinary free modules (instead of sheaves of modules
satisfying a local triviality condition). The translation of internal statements and
proofs is facilitated by an easy mechanical procedure.
We investigate how the internal language of the little Zariski topos
can be exploited to give simpler definitions and more conceptual
proofs of the basic notions and observations in algebraic geometry.
% For instance, any theorem about modules yields a corresponding theorem about
% sheaves of modules (with a small caveat).
To this end, we build a dictionary relating internal and external notions and
demonstrate its utility by giving a simple proof of Grothendieck's generic
freeness lemma in full generality. We also employ this framework to state a
general transfer principle which relates modules with their induced quasicoherent
sheaves, to study the phenomenon that some
properties spread from points to open neighborhoods, and to compare general
notions of spectra.
% We give a general sufficient condition for this spreading to occur, depending
% only on the logical form of the property in question.
We employ the big Zariski topos to set up the foundations of a synthetic account
of scheme theory. This account is similar to the synthetic account of
differential geometry, but has a distinct algebraic flavor. Central to the
theory is the notion of synthetic quasicoherence, which has no analogue in
synthetic differential geometry. We also discuss how various common subtoposes
of the big Zariski topos can be described from the internal point of view and
derive explicit descriptions of the geometric theories which are
classified by the fppf and by the surjective topology.
% No prior knowledge about topos theory or formal logic is assumed.
\chapter*{Acknowledgments}
%\thispagestyle{empty}
%\enlargethispage{1em}
I'm immensely grateful to Marc Nieper-Wißkirchen for his excellent supervision and
careful guidance, for trusting me with a lot of freedom, and for shaping me
mathematically. In this last regard I also acknowledge Jost-Hinrich Eschenburg,
Hansjörg Kielhöfer, and the contributors of the nLab.
These notes owe a special debt to Mike Shulman's work on the stack semantics of
toposes~\cite{shulman:stack}, without which this project wouldn't have been
started, and they greatly profited from insightful discussions with several people,
including Peter Arndt, Filip Bar, Andrej Bauer, Martin Brandenburg, Olivia
Caramello, Joost van Dijk, Adam Epstein, Felix Geißler, Simon Henry, Pol van Hoften, Matthias Hutzler, Simon
Kapfer, Georg Lehner, Guilhermo Frederico Lima de Carvalho e Silva, Tadeusz Litak, Zhen Lin
Low, Giovanni Morando, and Alexander Oldenziel. I'm grateful for their many valuable suggestions. I
particularly thank Adam Epstein for his great hospitality during my stay in
Warwick and Jiří Adámek, Jürgen Koslowski, and Ravi Vakil for their
much-appreciated encouragement.
I thank Tim Baumann, Joost van Dijk, Kathrin Gimmi, Matthias Hutzler, Sori Lee, Alexander Oldenziel, Lukas Stoll, and Marcus Zibrowius for their
careful readings of earlier drafts.
Dear to my heart is doing mathematics with children and school students. It was
a pleasure to work together with Kathrin Helmsauer and Sven Prüfer over the
last few years to establish and run Augsburg's Matheschülerzirkel, and I'm
grateful to the many people who invested their time into this project and shared our
vision.
%I fondly look back on mathematics camps together with these two and
%Meru Alagalingam, Tim Baumann, Martin Baur, Simone Beyser, Tim Dafler, Dominik
%Dirr, Johanna Fleckenstein, Caecilia Fröhler, Andrea Geck, Lukas Graf,
%Christoph Gräupner, Andreas Hohl, Christian Hübschmann, Jil Hümmer, Matthias
%Hutzler, Saadettin Karaca, Jorid Kretzschmar, Marco Lilienblum, Christian
%Lochner, Alexander Mai, Jessica Mandl, Moritz Meisel, Benjamin Mockl, Katharina
%Ohlhoff, Andreas Petrak, Dorothea and Veronika Pörtge, Peter Quast, Lisa
%Reischmann, Anna Rubeck, Caren Schinko, Raphael Schlarb, Eric Schlarmann,
%Maximilian Schlögel, Matthias Schlüter, Dominik Schmucker, Timo Schürg, Gesa
%Scupin, Benedikt von Seelstrang, Felix Stärk, Hannah Trost\-hei\-de, Peter
%Uebele, Philipp Wacker, Florian Wadas, David Wiedemann, Carina Willbold, Rolf
%Wittmann, Tanja Wolfer, Christopher Wulff, and Stephanie Zapf.
In particular, I thank my close family consisting of my sisters Dorothea and
Veronika Pörtge and my mother Gotlind Blechschmidt, who have accompanied me for
all my life and always encouraged and inspired me, Meru Alagalingam, Martin Frieb,
Michael Hartmann, Kathrin Helmsauer, Matthias Hutzler,
Christian Hübschmann, Jorid Kretzschmar, Jörg Lehmann, Alex\-an\-der Mai, Ninwe
Ninos, Sven Prüfer, Peter Quast, Lisa Reisch\-mann, Anna Rubeck, Ma\-xi\-mi\-li\-an
Schlögel, Peter Uebele, Philipp Wacker, my office mates Felix Geißler, Hedwig Heizinger,
Stephanie Zapf, and the wonderful participants of our courses in Papenburg, who
each supported me in a unique way. I'm indebted to Audrey Tang, who had a
strong and lasting influence on me many moons ago.
Here in Augsburg, we have a strong bond between undergraduates, PhD students,
and members of faculty. I'll try to carry our mathematical pizza seminars and
our non-mathematical and slightly nonstandard leisure time activities forward.
}
\setcounter{tocdepth}{1}
\tableofcontents
\chapter{Basics}
\section{Introduction}
{\tocless
\subsection*{Internal language of toposes}
A \emph{topos} is a category which shares certain categorical properties with
the category of sets; the archetypical example is the category of sets, and
the most important example for the purposes of this thesis is the category of
set-valued sheaves on a topological space.
Any topos~$\E$ supports an \emph{internal language}. This is a device which
allows one to \emph{pretend} that the objects of~$\E$ are plain sets and that
the morphisms are plain maps between sets, even if in fact they are not. For
instance, consider a morphism~$\alpha : X \to Y$ in~$\E$. From the \emph{internal
point of view}, this looks like a map between sets, and we can formulate the
condition that this map is surjective; we write this as
\[ \E \models \forall y\?Y\_ \exists x\?X\_ \alpha(x) = y. \]
The appearance of the colons instead of the usual element signs reminds us that
this expression is not to be taken literally --~$X$ and~$Y$ are objects of~$\E$
and thus not necessarily sets. The definition of the internal language is made
in such a way so that the meaning of this internal statement is that~$\alpha$
is an epimorphism. Similarly, the translation of the internal statement
that~$\alpha$ is injective is that~$\alpha$ is a monomorphism.
Furthermore, we can \emph{reason} with the internal language. There is a
metatheorem to the effect that if some statement~$\varphi$ holds from the
internal point of view of a topos~$\E$ and if~$\varphi$ logically implies some
further statement~$\psi$, then~$\psi$ holds in~$\E$ as well. As a simple
example, consider the elementary fact that the composition of surjective maps
is surjective. Interpreting this statement in the internal language of~$\E$, we
obtain the more abstract result that the composition of epimorphisms in~$\E$ is
epic.
There is, however, a slight caveat to this metatheorem. Namely, the internal
language of a topos is in general only \emph{intuitionistic}, not
\emph{classical}. This means that internally, one cannot use the law of
excluded middle~($\varphi \vee \neg\varphi$), the law of double negation
elimination~($\neg\neg\varphi \Rightarrow \varphi$), or the axiom of choice.
For instance, one rendition of the axiom of choice is that any vector space is
free. But it need not be the case that a vector space internal to a topos
is free as seen from the internal perspective: By the technique explained in
this thesis, this would imply the absurd statement that any sheaf of modules on
a reduced scheme is locally free.
The restriction to intuitionistic reasoning is not as confining as it might first
appear, in particular because there is a widely applicable metatheorem ensuring
that statements of a certain form are provable classically if and only if they
are provable intuitionistically. We will discuss practical consequences below (on
page~\pageref{sect:appreciating-intuitionistic-logic}).
\subsection*{Algebraic geometry}
We apply the internal language of toposes to algebraic geometry in two
different ways, corresponding to the two different toposes associated to a
scheme~$X$: the \emph{little Zariski topos} which is just the topos~$\Sh(X)$ of
set-valued sheaves on~$X$, and the \emph{big Zariski topos} which we introduce
below.
The internal language of the little Zariski topos can be used as follows.
The structure sheaf~$\O_X$ of a scheme~$X$ is a sheaf of rings in that its sets of
local sections carry ring structures and these ring structures are compatible
with restriction. From the internal point of view of~$\Sh(X)$,
the structure
sheaf~$\O_X$ looks much simpler: It looks just like a plain ring (and
not a sheaf of rings). Similarly, a sheaf of~$\O_X$-modules looks just like a
plain module over that ring.
This allows to import notions and facts from basic linear and commutative
algebra into the sheaf setting. For instance, it turns out that a sheaf
of~$\O_X$-modules is of finite type if and only if, from the internal
perspective, it is finitely generated as an~$\O_X$-module. Now consider the
following fact of linear algebra: If in a short exact sequence of modules the two
outer ones are finitely generated, then the middle one is too. The usual proof of
this fact is intuitionistically valid and can thus be interpreted in the
internal language. It then \emph{automatically} yields the following more advanced
proposition: If in a short exact sequence of sheaves of~$\O_X$-modules the
two outer ones are of finite type, then the middle one is too.
This example was not in any way special: \emph{Any (intuitionistically valid) theorem
about modules yields a corresponding theorem about sheaves of modules.}
The internal language machinery thus allows us to understand the basic notions
and statements of scheme theory as notions and statements of linear and
commutative algebra, interpreted in a suitable sheaf topos. This brings
conceptual clarity and reduces technical overhead.
In Section~\ref{sect:internal-language}, we explain how the internal language
machinery works, and then develop in Part~\ref{part:little-zariski} a
\emph{dictionary} relating common notions of scheme theory and corresponding
notions of algebra. Once built, this dictionary can be used arbitrarily often.
We stress that no in-depth knowledge of topos theory or categorical logic is
necessary to apply this apparatus.
In simple cases, the internal language can be regarded as a tool for ensuring
that certain kinds of ``fast and loose reasoning'' in algebraic geometry can be
rigorously justified. For instance, when trying to quickly gauge whether some
plausible-looking statement holds for schemes and sheaves, we might content
ourselves to check that the statement holds for rings and modules and then trust
that it also holds in the general case. Or when trying to construct a certain
sheaf of modules, we might content ourselves to construct it over affine open
subsets and then appeal to some gluing lemma, without meticulously checking the
details.
The internal language apparatus ensures that this kind of reasoning will never
result in wrong conclusions, provided that one can formulate the statements and
constructions in the internal language and that the correctness proof in the
affine setting is intuitionistically valid.
We believe that already this application of the internal language is useful to
working algebraic geometers. However, more advanced applications are also
possible. They result from considering internal statements whose logical form
is more complex, in particular from statements which quantify over subsets or which
contain implication and negation signs.
For instance, if~$X$ is a reduced scheme,
the internal universe of~$\Sh(X)$ has the peculiar feature that~$\O_X$ is
Noetherian and a field, even if~$X$ is not locally Noetherian and (as will
almost always be the case) the local rings~$\O_{X,x}$ are not fields. This fact
has no simple external counterpart; it's rather an intricate statement about
the interplay between the rings~$\Gamma(U, \O_X)$ for varying open subsets~$U
\subseteq X$.
Thanks to this particular feature, linear and commutative algebra over~$\O_X$
are particularly simple from the
internal point of view. For instance, Grothendieck's generic freeness lemma,
which is usually proved using a somewhat involved series of reduction steps,
admits a short, easy, and conceptual proof with this technique.
To briefly indicate a part of this, let~$\F$ be a sheaf of~$\O_X$-modules of finite
type. A basic version of Grothendieck's generic freeness lemma then states
that~$\F$ is locally free on some dense open subset of~$X$; this fact
is stated in Vakil's lecture notes as an ``important hard
exercise''~\cite[Exercise~13.7.K]{vakil:foag}. In fact, this proposition is just the
interpretation of the following basic statement of intuitionistic linear algebra in
the sheaf topos: Any finitely generated vector space is \notnot free.
The proof of this statement is entirely straightforward.\footnote{Intuitionistically,
the statement that any finitely generated vector space is \emph{free} is stronger than
the doubly negated version and cannot be shown. It would imply that any sheaf
of finite type is not only locally free on some dense open subset, but locally
free on the entire space. We discuss this example in more detail in
Section~\ref{sect:upper-semicontinuous-functions} and in particular in
Lemma~\ref{lemma:locally-free-dense}. A proof of Grothendieck's generic
freeness lemma in its full form is given in
Section~\ref{sect:generic-freeness}.
For concreteness, here is the standard intuitionistic proof that any finitely
generated vector space~$V$ is \notnot free. Let~$(x_1,\ldots,x_n)$ be a
generating family. If~$n = 0$, we are done. Else it's \notnot the case that
either some~$x_i$ can be expressed as a linear combination of the other
vectors, or not. The former implies
that~$(x_1,\ldots,x_{i-1},x_{i+1},\ldots,x_n)$ is a generating family, whereby
we can appeal to induction to obtain that~$V$ is \notnot free. The latter implies that~$(x_1,\ldots,x_n)$ is
linearly independent and therefore a basis. In both cases it follows that~$V$
is \notnot free, therefore~$V$ is indeed \notnot free.
In this argument, we used the intuitionistically valid proof
scheme~$\neg\neg\varphi \wedge (\varphi \Rightarrow \neg\neg\psi) \Longrightarrow
\neg\neg\psi$. We expand on this in
Section~\ref{sect:appreciating-intuitionistic-logic}.}
It is in this way that the internal language unlocks new approaches: by
making concepts accessible which would otherwise be too unwieldy to manage and
by allowing to import a huge corpus of prior work, namely the entire literature
on constructive algebra.
The internal language also sheds light on the phenomenon that
sometimes, truth of a property at a point~$x$ spreads to some open
neighborhood of~$x$; and in particular that sometimes, truth of a property at
the generic point spreads to some dense open subset. For instance, if the stalk
of a sheaf of finite type is zero at some point, the sheaf is even zero on some
open neighborhood; but this spreading does not occur for general sheaves which
may fail to be of finite type.
We formalize this by introducing a \emph{modal operator}~$\Box$ into the
internal language, such that the internal statement~$\Box\varphi$ means
that~$\varphi$ holds on some open neighborhood of~$x$. Furthermore, we
introduce a simple operation on formulas, the~\emph{$\Box$-translation}
$\varphi \mapsto \varphi^\Box$, such that~$\varphi^\Box$ means that~$\varphi$
holds at the point~$x$. This translation is defined on a purely syntactical
level. The question whether truth at~$x$ spreads to truth on a
neighborhood can then be formulated in the following way: Does~$\varphi^\Box$
intuitionistically imply~$\Box\varphi$?
This allows to deal with the question in a simpler, logical way, with the
technicalities of sheaves blinded out. We also give a metatheorem which
covers a wide range of cases. Namely, spreading occurs for all those properties
which can be formulated in the internal language without
using~``$\Rightarrow$'',~``$\forall$'', and~``$\neg$''.
To take up the example above, consider the property of a module~$\F$ being
the zero module. In the internal language, it can be formulated as~$(\forall x\?\F\_ x = 0)$.
Because of the appearance of~``$\forall$'', the metatheorem is not
applicable to this statement. But if~$\F$ is of finite type, there are
generators~$x_1,\ldots,x_n\?\F$ from the internal point of view, and the
condition can be reformulated as~$x_1 = 0 \wedge \cdots \wedge x_n = 0$; the
metatheorem is applicable to this statement.
\subsection*{Synthetic algebraic geometry}
All of the applications mentioned above employ the little Zariski topos of the base
scheme~$X$, the topos of sheaves on the underlying topological space of~$X$.
Its internal language simplifies the treatment of sheaves of rings and modules
over~$X$, but the treatment of~\emph{schemes} over~$X$ is simplified only a
little bit: From the internal point of view of~$\Sh(X)$, a morphism~$T \to X$
of schemes looks like a morphism~$T \to \pt$. Therefore relative scheme theory
is turned into absolute scheme theory (over the ring~$\O_X$), but it still
requires the machinery of locally ringed spaces.
The internal language of the \emph{big} Zariski topos of~$X$ allows for a more far-reaching
change of perspective. It incorporates Grothendieck's functor-of-points
philosophy in order to cast modern algebraic geometry, relative to the arbitrary
base scheme~$X$, in a naive \emph{synthetic} language reminiscent of the classical
Italian school.
The synthetic approach is best explained by contrasting it with the usual
approach to scheme theory, which is to layer it upon some standard form of set theory:
to give a scheme means to firstly give a set of points; then
to describe a topology on this set; and finally to equip the resulting space
with a local sheaf of rings. Basic objects of study in algebraic geometry, such
as closed subschemes of projective spaces, are in this way encoded using a large
amount of machinery.
There is also a somewhat lesser used, but philosophically rewarding and more
``economical'' approach within set theory: Grothendieck's functorial approach.
In this account of scheme theory, to give a scheme means to give a functor
from the category of commutative rings to the category of sets. For instance,
the Fermat scheme is given by the functor
\[ A \longmapsto \{ (x,y,z) \in A^3 \,|\, x^n + y^n - z^n = 0 \}, \]
that is, by a \emph{scheme} in the colloquial sense for prescribing a set of
solutions for any ring.
This approach requires fewer preparations and involves
only objects of intrinsic interest to algebraic geometry: $A$-valued points,
where~$A$ ranges over all rings. These tend to be better behaved, for instance in
that the set of~$A$-valued points of a product of schemes is isomorphic to the
product of the sets of~$A$-valued points, and are more fundamental from a
geometric point of view. In contrast, the set-theoretical points of a scheme in
the approach using locally ringed spaces actually parameterize irreducible
closed subsets, not points in an intuitive sense.
Canonical references for the functorial approach are lectures notes by
Gro\-then\-dieck~\cite{grothendieck:functorial-ag} and the book by Demazure and
Gabriel~\cite{demazure:gabriel}. A summary in English, including a proof of the
equivalence with the approach using locally ringed spaces, is contained in the
first chapter of~\cite{vezzani:fun}. At the Secret Blogging Seminar, there was
an insightful long-running discussion on the merits of the functorial
approach~\cite{secret-blogging-seminar:fpov}, and further philosophical background
is contained in~\cite{mclarty:ontology}. The thesis of Zhen Lin Low~\cite{low:local-models}
contains recent developments on an abstract theory of gluing local models.
The description of basic objects can still be somewhat involved in the
functorial approach. For instance, while the functor associated to
projective~$n$-space is given on fields by the simple expression
\[ \begin{array}{r@{}c@{}l}
K &{}\longmapsto{}& \text{the set of lines through the origin in~$K^{n+1}$} \\
&& \qquad \cong \{ [x_0 \hg \cdots \hg x_n] \,|\, \text{$x_i \neq 0$ for some~$i$} \},
\end{array} \]
on general rings it is given by
\[ \begin{array}{r@{}c@{}l}
A &{}\longmapsto{}& \text{the set of quotients~$A^{n+1} \twoheadrightarrow P$,
where~$P$ is projective of rank~1,} \\
&& \qquad \text{modulo isomorphism}.
\end{array} \]
On the one hand, typically only field-valued points admit a simple description.
On the other hand, the $A$-valued points for more general rings~$A$ are crucial
in order to impart a meaningful sense of cohesion on the field-valued
points. They therefore can't simply be dropped.\footnote{For instance,
let~$\ul{\AA}^1 : A \mapsto A$ be the functor associated to the affine line.
The Yoneda lemma guarantees that the set of morphisms~$\ul{\AA}^1 \to \ul{\AA}^1$
in the functor category~$[\Ring,\Set]$ is in canonical bijection with the
set~$\ZZ[U]$, as one would expect: Algebraic functions~$\AA^1 \to \AA^1$ should
be given by polynomials. (The discussion could also be relativized so that the
answer is the polynomial ring~$k[U]$, where~$k$ is some base field.) However, if we compute the
set of morphisms in~$[\mathrm{Field},\Set]$ we obtain~$\int_{K \in
\mathrm{Field}} \Hom(K,K)$, a set which contains pathological functions such as
some which permute the elements of the prime fields in arbitrary ways.}
We can resolve the tension by incorporating an automatic management of the
\emph{stage of definition}, the rings~$A$ such that we're
considering~$A$-valued points, into our language. Such a language is provided
by the internal language of the big Zariski topos. It allows for the Fermat
scheme to be given by the naive expression
\[ \{ (x,y,z) \? (\ul{\AA}^1)^3 \,|\, x^n + y^n - z^n = 0 \} \]
and for projective~$n$-space to be given by either of the expressions
\begin{multline*}
\qquad\text{the set of lines through the origin in~$(\ul{\AA}^1)^{n+1}$}
\quad\text{or} \\
\{ [x_0 \hg \cdots \hg x_n] \,|\, \text{$x_i \neq 0$ for some~$i$} \}.\qquad
\end{multline*}
This is not a specialized trick to give short descriptions of some schemes:
Like with the internal universe of any topos, the full power of intuitionistic
logic is available to reason about the objects constructed in this way.
We can thus add an approach to the list of ways of giving a rigorous foundation
to algebraic geometry, the synthetic approach which layers scheme theory not
upon a classical set theory, but rather directly encodes schemes as sets and
morphisms of schemes as maps of sets in the nonclassical universe provided by
the big Zariski topos of a base scheme. We can therefore use a simple,
element-based language to talk about schemes.
This is similar to synthetic approaches to other fields of mathematics, such as
differential geometry~\cite{kock:sdg}, domain
theory~\cite{hyland:synthetic-domain-theory}, computability
theory~\cite{bauer:synthetic-computability-theory}, and more recently and very
successfully homotopy theory~\cite{hott} and related
subjects~\cite{schreiber:cohesive,schreiber-shulman:qgft,riehl-shulman:synthetic-infinity-categories}.
The synthetic approaches allow in each case to encode the
objects of study directly as (nonclassical) sets, with geometric,
domain-theoretic, computability-theoretic, or homotopic structure being
automatically provided for.
The implicit algebro-geometric structure has visible consequences on the
internal universe of the big Zariski topos and endows it with a distinctive
algebraic flavor. For instance, the statement
``\emph{any} map~$\ul{\AA}^1 \to \ul{\AA}^1$ is a polynomial function''
holds from the internal point of view. This is also a property which sets the
internal universe of the big Zariski topos apart from the toposes studied in
synthetic differential geometry.
If one is content with building upon classical scheme theory, the big Zariski
topos~$\Zar(X)$ of a base scheme~$X$ can be constructed as the topos of
sheaves on the Grothendieck site~$\Sch/X$ of~$X$-schemes.\footnote{Some care is
needed in order to avoid set-theoretical issues of size. We discuss this fine
point in Section~\ref{sect:proper-choice-of-site}. If one is interested in
foundational questions and doesn't merely want to use the big Zariski topos in
order to employ its convenient internal language, one can rest assured that
there's a way to construct it without resorting to classical scheme theory. We
sketch this in Section~\ref{sect:big-zariski-without-classical-scheme-theory}.}
Explicitly, an object of~$\Zar(X)$ is a functor~$F : (\Sch/X)^\op \to \Set$
satisfying the gluing condition with respect to Zariski coverings:
If~$T = \bigcup_i U_i$ is a cover of an~$X$-scheme~$T$ by open subsets, the
diagram
\[ F(T) \longrightarrow \prod_i F(U_i) \xbigtoto{} \prod_{j,k} F(U_j \cap U_k) \]
should be an equalizer diagram. A premier example of an object of~$\Zar(X)$ is
the functor~$\ul{Y}$ of points associated to an~$X$-scheme~$Y$, mapping
an~$X$-scheme~$T$ to~$\Hom_X(T, Y)$. It satisfies the gluing condition since
one can glue morphisms of schemes in the Zariski topology.
The object~$\ul{\AA}^1$ which already appeared is the functor of points
of the affine line over~$X$, the~$X$-scheme~$\AA^1_X \defeq X \times_{\Spec\ZZ}
\ZZ[U]$. Its value on an~$X$-scheme~$T$ is
\[ \afflx(T) = \Hom_X(T, \AA^1_X) \cong \Hom_{\Spec\ZZ}(T, \Spec\ZZ[U]) \cong
\Gamma(T,\O_T). \]
This object has a canonical structure as a ring object in~$\Zar(X)$. In fact,
from the internal point of view of~$\Zar(X)$, it is a local ring and even a
field in the sense that nonzero elements are invertible. In the case~$X =
\Spec\ZZ$, this fact was first observed by Kock~\cite{kock:univ-proj-geometry}. At
the same time, it is not a reduced ring -- a feat possible only in an
intuitionistic context. This curious interplay is quite important, since the
sets
\[ \{ x\?\afflx \,|\, x = 0 \} \quad\text{and}\quad
\{ x\?\afflx \,|\, x^2 = 0 \} \]
should and do describe two different~$X$-schemes: the first is isomorphic
to~$X$ while the second is an infinitesimal thickening of~$X$, the vanishing scheme
of~$U^2$ in~$\AA^1_X$. In contrast, the sets~$\{ x\?\afflx \,|\, x \neq 0 \}$
and~$\{ x\?\afflx \,|\, x^2 \neq 0 \}$ should and do coincide. By the field
property, both conditions are equivalent to~$x$ being invertible.
The synthetic spectrum of an~$\afflx$-algebra~$A$ can be defined as
\[ \Spec(A) \defeq
\text{the set of~$\afflx$-algebra homomorphisms~$A \to \afflx$}. \]
On first sight, this definition seems to overlook potential non-maximal prime
ideals of~$A$, since it only gives the~$\afflx$-valued points. But in fact,
this description correctly reflects the relative spectrum construction.
It yields a simple correspondence between synthetic affine schemes and solution
sets of polynomial equations. For instance, it's easy to show that there is a
canonical isomorphism
\begin{multline*}
\qquad\Spec(\afflx[U_1,\ldots,U_n]/(f_1,\ldots,f_m)) \cong \\
\{ (u_1,\ldots,u_n) \? (\afflx)^n \,|\,
f_1(u_1,\ldots,u_n) = \cdots = f_m(u_1,\ldots,u_n) = 0 \}.\qquad
\end{multline*}
We give internal descriptions of further constructions of relative scheme
theory in Section~\ref{sect:basic-constructions}.
In order to be able to \emph{reason} internally (in contrast to only using the
internal language to describe~$X$-schemes and more general spaces in a simple
language), it's crucial to have strong and meaningful axioms available. One
such axiom posits that~$\afflx$ is a local and \emph{synthetically
quasicoherent} ring and implies all known ring-theoretic properties
of~$\afflx$. Synthetic quasicoherence is the internal analogue of the usual
condition on a sheaf of modules to be quasicoherent. This notion doesn't have a
counterpart in synthetic differential geometry and is central to our account of
synthetic algebraic geometry, since we derive all of its basic concepts such as
open and closed immersions and synthetic schemes from it.
Modal operators are useful in the big topos setting as well. For instance,
there is a modal operator~$\Box_\text{ét}$ in the big Zariski topos such that
the internal statement~$\Box_\text{ét} \varphi$ roughly means that~$\varphi$
holds on an étale covering and such that the translated
formula~$\varphi^{\Box_\text{ét}}$ means that~$\varphi$ holds in the \emph{big étale
topos} familiar from étale cohomology. In this way, we can access the internal
universe of the big étale topos from within the big Zariski topos. The
ring~$\afflx$ enjoys additional properties when studied in the étale topos,
where it is separably closed, in the fppf topos, where it is \emph{fppf-local},
and in the ph~topos, where it satisfies a strong form of algebraic
closure.
\subsection*{Limitations} The internal language is \emph{local}, in the sense
that if~$X = \bigcup_i U_i$ is an open covering and an internal statement
holds in the sheaf toposes~$\Sh(U_i)$, it holds in~$\Sh(X)$ as well. On the one
hand, this property is very useful. But on the other hand, it causes an inherent
limitation of the internal language:
Global properties of sheaves of modules like ``being generated by global
sections'', ``being ample'', or ``having vanishing sheaf cohomology'' and global properties of schemes like ``being
quasicompact'' can \emph{not} be
expressed in the internal language.
Thus for global considerations, the internal language of~$\Sh(X)$ is only
useful in that local subparts can be simplified. Also, some global features
reflect themselves in certain metaproperties of the internal language. For
instance, a scheme is quasicompact if and only if the internal language
has a weak version of the so-called disjunction property of mathematical
logic (Section~\ref{sect:compactness}).
The locality limitation only refers to locality with respect to the base
scheme. For instance, the little and big Zariski toposes of~$X$ \emph{can}
distinguish between affine and projective~$n$-space over~$X$, even though these
are locally isomorphic.
The internal languages of both toposes can be used on a case-by-case
basis, employing them as part of longer arguments in the context of ordinary scheme
theory where it's useful to do so. However, if one wants to stay solely in one
of the provided internal universes and not use ordinary scheme theory at all,
then one will of course run into the further limitation that internal scheme
theory, as put forward in this thesis, is only developed to a small extent.
\subsection*{Introductory literature} This text is intended
to be self-contained, requiring only basic knowledge of scheme theory. In
particular, we assume no prior familiarity with topos theory or formal logic.
Nevertheless, a gentle
introduction to topos theory is an article by
Leinster~\cite{leinster:introduction}. Standard references for the internal
language of toposes include the book of Mac~Lane and
Moerdijk~\cite[Chapter~VI]{moerdijk-maclane:sheaves-logic}, the book of
Goldblatt~\cite[Chapter~14]{goldblatt:topoi}, Caramello's and Streicher's lecture
notes~\cite{caramello:preliminaries,streicher:ctcl}, the book of
Borceux~\cite[Chapter~6]{borceux:handbook3}, and Part~D of
Johnstone's Elephant~\cite{johnstone:elephant}. Motivation and background on
the internal language can also be found in Chapter~0 of Shulman's lecture
notes~\cite{shulman:categorical-logic}.
In the 1970s, there was a
flurry of activity on applications of the internal language. An article by
Mulvey~\cite{mulvey:repr} of this time gives a very accessible
introduction to the topic, culminating in an internal proof of the Serre--Swan
theorem (with just one external ingredient needed).
\subsection*{Related work} The internal language of toposes was applied to algebraic geometry before. For
instance, Wraith used it to construct (and verify the universal property
of) the little étale topos of a scheme by internally developing the theory of
strict henselization~\cite{wraith:generic-galois-theory}. However, to the best
of our knowledge, systematically building a dictionary relating external and
internal notions has not been attempted before, and the use of modal operators
to study the spreading of properties from points to neighborhoods seems to be
new as well.
In particular, Tierney remarked in 1976 that a certain property of the internal
universe of the little Zariski topos ``is surely important, though its precise
significance is still somewhat obscure''~\cite[p.~209]{tierney:spectrum}. This
property can now be recognized as a small shadow of the internal
characterization of quasicoherence. We expand on this in
Section~\ref{sect:field-properties}.
In some regards, this thesis is an extended answer to a MathOverflow question
by Gubkin~\cite{mo:gubkin}, who inquired about uses of the internal language of
toposes in algebraic geometry.
Brandenburg put forward a related program of internalization in his PhD
thesis~\cite{brandenburg:tensor-foundations}. However, he internalizes
constructions of algebraic geometry not in toposes, but in tensor categories.
There is some overlap in working out precise universal properties, particularly
when dealing with the big Zariski topos.
In other branches of mathematics, the internal language of toposes is used as well. For
instance, there is an ongoing effort in mathematical physics to understand
quantum mechanical systems from an internal point of view: To any quantum
mechanical system, one can associate a so-called Bohr topos containing an
internal mirror image of the system. This mirror image looks like a
system of classical mechanics from the internal perspective, and therefore
tools like Gelfand duality can be used to construct an internal
phase space for the system~\cite{bohr1,bohr2,bohr3}.
In stochastics, the usefulness of an internal language was recently stressed by
Tao~\cite{tao:analysis-rel-measure-space}. Such a language makes the
common notational practice of dropping the explicit dependence of the
value~$X(\omega)$ of a random variable on the sample~$\omega$ completely
rigorous and simplifies the basic theory. Tao also highlighted how a suitable
language can be used to simplify ``$\varepsilon$/$\delta$ management'' in
analysis~\cite{tao:cheap-nsa}. Furthermore, there is a topos-theoretic approach to
measure theory, in which the sheaf of measurable real functions on
a~$\sigma$-algebra looks like the ordinary set of real numbers from an internal point
of view~\cite{jackson:sheaf-theoretic-measure-theory}; this has applications in
noncommutative geometry~\cite{henry:measure-theory-boolean-toposes}.
Intuitionistic methods have found many applications in computer science.
Recently, the internal language of a topos of trees and a suitable modal
operator was used to study guarded recursion, encompassing, for instance, an
internal Banach fixed-point theorem~\cite{birkedal:al:sgdt}.
In constructive mathematics, the internal language of toposes is routinely used
to obtain models of intuitionistic theories fulfilling certain anti-classical
axioms. For instance, there are toposes in which the axiom ``any map~$\RR \to
\RR$ is continuous'' (appropriately formulated) holds~\cite{kock:sdg,moerdijk:reyes:models}
and toposes in which the Church--Turing thesis ``any map~$\NN \to \NN$ is
computable'' holds (certain realizability toposes).
The internal language can also be used to extract computational content
out of classical constructions. To cite just one recent example, Mannaa and
Coquand used it to implement algorithms for working with the algebraic closure
of an arbitrary field of characteristic zero~\cite{mannaa:coquand:alg-closure}.
One way this thesis contributes to the program of constructive
mathematics is that intuitionistic mathematics gains new areas of application.
For instance, the constructive account of the theory of Krull dimension was
originally developed to remove Noetherian hypotheses, extract computational meaning, and
simplify proofs~\cite{dyn:krull-integral,dyn:char-krull}. It can now also be used to
reason about the dimension of schemes, since the topological dimension of a
scheme~$X$ coincides with the Krull dimension of the structure sheaf~$\O_X$
regarded as an ordinary ring from the internal perspective of~$\Sh(X)$
(Section~\ref{sect:krull-dimension}).
We obtained a second contribution to constructive mathematics as a byproduct of
deducing transfer principles which relate a module over a ring~$A$ with its
induced quasicoherent sheaf on~$\Spec A$: Using the internal language of the
little Zariski topos we can algorithmically turn certain non-constructive
arguments concerning prime ideals into constructive ones. We discuss this in
Section~\ref{sect:eliminating-prime-ideals}; it is related to the
\emph{dynamical methods in algebra} explored by Coquand, Coste, Lombardi, Roy,
and others~\cite{clr:dynamicalmethod,cl:logical}.
Caramello uses topos theory to build bridges between different mathematical
subjects, in a certain precise sense~\cite{caramello:1,caramello:2}. She
exploits that toposes can admit presentations by sites of different character. Our
contribution is certainly related to her grand research program in spirit, but since we
focus only on specific presentations of a few specific toposes associated to
schemes, there are as yet only few direct technical connections.
\subsection*{Notational conventions} To stress that a discussion takes place in
an intuitionistic context, we occasionally write~``$\forall x\?X$''
or~``$\exists x\?X$'' instead of~``$\forall x \in X$'' and~``$\exists x \in
X$'' not only in internal statements, where it's proper to do so, but also when
not reasoning internally.
If~$X$ and~$Y$ are sets, we mean by~``$[X,Y]$'' the set of all maps from~$X$
to~$Y$. This expression will often occur in internal formulas; its external
meaning will then be the Hom sheaf. We write pairs~$\langle a, b \rangle$ using
angle brackets. The preimage of a set~$M$ under a map~$f$ is
written~``$f^{-1}[M]$''. Similarly, the image is written~``$f[N]$''.
The constant sheaf with stalks~$M$ is written~``$\ul{M}$''.
}
\section{The internal language of a sheaf topos}\label{sect:internal-language}
At its heart, the internal language of a topos provides a coherent way of
translating any mentions of set-theoretical elements to
\emph{generalized elements}, carefully keeping track of and adapting
the stage of definition. We want to illustrate this with a simple example
before giving the formal definition.
A map~$f : X \to Y$ of sets is injective if and only if
\begin{equation}\label{inj}
\forall x,x' \in X\_ f(x) = f(x') \Longrightarrow x = x'.
\end{equation}
This condition can not only be interpreted in~$\Set$, but in any category~$\C$ whose
objects are structured sets and whose morphisms are maps between the underlying
sets. If we want to go beyond such kind of categories, we have to restate the
condition in purely category-theoretic language:
\begin{equation}\label{injcat}
\forall (1 \xra{x} X), (1 \xra{x'} X)\_ f \circ x = f \circ x'
\Longrightarrow x = x'.
\end{equation}
This condition makes sense in all categories which contain a terminal
object~$1$, and is equivalent to condition~\eqref{inj} in the case~$\C = \Set$.
This has a deeper reason: The one-element set~$1 = \{ \star \}$ is a
\emph{separator} of~$\Set$, that is objects of~$\Set$ are uniquely determined
by their \emph{global elements}, morphisms from the terminal object.
However, in categories in which the terminal object is not a separator,