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 .
Articles by others on the same topic
There are currently no matching articles.