Write the comonad as and its category of coalgebras for a comonad as . A coalgebra for a comonad is a map with and . A morphism satisfies . Let be the forgetful functor and let be the cofree coalgebra. The adjunction has the explicit correspondenceWe construct the three pieces of the elementary topos structure.
Because preserves finite limits, each underlying finite limiting cone has a unique coalgebra structure induced by the structures on its vertices. The counit and coassociativity equations can be checked after its jointly monic projections. Thus creates finite limits and reflects isomorphisms. A morphism of coalgebras is monic exactly when its underlying morphism is monic, by the diagonal criterion using the created pullback.
For exponentials in a coalgebra topos, fix coalgebras and and put in . On the cofree coalgebra there is an underlying evaluationThe two mapsuse in the second expression. Transpose them in to maps , and then transpose across to coalgebra morphisms . Take their equalizer in .
An underlying map corresponds to a coalgebra map . The equation saying that the original map is a coalgebra morphism is precisely , since for the structure . By the cofree adjunction, this is equivalent to , hence to unique factorization through . Thereforenaturally in . This constructs the required exponential object.
For the subobject classifier of a coalgebra topos, let be the underlying subobject classifier, and let classify the mono . Its cofree transpose is the coalgebra endomorphismDefine as the equalizer of and . The transpose of factors through this equalizer and gives .
Indeed, for a subobject classified by , the pullback has characteristic map . It is always contained in , by naturality of the counit. Equality holds exactly when restricts to a coalgebra structure on ; its axioms then follow by composing with the monomorphisms and . Under , the classifying map becomes . The equality of subobjects is . Transposing this equality gives , so exactly the coalgebra subobjects correspond to maps . Their pullback of is the desired subcoalgebra, and uniqueness follows from uniqueness of .
Thus we have finite limits, exponentials and a subobject classifier:The construction does not assume that preserves the underlying exponentials or underlying subobject classifier.
A decidable object in a topos has a decomposition , with representing inequality. In the internal logic of a topos, equality on is decidable. These categorical complements behave well under pullback.
For a subobject , pull back the displayed decomposition along . The diagonal pulls back to , while pulls back to its complement. Hence every subobject of a decidable object is decidable; the subobject itself need not be complemented in .
For two decidable objects, the diagonals of and give four disjoint summands of , according as each coordinate pair is equal or unequal. The both-equal summand is , and the other three give its complement. The terminal object is decidable, so induction gives closure under finite products, including the empty product.
For a family of decidable objects with an existing coproduct , products distribute over this coproduct, givingThe coproduct injections in a topos are disjoint. The diagonal consists of in each summand, and has complementConsequently every existing coproduct of decidable objects is decidable, including the initial object. In a Grothendieck topos all small coproducts exist. No assertion that arbitrary products preserve decidability is used.
Let be the full subcategory of quotients of decidable objects. It is closed under quotients, by composition of epimorphisms, and under small coproducts, by part (ii). It is also closed under subobjects: pull back a decidable cover along . The resulting cover of has domain a subobject of , hence a decidable object.
The terminal object lies in . If and are decidable covers, their product is an epimorphism . Part (ii) makes its domain decidable. Thus products, and then equalizers as subobjects of products, remain in . The inclusion preserves finite limits.
We construct a coreflective subcategory rather than claim that every object has a decidable cover. For , let be the union of all subobjects of which lie in . The Grothendieck topos is well-powered, so these subobjects form a set. Choose a decidable cover of each and take their coproduct. Its map to has image , so is itself a quotient of a decidable object. Any map from an object of to has image in , and therefore factors uniquely through . This givesThe induced idempotent comonad on preserves finite limits: is a right adjoint and preserves those limits. Its counit is the inclusion , and .
The coalgebras of this comonad are exactly the objects of . A coalgebra structure is a section of the monic counit, forcing the counit to be an isomorphism; conversely an object already in has the unique such structure. Thus . Part (i) now givesThis argument proves the required elementary-topos conclusion without presuming a small family of decidable generators for .
A local operator, also called a Lawvere-Tierney topology, is a map which internally satisfiesThe closure operation of a local operator sends a mono with characteristic map to the subobject classified by . It is inflationary, idempotent and pullback-stable. A mono is j-dense if its closure is its whole codomain, and j-closed if it equals its closure. A j-sheaf is an object for which restrictionis a bijection for every j-dense mono ; requiring only injectivity defines a j-separated object.
Here is a construction underlying the sheaf reflector for a local operator. The closed-subobject classifier is a j-sheaf: closed subobjects on a dense subobject extend uniquely by taking their closure in the larger object. Powers are also sheaves, because products of a dense mono with remain dense. A j-closed subobject of a sheaf is a sheaf: first extend a map into the ambient sheaf, then use density to force its image into the closed subobject.
Close the diagonal of . Its j-closure is an equivalence relation, using preservation of finite meets and pullback-stability to verify transitivity. The effective quotient is the separated reflection: every map from into a separated object identifies that closed diagonal and factors uniquely. For separated , the closed-singleton mapis monic. Its j-closed image closure is a sheaf, and is dense. Unique extension across that mono, following the separated quotient factorization, provesfor every sheaf . This proves reflectivity. The closure construction is pullback-stable; equivalently, separated quotients and the subsequent dense embeddings commute with the finite limiting comparisons, giving the usual left-exact sheaf reflector.
Finite limits of sheaves are computed in , because unique extensions can be taken componentwise. If is a sheaf, is a sheaf for any , by the same product-with-dense-mono argument. Thus sheaf exponentials are the ambient exponentials. Monos between sheaves have j-closed images: their closure is a sheaf, and the dense inclusion into it splits by the extension property, hence is an isomorphism. Therefore classifies precisely their subobjects. These observations establish is a reflective topos.
Now let classify the given subterminal object. Its open local operator and closed local operator areThe Heyting algebra identities verify all local-operator axioms: implication by fixed preserves meets and is idempotent, while adjoining preserves meets by distributivity and is idempotent.
For a mono in with characteristic predicate , closedness for means , or . Density for means , again . Thus the c(U)-closed monos are exactly the o(U)-dense monos.
Both densities together force and , hence : the only jointly dense monos are isomorphisms. More explicitly, the meet of these operators is pointwise andso .
For their join, every mono factors through the union with the pullback :The first mono is c(U)-dense, because adjoining fills its codomain; the second is o(U)-dense, because its image contains . Any local operator above both must therefore make every mono dense, since its dense monos are closed under composition. It is the largest operator . ConsequentlyThese are the complementary open and closed local operators in the ordered lattice of local operators, with order given by pointwise implication.
A first-order signature specifies sorts, function symbols with specified input and output sorts, and relation symbols with specified input sorts. A coherent formula is built from atomic relations and equalities using , , finite logical conjunctions, finite logical disjunctions, and existential quantification. A coherent theory is a set of sequents between coherent formulas in a common finite context; its axioms are interpreted as universally closed implications. Neither general negation nor universal quantification is allowed inside coherent formulas.
One complete presentation of coherent logic consists of the following axiom and rule schemes, together with the theory's sequents. All displayed formulas have compatible sorts and contexts, and bound variables can be renamed.
Identity and cut give andSubstitution replaces the free variables of any derivable sequent by well-typed terms, avoiding capture. Contexts can be enlarged by unused variables, and permuted or renamed.
The finite-meet rules are , , , andThe finite-join rules are , , , andInclude distributivity .
Existential introduction is . Existential elimination iswhere is absent from . Equivalently, the quantifier is left adjoint to weakening along the context projection. Include the Frobenius rule in coherent logicIt can also be derived from the usual coherent natural-deduction rules.
Equality has and the substitution schemeincluding atomic formulas and terms of the signature. Symmetry, transitivity and congruence for all functions and relations follow. These schemes impose no unintended inhabitedness axiom on a sort.
The coherent syntactic category has objects formulas in context , up to renaming. An arrow from to is an equivalence class, modulo provable equivalence, of formulas satisfyingandThese are provably total functional relations. The identity is the equality graph restricted by . If and are consecutive arrows, their composite is represented by . Equality, cut and existential rules give the category laws.
A coherent category has finite limits, pullback-stable regular-epi/mono image factorizations, and finite unions of subobjects stable under pullback. We verify these structures syntactically. The terminal object is the empty-context truth formula. Products conjoin formulas in disjoint contexts; equalizers add equality of the two output tuples. For a functional relation , its image in the target is represented by . Its factor onto that image is regular epic: two arrows out of the image agreeing on the source agree by existential elimination, and the same argument with the kernel pair gives the coequalizer property. Frobenius makes these image factorizations stable under pullback.
Every subobject of is represented by a formula with . Indeed, take the existential image of a monic functional relation; uniqueness makes its map to that image an isomorphism. Subobject inclusion is exactly provable implication. Finite unions are consequently disjunctions, with bottom as the empty subobject; distributivity and substitution make them pullback-stable. Hence is coherent.
The conservative syntactic model interprets a sort by , a function by its term graph, and a relation by its atomic-formula subobject. Induction on coherent formulas shows that is interpreted by the subobject of its context object. It satisfies every theory axiom by construction. Conversely, a sequent holds in this model exactly when the corresponding subobject inclusion holds, which is exactly derivability in . ThereforeThis is conservativity for coherent sequents, not a claim about non-coherent formulas.
Write and similarly for . The geometric morphism induced by a functor hasPrecomposition preserves all pointwise limits and colimits, so in particular it preserves finite limits. The Right Kan extension exists because the categories are small and sets have all small limits; its universal property gives . Thus these functors define a geometric morphism .
There is also , a left Kan extension, with . The Yoneda lemma identifies , since for every ,This is the representable calculation used in the next parts.
A representable functor is an indecomposable projective object. Given an epimorphism , evaluate at . Epimorphisms and coproducts in a presheaf category are pointwise, so is the image of some element of a particular . By the Yoneda lemma, that element defines , and its composite into corresponds to , hence is the identity. The selected component is split epic. More generally, evaluation sends any epimorphism to a surjection, so a map from lifts through any epimorphism; this also proves its ordinary projectivity.
Conversely, every presheaf has the canonical epimorphismwhose component is the natural transformation named by . It is pointwise surjective, since an element at is reached from its own summand at . If is indecomposable projective, one component has a section . The endomorphism of is idempotent and therefore corresponds to an idempotent morphism .
If idempotents split in , choose with , . Then : the mutually inverse maps are and . ThusWithout that hypothesis the argument still proves that every such object is a retract of a representable. The initial presheaf is not indecomposable projective, since its identity is the empty-coproduct epimorphism and has no component to select.
The key fact is that the extra left adjoint sends each representable to an indecomposable projective object. Let be epic. The inverse image preserves epimorphisms and coproducts, because it is a left adjoint between toposes. Apply it and lift the unit through the resulting epimorphism, using projectivity of . A map from to a coproduct selects one component, by evaluation at and the Yoneda lemma. Thus for some we obtain with .
Transpose across to . The displayed equality says that its composite back to is the identity. This proves the required indecomposable-projective property.
Since idempotents split in , part (ii) supplies objects and isomorphisms . Full faithfulness of the Yoneda embedding transports the action of on representable arrows to a functor . For ,These identifications are natural in both and . HenceIts right adjoint is consequently the right Kan extension from part (i), uniquely up to natural isomorphism. Thus the entire geometric morphism is induced by .
The canonical geometric morphism has inverse image the constant-presheaf functor and direct image the global sections functorIf the presheaf topos is a local topos, is also the inverse image of a geometric morphism . This morphism has an extra left adjoint . Apply part (iii) with source category and target category , using its idempotent-splitting hypothesis. Then is induced by a functor , choosing an object , and is naturally evaluation at .
Since evaluation at is , this says . Uniqueness of representing objects gives . Thus is a singleton for every : is terminal.
Conversely, if is terminal, and . Evaluation at that object preserves finite limits and has a right Kan extension as right adjoint, so is an inverse image functor. Therefore, under the permitted idempotent-completeness assumption,
The required condition is the common-refinement condition for nonempty-sieve coverage: for every pair , , there are arrows , withNecessity follows by pulling back the nonempty sieve generated by along : a member of the pullback sieve supplies such an . Conversely, this condition makes the pullback of every nonempty sieve on a category nonempty. The maximal sieve is nonempty, and the transitivity axiom holds: if a sieve is locally covering along every member of a nonempty covering sieve , choose and then ; their composite is in . Hence the nonempty sieves form a Grothendieck topology, called the atomic topology.
For all functions between nonempty finite sets, the two maps from a singleton to different points of a two-point set have no common refinement. Every potential domain remains nonempty, so the two constant composites cannot agree. The condition fails.
For surjections it holds: is nonempty and both projections are surjective. Work from now on in a small skeleton of nonempty finite sets and surjections. Every morphism is a regular epimorphism, with kernel pair , and is the coequalizer of that pair in .
A matching family in a representable on the sieve generated by is determined by a surjection equalizing that kernel pair. It factors uniquely through a function , which is surjective because is. This gives the unique amalgamation. A general nonempty covering sieve contains such an ; after amalgamating there, common refinements with any other member force agreement on the entire sieve. Therefore every representable is a sheaf, so this atomic site is subcanonical.
For any sheaf , every restriction is injective: equality after a covering arrow forces equality by the separated part of the sheaf condition. We shall also use descent along any surjection :is an equalizer of sets. These are the descent identities for the atomic finite-surjection site.
Consider primitive , with a common restriction along , . Suppose have but . Let identify just the two points . Define the finite nonempty setBoth projections are surjective, since contains every diagonal pair. There is also a surjectionIndeed the target consists of diagonal pairs, which are reached because is surjective, and the two off-diagonal pairs corresponding to , reached by and .
Since , the common-restriction equality gives . If are the target kernel-pair projections, this isInjectivity of gives the kernel-pair matching condition on . Descent along then writes , contradicting primitivity. Thus ; interchange the roles to obtain equality. This is the primitive-element kernel rigidity lemma.
Equal kernels produce a unique bijection with . Now , and injectivity impliesIn particular equivalent primitive elements have the same cardinality and differ only by transport along a bijection.
Every element descends to a primitive one: whenever it is not primitive, descend along a surjection reducing the cardinality by one; this process terminates at or before cardinality one. Kernel rigidity shows that all primitive ancestors of lie in one equivalence class. Let be the elements with primitive-ancestor class . Restriction along a surjection preserves this class, so each is a subfunctor andpointwise. Each is a sheaf. A matching family glues in , and one member along a nonempty covering arrow already determines the primitive class of the glued element; it must be .
Choose a representative primitive of . The Yoneda map named by has image exactly . It reaches all descendants of , and every equivalent primitive ancestor is its transport along a bijection. It is therefore pointwise surjective onto and is epic as a map of sheaves. We obtain the primitive decomposition of an atomic finite-surjection sheafThis includes the empty coproduct for an empty sheaf.
Each nonempty is an atom in a topos. If a sheaf subobject has an element at some , membership descends along the covering surjection , so belongs to . All its restrictions then belong to , giving . Thus every subobject of any selects entire components of this coproduct, and its complementary selection is again a sheaf subobject. Its characteristic map sends selected components to and all others to .
The constant two-element presheaf is a sheaf: a matching family on a nonempty sieve has the same value on all its arrows, since any two have a common refinement. The value extends uniquely. It therefore supplies these characteristic maps, with truth the inclusion of the value. Equivalently, a J-closed sieve here is either empty or maximal, because every nonempty sieve covers. Hence
Let be a small skeleton of the finitely presented models of an algebraic theory. The classifying topos assertion means that for every Grothendieck topos there is an equivalencenatural under inverse image along geometric morphisms. On the left, morphisms are transformations between inverse image functors, and on the right they are model homomorphisms. A model in interprets the sorts by objects, the operations by arrows, and the equations by equality of the resulting arrows. Finite products suffice for these algebraic operations.
The generic model of an algebraic theory is the tautological covariant functor: for each sort its component iswith all operations interpreted pointwise. Pulling back by a geometric morphism gives its classified model. For a single-sorted theory, this is simply the underlying-set functor with its pointwise algebraic structure.
The orientation is important: is the presheaf topos on , and the generic model is covariant on finitely presented algebras. Such an algebra is a finite-generator, finite-relation presentation. In the algebraic syntactic category it corresponds to the formula imposing its relations, with arrows reversed. The finite-presentability/filtered-colimit description of algebraic models gives the above classifying equivalence; a detailed proof is not needed for this part.
Take to be the category of finitely presented commutative rings with identity, and put . In its presheaf topos, the tautological ring is generic. The additional domain axioms are coherent sequents, so they are imposed by a quotient-theory coverage on .
Concretely, declare the zero ring covered by the empty family. For every finitely presented and elements with , declare the two opposite quotient arrows associated withto be a covering family at . These quotient rings are finitely presented. Pullback and transitivity generate a Grothendieck topology from these families. The empty cover forbids ; the two quotient covers make every zero product locally have a zero factor. Conversely, any internal integral domain satisfies exactly the continuity conditions prescribed by these generating covers. Thusand its generic domain is the associated sheaf , with the ring operations transported through the left-exact sheaf reflector.
This coverage is not standard, meaning not all representables are sheaves; in modern terminology it is not subcanonical. For an explicit obstruction, use and . The two quotient arrows are the same map , so their generated sieve is a singleton cover. Consider the representable on corresponding to :Its distinct sections and become equal after restriction to . Hence this representable is not even separated for . The nilpotent element has to disappear in the generic domain, which explains this failure of standardness.
Work in the domain-classifying site of part (ii), with generic domain . For finitely presented rings , the object is an available stage. Tuples of sections of are locally represented by tuples of actual elements of , because is locally surjective and sheafification preserves finite products. It is therefore enough to prove the requested implication on such representatives.
We first note the empty-cover criterion for the domain-classifying site: is initial if and only if the finitely presented ring is the zero ring. One direction is the generating empty cover. Conversely, any nonzero ring has a maximal ideal and hence a homomorphism to a field. That field is a set-based integral domain and defines a point of the classifying topos. The inverse image of at this point is , which is nonempty for the chosen field . It therefore cannot be the inverse image of an initial object. This uses only the ordinary maximal-ideal existence principle externally, not excluded middle in the internal logic.
Suppose represent a tuple lying in the negation of the all-units subobject. Write and consider the finitely presented localization of a ringEvery is invertible in , since is an inverse. But the pulled-back tuple still lies in the negation of the all-units subobject. Thus the whole stage maps into both that subobject and its negation, forcing this stage to be initial. The empty-cover criterion gives .
The localization is zero precisely when in for some integer , by the equality criterion in localization. Repeated use of the generating zero-product covers now gives a covering familyIndeed, splitting and inducting first forces locally; splitting the product then forces one locally. More formally the two inductions are coherent derivations from the zero-product axiom, so their quotient families belong to the generated topology. The sheaf semantics of disjunction consequently givesThis is the finite-tuple weak-field property of the generic integral domain. The argument is intuitionistically valid inside the topos, although its description of the site uses ordinary external set theory. There is no appeal to preservation of negation by an arbitrary geometric inverse image.
For the converse assertion, let be any internally nontrivial commutative unital ring satisfying the implication. Assume . If and were both units, multiplying by their two inverses would give , contradicting nontriviality. ThereforeThe assumed two-variable implication then gives . Together with nontriviality this is exactly the internal integral-domain axiom. Hence a nontrivial ring satisfying the two-variable case is an integral domain.
For example, the ordinary integral domain fails the one-variable implication at . This does not contradict the generic result: the displayed implication uses negation and is non-coherent, so it need not survive the inverse image that classifies an arbitrary set-based domain.
Articles by others on the same topic
There are currently no matching articles.