nLab Penon open

Idea

An intrinsic notion of an open subobject in an elementary topos.

Definition

A monomorphism UXU\to X in an elementary topos EE is a Penon open if the following statement holds in the internal logic of EE:

xXyX(xU)(¬(y=x)yU).\forall x\in X \forall y\in X(x\in U)\to (\neg(y=x)\vee y\in U).

Properties

If UXU\to X is a Penon open, then

xU({yX¬¬(y=x)}U).\forall x \in U(\{y\in X\mid \neg\neg(y=x)\}\subset U).

References

Created on February 15, 2025 at 01:25:09. See the history of this page for a list of all contributions to it.