9
$\begingroup$

Using the internal logic of a topos it's often possible to derive newer theorems about sheaves from earlier ones about simpler objects, assuming that you can prove the earlier ones constructively. In addition, Barr's Theorem allows one to directly reuse classical results when they have a geometric statement relative to a geometric theory.

How far can you take this? Can scheme-theoretic algebraic geometry can be developed internally in the appropriate topoi, or are there some notions that have inherently extrinsic definitions and proofs?

Improve this question
$\endgroup$
6
  • 4
    $\begingroup$ Algebraic geometry can be developed internal to a sufficiently nice symmetric monoidal category; e.g. you get algebraic geometry over a base scheme $S$ by taking the symmetric monoidal category to be $\text{QCoh}(S)$. According to the nLab this idea goes back to Deligne but the first reference that comes to my mind is Brandenburg: arxiv.org/abs/1410.1716. $\endgroup$
    – Qiaochu Yuan
    Commented Dec 3, 2016 at 7:00
  • 4
    $\begingroup$ I'd also point out the notes of Ingo Blechschmidt, Using the internal language of toposes in algebraic geometry (rawgit.com/iblech/internal-methods/master/notes.pdf) $\endgroup$
    – David Roberts ♦
    Commented Dec 3, 2016 at 7:12
  • $\begingroup$ @DavidRoberts Thanks, that's pretty much what I was looking for. $\endgroup$
    – Cameron Zwarich
    Commented Dec 4, 2016 at 21:01
  • $\begingroup$ @CameronZwarich would you like it as an official answer? $\endgroup$
    – David Roberts ♦
    Commented Dec 5, 2016 at 0:46
  • 4
    $\begingroup$ Deligne describes algebraic geometry over Tannakian categories in his paper "La droite projective moins trois points". $\endgroup$
    – Jesse Silliman
    Commented Dec 5, 2016 at 1:43

2 Answers 2

Reset to default
10
$\begingroup$

The notes of Ingo Blechschmidt, Using the internal language of toposes in algebraic geometry cover this. See also his lecture at Topos à l'IHÉS of the same name.

His work very much extends Hakim's thesis.

Improve this answer
$\endgroup$
10
  • 1
    $\begingroup$ It would be great to see a specific reference for such a "nasty" calculation or proof in the traditional setting that becomes somehow a lot simpler with this machinery. I conjecture that the effort one has to put in to learn this internal topos stuff cancels out any benefit (i.e., what you might think looks "nasty" is seen as straightforward to someone who has traditional expertise rather than internal-topos expertise), so it's just a matter of shifting where one puts in the effort at learning some background. But it is easier to judge against specific illustrations of such applications. $\endgroup$
    – nfdc23
    Commented Dec 5, 2016 at 2:10
  • 1
    $\begingroup$ I just watched the entire video and didn't see any such examples. (There was something referred to as an "important hard exercise", but it is an easy exercise from the traditional point of view, nothing hard about it.) Gabber raised a very apt point from the back of the room as well: one needs to know the traditional sheaf-theoretic methods when doing more advanced things (for generic flatness and so on), so it is good to get practice with such ideas in the simpler settings first. I remain puzzled about the utility, but will let it lie there. $\endgroup$
    – nfdc23
    Commented Dec 5, 2016 at 3:49
  • 1
    $\begingroup$ @nfdc23 From page 8 of Ingo's thesis, an example is the fact that any finite-type sheaf of $\mathcal{O}_X$-modules is locally free on a dense open subspace. Ingo points out that in Vakil's notes, this is an "hard, important exercise". In intuitionistic logic, it's the statement that a finite-type sheaf is "not not free", and this is apparently straightforward to prove. $\endgroup$
    – Tim Campion
    Commented Apr 7, 2017 at 15:43
  • 1
    $\begingroup$ @nfdc23: The phrase "internal language of toposes" sounds intimidating. But I can guarantee that one doesn't need a firm grasp of the 1000+ pages of the Elephant in order to apply this useful tool. :-) It's enough to learn the translation rules (the Kripke–Joyal semantics) and to distinguish constructive from nonconstructive proofs. After a short episode of confusion and anger, the latter comes quite easily. And the former takes no more than a couple of minutes. :-) $\endgroup$
    – Ingo Blechschmidt
    Commented May 11, 2017 at 17:06
  • 1
    $\begingroup$ @nfdc23: The key reason why the proof of Grothendieck's generic freeness lemma is much easier using the internal language is that the structure sheaf $\mathcal{O}_X$ looks like a Noetherian ring and in fact like a field from the internal point of view, even if the scheme $X$ is not locally Noetherian. This simplifies the situation to the easiest nontrivial case (from an arbitrary not necessarily Noetherian base ring to a field). This fact doesn't have any concise external counterpart: neither the sets $\mathcal{O}_X(U)$ nor the stalks $\mathcal{O}_{X,x}$ are Noetherian or fields. $\endgroup$
    – Ingo Blechschmidt
    Commented May 12, 2017 at 8:55
8
$\begingroup$

Perhaps you might find some answers in Monique Hakim's book, Topos annelés et schémas relatifs. I only looked at it briefly long ago, so I can't be sure if it's relevant, but Mathreviews quotes part of the introduction "... Au Chapitre IV on définit la catégorie SchS des schémas relatifs sur un topos annele S ..." So maybe it is.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Hakim's thesis is indeed a treasure trove. But she doesn't use the internal language at all, which was not yet developed at her time. With the internal language, some of her constructions and proofs can be simplified; for instance, her very general spectrum functor from ringed toposes to locally ringed toposes is given by interpreting a (constructively sensible formulation of the) usual spectrum construction in the internal language. The universal property of the construction then follows from the well-known universal property of the usual spectrum. $\endgroup$
    – Ingo Blechschmidt
    Commented May 12, 2017 at 12:43

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .