Elementary topos

An elementary topos is a category with finite limits, a cartesian-closed structure, and a subobject classifier. These axioms support an internal intuitionistic higher-order logic.

A subobject classifier is a monomorphism $\top :1\to \Omega$ such that every monomorphism $A^{\prime }\hookrightarrow A$ is, uniquely, a pullback of $\top$ along a characteristic map ${\chi }_{A^{\prime }}:A\to \Omega$.

A Lawvere-Tierney topology on a topos is a morphism $j:\Omega \to \Omega$ satisfying, internally,It is also called a local operator.

If a subobject $A^{\prime }\hookrightarrow A$ has characteristic map $\chi :A\to \Omega$, its $j$-closure is classified by $j\chi$. This closure operation is inflationary, idempotent, and stable under pullback.

A monomorphism is $j$-dense when its $j$-closure is its whole codomain. It is $j$-closed when it equals its closure. Dense monomorphisms are stable under pullback, and a monomorphism that is both dense and closed is an isomorphism.

An object $X$ is a $j$-sheaf when every map $A^{\prime }\to X$ defined on the domain of a j-dense monomorphism $A^{\prime }\hookrightarrow A$ extends uniquely to a map $A\to X$.

The closed-subobject classifier is the equalizerIt classifies $j$-closed subobjects and is itself a j-sheaf. The local operator factors as a split epimorphism $q:\Omega \twoheadrightarrow {\Omega }_j$ followed by the canonical inclusion $i:{\Omega }_j\hookrightarrow \Omega$.

The full subcategory of $j$-sheaves is reflective. Its reflector $L$ sends every $j$-dense monomorphism to an isomorphism and preserves finite limits.

For a local operator $j$, the following are equivalent: $L$ preserves the subobject classifier; $L(q):L\Omega \to {\Omega }_j$ is an isomorphism; the canonical inclusion $i:{\Omega }_j\hookrightarrow \Omega$ is $j$-dense; and every monomorphism $A^{\prime }\hookrightarrow A$ factors as a $j$-closed mono $A^{\prime }\hookrightarrow A^{\prime \prime }$ followed by a $j$-dense mono $A^{\prime \prime }\hookrightarrow A$.