# Uses of the internal logic of a topos in algebraic geometry?

I see why topoi arise naturally in AG, but I'm having a hard time finding examples, if any, of the application of their more logical side to geometric questions.

I'm looking for examples of proofs in AG using the internal logic of topoi, or an explanation of why there aren't (m)any.

• What's your question exactly? – Marko Karbevski Jul 17 '17 at 15:37
• I'm looking for examples of proofs in AG using the internal logic of topoi, or an explanation of why there aren't (m)any. – dlahoti Jul 17 '17 at 15:39
• Ingo Blechschmidt's thesis contains numerous examples: github.com/iblech/internal-methods – Dmitri Pavlov Jul 18 '17 at 16:28

There are several such examples (although not being well-versed in the subject, I can't say how serious a role internal reasoning plays in algebraic geometry, just that examples exist). A few can be found in the answers to this other question. Of particular interest is Ingo Blechschmidt's answer; he shows how the statement

Let $\mathcal{F}$ be an $\mathcal{O}_X$-module locally of finite type. Then $\mathcal{F}$ is locally free iff its rank is constant.

can be proved using internal logic, roughly as follows:

• Reasoning internally, we translate the question to one about usual modules inside the topos of sheaves on $X$.

• This reduces the problem to the task of proving a linear algebra fact constructively, which one can do.

I think this provides a very nice example of what internal logic can do: it lets you answer a complicated question by interpreting it as a conceptually much simpler question inside a different topos.

(Actually, I guess this is more accurately a description of the use of the internal language of the topos, and not the internal logic per se; that is really the second bullet point.)

• Incidentally, I'm curious whether a theorem in algebraic geometry has every been first proven using internal logic, rather than being proved initially via standard means and then reproved (possibly more elegantly) by internal logic. – Noah Schweber Jul 17 '17 at 17:04