Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Flasque/flabby presheaves valued in a general category

David Michael Roberts (Jul 11 2026 at 07:32):

[I posted this on the nForum, but it will probably get more eyes and comments here]

I have a proposal for a flasque (pre)sheaf with values in a general category C that should work in more generality: that the restriction maps be [[strong epimorphisms]] . Mathlib has adopted the definition that the restriction maps be just plain epimorphisms, but I dispute this, and I’m aiming to reprove all the results in mathlib in Lean using the stronger definition (and generalise them somewhat). Since for C a concrete category the desideratum is “surjection on underlying maps of sets”, plain epis are too weak. One might argue for extremal epimorphisms, though if the value category has finite limits, extremal=strong and the distinction disappears. I’m interested to hear others’ thoughts.

The notion in the internal logic of a topos, as a pointwise notion, feels to me a generalisation that doesn’t really make sense in weaker doctrines. Also, any C where the hierarchy of epimorphisms collapses down to extremal = effective (and everything in between) doesn’t really give good data on what a general definition should be.

I guess a good test would be if a version of the Godement resolution works as desired for general-ish C (allowing for the fact it will almost certainly be a cosimplicial object rather than a cochain complex). For instance for a Barr-exact or even regular category things should “just work”.

David Michael Roberts (Jul 11 2026 at 08:08):

So for instance, if C were a regular category, sheaves with values in C should surely be said to be flasque is the restriction maps are regular epimorphisms. So the class of epis in a regular category that coincide with regular epis should be the candidates. Another desideratum to my mind is closure under composition. Obviously, for concrete categories C of models of some algebraic theory, the correct notion of epi should probably be those morphisms surjective on underlying sets.

Morgan Rogers (he/him) (Jul 12 2026 at 09:06):

Since most things proved using sheaves around the time of SGA would have freely exploited the fact that set epis are surjections, do you already have some example(s) of results for flabby sheaves whose proofs actually exploit a stronger property than being a plain epi?

David Michael Roberts (Jul 12 2026 at 09:18):

I was thinking statements for regular-category-valued flabby sheaves that are analogous to the theorems about short exact sequences of flabby sheaves valued in an abelian category, except about congruences and coequalisers. Because I think getting the statements for eg semiabelian, or Barr-exact, or regular categories in such a way the abelian category theorems are a corollary is a perfectly natural thing to try. And in the case of a regular category, strong epi = regular epi.

David Michael Roberts (Jul 12 2026 at 09:38):

Perhaps better to say is that (conceptually) short exact sequences get replaced by an effective epi and its kernel pair a regular category. So given an effective epi, one might recovers the usual theorems about ses of flabby sheaves when all the reguired replacements are made. Here it's conceivable that since in a regular category plain epis and effective=regular=strong epis are different, the theorem only works for flabby=restrict maps are strong/regular/effective.

David Michael Roberts (Jul 12 2026 at 09:43):

For instance there is an argument that requires that the restriction map of the flabby sheaf sits in an exact diagram as in the picture:

One might view this as a template for an abstract diagram chase argument in an abelian category, where the fact $A'(X) \to A'(U)$ is a quotient map (=regular epi) is what is used, not the fact it's an epimorphism.

Morgan Rogers (he/him) (Jul 12 2026 at 11:13):

I've been thinking about epis in the category of commutative monoids this week, and this strikes me as a setting in which the failure would be demonstrable. But even before that, as your example shows, it doesn't make so much sense to talk about ordinary epis in a setting where exact sequences are being employed.

Morgan Rogers (he/him) (Jul 12 2026 at 11:16):

(That's what Barr's notion of exactness is supposed to capture, anyhow)

Morgan Rogers (he/him) (Jul 12 2026 at 11:18):

Are you aware of a context in which someone has employed the plain epi version of flasque sheaf valued in a category where these don't coincide with strong epis?

David Michael Roberts (Jul 12 2026 at 11:59):

Oh, yes, cohomology of sheaves where the coefficients are commutative monoids (whatever that should look like) will also surely be a test of what is the good notion here.

David Michael Roberts (Jul 12 2026 at 12:05):

Morgan Rogers (he/him) said:

ich someone has employed the plain epi version of flasque sheaf valued in a category where these don't coincide with strong epis?

No. I was told that the mathlib definition for arbitrary categories used plain epis as a formalisation convenience, but actually the theory is only currently (and known/projected to be) applied to abelian categories, where of course epis = effective descent morphisms and every variant of epimorphism between those (so there are only two variants: ordinary epis, and split epis). This is I realised analogous to how division for a field is defined as a global function, even division by zero, but all uses of division will come with a hypothesis that the denominator is nonzero as appropriate. Except here it's "flabby has a convenient but technically wrong definition, except all uses will come with the hypothesis the value category is abelian, where the definition is via a theorem actually correct".

David Michael Roberts (Jul 12 2026 at 12:07):

So I have no examples where anyone has used the too-lax definition of "restriction maps = plain epi" in a weak setting, and neither could anyone over at the mathlib zulip. The definition is purely technically pragmatic, though I'm firmly of the opinion it could be 'corrected' at essentially epsilon cost in proofs (an extra application of a lemma that says all epis are strong epis in an abelian category)

David Michael Roberts (Jul 12 2026 at 12:21):

@Morgan Rogers (he/him) have you thought about a Godement-style resolution for commutative monoid sheaves?

Morgan Rogers (he/him) (Jul 12 2026 at 13:27):

Not explicitly, although it so happens that I was thinking about coequivalence relations in commutative monoids, and those seem relevant in the context of Godement resolutions, since Godement uses cokernels.

I notice that Godement's product of stalks construction only produces a sheaf which is flasque in a pointed context: for a sheaf of sets which may be empty over some opens, the restriction maps are not surjective. Conversely, in the context of commutative monoids the projection maps will be surjective (assuming AC); they'll even be split.

Morgan Rogers (he/him) (Jul 12 2026 at 13:31):

Actually I can remove the parenthetical from that last sentence: they split even without the axiom of choice because we have a canonical element

David Michael Roberts (Jul 12 2026 at 21:22):

ah, so cat with a zero object is too strong for a test case? the map to 0 is always split epi, which gives a lot

Morgan Rogers (he/him) (Jul 13 2026 at 08:21):

For Godement specifically it seems crucial that one can distinguish between general epi and strong epi for maps to the terminal object. An example would be $\mathbf{CMon}/\mathbb{Z}$.

You can construct a sheaf taking value either $\mathbb{N}$ or $\mathbb{Z}$ at every open of a space, so that some stalks are $\mathbb{N}$ and others are $\mathbb{Z}$. The Godement sheaf will assign to an open $U$ either $\mathbb{N}$ (if the stalk at any $x\in U$ takes this value) and $\mathbb{Z}$ otherwise, including at the empty set. So the restriction maps will be epic but not strong epic.

How does the resolution behave? Well, I think what I've just described ends up being identical to the original sheaf, so it's not doing much :sweat_smile: