University of Gothenburg/Chalmers
April 17-20, 2023
Some talks are talking place internal to the Zariski topos and are marked as such for better orientation.
Basics of Synthetic Algebraic Geometry and our three axioms.
Definition of affine-open subsets, qc-open subsets and finally schemes.
Proof of "boundedness" and the correspondence between affine opens and (pointwise) qc-opens.
Definition of standard projective space. Proof that this is a scheme.
First I will compare our definition of scheme with the definition of schemes as functor of points that one can find in the books of Demazure-Gavriel, Eisenbud-Harris, Jantzen and in one blog post of David Madore. Some differences are
-we work with f.p. algebra, while most presentations work with "arbitary" algebra (or algebra in a fixed universe)
-we limit ourselves to quasi compact quasi separated schemes
-we can express the definition in an internal way
Next, as an example of how to "compute" semantics (first in a 1-topos setting) I will present the semantics of the projective space Pn, and explain why we get something like the definition in Demazure-Gabriel, a result that was first claimed in technical report of Anders Kock.
Links: Dana Scott on presheaf models, master thesis with details on presheaf models
Every Grothendieck topos classifies a geometric theory, which is determined up to Morita equivalence. In this talk I will describe the structures classified by the topos of sheaves on the site CartSpTop of topological manifolds with the open cover topology [1] as "flat, archimedean, real-continuous algebras".
As a replacement for sheaves on a scheme X, we use dependent R-modules over X, which we call bundles.
We will define cohomology, using the known construction of Eilenberg-MacLane spaces in HoTT.
We will prove a vanishing result for higher cohomology of weakly quasi-coherent bundles on affine schemes.
An overview of the construction of models of cubical type theory.
We define formally étale maps in a synthetic setting as maps having the right lifting property against closed dense embeddings. We prove that being étale is a left exact modality for types. Then we define formally unramified maps as maps with formally étale diagonals. We prove that a map between scheme is unramified if and only if its differentials are injective.
Following Hartshorne.
Synthetic definition of compactness, proof that projective space has this property.