Enough injectives with just Zorn’s lemma and not the axiom of
choice:

draft
paper (see appendix)

2024 Verona Minicourse on extracting programs from proofs

HoTTEST 2023: slides (Agda code)

Herrsching 2023: slides

Niš:
slides

Fischbachau:
slides,
Agda
exercises

plenary

Slides for Brixen 2022:
informal,
plenary

Slides
for Schlehdorf 2022

Slides
for Dagstuhl 2021

Slides
for Antwerp 2022

Slides
for CiE 2022

Slides
for CIRM 2023
(rough
early draft of a preprint)

# About me

I’m a mathematician working in applied topos theory. I obtained my PhD in October 2017 under the supervision of Marc Nieper-Wißkirchen at the University of Augsburg. Besides research, I love teaching mathematics at all levels and am passionate about doing mathematics with school students. Currently I’m back in Augsburg. During the academic year 2018/2019, I was working at the Università di Verona under the supervision of Peter Schuster. In the winter term 2017/2018, I was substituting a junior professor at the University of Augsburg, and during the summer of 2018, I was a guest at the Max Planck Institute for Mathematics in the Sciences in Leipzig.

I explore applications of the internal language of toposes, particularly in commutative algebra and in algebraic geometry.

**Short research summary****Research statement****PhD thesis: Using the internal language of toposes in algebraic geometry**(large portions require only familiarity with scheme theory, not with topos theory; slides, more slides, 2015 talk at the IHÉS)

**Paper: An elementary and constructive proof of Grothendieck’s generic freeness lemma****Paper: Flabby and injective objects in toposes****Short note: A constructive Knaster–Tarski proof of the uncountability of the reals**(joint with Matthias Hutzler)**Paper: Exploring mathematical objects from custom-tailored toposes****Preprint: Reflections on reflection for intuitionistic set theories**(joint with Andrew Swan)**Paper: A general Nullstellensatz for generalized spaces****Expository paper: Generalized spaces for constructive algebra****Paper: Maximal ideals in countable rings, constructively**(joint with Peter Schuster)**Paper: A constructive picture of Noetherian conditions and well quasi-orders**(joint with Gabriele Buriola and Peter Schuster)**Expository paper: A primer to the set-theoretic multiverse philosophy****Paper: Reifying dynamical algebra: maximal ideals in countable rings, constructively**(joint with Peter Schuster)

- UNILOG talk:
**Exploring the internal language of toposes** - Como talk:
**How topos theory can help commutative algebra**(for topos theorists) - Leipzig talk:
**How topos theory can help algebra and geometry**(for a general mathematical audience) - Colloquium Logicum/Münchenwiler/Padova talk:
**New reduction techniques in commutative algebra driven by logical methods** - PSSL104 talk:
**How not to constructivize cohomology**(also see paper) - 6WFTop/CT2019 talk:
**A general Nullstellensatz for generalised spaces**(also see rough draft) - Dagstuhl 2021 talk:
**Bridging the foundational gap: Updating algebraic geometry in face of current challenges regarding formalizability, constructivity and predicativity**

I contribute to the nLab and to the Stacks Project, and encourage everyone to consider Eugenia Cheng’s manifesto for inclusivity in category theory and mathematics at large.

**Recent results by Matthias Hutzler:** The
infinitesimal topos classifies the theory of quotients of local algebras
by nilpotent ideals (master’s thesis), Syntactic
presentations for glued toposes and for crystalline toposes (PhD
thesis)

**Recent result by Johannes Riebel:** The
undecidability of BB(748)

## Travel plans

- April 2018: PSSL 103 in Brno
- April 2018: Oberseminar Mathematische Logik in Munich
- April 2018: Computational Approaches to the Foundations of Mathematics in Munich
- May 2018: Summer School on Types, Sets and Constructions in Bonn
- May 2018: Philosophy of mathematics: objects, structures, and logics in Mussomeli
- June 2018: UniLog in Vichy
- June 2018: Toposes in Como in Como
- July 2018: Jugendschülerakademie in Papenburg
- August 2018: Mathematics camp in Violau
- September 2018: Colloquium Logicum 2018 in Bayreuth
- September 2018: Proof and Computation in Fischbachau
- October 2018: PSSL 104 in Amsterdam
- October 2018: EUTYPES2018 in Aarhus
- October 2018: Münchenwiler Meeting in Münchenwiler
- February 2019: Motivic Verona in Verona
- March 2019: Compact course on proof interpretations in Verona
- April 2019: Workshop on Formal Topology in Birmingham
- Spring 2019: Warwick
- July 2019: Category Theory 2019
- September 2019: Proof and Computation in Herrsching

Illustration: Carina Willbold (CC BY-SA)