Workshop on Internal Methods in Algebraic Geometry

University of Gothenburg/Chalmers
April 17-20, 2023

Talk Content

Some talks are talking place internal to the Zariski topos and are marked as such for better orientation.

Felix Cherubini: Schemes (Internal) boardshots

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.

Matthias Hutzler: Projective Space (Internal) boardshots

Definition of standard projective space. Proof that this is a scheme.

Thierry Coquand: Some comments on the definition of schemes boardshots

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

Jonas Frey: Cartesian Spaces boardshots

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".

Matthias Hutzler: Bundles of Modules (internal) boardshots

As a replacement for sheaves on a scheme X, we use dependent R-modules over X, which we call bundles.

Felix Cherubini: Cohomology (internal) boardshots

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.

Christian Sattler: Cubical Models boardshots

An overview of the construction of models of cubical type theory.

Hugo Moeneclaey: Etale and Unramified Morphisms (internal) boardshots

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.

Nicolas Beck: Fibered Categories boardshots

Marc Nieper-Wißkirchen: Serre-Duality for Projective Space over a Field boardshots

Following Hartshorne.

David Wärn: Proper Schemes (internal) boardshots

Synthetic definition of compactness, proof that projective space has this property.

Ingo Blechschmidt: Čech-Cohomology (internal?) boardshots

Thierry Coquand: Justification of the Axioms boardshots

David Wärn: Differential Geometry (internal) boardshots

Joisselin Poiret: Formalization (internal in some way) boardshots