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

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 CartSp_{Top} 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