Injective Hulls In a Locally Finite Topos

TL;DR

This paper proves that in a locally finite topos, every object can be uniquely extended to an injective object, providing a foundational result with implications for topos-theoretic calculations.

Contribution

It introduces a construction for essential injective extensions in locally finite toposes, advancing the understanding of their structure.

Findings

Every object has a unique essential injective extension.

The extension construction is applicable in topos-theoretic calculations.

The work is motivated by software for topos computations.

Abstract

We show that in a locally finite topos, every object has an essential extension that is injective, and that this extension is unique up to isomorphism. The construction was motivated by work on Bewl, a software project for doing topos-theoretic calculations.