Let have the diagonal right monoid action , and put . Define the right action on this set of equivariant maps of monoid sets byIt really stays in : . Also and , so it satisfies the right-action law. Left multiplication in the first argument is intentional; no commutativity of has been assumed.
Define the evaluation map of an exponential objectIt is equivariant, becauseFor any right -set and equivariant map , define its currying byFor fixed , this is equivariant in the diagonal variables: . The map is also equivariant, sinceIt satisfies .
Conversely, given an equivariant , set . Evaluation makes this equivariant, and currying recovers :These constructions are inverse and natural in . Therefore they establish the exponential object universal propertyThis is the exponential of right monoid actions, not the set of ordinary maps with an arbitrarily guessed action.
When is a group, evaluation at its identity gives a bijection from the previous equivariant-map set to all functions . For an arbitrary function , the inverse construction isIndeed,so is an equivariant map. Conversely, if is equivariant, implies , so for .
Transport the right action from part (a) through this bijection. At its value isThus the exponential of right group actions isFor clarity, the right-action law holds even in a nonabelian group:Evaluation is equivariant because . The underlying functions need not be equivariant; the fixed points of this exponential action are exactly the equivariant functions.
At a point , all restrictions of the constant presheaf of sets are identities. Two representatives and give the same germ precisely when , so its stalk is canonically . The disjoint union of the stalks is therefore the set .
The topology of the associated étale space of a presheaf has basic opens obtained from sections over open . For the constant section , that basic open is . These are exactly the basic opens of the product topology with discrete. Consequently the germ-space identification is a homeomorphism over , and the projectionis a local homeomorphism.
A continuous section over has the form , where is continuous, equivalently locally constant. Its sections form the constant sheaf of sets:The sheaf gluing axiom follows by gluing the functions; continuity is local. This includes being a singleton, even when the constant presheaf's value on the empty open set was . The construction is its sheafification.
A function acts by postcomposition on locally constant functions, defining a functor . It preserves identities and composition.
To prove the adjunction with the global sections functor, let be a sheaf. A sheaf morphism gives a functionConversely, suppose global sections are prescribed for every . For a locally constant , its fibres are disjoint open sets covering . Restrict to and glue these sections. They agree on intersections, which are empty, so unique gluing defines . Restriction to smaller opens commutes with this construction, making a sheaf morphism.
Applying the two constructions successively returns the original data: a locally constant function is locally one of the constant functions, and sheaf morphisms respect those restrictions and unique gluing. Naturality in and follows from postcomposition and restriction. HenceFor an empty space the same proof works: all global sections sets are singletons, and the sheaf category is degenerate. Constant sheaves are generally locally constant rather than globally constant on disconnected opens.
Write and similarly for . The induced inverse-image functor is precomposition:All categorical limits in a presheaf category are computed pointwise. Thus preserves every limit, in particular finite limits.
Because the indexing categories are small and is complete and cocomplete, both Kan extensions along exist. Their universal properties giveFor example their values are the comma-category formulasThe comma categories here are formed in : an object of the first involves there, equivalently in . An object of the second involves there, equivalently in . Keeping the opposite category explicit prevents reversal of the two constructions.
The right-hand adjunction and finite-limit preservation are exactly the axioms for a geometric morphism . The extra left adjoint makes it an essential geometric morphism. On representable presheaves, its left adjoint satisfies , by the Yoneda lemma and the left adjunction. This identifies the induced morphism directly with the original functor .
Present the Grothendieck topos as for a small site. Let be sheafification and the inclusion. The standard sheafification construction supplies , with preserving finite limits. Concretely, matching-family constructions commute with finite limits, and their directed refinement over covering sieves does so as well. Limits of sheaves are computed in the presheaf category, so has finite limits; its colimits are sheafifications of presheaf colimits.
For sheaves , form the presheaf exponentialIt is a sheaf. Indeed, for a covering sieve , one has . Exponential adjunction, sheafification adjunction and left exactness giveThese are the restriction comparisons, proving the sheaf condition. Restricting the presheaf exponential adjunction to sheaves now makes in .
The subobject classifier is the sheaf of J-closed sieves. A sieve on is J-closed when, for every , implies . Pullback of sieves defines its restrictions, and the maximal sieve defines truth. Local sieve data glue by taking the J-closure of their compatible generated sieve; uniqueness follows because membership in a J-closed sieve is local. This proves that is a sheaf.
For a subsheaf , the characteristic morphism sends toThis sieve is J-closed because local membership in a subsheaf descends by its gluing axiom. Pulling truth back recovers exactly . Conversely, pulling back truth along any morphism into gives a subsheaf, and the same formula recovers that morphism. Finite limits, exponentials and this classifier make every Grothendieck topos an elementary topos.
Here are the explicit Heyting operations on subsheaves of an object . Intersections give meets:The top is . Arbitrary joins are local unions:Equivalently, locally lies in one of the , with the index allowed to vary across the covering arrows. This is the J-closure of the pointwise union, or its sheafification. It is the smallest subsheaf containing every , since any such subsheaf must contain sections locally in it.
The bottom is the empty join, namely the initial subobject. Its value at consists of all if the empty sieve covers , and is empty otherwise. This detail matters on sites with empty covers; it is not safe to use an always-empty presheaf as the initial sheaf.
Implication is described without any pointwise-complement assumption:Restrictions preserve this condition. It is also local: pull a covering sieve back along an arbitrary , use membership in on those restrictions, then descend their membership in . Thus it is a subsheaf. It satisfies the defining Heyting algebra adjunctionFor the forward direction take the identity restriction. For the reverse direction every restriction of a section of remains in , so membership in forces membership in . Negation is . These formulas give the complete Heyting algebra structure on ; in general negation is a pseudocomplement rather than a set-theoretic complement.
In a Grothendieck topos defineThe coproduct universal property gives , naturally. Thus . On any sheaf presentation, is the composite of the constant-presheaf functor with sheafification. The former preserves finite limits pointwise, and the latter is left exact, so preserves finite limits. Therefore these functors define a geometric morphism .
For uniqueness, let be any such geometric morphism. Its inverse image is a left adjoint and preserves the terminal object. Every set has the canonical coproduct decomposition , soThese isomorphisms respect all functions between sets, giving a natural isomorphism . The right adjoint is then unique up to the corresponding natural isomorphism, so . There is a unique geometric morphism to sets, up to isomorphism, called the global sections geometric morphism. This also applies to the degenerate topos.
For the covariant category in this part, put and . Its global-sections functor is , the limit of the diagram. If is also an inverse image, it is a left adjoint and preserves all small colimits.
Consider the canonical pointwise-surjective mapAt , the summand contains , so is an epimorphism. In a presheaf topos epimorphisms are regular, and a colimit-preserving functor preserves their coequalizer presentations. Thus is surjective. Since preserves coproducts, some summand has a global element, yielding a section of its unique map . The constant singleton functor is a retract of a covariant representable.
Conversely, if is such a retract in a category, is a retract of , which is evaluation at by the Yoneda lemma. Evaluation preserves colimits pointwise. The colimit comparison for a retract functor is a retract of the evaluation comparison; a retract of an isomorphism is an isomorphism, so preserves all small colimits. It also preserves finite limits because it is representable. A right adjoint can be constructed byFor , precomposition gives , and applying and then gives . The presentation of every functor as a colimit of representables gives . Hence , so is an inverse image and the topos is local.
The retract condition has a precise interpretation as the initial object criterion for a covariant local topos. Write the section as a natural family . Naturality says for every . Put . Then and every satisfies . In the idempotent completion of , the object is initial: an arrow from it to must satisfy , and the identities force ; this arrow exists because and .
Conversely an initial object in the idempotent completion gives that natural family and the retract. ThereforeIf is already idempotent-complete, this is equivalent to an initial object in itself, and is evaluation there. The word is initial, not terminal, because this question uses covariant functors.
One cannot omit idempotent completion for a general small category. Take the one-object category of the monoid with absorbing zero. It has no initial object because its endomorphism set has two elements, but the natural family satisfies for every . Its covariant functor category is local. Concretely, a functor is a set with an idempotent operator, and its global sections are the fixed points of that operator.
For a topological space , there is an equally explicit criterion. If is local, apply to the epimorphism associated with any open cover , regarding the opens as subterminal sheaves. Since is a singleton exactly when , and otherwise empty, coproduct and epimorphism preservation force some .
Thus every open cover of contains itself. Conversely this open cover criterion for a local sheaf topos condition is equivalent to existence of a point whose only open neighborhood is : the union of all proper open sets cannot be all of , so choose outside it. Such a point plainly forces any cover to contain . Empty spaces fail the condition.
At this point, the stalk functor is simply , since there is only one open neighborhood. Its right adjoint is the skyscraper sheaf of setsA morphism is determined exactly by its map , because all proper opens omit . Hence , and preserves finite limits, proving locality. ConsequentlyIn a space this distinguished point is unique and closed. In a space the condition forces to be a singleton. Indistinguishable points in a non- space can all have this property; uniqueness of an actual point is not part of the general criterion.
A geometric formula is built from atomic formulas, including equality, using finite conjunctions, arbitrary set-indexed disjunctions and existential quantification in a finite variable context. Truth is the empty conjunction and falsity the empty disjunction. A geometric theory is a set of sequents between such formulas over a many-sorted signature. The context supplies the universal force of an axiom; unrestricted universal quantification, implication and negation are not formula constructors in this fragment.
These choices are exactly suited to inverse image functors of geometric morphisms. Finite-limit preservation handles equality and conjunction; colimit and image preservation handle disjunction and existential quantification. Therefore an inverse image carries an internal model of a geometric theory to another model.
Construct the geometric syntactic category as follows. Objects are formulas in context , modulo provable renaming and equivalence. A morphism to is an equivalence class of formulas that are provably total and single-valued:The last notation abbreviates componentwise equality. Identity is equality of the context variables; composition is existential conjunction over the intermediate tuple. The category has finite limits, formed through conjunction and equality.
Give it the geometric syntactic topology . A family of arrows represented by into covers whenPullback stability is substitution, and transitivity comes from distributing existential conjunction through the covering disjunctions. Thus the generated sieves define a Grothendieck topology. Empty covers impose the interpretation of falsity as the initial object.
The classifying topos isIts universal model assigns a sort the sheafified representable of , functions their definable graph morphisms and relations their definable subobjects. The syntactic covering conditions make the axioms valid in this model.
For the universal property, interpreting formulas in a model in a Grothendieck topos gives a finite-limit-preserving, -continuous functor : covers go to jointly epimorphic families precisely because the relevant sequents hold. The Diaconescu equivalence for geometric morphisms associates to this functor a geometric morphism . Conversely, pulling back along a geometric morphism gives a model. The constructions on models and their homomorphisms are inverse up to natural isomorphism, yieldingnaturally in . This proves the required classifying property, not merely classification of set-valued models.
Yes, with the Horn/Cartesian-fragment convention. A Horn theory uses positive finite-conjunction sequents and has a Cartesian syntactic category with finite limits. Provably uniquely witnessed existential formulas can also be admitted without changing the finite-limit nature of its semantics. Its internal models are precisely finite-limit-preserving functors from that category.
For a category with finite limits, flat functors into a Grothendieck topos are exactly finite-limit-preserving functors. In sets, the reason is concrete: the category of elements of a covariant left-exact functor is cofiltered. Its terminal object supplies nonemptiness, products supply cones over pairs of elements, and equalizers supply equalizing cones over parallel arrows. Conversely a cofiltered category of elements expresses the functor as a filtered colimit of covariant representables; filtered colimits of sets commute with finite limits. The internal version uses the same cone conditions locally.
The presheaf form of the Diaconescu equivalence for geometric morphisms therefore identifies geometric morphisms intowith internal Horn models, naturally in the domain topos. This is the presheaf classifier of a Horn theory.
Equivalently, using a small skeleton of the category of finitely presented set-based Horn models, the classifier is , with covariant functors. The duality sends a formula to the model generated by its tuple subject to its finite constraints. The presheaf claim does not extend merely because a general geometric or regular theory has no written disjunctions: arbitrary existential witnesses are not uniquely witnessed Horn data.
Morita equivalence of geometric theories means equivalence of their classifying toposes. Equivalently, their categories of models in every Grothendieck topos are equivalent pseudonaturally with respect to inverse image. Agreement only of their set-based model categories, without this natural internal-model structure, is not the definition.
Suppose . A property expressed intrinsically in terms of the topos is the same under either presentation. One can therefore translate a site or logical characterization of that property from into one for . Examples include Booleanity, connectedness, atomicity and the structure of the subtopos lattice. The bridge is the common invariant , rather than an assumed literal identification of the two signatures.
The duality between geometric quotients and subtoposes makes this precise. A geometric quotient theory of adds geometric axioms over the same signature. Quotients are identified when they prove the same geometric sequents. The theorem givesThe subtopos corresponding to is its classifying topos. Stronger axioms correspond to smaller subtoposes under inclusion.
The site mechanism explains the correspondence. On , an additional sequent requires the associated family of definable images to cover its antecedent. Adding these covering sieves produces a topology and a geometric embeddingConversely, subtoposes correspond to such larger topologies; requiring their extra definable covers gives the corresponding deductively closed quotient theory. Pulling the universal model into the subtopos supplies the universal model of the quotient.
Given a quotient , transport its subtopos along the chosen equivalence of classifying toposes. Apply the duality again to obtain a quotient of . Their classifying toposes are equivalent, soThis is an explicit transfer principle for whole families of theory extensions and their order relations. Intrinsic constructions such as open, closed or Boolean subtoposes can likewise be described in each syntax. Different descriptions may look unrelated, but their equality is explained by the common subtopos. No universal translation of individual formulas is asserted without choosing the relevant equivalence and interpretations.
Articles by others on the same topic
There are currently no matching articles.