Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

June 19, 2011

Flat Functors and Morphisms of Sites

Posted by Mike Shulman

There’s something about the notion of flat functor that confused me vaguely in the background for a long time. Eventually I tracked it to its source: the same term is used with two slightly different meanings! As a preview of part of my CT2011 talk, today I’ll explain what those meanings are, and how a mutual generalization of them gives us a better notion of “morphism of sites”.

The starting point is that a Set-valued functor F:CSetF\colon C \to Set is flat if its category of elements is cofiltered. If CC has finite limits, then this is equivalent to FF preserving them; thus a flat functor “would preserve all finite limits if they existed.” This is also a reasonable thing to say because F:CSetF\colon C\to Set is flat if and only if the induced functor [C op,Set]Set[C^{op},Set] \to Set preserves finite limits (which [C op,Set][C^{op},Set] always has, unlike CC). In topos-theoretic terms, F:CSetF\colon C\to Set is flat if and only if the induced adjunction Set[C op,Set]Set \leftrightarrows [C^{op},Set] is a geometric morphism; thus flat functors F:CSetF\colon C\to Set are equivalent to points of the presheaf topos [C op,Set][C^{op},Set].

Now let’s generalize this to codomain categories other than SetSet. Starting from the first definition, a natural line of thought might go like this. The category of elements of F:CSetF\colon C\to Set is the same as the comma category (1/F)(1/F), where 11 is the 1-element set. In particular, it only knows about maps from 11 into the images of FF—but this is enough to characterize finite limits in SetSet. With a codomain other than SetSet, therefore, we may expect to need maps out of all objects rather than just out of 11.

Thus, it seems reasonable to define a functor F:CDF\colon C\to D to be representably flat if for each dDd\in D, the comma category (d/F)(d/F) is cofiltered—or equivalently, if the functor Hom D(d,F()):CSetHom_D(d,F(-))\colon C \to Set is flat. (This is often called just “flat”, but I’m adding an adjective for clarity later on.) If CC has finite limits, then FF is representably flat if and only if it preserves them.

This notion of flatness has some nice properties. For instance, if CC has finite limits, then F:CDF\colon C\to D is representably flat if and only if it preserves them. Moreover, if CC and DD are small, then F:CDF\colon C \to D is representably flat if and only if the induced functor Lan F:[C op,Set][D op,Set]Lan_F\colon [C^{op},Set] \to [D^{op},Set] preserves finite limits. Therefore, if CC and DD are small sites and F:CDF\colon C \to D is representably flat, then the composite of Lan FLan_F with sheafification provides a left-exact left adjoint to F *:Sh(D)[C op,Set]F^\ast\colon Sh(D) \to [C^{op},Set]. If FF also preserves covers, then F *F^\ast lands inside Sh(C)Sh(C), so in this case we have an induced geometric morphism Sh(D)Sh(C)Sh(D) \leftrightarrows Sh(C). Thus, one often defines a morphism of sites to be a representably flat functor which preserves covers (cf. for instance C2.3.7 in Sketches of an Elephant).

On the other hand, however, the fact that points of [C op,Set][C^{op},Set] are equivalent to flat functors F:CSetF\colon C\to Set suggests that [C op,Set][C^{op},Set] should be the classifying topos for flat functors defined on CC. That is, for any (Grothendieck) topos EE, geometric morphisms E[C op,Set]E \to [C^{op},Set] should be equivalent to “flat functors defined on CC” internal to EE. This is true as long as we define “flat functors defined on CC internal to EE” correctly. The straightforward approach is to write down a geometric theory whose models in SetSet are flat Set-valued functors.

If you like geometric logic, that’s a nice exercise, but it just comes out to a functor F:CEF\colon C \to E with the following property. For any finite diagram G:ICG\colon I\to C, consider the family of all cones Δ(x)G\Delta(x)\to G over GG in CC. Each of these cones induces a cone Δ(Fx)FG\Delta(F x) \to F G in EE, which therefore factors through the limit limFG\lim F G (which, of course, exists in EE). We then ask that the family of all these factorizations is jointly epimorphic onto limFG\lim F G.

This is just the notion of flatness for a Set-valued functor, rephrased in terms of diagrams. Let’s call such a functor internally flat; then geometric morphisms E[C op,Set]E \to [C^{op},Set] are equivalent to internally flat functors CEC\to E. More precisely, F:CEF\colon C\to E is internally flat if and only if the induced functor [C op,Set]E[C^{op},Set] \to E preserves finite limits, which is a natural generalization of the characterization of flat Set-valued functors we started from. See for instance VII.7-8 of Sheaves in Geometry and Logic, and B3.2.3 of Sketches of an Elephant.

Now, representable flatness and internal flatness are not the same! In fact, even for Set-valued functors, internal-flatness is equivalent to flatness in the original sense, but representable flatness is a good deal stronger (although of course they agree when the domain CC has finite limits).

Exercise: Find a functor F:CSetF\colon C\to Set which is internally, but not representably, flat.

I don’t know about you, but I find this a bit bothersome, especially since people don’t usually put adjectives like “representably” and “internally” in front of “flat” to clarify which notion they mean. However, I got much happier about it when I realized that representable and internal flatness are actually two special cases of a single general notion.

To wit, suppose that CC is a category and DD is a site, and define F:CDF\colon C\to D to be covering flat if, for any finite diagram G:ICG\colon I\to C, and any cone T:Δ(u)FGT\colon \Delta(u) \to F G over FGF G in DD, the sieve

{h:vu|there exists a cone S:Δ(w)G such that Th factors through F(S)} \{ h\colon v \to u \;|\; \text{there exists a cone }\; S\colon \Delta(w) \to G \;\text{ such that }\; T h \;\text{ factors through }\; F(S) \}

is a covering sieve of uu in DD.

Let’s see how this reproduces representable flatness and internal flatness. First, suppose DD is a Grothendieck topos with its canonical topology, whose covering sieves are the jointly epimorphic ones. Then for any G:ICG\colon I \to C, the limiting cone Δ(limFG)FG\Delta(\lim F G) \to F G is a particular cone TT (as in the definition of covering flatness). In that case, the sieve in question is generated by the family of all factorizations through limFG\lim F G of cones over GG in CC. Thus, covering flatness implies that this family is jointly epic, which is internal flatness. Covering flatness appears to say even more than this, since it refers to any cone over FGF G; but when FGF G has a limit, it suffices to consider the limiting cone, since covering sieves are stable under pullback. So when the codomain is a topos (such as SetSet) with its canonical topology, covering flatness reduces to internal flatness.

Second, suppose DD has the trivial topology, in which a sieve is covering just when it contains a split epimorphism. Then covering flatness asserts that for any G:ICG\colon I \to C and any cone T:Δ(u)FGT\colon \Delta(u) \to F G, there exists a cone S:Δ(w)GS\colon \Delta(w) \to G such that TT factors through F(S)F(S) (since there is some hh in the above sieve which is split epic). But GG and TT together are precisely a finite diagram in (u/F)(u/F), and SS such that TT factors through F(S)F(S) is precisely a cone over this diagram in (u/F)(u/F). Thus, when the codomain has a trivial topology, covering flatness reduces to representable flatness.

So that’s nice, but can we do anything else with covering flatness? Well, recall that one of the uses of representable flatness was to define morphisms of sites. If F:CDF\colon C \to D is representably flat, then Lan F:[C op,Set][D op,Set]Lan_F\colon [C^{op},Set] \to [D^{op},Set] preserves finite limits; hence if DD is a site then so does the composite [C op,Set]Lan F[D op,Set]sheafifySh(D) [C^{op},Set] \xrightarrow{Lan_F} [D^{op},Set] \xrightarrow{sheafify} Sh(D) since sheafification always preserves finite limits. But at least a priori, representable flatness is more than we need for this, since we don’t actually need Lan FLan_F itself to preserve finite limits, only its composite with sheafification. The weaker notion of covering flatness is exactly right!

Exercise: Prove that if CC is a small category and DD is a small site, then a functor F:CDF\colon C \to D is covering flat if and only if the composite [C op,Set]Lan F[D op,Set]sheafifySh(D) [C^{op},Set] \xrightarrow{Lan_F} [D^{op},Set] \xrightarrow{sheafify} Sh(D) preserves finite limits.

Therefore, if we were to define a morphism of sites F:CDF\colon C \to D to be a functor which is (1) covering flat and (2) cover-preserving, this would be sufficient to induce a geometric morphism Sh(D)Sh(C)Sh(D) \to Sh(C). I don’t know whether there are any especially interesting functors which are morphisms of sites in this sense but not the classical one, but the extra generality is aesthetically pleasing and formally convenient. For instance, one nice thing is that the inclusion of any dense sub-site is always a morphism of sites in the new sense, though not necessarily in the classical one.

More importantly, this notion of “morphism of sites” now matches exactly the corresponding theory for classifying topoi. Recall that when EE is a topos, geometric morphisms E[C op,Set]E\to [C^{op},Set] are equivalent to internally flat, or equivalently covering flat, functors CEC\to E. If CC is moreover itself a small site, then geometric morphisms ESh(C)E\to Sh(C) are classically known to correspond to internally/covering flat functors which are also cover-preserving—in other words, morphisms of sites in the new sense, where EE is equipped with its canonical topology. That means that modulo size issues (which I’ll address in my CT talk), the functor

Sh():SiteTopos op Sh(-) \colon Site \to Topos^{op}

(where SiteSite is defined using the new notion of morphism of sites) is left adjoint to the forgetful functor

U:Topos opSite U\colon Topos^{op} \to Site

which sends a topos to its underlying category equipped with its canonical topology, and a geometric morphism to its inverse image functor. But things are actually even better than that, because UU is fully faithful: a functor between Grothendieck topoi is the inverse image functor of a geometric morphism precisely when it is a morphism of sites for the canonical topologies. In other words, the (2-)category of topoi is a reflective subcategory of the (2-)category of sites.

I’ll finish with a puzzle for the reader, connecting the new notion of covering flatness back to the original intuition for flat functors.

Puzzle: Under what conditions on CC and DD can we say that F:CDF\colon C\to D is covering flat if and only if it preserves finite limits? (Hint: we need some conditions on DD in addition to CC.)

Posted at June 19, 2011 3:26 AM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2411

60 Comments & 1 Trackback

Re: Flat Functors and Morphisms of Sites

representable and internal flatness are actually two special cases of a single general notion.

[…]

the inclusion of any dense sub-site is always a morphism of sites in the new sense

[…]

the (2-)category of topoi is a reflective subcategory of the (2-)category of sites [with the new morphisms of sites].

That’s nice. It gives a refined precise sense of how Sh():Site opToposSh(-) : Site^{op} \to Topos is a completion operation.

Have you thought about possible higher analogs of this definition of covering-flat functors?

Posted by: Urs Schreiber on June 21, 2011 10:13 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Have you thought about possible higher analogs of this definition of covering-flat functors?

Yes; my current thought is that the higher analogue should be the entirely straightforward thing. But I haven’t had time to start writing down the details yet.

Posted by: Mike Shulman on June 21, 2011 6:01 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Thanks, Mike. This is something I’ve wanted to get straight for years, and hopefully your post will help me to do so. (I haven’t had time to read it properly yet.)

There’s some confusion between “flat” and “representably flat” in Borceux’s Handbook. He gives the usual definition of flatness for a SetSet-valued functor, then defines an arbitrary functor F:ABF: A \to B to be flat if the composite

AFBB(b,)Set A \stackrel{F}{\to} B \stackrel{B(b, -)}{\to} Set

is flat for all bBb \in B. (This is what you call representably flat.) But he doesn’t note—though I’m sure he knows it—that the two definitions contradict each other when B=SetB = Set.

Posted by: Tom Leinster on June 21, 2011 12:50 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

A Grothendieck topology on a small category CC amounts to a subtopos of Psh(C)=Set C opPsh(C) = Set^{C^{op}}, or equivalently a finite limit-preserving idempotent monad on Psh(C)Psh(C). So, a (small) site amounts to a pair (C,T)(C, T) where CC is a small category and TT is a finite limit-preserving idempotent monad on Psh(C)Psh(C).

This suggests a way of defining “morphism of sites”.

If it weren’t for the qualification “finite limit-preserving idempotent”, I’d have little hesitation in defining a morphism (C,T)(D,U)(C, T) \to (D, U) to be a functor f:CDf: C \to D together with a natural transformation making f *=Ran F:Psh(C)Psh(D)f_* = Ran_F: Psh(C) \to Psh(D) into a lax map of monads, or equivalently a natural transformation making f *=f:Psh(D)Psh(C)f^* = -\circ f: Psh(D) \to Psh(C) into a colax map of monads.

If I’m not mistaken, idempotency means that there can be at most one such natural transformation (given ff). In that case, a morphism (C,T)(D,U)(C, T) \to (D, U) of sites is a functor f:CDf: C \to D satisfying a property, not carrying extra structure.

I’m too lazy right now to complete the thought. We have to decide what to do about “finite limit-preserving”. Does that mean the natural transformation part of the colax map of monads ought to be cartesian? (That could make the property to be satisfied by ff more demanding.) In any case, we should do exactly what’s necessary to arrange that the commutative square of functors

Psh(C) T Psh(D) U Psh(C) Psh(D) \begin{matrix} Psh(C)^T &\to &Psh(D)^U \\ \downarrow & &\downarrow \\ Psh(C) &\to &Psh(D) \end{matrix}

induced by the lax map of monads (C,T)(D,U)(C, T) \to (D, U) is in fact a commutative square of geometric morphisms.

Is that what your definition of “morphism of sites” achieves?

Posted by: Tom Leinster on June 21, 2011 3:07 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Let me try to say that more intelligibly.

A (small) site can be defined as a small category CC together with an idempotent monad on Psh(C)=Set C opPsh(C) = Set^{C^{op}} whose functor part preserves finite limits. By general stuff about idempotent monads, such a monad TT amounts to a full subcategory of Psh(C)Psh(C) for which the inclusion has a finite limit-preserving left adjoint. That subcategory is the category of TT-algebras, and the inclusion is the forgetful functor. And in the standard terminology, that subcategory is the category of sheaves on the site.

Now take two such things, (C,T)(C, T) and (D,U)(D, U). We want to find a good notion of morphism (C,T)(D,U)(C, T) \to (D, U).

A lax map of monads (a.k.a. monad functor) (Psh(C),T)(Psh(D),U)(Psh(C), T) \to (Psh(D), U) is a functor F:Psh(C)Psh(D)F: Psh(C) \to Psh(D) together with a natural transformation UFFTU F \to F T satisfying coherence axioms. It can also be described as a functor Psh(C) TPsh(D) UPsh(C)^T \to Psh(D)^U on categories of algebras (sheaves) such that the square

Psh(C) T Psh(D) U Psh(C) F Psh(D) \begin{matrix} Psh(C)^T&\to&Psh(D)^U\\ \downarrow&&\downarrow\\ Psh(C)&\stackrel{F}{\to}&Psh(D) \end{matrix}

commutes. Because the monads are idempotent, the vertical arrows are inclusions, so there is at most one such functor for each FF. That is, being a lax map of monads is a property of FF, not extra structure.

Now our categories are of a special form (PshPsh of something), so our functor FF should be of a special form: PshPsh of something, that is, f *=Ran ff_* = Ran_f for some functor f:CDf: C \to D. Now all three functors in this square except perhaps the top one are the direct image parts of geometric morphisms. It seems natural to demand that the top one should be a geometric morphism too.

So: I think a morphism (C,T)(D,U)(C, T) \to (D, U) of sites should be a functor f:CDf: C \to D such that f *:Psh(C)Psh(D)f_*: Psh(C) \to Psh(D) restricts to a functor Sh(C)Sh(D)Sh(C) \to Sh(D) (i.e. Psh(C) TPsh(D) UPsh(C)^T \to Psh(D)^U), and that restricted functor has a finite limit-preserving left adjoint.

That condition on ff could be reformulated in terms of covering sieves. I’d like to know if it’s the same as Mike’s notion, or perhaps the standard notion. I could probably figure it out for myself, but maybe someone will want to do it for me :-)

Posted by: Tom Leinster on June 21, 2011 4:20 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

I think you’ve got your variance a bit mixed up. A functor f:CDf\colon C\to D induces two adjunctions between presheaf categories:

Lan f:Psh(C)Psh(D):f * Lan_f : Psh(C) \rightleftarrows Psh(D) : f^*

f *:Psh(D)Psh(C):Ran f f^* : Psh(D) \rightleftarrows Psh(C) : Ran_f

Of these, the second is always a geometric morphism Psh(C)Psh(D)Psh(C) \to Psh(D) in the same direction as ff, while the first is a geometric morphism Psh(D)Psh(C)Psh(D) \to Psh(C) in the opposite direction to ff precisely when Lan fLan_f is left exact, i.e. when ff is representably flat.

Now, given topologies on CC and DD, we can ask either of those two adjunctions to induce a geometric morphism between sheaf topoi. I claimed in my post that ff is a morphism of sites, in the new sense I’m proposing (covering-flat and cover-preserving), if and only if (1) f *f^\ast maps Sh(D)Sh(D) into Sh(C)Sh(C) and (2) the composite Sh(C)Lan fPsh(D)sheafifySh(D)Sh(C) \xrightarrow{Lan_f} Psh(D) \xrightarrow{sheafify} Sh(D) is left exact, so that the first adjunction becomes a geometric morphism Sh(D)Sh(C)Sh(D) \to Sh(C). The point of the new definition, though, is that ff need not be representably flat, so that there is no geometric morphism Psh(D)Psh(C)Psh(D) \to Psh(C) at all.

(I should perhaps point out that for sites with finite limits, the new and old definitions of “morphism of sites” coincide, and all of these facts are well-known. Cf. for instance C2.3.8 of Sketches of an Elephant. The theorem that “toposes are a reflective subcategory of sites” is stated for finitely-complete sites in C2.3.9.)

On the other hand, asking the second adjunction to induce a geometric morphism Sh(C)Sh(D)Sh(C) \to Sh(D) is a different sort of condition on ff; Johnstone calls it being cover-reflecting. The theorem that this exactly classifies for which ff you get a geometric morphism Sh(C)Sh(D)Sh(C) \to Sh(D) is C2.3.18. Since f *f^* is always left exact, in this case there is no flatness condition on ff required.

Posted by: Mike Shulman on June 21, 2011 5:32 PM | Permalink | PGP Sig | Reply to this

Re: Flat Functors and Morphisms of Sites

Mike wrote:

I think you’ve got your variance a bit mixed up.

So I did.

The (usual) relationship between topological spaces and toposes is covariant. The relationship between topological spaces and sites is contravariant. So, the relationship between sites and toposes is contravariant. But in my previous comment, I was looking for a covariant relationship.

Thanks for the clarification of this and other points.

Posted by: Tom Leinster on June 26, 2011 12:23 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Tom wrote:

A Grothendieck topology on a small category CC amounts to a subtopos of Psh(C)=Set C opPsh(C) = Set^{C^{op}}, or equivalently a finite limit-preserving idempotent monad on Psh(C)Psh(C).

Two beginner’s questions:

1) Is that idempotent monad called ‘sheafification’? If I sheafify a presheaf twice, it’s the same as sheafifying once, so that sounds like an idempotent monad. And a Grothendieck topology determines, and maybe even is determined by, a process of sheafification.

2) Is that idempotent monad called a ‘Lawvere–Tierney topology’? I’ve never understood those at all, though Jim Dolan tried to explain them to me a long long time ago.

I originally decided to post this question just because I vaguely remembered that there was something idempotent about Lawvere–Tierney topologies. But then I peeked at the nLab entry and read:

If CC is a small category, then choosing a Grothendieck topology on CC is equivalent to choosing a Lawvere–Tierney topology in the presheaf topos Set C opSet^{C^op} on CC.

So now it looks like the answer to question 2) is yes.

If the answers to questions 1) and 2) are both yes, I’ll be really happy. Since that ancient conversation with Jim, I’ve become comfortable with sheafification. So I’d be delighted if a ‘Lawvere-Tierney topology’ turned out to be nothing but a sheafification functor.

Posted by: John Baez on June 25, 2011 10:06 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

1) Yes. (And, therefore, a Grothendieck topology is indeed determined by the sheafification monad that it induces.)

2) No, although there is a canonical one-to-one correspondence between the two things you’re asking about: finite-limit-preserving idempotent monads on Psh(C)Psh(C) and Lawvere–Tierney topologies on Psh(C)Psh(C).

A Lawvere–Tierney topology on a topos EE is usually defined as a map j:ΩΩj: \Omega \to \Omega satisfying certain axioms. The answer to your question 2 must be no, because a Lawvere–Tierney topology on Psh(C)Psh(C) is not of the same type as a monad on Psh(C)Psh(C). But perhaps you’ll be moderately happy that the two things correspond canonically to one another, even though they’re not literally the same.

For an arbitrary topos EE, there’s a canonical one-to-one correspondence between the following three things:

  • subtoposes of EE
  • finite-limit-preserving idempotent monads on EE
  • Lawvere–Tierney topologies on EE.

When EE is a presheaf category Psh(C)=Set C opPsh(C) = Set^{C^{op}}, a fourth item can be added to the list:

  • Grothendieck topologies on CC.

Starting from a Grothendieck topology JJ on CC, the corresponding subtopos of Psh(C)Psh(C) is Sh(C,J)Sh(C, J), and the corresponding monad on Psh(C)Psh(C) is sheafification. I don’t know a very compelling way to describe the corresponding Lawvere–Tierney topology.

Posted by: Tom Leinster on June 25, 2011 4:10 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

For an arbitrary topos E, there’s a canonical one-to-one correspondence between the following three things:

One other thing I would add to that list:

  • Universal closure operators

A universal closure operator consists of, for every object XX, a closure operator (= a monad, necessarily idempotent) on the poset Sub(X)Sub(X) of subobjects of XX, which is preserved by pullback. By the Yoneda lemma, since Ω\Omega classifies subobjects, this is the same as a map j:ΩΩj\colon \Omega \to \Omega satisfying suitable properties, i.e. a Lawvere-Tierney topology.

Starting from a Grothendieck topology J on C, the corresponding subtopos of Psh(C) is Sh(C,J), and the corresponding monad on Psh(C) is sheafification.

And the corresponding universal closure operator is “relative sheafification” — that is, it closes up a sub-presheaf under all gluings that exist in the containing presheaf.

I don’t know a very compelling way to describe the corresponding Lawvere–Tierney topology.

It’s the classifying map of the Grothendieck topology!

Recall that Ω\Omega in a presheaf category is the object of sieves: for each cCc\in C, Ω(c)\Omega(c) is the set of sieves on cc (that is, sieves in C/cC/c). Since Ω\Omega is the subobject classifier, a map j:ΩΩj\colon \Omega\to\Omega classifies a subobject JΩJ\hookrightarrow \Omega, and in this case it turns out that J(c)J(c) is the set of covering sieves on cc. The axioms satisfied by a collection of covering sieves to be a Grothendieck topology correspond exactly to the axioms on an endomorphism of Ω\Omega in a presheaf category to be a Lawvere-Tierney topology.

Posted by: Mike Shulman on June 25, 2011 5:15 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

It’s the classifying map of the Grothendieck topology!

Of course. Indeed, I wrote exactly that in my informal introduction. Not at my best today.

Posted by: Tom Leinster on June 25, 2011 6:02 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

I had a day like that this week too. At lunch I explained to someone why the double-negation of the law of excluded middle is still valid intuitionistically. Then in the afternoon, I couldn’t remember how to prove that “for all P, not-not-P implies P” is equivalent to LEM.

Posted by: Mike Shulman on June 25, 2011 6:23 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

The subobject JΩJ \rightarrowtail \Omega may also be obtained by taking the subobject :1Ω\top \colon 1 \rightarrowtail \Omega—which picks out the maximal sieve on each object—applying the sheafification functor LL to it, so obtaining a subobject L1LΩL1 \rightarrowtail L\Omega, and pulling this back along the unit ΩLΩ\Omega \to L\Omega.

Posted by: Richard Garner on June 27, 2011 2:03 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

I’m glad to see the technical difficulties have been resolved, Richard, so that you’re able to post here again. (That is, if they have been resolved—maybe it’s just Mike pretending to be you.)

I don’t doubt the correctness of what you write, but I hope you don’t mind if I use it as a springboard for explaining something I find offputting about topos theory. It always seems to be full of calculations. Yes, sure, there are some wonderful big concepts in the subject, and that’s very attractive. But it also seems to carry a heavy weight of calculation.

For example, I have that difficulty when it comes to Lawvere–Tierney topologies. Sure, I can prove that the various things listed here all correspond one-to-one with each other, but certain parts of the proof seem like meaningless algebraic manipulation to me, of the sort that many category theorists might sneer at if it were differential equations rather than arrows. I’d like something conceptual instead.

I’m sure that’s my own lack of understanding, and that it’s not meaningless to everyone. But whenever I see an argument in topos theory that says something like “apply this functor, pull back along this, factorize like that”, I kind of internally groan and think “I’ll never be a topos theorist”.

Posted by: Tom Leinster on June 27, 2011 2:55 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Well, in fact, I am going through a proxy at the moment; it seems that the site is still blocking the IP address from which I would normally post…

I agree that there is a certain amount of fiddle in topos theory. But I think there are good conceptual explanations behind most of the things involved, even if those are not on the face of it entirely apparent.

For instance, the fact that I just cited about JJ is really just obtained by combining some general facts about reflective subcategories which can be found in [Cassidy, Hebert and Kelly 1985] together with the definition of subobject classifier.

Given any category CC and a reflective subcategory DCD \hookrightarrow C, the subcategory DD can be reconstructed as the full subcategory of objects orthogonal to the class of maps \mathcal{E} which are inverted by the reflector L:CDL \colon C \to D; thus to know LL it is enough to know \mathcal{E}. This is a classical and well-known fact.

If CC has finite limits, and LL preserves pullbacks along maps in the subcategory DD (this condition is called semi-left-exactness by Cassidy, Hebert and Kelly), then the \mathcal{E}-maps are the left class of an orthogonal factorisation system on CC. The \mathcal{M}-maps may be characterised either as the pullbacks in CC of maps in DD, or as the maps of CC at which the naturality square of the reflector 1L1 \to L is cartesian. Thus in this case, to know LL, it is enough to know \mathcal{M}.

On the other hand, if CC has finite limits and LL preserves kernel-pairs, then DD can in fact be reconstructed as the subcategory orthogonal to all the monomorphisms inverted by LL; this is, for example, Lemma A4.3.6 in the Elephant. Thus in this case, to know LL it is enough to know the monomorphisms in \mathcal{E}.

Combining the previous two cases, if the semi-left-exact LL preserves kernel-pairs, then it in particular preserves monomorphisms, and so the (,)(\mathcal{E}, \mathcal{M})-factorisation system on morphisms restricts to one on monomorphisms. Thus in this case, it suffices to know the monomorphisms in \mathcal{M}.

If moreover LL preserves all pullbacks, then the \mathcal{E}- as well as the \mathcal{M}-maps are stable under pullback. So if CC now has a subobject classifier, then the (,)(\mathcal{E}, \mathcal{M}) factorisation of an arbitrary monomorphism m:ABm \colon A \rightarrowtail B is obtained by pulling back that of the generic subobject :1Ω\top \colon 1 \rightarrowtail \Omega along the classifying map of mm. So in this case, it is enough to know the \mathcal{M} part of the (,)(\mathcal{E}, \mathcal{M})-factorisation of \top.

And what is this? Well, as for any (,)(\mathcal{E}, \mathcal{M}) factorisation obtained from a semi-left-exact LL, the \mathcal{M}-part is obtained by first applying LL to the map in question, and then pulling back along the unit of the reflector at the codomain. In other words, one takes L()L(\top) and pulls it back along ΩLΩ\Omega \to L \Omega; and this is the description of JΩJ \rightarrowtail \Omega that I gave previously.

Posted by: Richard Garner on June 27, 2011 10:12 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

I’m not sure how applicable this is to the specific examples in question, but I’ve found that

  1. many complicated manipulations of limits and colimits used in topos theory are just “diagrammatic” translations of proofs that would be obvious and “follow-your-nose” when phrased in the category of sets, and

  2. in such cases, the diagrammatic manipulations can usually be completely replaced by just performing the proof with sets, in a constructive and structural way, and then waving the wand called “internal logic”.

I find that this immensely simplifying fact is obscured in many books on topos theory, perhaps because the internal logic is viewed as a complicated thing which must be postponed until the end. True, the idea of internal logic may be a bit difficult to grasp at first, justifying its postponement in an introductory work, but I think it should be emphasized more that once it is introduced, it greatly simplifies many things. (There are at least some hints of this in Sketches of an Elephant.)

(By the way, generalizing the internal logic to the stack semantics expands this to include even more situations, including the theory of arbitrary indexed categories over a topos.)


I will now indulge myself by relating a personal anecdote, allowing me a springboard to ask another unrelated question. (-: At OPLSS, where I am right now, someone brought up the fact, easily proven in classical logic, that any endomorphism of the set {true,false}\{true, false\} of truth values must be equal to its cube, f=ffff = f\circ f \circ f. The question was then asked, is anything analogous true in intuitionistic logic? Peter Lumsdaine remembered an exercise from Johnstone’s book Topos theory, which, when we tracked it down, turned out to say that in an (elementary) topos, any monic endomorphism of the subobject classifier is its own inverse, 1=ff1 = f\circ f.

The exercise came along with a three-step hint for how to prove it, which involved first showing that some square is a pullback, then showing that some other square commutes, and finally deducing the result. Peter Lumsdaine and I did the exercise separately and then compared notes, and unsurprisingly, we’d both chosen to rephrase the hint in terms of the internal logic, rather than working with pullback squares and so on. Each step of the hint more or less proved itself when working in the internal logic, but I’d have to think for a while to figure out how to rephrase the argument in terms of pullback squares.

But now my unrelated question: unfortunately, although the proof (using the hint) was straightforward, it didn’t give us any intuition for why such a thing must be true! Anyone have any ideas?

Posted by: Mike Shulman on June 27, 2011 5:30 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Mike, I agree: the magic wand called “internal logic” is a wonderful thing, and (for my taste) should be waved much more often. And I’m not just talking about topos theory here.

The referee for my “informal introduction” suggested that I include more material about topos theory as generalized set theory. I’ve just submitted a revised version which does just that. The new material is along the same lines as a (pretty rough) set of notes that I wrote for a friend a while back. They’re essentially about the internal logic of finite product categories, though phrased in a very down-to-earth way.

My friend’s situation was that she knew that some rather complicated identities held for ordinary groups, and wanted to know whether there was a way of deducing that they held for arbitrary internal groups without drawing some massive diagrams. The notes were my way of saying “yes”.


I don’t have any original thoughts on endomorphisms of Ω\Omega, but I do have Volume 9, No. 1 of Algebra Universalis. This contains the following article:

P. T. Johnstone, Automorphisms of Ω\Omega.

Abstract. Let EE be a topos, with subobject classifier Ω\Omega. We show that automorphisms of Ω\Omega in EE are in 1-1 correspondence with closed boolean subtoposes of EE, the group operation corresponding to symmetric differences of subtoposes. This helps to explain an earlier result of D. Higgs, which implied that aut(Ω)aut(\Omega) was an elementary abelian group of exponent 2. We also use this result to give an explicit description of aut(Ω)aut(\Omega) when EE is a spatial topos or a topos of presheaves.

Maybe that will help.

Posted by: Tom Leinster on June 27, 2011 5:42 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

P. T. Johnstone, Automorphisms of Ω.

Lovely, thank you! I haven’t read it carefully, but the overall conclusion is a fairly satisfying answer.

Posted by: Mike Shulman on June 28, 2011 6:39 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Mike, interesting post! Regarding your comment about internal logic, could you give some references that have some easy examples of arguments that can be simplified using the viewpoint of internal logic? Whenever I do anything with toposes, I find myself acting as though sheaves are really just sets, as long as you don’t do anything obviously forbidden. I never worried too much about what “obviously forbidden” meant, but now I’m hoping internal logic will tell me an actual answer. (Or if not, it’ll probably help in some other way.)

Posted by: James Borger on June 28, 2011 12:35 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

I also find it useful to think about the “internal logic” in terms of embedding theorems.

For instance, suppose that you want to prove that in any regular category, and for any map f:XYf \colon X \to Y in that topos, on forming the kernel-pair KK of ff and the coequaliser QQ of that, the induced comparison map QYQ \to Y is monomorphic.

Well, this is so in SetSet; whence in any presheaf topos, since finite limits and colimits are pointwise there; but then also in any sheaf topos, since the calculation may be done in presheaves, where it holds, and reflected back down.

This now becomes true in any small regular category, since any such embeds fully into a Grothendieck topos via a functor preserving (and so reflecting) all of the relevant structure. This is a “completeness theorem” for regular logic, if you like.

And in fact, this is enough to make the result true in any regular category CC, as given a particular ff in it for which we wish to verify the above fact, we may take the closure of ff in CC under finite limits and coequalisers of kernel-pairs; the resultant subcategory will then be regular and small, and so by the previous paragraph, will admit an embedding into a Grothendieck topos, using which the desired conclusion may be reflected down into CC.

The corresponding argument in the internal logic is really just a syntactic reformulation of this one (the embedding of the small regular CC into a sheaf topos corresponding to the passage to generalised elements).

Posted by: Richard Garner on June 29, 2011 3:58 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

I’m not trying to start an argument, and obvious I can’t argue anyway with the assertion that you find something useful. But just to provide a diversity of opinions to the bystanders, let me say that I don’t find it useful to think about internal logic in terms of embeddings. (Except, of course, when explaining something like the stack semantics to people who do insist on always thinking in such terms.) It seems to me like making a simple thing complicated to invoke smallness hypotheses, presheaves, sheaves, reflectability, etc. when the internal logic has a straightforward, direct, and first-order definition in terms of the category itself. Not that I have anything against embedding theorems in principle (Steve and I used embedding theorems quite extensively in our work on F-categories), but I think of them as a technical device (and a big hammer) rather than an explanatory tool.

So rather than say that the internal logic argument is a “syntactic reformulation” of the embedding argument, I would say that the embedding argument is a complicated way of rephrasing the internal logic of one category (say, a regular one) in terms of the internal logic of another category (its topos of sheaves) which we might happen to feel more comfortable with (maybe because we’ve “constructed it out sets” somehow). (-:

Also, I think that describing the embedding in the way that you did makes it sound as though there is something magical or universal about Grothendieck toposes among all the sorts of categories that have internal logic, which I don’t think is the case. It just so happens that we care about Grothendieck toposes more than we do about some other kinds of categories, and many interesting fragments of logic happen to embed into the geometric logic of Grothendieck toposes. But, for instance, the higher-order logic of an elementary topos, or the first-order logic of a Heyting category, or even the lambda calculus of a cartesian closed category, does not so embed.

Posted by: Mike Shulman on June 29, 2011 5:37 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

This sounds to me like an echo of an age-old debate which is expressed in the preface (or introduction, I forget which) of Johnstone’s baby Elephant, where he decries a bit the use of embedding theorems à la Freyd. Johnstone seems to prefer direct categorical syntax as getting to the heart of the matter. But embedding theorems obviously have their followers as well, as expressed by Freyd obviously (his book with Scedrov, Categories, Allegories, is a tour de force exposition of the utility of embedding theorems), and also by Barr and Wells in Toposes, Theories, and Triples. I find both sides very interesting.

Posted by: Todd Trimble on June 29, 2011 7:37 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

James wrote:

Mike, interesting post! Regarding your comment about internal logic, could you give some references that have some easy examples of arguments that can be simplified using the viewpoint of internal logic?

I’m not Mike, and I’m sure it’s rude to cite oneself, but I’ll go ahead anyway.

Challenge: prove that for an internal group XX in a finite product category, the square

X×X sym X×X i×i X×X m m X i X \begin{matrix} X \times X &\stackrel{sym}{\to} &X \times X & \stackrel{i \times i}{\to} & X \times X\\ m\downarrow& & & &\downarrow m \\ X & &\stackrel{i}{\to}& &X \end{matrix}

commutes. (Here mm is multiplication and ii is inversion.) This is the diagram saying “(xy) 1=y 1x 1(x y)^{-1} = y^{-1} x^{-1}”.

It’s not that hard: as usual, you simply fill the diagram in with instances of the diagrams expressing the group axioms. But it’s tedious: unless I’m missing something clever, it can’t be done with fewer than about ten inner diagrams.

However, the magic of internal logic lets you say: there’s a string of equations proving it for groups in SetSet, so it’s automatically also true in an arbitrary finite product category. Done!

If that’s not enough to convince you, consider, say, the commutator identity

[x,[y,z]]=[xy,z][z,x][z,y]. [x, [y, z]] = [x y, z][z, x][z, y].

Proving this diagrammatically would take you to a world of pain. But it’s clear how to prove it for ordinary groups: simply expand both sides and cancel. And then the same magic lets you conclude that the equation also holds (i.e. the corresponding diagram commutes) for internal groups in an arbitrary finite product category.

This is explained on pages 11–13 of (the new version of) this.

Here, for simplicity, I’m discussing the internal logic of a finite product category, not a topos. But the principle is the same.

Posted by: Tom Leinster on June 29, 2011 4:55 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Thanks, Tom! That’s a very nice example. The commutativity of diagrams of that sort is “obvious” in simple examples like topological spaces and smooth manifolds, where the category in question has a faithful underlying-set functor, so that an internal group is just an ordinary group with extra structure—but the internal logic applies just as well in other more complicated cases. One application of that sort is to commutative Hopf algebras, which are just internal group objects in the cartesian monoidal category Rings opRings^{op}. That way you can easily prove things like any commutative Hopf algebra has a unique antipode, which is perhaps not at all obvious from staring at the explicit definition of a Hopf algebra.

An example that I’ve personally had occasion to use is when you have a topos and you want to construct a model of material set theory. I find it much easier to do when working in the internal logic (or, if you need unbounded quantifiers, the stack semantics), so that you’re essentially constructing a model of material set theory from a model of structural set theory, and you don’t need to worry about restating the complicated properties of material-set models as “well-founded extensional rooted trees” in diagrammatic terms. A simple exposition of this sort of thing is in VI.10 of Sheaves in Geometry and Logic; I wouldn’t want to try rewriting that chapter in diagrammatic language!

I never worried too much about what “obviously forbidden” meant, but now I’m hoping internal logic will tell me an actual answer.

It will! The answer is: you’re allowed to do anything as long as you don’t leave the fragment of logic which is valid in the internal language of the category you’re working in. In a topos, that essentially means you can do arbitrary mathematics as long as you stay in intuitionistic logic (no LEM or AC). In a finite-product category, you can use finite-product logic (which more or less means equational reasoning); in a regular category you can use regular logic; and so on. It takes some practice to get used to “doing mathematics in fragments of logic”, but fortunately, the most useful fragments are probably also some of the easiest to get used to: intuitionistic logic in a topos and equational reasoning in a finite-product category. Finite-limit logic in a finite-limit category is also useful and not too hard to grok.

(I suppose one might add closed symmetric monoidal categories and multiplicative intuitionistic linear logic, but as I haven’t yet managed to get close to grokking linear logic as a place in which to “do mathematics”, I won’t.)

The nLab has a fairly extensive page on different logics and the categories in which they are valid.

Posted by: Mike Shulman on June 29, 2011 5:21 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Ah. Thanks, Tom and Mike. Then unless I’m mistaken, internal logic is just what an algebraic geometer would call using the functor of points. If that’s right, then I’m pleased/disappointed to learn that I know it already. Hardly a day goes by around here without me using it!

But I think there is still something that hasn’t sunk in, which is the fragments-of-logic part that Mike mentioned. For a long time, I never really paid logic too much attention. (And, or, and not – what is there to say that about them that isn’t obvious?!) So I think I don’t really know what parts of logic I’m using when I do things and that this is the source of discomfort I sometimes feel when thinking about sheaves. The little theorem that Richard mentions above is a good example. I would say it’s obviously true, but I don’t really know why I think its truth is obvious. Then the doubt starts creeping in, and then I either suppress it and keep typing or I take the time to write out a classical sheaf-theoretic argument on a piece of paper which I then throw away.

I suppose one remedy is just to pay closer attention to the logic used in the proofs of little facts about sets until I get a better feel for exactly which fragments of logic I’m using and when.

But I wonder if there could be cheat. When I look at Richard’s example, the reason I think it’s obvious is not because I go over the proof in my head and then decide that it doesn’t use anything obviously forbidden. What I do is think: 1) True for sets? Check. 2) Not using any forbidden concepts? Check. 3) QED.

This takes three mental clock cycles, whereas running over the proofs for sets would take twice the length of the proof. One for each statement, and one to check that it doesn’t use anything forbidden.

So I wonder – could there be a meta-theorem to the effect that if a mathematical statement about objects (or morphisms or …) in a category of a given type (a topos, say) doesn’t use any forbidden syntax and if that statement is true in the category of sets, then it is true in any topos? It seems that, without realizing it, I’ve been pretending such a theorem exists for years.

Posted by: James Borger on June 29, 2011 10:02 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Jim, now I have a question for you. You say:

unless I’m mistaken, internal logic is just what an algebraic geometer would call using the functor of points.

I entirely don’t understand this. I thought the “functor of points” approach meant regarding a scheme as a functor RingSetRing \to Set. (It’s called the “functor of points” of the scheme, right?) What does this have to do with internal logic?

I guess what’s happening is that the phrase “functor of points” means a lot more than just viewing schemes as functors on rings. I’d be pleased to hear what it really does mean. Thanks.

Posted by: Tom Leinster on June 29, 2011 5:21 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

It seems to me that the missing link between “internal logic” and the “functor of points” is Richard’s post about viewing internal logic via the Yoneda embedding. As I said there, I prefer for various reasons not to think about the internal logic that way—for one thing, it seems to me that the notion of internal logic is more general than that approach can naturally capture. But finite-product logic, at least, can easily be expressed by passing to the presheaf topos, where we can reason that each set in the image of a group-object presheaf is itself a group and apply things we know about groups in Set.

Posted by: Mike Shulman on June 29, 2011 5:34 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Yes (I think). It might also be helpful to point out that the category of affine schemes is a generating subcategory (I hope I got the right term) of the category of all schemes, and that the category of affine schemes is equivalent to the category of rings. This is why the category of schemes is a full subcategory of the category of functors from Rings to Sets.

Does that clear things up, Tom?

Posted by: James Borger on June 30, 2011 11:46 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Actually, I still didn’t get it from Mike’s comment. I’d wanted to know what the connection was between

(i) viewing a scheme as a (suitable) functor RingSetRing \to Set

and

(ii) internal logic.

As Mike’s comment didn’t mention schemes, it didn’t answer my question.

However, I did some thinking this morning and I think I see the point now. (I suspect Mike already saw it, even if I didn’t understand.) The category SchSch of schemes is a full subcategory of the functor category [Ring,Set][Ring, Set]. For the purposes of this comment, all we need to know about SchSch is that it contains all the representables Hom(k,)Hom(k, -), for rings kk. And you crazy algebraic geometers have a special name for the object Hom(k,)Hom(k, -) of SchSch: you call it Spec(k)Spec(k).

A “kk-point” of a scheme XX is an element of X(k)X(k), or from a more traditional alg geom viewpoint, a map of schemes Spec(k)XSpec(k) \to X. (The two are the same by Yoneda.) In the notes I linked to earlier, that would be called a “generalized element” of XX, of shape Spec(k)Spec(k). Internal logic is all about phrasing everything in terms of generalized elements. The functor of points approach is all about phrasing everything in terms of generalized elements of shape Spec(k)Spec(k), for rings kk. If I’m on the right track, that’s the connection between (i) and (ii).

When we’re doing internal logic in an arbitrary category EE, we usually have to consider generalized elements of all possible shapes. But when we’re doing it in a presheaf category [C op,Set][C^{op}, Set], it’s usually enough to consider generalized elements of shape Hom(,c)Hom(-, c), for cCc \in C. That’s because a generalized element of X:C opSetX: C^{op} \to Set, of shape Hom(,c)Hom(-, c), is by Yoneda the same thing as an element of X(c)X(c). I guess this could be formalized by saying that the representables form a dense, or maybe generating, subcategory of [C op,Set][C^{op}, Set], as Jim suggests.

(This principle is reflected in the phrase “category of elements”: an object of the category of elements of XX is a generalized element of representable shape.)

Posted by: Tom Leinster on June 30, 2011 12:56 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

And you crazy algebraic geometers have a special name for the object Hom(k,)Hom(k,−) of SchSch: you call it Spec(k)Spec(k).

Strictly speaking it’s a bit different. The functor Spec():CRing opLocRingSpaceSpec(-) : CRing^{op} \to LocRingSpace is defined as taking values in locally ringed spaces. Only after the fact does one prove that the external Yoneda embedding

SchemeLocRingSpaceSh(CRing op) Scheme \hookrightarrow LocRingSpace \to Sh(CRing^{op})

given by

(X,𝒪 X)LocRingSpace(Spec(),(X,𝒳 X)) (X, \mathcal{O}_X) \mapsto LocRingSpace(Spec(-), (X, \mathcal{X}_X))

is full and faithful. Only with this implicitly understood does the Spec()Spec(-) notation become nothing but Yoneda embedding. But the extra step in between is useful information not be be disregarded.

The best exposition of the category-theoretic basics of geometry is Structured Spaces . The issues discussed here are around section 2.4.

Posted by: Urs Schreiber on July 2, 2011 7:56 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Strictly speaking it’s a bit different.

I don’t see the problem. The category of schemes is a full subcategory of [CRing,Set][CRing, Set]. Of course, some people prefer to say “is equivalent to” rather than “is”, because they take the definition of scheme to be “locally ringed space satisfying such-and-such”. But we can equally well take the definition of scheme to be “functor CRingSetCRing \to Set satisfying such-and-such”. I often find it useful to think in terms of the second definition, and that’s what I was doing in my comment.

(Of course I was teasing a bit in that sentence you quoted: I know that historically, it wasn’t just a matter of giving a hom-functor a funny name.)

Are you just saying that the equivalence between

scheme as functor CRingSetCRing \to Set

and

scheme as locally ringed space

has some genuine content? If so, I certainly agree.

Posted by: Tom Leinster on July 2, 2011 1:24 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

could there be a meta-theorem to the effect that if a mathematical statement about objects (or morphisms or …) in a category of a given type (a topos, say) doesn’t use any forbidden syntax and if that statement is true in the category of sets, then it is true in any topos?

There is such a theorem! (And there’s nothing meta- about it, except in the sense that any theorem about logic is “meta”.) In Sketches of an Elephant (section D1.5) this theorem is called classical completeness, and states (in its maximally general form):

If T is a coherent theory, then any coherent sequent which is true of all T-models in Set is provable from T in coherent logic (and therefore true of all T-models in any coherent category; in particular, in any topos).

Coherent logic is the fragment of (finitary) logic containing “true”, “false”, “and”, “or”, and “there exists”. A coherent sequent is (for the layman) a statement of the form “for all x 1,,x nx_1,\dots,x_n, ϕ\phi implies ψ\psi”, where ϕ\phi and ψ\psi are coherent formulas—so you’re allowed one “implies” and one string of “for all”s on the very outside. (This may seem kind of arbitrary if you’re not used to thinking about sequents. One way to motivate it is to think about equational theories, where we have statements in the theory of a group like “for all x,yx,y, (xy) 1=y 1x 1(x y)^{-1} = y^{-1} x^{-1}”.)

So that tells you exactly what the “forbidden syntax” is to make your theorem true: any statement that isn’t a coherent sequent.

Posted by: Mike Shulman on June 29, 2011 7:56 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Excellent! (By the way, is a meta-theorem actually different from a theorem? I thought it was just what logicians called theorems in logic, and I was trying to play along.)

Suppose we take Richard’s sample theorem above. Is that an example of a coherent sequent? What I don’t find obvious is how to express the part of the theorem that introduces QQ as the coequalizer.

Posted by: James Borger on June 30, 2011 12:24 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

is a meta-theorem actually different from a theorem? I thought it was just what logicians called theorems in logic

It would get kind of cumbersome if logicians had to add “meta-” in front of all of their theorems. I suppose they might say “meta-theorem” sometimes for pedagogical purposes, to distinguish a theorem in the mathematical field called logic from the object of study of that field which is also sometimes called a “theorem”, but in practice, I think they just rely on context.

Suppose we take Richard’s sample theorem above. Is that an example of a coherent sequent?

Here’s how to view Richard’s theorem in this light. The first thing to note is that the theorem refers to a “coherent theory”, which I didn’t define. A coherent theory is just a set of coherent sequents. So the theorem says, if a bunch of coherent sequents imply another coherent sequent in Set, then they also imply it in any coherent category.

Now suppose we’re given f:ABf\colon A\to B, its kernel pair r,s:KAr,s\colon K \rightrightarrows A, their quotient q:BCq\colon B\to C and the resulting map m:CBm\colon C \to B. A logician would say these objects and morphisms form the language in which our theory is written. Now the fact that (r,s)(r,s) is the kernel pair of ff is expressed by the sequents

k 1,k 2K(r(k 1)=r(k 2)ands(k 1)=s(k 2)impliesk 1=k 2)\forall k_1,k_2 \in K (\; r(k_1)=r(k_2) \;\text{and}\; s(k_1)=s(k_2) \;\text{implies}\; k_1=k_2 \;) kK(true impliesf(r(k))=f(s(k))\forall k\in K (\text{true implies}\; f(r(k)) = f(s(k)) a 1,a 2A(f(a 1)=f(a 2)implieskKsuch thatr(k)=a 1ands(k)=a 2)\forall a_1,a_2\in A (\; f(a_1) = f(a_2) \;\text{implies}\; \exists k\in K \;\text{such that}\; r(k) = a_1 \;\text{and}\; s(k)=a_2 \;)

The first says that (r,s)(r,s) are jointly monic, the second says that it contains only pairs in the kernel, and the third says it contains everything in the kernel. (I wrote “true implies” just to make it clear that the second is actually a “sequent” in the sense I described. Of course, it can be omitted in practice, since saying that true implies ϕ\phi is the same as saying ϕ\phi.) It follows that (r,s)(r,s) is an internal equivalence relation.

Similarly, the fact that qq is the quotient of the equivalence relation (r,s)(r,s) is expressed by the sequents

kK,q(r(k))=q(s(k))\forall k\in K, q(r(k)) = q(s(k)) cC,aAsuch thatq(a)=c\forall c\in C, \exists a\in A \;\text{such that}\; q(a)=c

which express that qr=qsq\circ r = q \circ s and that qq is regular epic, together with copies of the first three sequents with ff replaced by qq, asserting that (r,s)(r,s) is also the kernel pair of qq.

Finally, we need the sequent

aA,m(q(a))=f(a)\forall a\in A, m(q(a)) = f(a)

asserting that mq=fm\circ q = f. These nine sequents form the theory; now the sequent whose truth we are interested in is

c 1,c 2C,m(c 1)=m(c 2)impliesc 1=c 2\forall c_1,c_2\in C, m(c_1) = m (c_2) \;\text{implies}\; c_1=c_2

which says that mm is monic. Since all of these are coherent sequents, the fact that the first nine imply the last in Set tells us that they also imply it in any coherent category. In fact, since all of these are actually regular sequents (they don’t use “or” or “false” either), the corresponding “classical completeness” theorem for regular categories tells us that this also holds in any regular category, as Richard said.

I realize that this may seem very complicated at first sight! But with practice, it becomes obvious that some statement or other can be expressed in some fragment of logic or other, without having to write down all of the sequents.

Posted by: Mike Shulman on June 30, 2011 8:55 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Great! Thanks, Mike. This is helping a lot. So the coherent theory will often vary from one application to the next. It seems that to a first approximation, if you’re trying to prove a theorem of the form “Let a,b,c… Then for all x…, we have y=z”, then the “Let a,b,c…” part is handled by the theory, and part after the “then” is of course the sequent. Is that reasonable general rule?

I am still uncertain about one part of what you wrote, though, and I think it will take us back to internal logic. It’s the meaning of existential quantifiers (and maybe also equality) in your formulation of Richard’s theorem in terms of generalized elements. Existential quantifiers have to (I think) be interpreted locally in a topos, but then we’ll find ourselves comparing generalized elements with different domains. So it seems that one needs to say a few more words to make this legit, something that explains how to interpret the logical language in the category in question. (Not sure if that makes sense. It’s just my own way of putting it.)

For example, for f:XYf:X\to Y to be an epimorphism, we want to say that yYxX(f(x)=y)\forall y\in Y \exists x\in X (f(x)=y). To make this work in a topos, we have to interpret it as follows: for all objects UU, and all yY(U)y\in Y(U), there exists a cover UU' of UU and an element xX(U)x\in X(U') such that f(x)=y| Uf(x)=y|_{U'}. So the symbol \exists automatically allows you to pass to covers and also the symbol == can apparently allow you to compare generalized elements with different domains. How does that work exactly?

This seems to be an aspect of internal logic that goes beyond generalized elements / the functor of points.

Posted by: James Borger on July 1, 2011 1:43 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Your “general rule” seems reasonable to me. Another way to say it is that in a statement of the form “given any structure of such-and-such sort, thus-and-so holds” the such-and-such structure will be the theory and the thus-and-so will be the sequent.

So it seems that one needs to say a few more words to make this legit, something that explains how to interpret the logical language in the category in question.

Of course one does! The process of setting up the internal logic of a category is precisely the process of explaining how to interpret a suitable logic into that category. This is true for all fragments of logic, not only quantifiers; it’s just somewhat simpler for, say, finite-limit logic.

There are two basic ways to describe this interpretation. One is in terms of classifying subobjects: every formula ϕ\phi with free variables x,yx,y, say, is interpreted by a subobject [ϕ]X×Y[\phi] \hookrightarrow X\times Y, with “and” and “or” interpreted by intersection and union, and quantifiers by images and dual-images (left and right adjoints to pullback of subobjects). Then a sequent “ϕ\phi implies ψ\psi” is satisfied if [ϕ][ψ][\phi] \subseteq [\psi]. The nlab page on internal logic summarizes how this works.

The second description is Kripke-Joyal semantics, which is basically what the “sheaf semantics” (exactly as you described it) would be for the topos of sheaves on the category in question. The equivalence of the two definitions is a fun exercise if you’ve never done it. I’m not sure exactly what you’re asking, though, because you just described exactly how this semantics captures existential quantification and equality; what more do you want to know? Do you want to know how it works in the other approach?

This seems to be an aspect of internal logic that goes beyond generalized elements / the functor of points.

Yes, indeed, internal logic beyond finite-limit logic goes past what you can say by passing to a presheaf category. Richard handled that by passing to the sheaf topos instead.

Posted by: Mike Shulman on July 1, 2011 5:04 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

OK, here’s something I’d like to know: Let xx and yy be generalized elements of ZZ, with possibly different domains of definition XX and YY. Does the expression x=yx=y have a meaning? If so, what is it?

Maybe I’ll try to answer my own question. I’ll say that x=yx=y is true if XX and YY admit a common refinement over which we have x=yx=y in the usual sense. In other words, x=yx=y means that there exists an object UU, an epimorphism from UU to XX, and an epimorphism from UU to YY such that x| U=y| Ux|_U=y|_U. I think I’m OK with this definition.

Now let me try to give a more internal take. We have a subobject X× ZYX\times_Z Y of X×YX\times Y, which is where xx and yy agree, the “locus of equality”. One might even write [x=y][x=y] for this subobject. Then we have x=yx=y in the sense above if and only if the projections from [x=y][x=y] to XX and to YY are epimorphisms.

Is that all OK? I’m not completely confident, even though it seems that if you want to identify a generalized element with that element pulled back to a refinement, then the definitions above are the weakest ones that allow this.

Posted by: James Borger on July 1, 2011 7:26 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Let xx and yy be generalized elements of ZZ, with possibly different domains of definition XX and YY. Does the expression x=yx=y have a meaning?

I would say no; it’s a type error.

if you want to identify a generalized element with that element pulled back to a refinement

I think this is a misleading way to think. In particular, it suggests some sort of “equivalence relation” on generalized elements defined at different stages, which is not just a type error but discards important information about which morphisms relate generalized elements at different stages. For instance, we might have generalized elements x:XZx\colon X\to Z and y:YZy\colon Y\to Z and some cover p:YXp\colon Y\to X such that xp=yx p = y, but some other cover q:YXq\colon Y\to X such that xqyx q \neq y. When considering the validity of more complicated logical formulas, which morphism we use to pull xx back to YY may make a difference.

I feel like this is not a very good answer. I can think of several other things to say, but which one is relevant depends on what you have in mind. Can you say what leads you to ask about comparing generalized elements defined at different stages?

Posted by: Mike Shulman on July 1, 2011 5:36 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

OK, good. Frankly I’m relieved that you’d call it a type error, even though I was trying my best to like it.

The reason why I wanted to make sense of it is to try to understand how the internal logic unpacks in a statement like “f:XYf:X\to Y is an epimorphism if and only if yYxX(f(x)=y)\forall y\in Y \exists x\in X (f(x)=y)”.

I guess I was assuming that there’s some kind of pre-compiler which would expand the logical symbols as if they were macros into something in terms of external logic. So, “yY\forall y\in Y” would become “for all objects U yU_y and all morphisms y:U yYy:U_y\to Y”. Then “xX\exists x\in X” would become “there exists an object U xU_x and a morphism x:U xXx:U_x\to X”, but then when we’d have to make sense of “f(x)=yf(x)=y”, and the generalized elements on the two sides have different domains. So I was trying to find a way to make that work.

Now I suppose you’ll tell me that this compilation process is a bit more sophisticated in that when it tries to compile “yY\exists y\in Y”, it does so in a way that is sensitive to its context.

So can you tell me a mechanical way to translate a sentence in the internal logic of topos into a statement in external logic? Apologies if this is on the nLab page (or, worse, in a comment above). I couldn’t see it there, but I probably wouldn’t be able to recognize it if it were there.

Posted by: James Borger on July 2, 2011 4:17 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Ah, I see what you’re getting at! Yes, your intuition is exactly right: there is a compiler, and it is (minimally) context-sensitive. What happens is that as you compile the statement “from the outside in”, the compiler keeps track of the current stage of definition, and the generalized element at that stage denoted by each variable. Thus, the process of compilation of “yY,xX,f(x)=y\forall y\in Y, \exists x\in X, f(x)=y” goes like this:

  • We begin with the current stage being the terminal object, 11.

  • First we hit “yY\forall y\in Y”, which gets compiled to “for any object U yU_y equipped with a morphism p y:U y1p_y\colon U_y\to 1 (since 11 is the current stage of definition), and any generalized element [y]:U yY[y]\colon U_y\to Y, …”.

  • Now the current stage of definition gets set to U yU_y, and we remember that the variable yy denotes the morphism [y]:U yY[y]\colon U_y\to Y.

  • Next we hit “xX\exists x\in X”, which gets compiled to “…there exists an object U xU_x equipped with a regular epimorphism p x:U xU yp_x\colon U_x \twoheadrightarrow U_y (since U yU_y is the current stage of definition), and a generalized element [x]:U xX[x]\colon U_x\to X, such that …”.

  • Now the current stage of definition gets set to U xU_x, we remember that the variable xx denotes the morphism [x]:U xX[x]\colon U_x\to X, and we also update the variable yy to now denote the composite [y]p x:U xY[y]\circ p_x\colon U_x\to Y (so that it is also defined at the current stage).

  • Finally, we hit “f(x)=yf(x) = y”, which gets compiled to “…, f[x]=[y]p xf \circ [x] = [y]\circ p_x”. We obtained this by replacing the variable xx by its current denotation [x][x] and the variable yy by its current denotation [y]p x[y]\circ p_x. Note that this is an equation at the current stage of definition, U xU_x, and as such it is not a type error; it equates two morphisms with domain U xU_x and target YY.

Thus, noting that the morphism p yp_y is unique and thus irrelevant, the end result of compilation can be easily optimized to “for any object U yU_y, and any generalized element [y]:U yY[y]\colon U_y\to Y, there exists an object U xU_x equipped with a regular epimorphism p x:U xU yp_x\colon U_x \twoheadrightarrow U_y, and a generalized element [x]:U xX[x]\colon U_x\to X, such that f[x]=[y]p xf \circ [x] = [y]\circ p_x”.

If ff is itself a regular epimorphism, then this is true, since we can always take p xp_x to be the pullback of ff along [y][y], which is regular epic since regular epis are stable under pullback in any regular category. Conversely, if this is true, then considering the special case U y=YU_y=Y and [y]=1 Y[y]=1_Y, we find that there is a regular epimorphism p:UYp\colon U\twoheadrightarrow Y which factors through ff, which suffices to show that ff is itself regular epic.

I’ve never seen the Kripke-Joyal semantics presented as a “process of compilation”, but now that you suggested the idea, I think it is a very natural way to describe it. The nLab page doesn’t currently describe the Kripke-Joyal semantics, but maybe with this primer you can now go read Section VI.6 of Sheaves in Geometry and Logic and it will make a little bit of sense. A handy translation key is that logicians write “UU\,\Vdash …” to mean “at stage UU, …”, and pronounce it “UU forces …”.

Posted by: Mike Shulman on July 2, 2011 7:34 AM | Permalink | PGP Sig | Reply to this

Re: Flat Functors and Morphisms of Sites

Excellent! Thanks! I’ll have to ruminate on that a bit, but I’m sure it answers all my questions.

Also, thanks for explaining the “forces” symbol. As you say, all this might be just enough enable me to read that section of Mac Lane-Moerdijk now.

Posted by: James Borger on July 3, 2011 1:37 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

James, regarding your comment about the “local” interpretation of existentials / disjunctions et cetera being at odds with the functor of points / generalised elements idea. One way of thinking about it is this. If we were dealing with finite limit categories, we could simply use and interpret generalised elements in a naive way; for any finitely complete category has its Yoneda embedding into a presheaf category, this preserves finite limits, and in the presheaf category finite limits are pointwise. (In this post I ignore size problems for simplicity). So in this case, we may argue with generalised elements in the naive way.

If we were dealing instead with regular categories, and their regular logic, then we cannot use the naive interpretation. Indeed, the Yoneda embedding is no longer suitable as an embedding as it is typically not regular. Instead we embed into the category of sheaves for the regular topology; now the embedding is regular so we can reflect arguments about regular logic back down, but unfortunately in this subcategory colimits, in particular coequalisers of kernel-pairs, need no longer be pointwise. It is the failure of these colimits to be pointwise which makes the naive interpretation of existential quantifiers incorrect.

How do we patch this up? Well, to calculate coequalisers of kernel-pairs in the category of sheaves, one calculates first in presheaves and then applies sheafification. The “local” interpretation of existential quantifiers is precisely what is needed to account for the gap between the coequaliser of a kernel-pair computed in presheaves, and that computed in sheaves.

Posted by: Richard Garner on July 4, 2011 9:32 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Thanks, Richard. I *think* I knew all that already, at least at a philosophical level. I guess I wanted to know exactly what the sheaf-theoretic interpretation of logical symbols is. I knew that the most naive one (the one in presheaves) was wrong because existential quantifiers have to be interpreted locally, because as you say, one computes colimits of sheaves by sheafifying the presheaf colimit. But I still didn’t understand in a formal sense what it means to interpret them locally, as you can see by my clumsy attempts above. In any application of sheaf theory, it was always obvious what to do, but I wanted to know how to do it systematically, without thinking at all.

Posted by: James Borger on July 4, 2011 1:35 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

I suppose one might add closed symmetric monoidal categories and multiplicative intuitionistic linear logic, but as I haven’t yet managed to get close to grokking linear logic as a place in which to “do mathematics”, I won’t.

Has anyone suggested the possibility of “doing mathematics” like this?

I ask because I need to revise an article of mine on Michael Friedman’s ‘Dynamics of Reason’. I object there to the suggestion he makes that quantum logic might constitute a fundamental change in mathematical principles, a ‘revolution’ if you prefer. I wrote

It seems as though for Friedman a change in our mathematical principles following the ‘foundational’ period must impact on either the set theoretic framework or the classical logic used with it. I think not. Even if quantum logic gets up and running, it is just going to be seen as one way of viewing the structure of orthomodular lattices, a piece of mathematics perfectly capable of being formulated in terms of set theory and good old classical logic. Nobody is going to start systematically ignoring the distributive law in the meta-language. Nobody will say “I have an orthomodular lattice which is boolean and I know that any orthomodular lattice is either finite or infinite, but I cannot say that my orthomodular lattice is either finite and boolean or infinite and boolean”. No, if that line of von Neumann should prove to be a fruitful way to view quantum mechanics, it must be taken at an intra-mathematical conceptual level, for example, as being part of noncommutative geometry, or perhaps the category theorists will tell us it points to the right setting for quantum mechanics in some variety of monoidal category. It is already at this level that we shall have to be able to speak of radical overhaul, just as while the discovery that the internal logic of a topos is constructive does not mean than Errett Bishop triumphed, one can claim with some justification that the very arrival of the topos notion marked such an overhaul. So, if Friedman cannot see this and other aspects of what has taken place in mathematics in the post-1930 era as already involving a radical overhaul, then I suspect his scheme is in trouble.

Posted by: David Corfield on June 29, 2011 8:43 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

I don’t really know the answer to the question of whether anyone has suggested “doing mathematics” like this, at least, not if you mean doing all of mathematics taking linear logic as foundational.

However, after reading just the excerpt you posted (but not your whole article, or any of Friedman’s), my inclination is to say that that’s not the whole story. If the point is only about what has already happened in mathematics overall as a result of the internal logic of topos theory, then perhaps it is true to say that it is viewed merely as “a piece of mathematics perfectly capable of being formulated in… good old classical logic.” But if the point is about the eventual implications of that discovery, which may not yet have percolated through mainstream mathematics, then I think there is more to be said.

I very much like the following analogy, which I learned from J.L. Bell’s book Toposes and local set theories. The mathematics of Einstein’s theory of relativity could, in theory, be formulated in terms of the following conceptual framework: there is a global, unique notion of what it mean to “be at rest” and a corresponding global unique notion of “being in motion”. Hence, every object in the universe has an absolute velocity vector. Objects in (absolute) motion are subject to length contraction and time dilation, and moreover if they are in uniform motion, then they are subject to the illusion that they are at rest and the rest of the universe is moving.

Staying within this conceptual framework, one might even manage to arrive at the following conclusion: it is a good idea to formulate physical theories and arguments in such a way that they make no reference to the absolute notions of “rest” and “motion”, because then their conclusions will still be valid even in the illusory worlds experienced by observers who are in absolute motion.

However, the conceptual revolution implied by the theory of relativity goes beyond even this: it says that there is no absolute notion of “rest” and “motion” – any inertial reference frame is as good as any other. It is not the case that one observer’s belief that she is at rest is “true” and another’s is “false” – both are equally valid.

Similarly, to say that the internal logic of a topos is constructive, but that this fact is just another piece of mathematics formulated in set theory and good old classical logic, misses the point. Even the conclusion that because of this, it is better to formulate mathematical arguments constructively so that they can be applied inside any topos, is not the whole story. The point is that any topos is really as good as any other, including what we like to think of as the “good old” topos of sets that satisfy classical logic and (maybe) the axiom of choice.

It isn’t topos theory alone which leads us to this conclusion. Set theory and forcing (which, of course, can mostly be rephrased in topos-theoretic terms) also suggest that any model of set theory is as good as any other—although many set theorists stubbonly cling to the idea that there is a “true” universe of sets out there. (-: Of course, most set theorists usually stick to models of set theory that also satisfy LEM and AC, making them look rather more alike than different to the unspecialist eye. In fact, there is also a nice anology to be drawn between LEM+AC and the property of being an inertial reference frame, so that the inclusion of non-classical toposes corresponds to the theory of general relativity. (And, of course, it’s worth noting that the reference frame we live in is not inertial!)

So, could quantum or linear logic have similar implications? Arguably, quantum mechanics has had a similar effect on physics already—it’s now accepted that asking “which slit did the electron go through” is not really even meaningful. It’s not clear to me that it necessarily will have such an effect on mathematics, but I wouldn’t rule it out.

Posted by: Mike Shulman on June 29, 2011 5:27 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Thanks for this. I can see I need to reformulate things, because it doesn’t convey what I wanted to say, which was in essence that’s there’s been conceptual overhaul/revolution enough post 1930s set theory. We don’t have to wait for something as radically different as people doing mathematics with quantum logic.

Friedman paints an interesting picture of physics proceeding through transformations where new constitutive principles are introduced, which allow the expression of laws. What were empirical regularities can become principles, e.g, the identity of gravitational and inertial mass becomes the equivalence principle; what were principles can become approximately true regularities, e.g., Euclidean structure.

He suggests that this kind of revolutionary reversal doesn’t happen in mathematics, and I disagree, suggesting the adoption of category theory and the definition in its terms of a cohomology theory constitutes a parallel.

I think he’s being driven to look to something like the adoption of quantum logic as the right kind of radical transformation since he believes that if it were possible to express a piece of mathematics in an existing foundational system, we wouldn’t have expanded our expressive resources.

Posted by: David Corfield on June 29, 2011 9:14 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Ah, I see! Then, yes, I agree that that sort of reversal does happen in mathematics.

he believes that if it were possible to express a piece of mathematics in an existing foundational system, we wouldn’t have expanded our expressive resources.

By that logic, since any computer program can be compiled to machine code, we wouldn’t be inventing new programming languages. (-:

Posted by: Mike Shulman on June 29, 2011 9:58 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Thanks, Tom and Mike! I think I’m no longer scared of Lawvere–Tierney topologies, since while I still don’t completely understand them, you’ve sort of explained them, and I now see they’re equivalent to some things I do understand.

Posted by: John Baez on June 25, 2011 7:05 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Another way to think about a Lawvere-Tierney topology is as a particular sort of modality in the internal logic. Since Ω\Omega is the “set of truth values” in the internal logic, a morphism j:ΩΩj\colon \Omega\to\Omega is an operation on truth values. The axioms say that it satisfies:

  • j(true) is true.
  • j(P) if and only if j(j(P)).
  • j(P and Q) if and only if j(P) and j(Q).

which implies also that if P, then j(P). It’s kind of fun then to think about what it means, in terms of this modality in the internal logic, for an object to be a sheaf.

Posted by: Mike Shulman on June 25, 2011 7:17 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Which reminds me of yet another loose end I have lying some place.

Posted by: David Corfield on June 27, 2011 9:04 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

I take it that the history of the term ‘flat functor’ takes us back to Serre’s flat modules. Can anyone give a sense of why he used the epithet ‘flat’? And, if so, is anything of this flatness visible in the generalized setting that Mike’s talking about?

Posted by: David Corfield on June 23, 2011 9:33 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Indeed! I have no idea why Serre chose the word “flat”, but the generalized sense in question here definitely still has a connection to his meaning. A module MM is flat if the functor MM\otimes - preserves exact sequences. This is equivalent to saying that it preserves kernels and cokernels. But since MM\otimes - has a right adjoint Hom(M,)Hom(M,-), it always preserves cokernels. And since the category of modules is additive and MM\otimes - is an additive functor, it automatically preserves finite products, since they coincide with finite coproducts. Thus, it preserves exact sequences if and only if it preserves all finite limits.

Now, for any functor F:CEF\colon C\to E, the induced functor [C op,Set]E[C^{op},Set] \to E can be described as a tensor product of functors with FF (a coend):

GG CF cCGc×FcG\mapsto G\otimes_C F \coloneqq \int^{c\in C} G c \times F c

And, as we saw, FF is internally flat just when this functor preserves finite limits.

Posted by: Mike Shulman on June 23, 2011 5:05 PM | Permalink | PGP Sig | Reply to this

Re: Flat Functors and Morphisms of Sites

Eisenbud in his Commutative algebra textbook (Springer GTM), chapter 6, explains the intuition behind the notion of a flat family (and then goes on into the Tor, flat module etc. discussion) which fits the terminology to some extent.

Posted by: Zoran Skoda on June 25, 2011 4:21 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

I assumed that flatness of modules had something to do with flatness of connections. A quick bit of googling didn’t enlighten me, though. Urs…?

Posted by: Tom Leinster on July 3, 2011 2:22 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

I always assumed that “flat” was coined to mean something like “torsionfree” but for more general situations:

(1) A module over a PID is flat iff it is torsionfree.

(2) On the other hand, in differential geometry, a curve in 3\mathbb{R}^3 is flat iff it has zero torsion.

Perhaps someone, maybe Serre, noticed this and was indulging in some free association (perhaps aided by the fact that PIDs are “curves”, 1-dimensional schemes)?

Posted by: Todd Trimble on July 3, 2011 11:55 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

No one else has posted their answer to Mike’s first exercise, so I’ll post mine.

The exercise asks for an example of a functor F:CSetF: C \to Set that is internally but not representably flat. In other words, FF is to be flat in the usual sense, but there is to be some set SS such that the composite of FF with

Set(S,)=() S:SetSet Set(S, -) = (-)^S: Set \to Set

is not flat.

My answer: let CC be any category that is neither empty nor cofiltered (for instance, the two-object discrete category). Choose an object cc of CC, as we may since CC is nonempty. Then F=C(c,)F = C(c, -) is representable and therefore flat. Now the representable

() :SetSet (-)^\emptyset: Set \to Set

has constant value 11, so its composite with FF has constant value 11. Hence the category of elements of () F(-)^\emptyset \circ F is isomorphic to CC. But CC is not cofiltered, so () F(-)^\emptyset \circ F is not flat.

Posted by: Tom Leinster on June 24, 2011 3:47 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Very nice, Tom! That’s simpler than the example I had in mind. Although on reflection, I guess my example is actually a special case of yours. I was thinking of the case when C=BGC=B G is the delooping of a group, so that a flat functor CSetC\to Set is the same as a GG-torsor (a free transitive GG-set)—and any such functor is representable!

Posted by: Mike Shulman on June 24, 2011 4:39 PM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Is the answer to your puzzle that CC must have finite limits, and the topology on DD must be subcanonical?

A yet more interesting problem is that of when, for the covering-flat F:CDF \colon C \to D, the pointwise left Kan extension Lan YFLan_Y F preserves finite limits, insofar as it exists. A sufficient condition, again when the topology on DD is subcanonical, is given in terms of Anders Kock’s notion of postulatedness: more specifically, the colimits used in the computation of the left Kan extension Lan YFLan_Y F must be postulated, which is to say that they behave in DD as they do in a Grothendieck topos. I believe this sufficient condition is, in fact, also necessary.

Apart from Anders Kock’s original preprint on this, there is further work by Karazeris, and by Karazeris and Protsonis. (Karazeris considers the notion that you call covering-flat in his “Notions of flatness relative to a Grothendieck topology”).

Posted by: Richard Garner on June 27, 2011 1:46 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

Is the answer to your puzzle that C must have finite limits, and the topology on D must be subcanonical?

Yes, that’s one sufficient condition. I believe a slightly different sufficient condition is that C and D both have finite limits, and covering families in D are extremal-epic. I don’t actually know a necessary and sufficient condition.

Thanks for the references!

Posted by: Mike Shulman on June 27, 2011 2:24 AM | Permalink | Reply to this

Re: Flat Functors and Morphisms of Sites

The referee of my exact-completions paper has pointed out that to answer the puzzle, it suffices for CC to have finite limits and for covering families in DD to be strong-epic. This simultaneously generalizes both of these answers, since effective-epic families are always strong-epic, while extremal-epic families are strong-epic in the presence of finite limits.

Posted by: Mike Shulman on May 15, 2012 9:31 PM | Permalink | Reply to this
Read the post Exact completions and small sheaves
Weblog: The n-Category Café
Excerpt: Most kinds of exact completion, including categories of sheaves, are a special case of a reflection from certain sites into higher-ary exact categories.
Tracked: March 21, 2012 3:57 AM

Post a New Comment