A Note About Models of Synthetic Algebraic Geometry

TL;DR

This paper presents a constructive approach to modeling Synthetic Algebraic Geometry over rings, ensuring finitely presented algebras have decidable equality within a weak meta-theoretic framework.

Contribution

It introduces a new model construction for Synthetic Algebraic Geometry that guarantees decidable equality for finitely presented algebras in a weak, constructive setting.

Findings

Finitely presented k-algebras have decidable equality in the model.

Construction is compatible with a weak, constructive meta-theoretic framework.

The approach aligns with dependent type theory with universes.

Abstract

We show how to build models of Synthetic Algebraic Geometry over rings k such that finitely presented k-algebra have a decidable equality. The construction is done in a constructive and weak (same proof theoretic strength as dependent type theory with universes) meta theory.