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 nondegenerate elementary topos is two-valued when its terminal object has exactly the empty and whole subobjects. This is a global-truth property, distinct from being a Boolean topos, which requires complements for all subobjects of all objects.

A noninitial object is irreducible, or supercompact, when every family of subobjects with union the whole object contains the whole object as one member. This concerns unions of subobjects rather than disjoint coproduct decompositions. Irreducible representable sheaves for the regular coverage follow from the one-arrow nature of that coverage.

A Boolean topos is an elementary topos in which every subobject has a complement, equivalently its internal truth-value Heyting algebra satisfies excluded middle. Its internal first-order logic is classical. Being Boolean alone does not imply that it has enough set-valued points.

A logical functor between elementary toposes preserves finite limits, exponential objects and the subobject classifier, with their canonical comparison maps. It therefore preserves power objects and the double-power-object monad. If it has a left adjoint, power-object monadicity and the adjoint lifting theorem for monad algebra functors give it a right adjoint as well.

A power object $PA$ represents parameterized subobjects of $A$: $\mathcal{E}(X,PA)\cong \mathrm{Sub}(X\times A)$. In an elementary topos, it is ${\Omega }^A$, with the membership subobject supplied by evaluation at the subobject classifier.

If a Cartesian category has power objects, its slice categories do too. In $\mathcal{E}/A$, the constant family $A\times X\to A$ has power object $A\times PX\to A$, since its product with a family $Y\to A$ is $X\times Y$. An arbitrary family $p:X\to A$ is a subobject of the constant family through its graph $(p,1_X)$, so the power object of a subobject construction applies in the slice.

For a monomorphism $Y\hookrightarrow X$ in a Cartesian category, intersect the universal membership relation on $X\times PX$ with $Y\times PX$. The resulting subobject is classified by $r:PX\to PX$, and $r^2=r$. The equalizer of $r$ and the identity represents precisely families of subobjects of $X$ contained in $Y$, hence is a power object for $Y$. This construction only requires the power object of $X$ and finite limits.

An arrow $f:A\to B$ induces $Pf:PB\to PA$ by inverse image of predicates. Transposition of predicates on $A\times B$ gives $\mathcal{E}(A,PB)\cong \mathcal{E}(B,PA)$ and the adjunction $P^{\mathrm{op}}⊣P$. The induced monad on the topos is double power-object formation; it is distinct from the covariant powerset monad on sets.

The contravariant power-object functor of an elementary topos is monadic. Its double-power unit ${\eta }_A(a)(S)=(a\in S)$ is monic, which helps prove that $P$ reflects isomorphisms. Finite equalizers and the fact that power objects turn coreflexive equalizers into coequalizers give the remaining hypotheses of the crude monadicity theorem.

For an elementary topos, existence of products in a category indexed by a fixed set is equivalent to existence of the corresponding coproducts in a category. The power-object monadicity equivalence ${\mathcal{E}}^{\mathrm{op}}\simeq {\mathcal{E}}^{PP}$ gives the forward direction because Eilenberg-Moore categories create limits. For the converse, the diagonal into the pointwise product category is a logical functor. A coproduct is its left adjoint; the adjoint lifting theorem for monad algebra functors, applied through power-object monadicity, then gives its right adjoint, namely the product. The required reflexive coequalizers on the algebra side are opposites of finite equalizers in the topos.

For a coreflexive pair $f,g:B\rightrightarrows A$ with equalizer $e:E\hookrightarrow B$, direct image along the mono $f$ satisfies $Pf{\exists }_f=1$ and $Pg{\exists }_f={\exists }_{e}Pe$. Thus any map $h:PB\to Z$ equalizing $Pf,Pg$ obeys $h=h{\exists }_{e}Pe$. Since $Pe{\exists }_e=1$, the map $Pe$ is their coequalizer. These identities hold for parameterized subobjects in any elementary topos.

An atom is a noninitial object with only the empty and whole subobject. In the atomic finite-surjection site, the sheaf component generated by one primitive class is an atom: membership of one descendant in a subobject descends to its primitive ancestor and then propagates to all descendants. A decomposition into atoms makes subobjects selections of components.

Global sections are the maps from the terminal object: $\Gamma (X)=\mathrm{Hom}(1,X)$. For a Grothendieck topos, this is the direct image of its geometric morphism to sets. In a presheaf category, it is right adjoint to the constant-presheaf functor.

A geometric morphism $f:\mathcal{E}\to \mathcal{F}$ is an adjunction $f^{\ast }⊣f_{\ast }$ with finite-limit-preserving inverse image $f^{\ast }:\mathcal{F}\to \mathcal{E}$. Inverse image also preserves colimits as a left adjoint. An extra left adjoint $f_{!}⊣f^{\ast }$ makes it essential.

For a geometric morphism $f:\mathcal{E}\to \mathcal{F}$, the displayed internal frame represents $X\mapsto {\mathrm{Sub}}_{\mathcal{E}}(f^{\ast }X)$. The localic part is ${\mathrm{Sh}}_{\mathcal{F}}(L)\to \mathcal{F}$. Its basic open families pull back to the subobjects of $f^{\ast }X$ they represent; gluing these gives a full faithful, subobject-closed inverse image, hence the hyperconnected geometric morphism part. The represented subobject functor recovers the internal frame, proving uniqueness up to equivalence over $\mathcal{F}$.

A geometric morphism $h$ is hyperconnected when its inverse image functor of a geometric morphism is full and faithful and its essential image is closed under subobjects. It then identifies all subobjects of $h^{\ast }X$ with subobjects of $X$, and its image is closed under quotients as well, by descending the kernel-pair relation.

A geometric morphism $p:\mathcal{D}\to \mathcal{F}$ is localic when $\mathcal{D}$ is, over $\mathcal{F}$, the topos of sheaves on an internal locale of $\mathcal{F}$. Equivalently, subobjects of the objects $p^{\ast }X$, with $X\in \mathcal{F}$, form a separating family in $\mathcal{D}$.

Geometric morphisms into a sheaf topos correspond to continuous flat functors from its site into the domain topos, with continuity meaning that covers become jointly epimorphic families. Pulling back sheafified representables gives the functor; the tensor construction gives the inverse image in the other direction. This representation theorem should not be confused with the separately named Diaconescu theorem about choice and excluded middle.

Every Grothendieck topos has a unique geometric morphism to sets, up to isomorphism. Its inverse image is $\Delta S={\coprod }_{s\in S}1$ and its direct image is $\Gamma A=\mathrm{Hom}(1,A)$. A geometric inverse image out of sets must have this form because it preserves coproducts and the terminal object. A local topos is one for which $\Gamma$ itself is an inverse image.

The inverse image is a finite-limit-preserving left adjoint with right adjoint $f_{\ast }$. It preserves arbitrary colimits, and hence images as well as finite limits. These properties preserve the interpretation of geometric formulas. It need not preserve Heyting implication or every universal quantifier.

A geometric morphism is essential when its inverse image has an additional left adjoint. For a functor of small categories, precomposition on presheaves has left Kan extension and Right Kan extension as its two adjoints. Precomposition preserves finite limits pointwise, so this is an essential geometric morphism.

For $f:\mathcal{E}\to \mathcal{F}$, the comonad $G=f^{\ast }{f}_{\ast }$ is Cartesian, and its coalgebra topos $\mathcal{D}$ gives a factorization $f=i\circ p$. Here $p^{\ast }$ is the faithful forgetful functor and $i^{\ast }$ is the comparison functor. Its right adjoint sends $(A,a)$ to $\mathrm{Eq}(f_{\ast }a,{\eta }_{f_{\ast }A})$; applying $f^{\ast }$ identifies the comparison counit with the equalizer $a:A\to GA$ of $Ga,{\delta }_A$, proving that $i_{\ast }$ is full and faithful.

A geometric embedding is a geometric morphism whose direct-image functor is full and faithful. Its inverse image presents a left-exact reflective subcategory of the target topos. It is the second part of the surjection-embedding factorization of a geometric morphism.

A subtopos is a Grothendieck topos embedded by a geometric embedding, considered up to equivalence over the ambient topos. On a site $(\mathcal{C},J)$, subtoposes correspond to Grothendieck topologies $J^{\prime }\supseteq J$. On a classifying topos this is the duality between geometric quotients and subtoposes.

A geometric morphism is surjective when its inverse-image functor is faithful, equivalently conservative for geometric inverse images. Reflection of isomorphisms of subobjects already proves faithfulness by applying the inverse image to equalizers of parallel arrows. The surjection-embedding factorization of a geometric morphism separates this property from a fully faithful direct image.

For a geometric morphism, the characteristic map of $f^{\ast }\top$ induces a comparison $f^{\ast }{\Omega }_{\mathcal{E}}\to {\Omega }_{\mathcal{F}}$ whose adjoint transpose is $\lambda$. Composing with a characteristic map classifies the inverse-image subobject. Thus monicity of $\lambda$ is equivalent to reflection of equality of subobjects under $f^{\ast }$, and hence to faithfulness of the inverse image: apply reflection to equalizers of parallel arrows. Conversely faithfulness reflects when a pulled-back monomorphism is an isomorphism, by comparing its characteristic map with truth; intersections then reflect equality of arbitrary subobjects.

A topos over sets is local when its global sections functor is itself an inverse image functor. For an idempotent-complete small indexing category, its presheaf topos is local exactly when the indexing category has a terminal object: then global sections are evaluation at that object.

Equivalently every open cover of $X$ contains $X$ as a member, so the top element of its open-set lattice is supercompact in the frame sense. Necessity follows from preservation of coproducts and epimorphisms by global sections. Conversely the union of all proper opens misses a point $x$, and the stalk functor there equals global sections. Its right adjoint is a skyscraper sheaf of sets. Empty spaces fail; a T1 space satisfies the condition exactly when it is a singleton.

The constant singleton functor must be a retract in a category of a covariant representable functor. Necessity follows by applying a colimit-preserving global-sections functor to the canonical coproduct of representables onto the terminal functor. Conversely its Hom functor is a retract of evaluation, preserves colimits and has a right adjoint. Such a retract is represented by an initial object in the idempotent completion. For an idempotent-complete category an actual initial object suffices; without this hypothesis an absorbing-zero monoid gives a counterexample to the unqualified claim.

A functor $F:\mathcal{C}\to \mathcal{D}$ induces a geometric morphism from the presheaf topos on $\mathcal{C}$ to that on $\mathcal{D}$. Its inverse image is precomposition with $F^{\mathrm{op}}$, its direct image is Right Kan extension and its extra left adjoint is left Kan extension. The extra left adjoint sends $yC$ to $y(FC)$.

The geometric morphism induced by $T:\mathcal{C}\to \mathcal{D}$ is a geometric embedding exactly when $T$ is full and faithful. Its right adjoint has $(f_{\ast }H)(d)=\mathrm{Nat}(\mathcal{D}(T-,d),H)$. The counit at $c$ is precomposition with $\mathcal{C}(-,c)\to \mathcal{D}(T-,Tc)$. It is invertible for all $H$ precisely when that comparison presheaf is an isomorphism, by the Yoneda lemma, which is precisely full faithfulness of $T$.

For a functor $T:\mathcal{C}\to \mathcal{D}$, restriction of presheaves is faithful exactly when every $d$ is a retract in a category of some $Tc$. Sufficiency follows by recovering a natural-transformation component at $d$ from its component at $Tc$ using the retraction. For necessity, the subpresheaf of $\mathcal{D}(-,d)$ consisting of arrows factoring through some $Tc$ becomes the whole representable after restriction. Faithfulness of a geometric inverse image reflects such a monomorphism being an isomorphism. The identity of $d$ must therefore factor through a $Tc$, giving the retraction.

A Grothendieck topos is a category equivalent to the sheaves on a site for a small Grothendieck topology. It is an elementary topos with all small colimits and a small generating family. Small disjoint coproducts, effective quotients and the set of subobjects of any fixed object allow many constructions by unions.

A topos classifies a geometric theory when geometric morphisms into it from any Grothendieck topos correspond naturally to internal models of that theory. Pulling back one generic model gives the corresponding model. For a finitary algebraic theory, the classifying topos is the covariant functor category on finitely presented models.

In the sheaf topos for the Zariski coverage on finitely presented rings, the universal local ring is represented by the polynomial ring $\mathbb{Z}[t]$. At the stage of a finitely presented ring $A$, its section set is $A$, and restriction along $A\to B$ is that ring map. It is internally local because the localizations at $x$ and $1-x$ cover each stage. Its square-zero infinitesimals are represented by $\mathbb{Z}[\epsilon ]/({\epsilon }^2)$. Stage rings need not themselves be local or reduced; their variation supplies the internal local and infinitesimal semantics.

For $D=\{d\in R:d^2=0\}$ in the generic local ring, every internal map $D\to R$ has a unique affine expression $d\mapsto a+bd$. At the stage $A$, such maps are elements of $A[\epsilon ]/({\epsilon }^2)$, which is freely $A\oplus A\epsilon$ as an $A$-module. This decomposition is natural under ring maps and proves the isomorphism. Testing only on ordinary fields loses the generic infinitesimal and would give an incorrect uniqueness argument.

Finite strict total orders and increasing injections, including the empty order, give a presheaf classifier for strict total orders. Trichotomy locally merges two finite sorted tuples, identifying equal entries. A strict map from a chain is injective, so parallel maps admitting the same realization are already equal. Reflexification gives a geometric morphism to the classifying topos of linear orders; pulling back weak totality gives exactly strict trichotomy.

With empty objects allowed, finite totally ordered sets and all weak order-preserving functions give a presheaf classifier for weak total orders. Finite tuples in a model can locally be merged into a sorted tuple using finitely many totality disjunctions. Equalizing two maps between finite chains amounts to collapsing the convex intervals forced equal. These two constructions give the flatness conditions without assuming decidable equality.

Let $\mathbf{FinSPos}$ contain finite strict partial orders and strict order-preserving functions. Its covariant set-valued functor category classifies the strict theory. A finite presentation with a strict cycle is contradictory; every other finite diagram gives a finite strict partial order. Equalizing finitely many element identifications either gives such an order or forces a forbidden cycle, so the internal model-to-flat-functor construction remains valid. The reflexification of a strict partial order induces a surjective geometric morphism to the weak-order classifier, but not a geometric embedding because strict maps exclude collapse of comparable elements.

Let $\mathbf{FinPos}$ contain finite partially ordered sets and all order-preserving functions, including the empty object. The covariant functor category $[\mathbf{FinPos},\mathbf{Set}]$ classifies weak partial orders. Finite positive presentations reduce to finite preorders with mutually comparable cycles identified. An internal model $M$ gives a flat functor $P\mapsto \mathrm{Hom}(P,M)$ on ${\mathbf{FinPos}}^{\mathrm{op}}$; conversely the corresponding filtered presentation by finite models recovers its carrier and order relation.

Each geometric quotient theory is classified by the corresponding subtopos of the original classifying topos. Extra axioms impose extra covers on the geometric syntactic topology. Conversely additional definable covers give the corresponding deductively closed quotient. Under Morita equivalence of geometric theories, transporting a subtopos produces a corresponding quotient of the other theory, with equivalent classifiers. Stronger axioms correspond to smaller subtoposes under inclusion.

Geometric theories are Morita-equivalent when their classifying toposes are equivalent. This gives equivalent internal model categories pseudonaturally in every Grothendieck topos. A common classifying topos transports intrinsic invariants between different presentations; agreement of set-valued model categories alone is insufficient. The duality between geometric quotients and subtoposes transfers geometric theory extensions along such an equivalence.

On the opposite of finitely presented commutative rings, cover the zero ring by the empty family and cover $A$ by $A/(a),A/(b)$ whenever $ab=0$. The generated topology classifies nontrivial integral domains, with generic model the sheafified tautological ring. It is not subcanonical: at $\mathbb{Z}/4$, the covering quotient to $\mathbb{Z}/2$ identifies the distinct sections $0$ and $2$ of the polynomial-ring representable.

In the generic domain, negation of simultaneous invertibility of finitely many elements implies that one is zero. At a ring stage, localize at their product $t$. All become units, so a tuple satisfying the negation makes the localized stage empty. The empty-cover criterion for the domain-classifying site then says $A[1/t]=0$, hence $t$ is nilpotent. Repeated zero-product covers force one factor to vanish locally. The two-variable property conversely forces the integral-domain axiom in any nontrivial internal ring.

For a finitely presented ring $A$, its sheafified representable is initial exactly when $A$ is the zero ring. The zero ring has a generating empty cover. Every nonzero ring maps to a field by quotienting by a maximal ideal, and that set-based domain gives a point at which the representable has a section, precluding initiality.

Adding coherent or geometric axioms to a theory determines a coverage on a site for its classifying topos. The antecedent presentation is covered by presentations where its consequent disjuncts and witnesses hold. Sheafification imposes those axioms on the generic model. An inconsistent antecedent gets an empty cover.

In $[{\mathbb{T}}_{fp},\mathbf{Set}]$, the generic model assigns to each finitely presented algebra its underlying set at each sort, with the algebraic operations pointwise. It is covariant on algebra homomorphisms. Pullback along a geometric morphism yields its classified internal model.

An object is decidable when its diagonal is a complemented subobject of its square. Equivalently its internal equality is decidable. Pullback gives closure under subobjects; coordinatewise equality gives closure under finite products. For an existing coproduct, unequal summands together with the complements of the diagonal in each equal summand form the diagonal complement.

A covariant set-valued functor $F$ is a decidable object precisely when every transition map $F(u)$ is injective. The pointwise complement of its diagonal consists of unequal pairs; it is a subfunctor exactly when transition maps preserve inequality. For left M-sets, this says that every action map is injective.

In a Grothendieck topos, an object is a quotient of a decidable object when it has an epic cover by one. These objects are closed under subobjects, small coproducts, quotients and finite limits. Their union inside any fixed object gives the largest subobject of this kind, defining a coreflective subcategory. The induced idempotent comonad is left exact, so the full subcategory is a topos.

The subobject classifier supplies intuitionistic truth values. Subobjects interpret predicates, finite limits interpret finite conjunctions and equality, and suitable image and adjoint constructions interpret quantifiers. One must distinguish internal intuitionistic arguments from classical reasoning in the external category of sets.

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$.

In the covariant functor category $[\mathbb{N},\mathbf{Set}]$, the classifier at $n$ consists of thresholds $k\ge n$ and the empty threshold $\infty$. Its transition to $n+1$ sends $k$ to $\max (k,n+1)$. The displayed maps commute with transitions and are all surjective, so define an epimorphism. They identify $n$ and $n+1$, so the endomorphism is not an isomorphism.

In a category with finite limits and a subobject classifier, every monic endomorphism $f$ of $\Omega$ is an involution. The subobject $g:U\hookrightarrow \Omega$ classified by $f$ is subterminal, since $fg=\top {!}_U$ is monic. If $V\hookrightarrow U$ is classified by $g$, pullback uniqueness gives $f\top {!}_U=g$, hence $f^{2}g=g$. If $u$ classifies $U\hookrightarrow 1$, the pullback of $g$ along $f$ is $\top {!}_U$, so $f^2(p)=u\wedge p$. Monicity implies $u=\top$, because $u\wedge u=u\wedge \top$, proving the displayed identity.

The subobject classifier $\Omega$ of a topos carries internal truth, falsity, meet, join and implication. Its generalized elements over $X$ are subobjects of $X$; implication satisfies $R\le (P\Rightarrow Q)$ exactly when $R\cap P\le Q$. Pullback-compatible operations make this an internal Heyting algebra, not merely a structure on global truth values.

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

The pullback of the truth point along a local operator $j$ is the subobject $J\hookrightarrow \Omega$. A monomorphism with characteristic map $\chi$ is j-dense exactly when $\chi$ factors through $J$. Its internal order is inherited from the Heyting algebra of truth values. Having a least global element is an internal condition over all parameter objects, not just a condition on global truth values.

For a subterminal truth value $u$, the quasi-closed local operator is relative double negation $q(U)(p)=((p\Rightarrow u)\Rightarrow u)$. It has bottom value $q(U)(0)=u$. Its fixed truth values are Boolean with relative bottom $u$, inherited meet, join closed by $q(U)$ and complement $p\Rightarrow u$. Therefore its sheaf topos is a Boolean topos.

In $\mathcal{E}/\Omega$, the generic truth mono $\top :1\hookrightarrow \Omega$ defines a quasi-closed Boolean subtopos. Its composite to $\mathcal{E}$ is surjective. If a predicate $p(x)$ pulled back from $\mathcal{E}$ becomes dense, then $((p(x)\Rightarrow u)\Rightarrow u)=1$ for the generic truth $u$. Substitution $u=p(x)$ yields $p(x)=1$, proving reflection of invertible monos and hence faithfulness.

For a subterminal object classified by $u$, the closed local operator is $p\mapsto u\vee p$. Its closed monos contain the pullback of that subterminal, hence are exactly the monos dense for the corresponding open local operator.

For a subterminal object classified by $u$, the open local operator is $p\mapsto (u\Rightarrow p)$. Its dense monos are exactly those whose image contains the pullback of that subterminal. It is complementary to the corresponding closed local operator.

For $j=o(U)$, the dense monomorphism classifier consists of the truth values above $u$, so has least element $u$. Conversely, if it has least element $u$, density of a monomorphism is exactly containment of the pulled-back subterminal $U$. For a subobject $S\subseteq X$, the mono $S\to \overline{S}$ is dense, so $U\cap \overline{S}\subseteq S$ and $j(p)\le u\Rightarrow p$. Since $j(u)=\top$, applying $j$ to $u\wedge (u\Rightarrow p)\le p$ gives $u\Rightarrow p\le j(p)$. Hence equality holds.

The open local operator and closed local operator associated with $U$ have meet the identity and join the largest local operator. The meet identity is $(u\Rightarrow p)\wedge (u\vee p)=p$. Every mono factors through its union with $U$ as a closed-operator-dense mono followed by an open-operator-dense mono, proving that their join makes every mono dense.

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 mono is j-closed if it equals its closure under the local operator $j$. Its characteristic map factors through the closed-subobject classifier ${\Omega }_j$. A j-closed subobject of a j-sheaf is a j-sheaf; a mono that is both closed and j-dense is an isomorphism.

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$.

An object is j-separated when two maps into it which agree on a j-dense monomorphism are equal. Equivalently its diagonal is j-closed. Quotienting an arbitrary object by the j-closure of its diagonal gives its separated reflection, used in constructing the sheaf reflector for a local operator.

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$.