Zulip Chat Archive

Stream: maths

Topic: sheaves of modules


view this post on Zulip Scott Morrison (Jul 25 2020 at 09:14):

I was thinking a bit about how to do sheaves of modules (over a fixed sheaf of rings O). (The difficult is already all at the presheaf level, I think.) (Everywhere here I'm just thinking about presheaves on a space: no sites, no toposes.)

I can think of three options, and none of them are great.

  1. Consider the category whose objects are pairs (R, M), with R a ring and M an R-module. Now take a presheaf valued in this category, and additionally ask for an isomorphism between the "ring part" of this presheaf and O.

  2. Given O, we get a Cat valued presheaf, by sending each ring R to Module R. Now do the Grothendieck construction on this (eek, 2-categorical stuff, dependent type theory hell everywhere!) and call this C_O. We can take a presheaf F with values in C_O, and ask for a natural isomorphism from (F composed with the "base" functor from C_O back to (opens X)^op) to the identity functor on (opens X)^op.

  3. We can just write down what it means to be a presheaf of modules explicitly, not even attempting to make it a functor from (opens X)^op to somewhere... From this we can extract the underlying (non-dependent) presheaf of Types, and maybe hobble along using the general API only with that part.

view this post on Zulip Kenny Lau (Jul 25 2020 at 09:17):

a module M over a ring R consists of:

  1. a structure of an abelian group on M (maps + : M \to M \to M and - : M \to M and 0 : M satisfying properties)
  2. a scalar multiplication R \to M \to M satisfying more properties

so likewise a sheaf of modules M over a sheaf of rings R consists of:

  1. a structure of an abelian group on M (maps + : M \to M \to M and - : M \to M and 0 : M satisfying properties)
  2. a scalar multiplication R \to M \to M satisfying more properties

view this post on Zulip Kenny Lau (Jul 25 2020 at 09:21):

or, categorically, a sheaf or rings is a ring object in the category of sheaves, and likewise for modules

view this post on Zulip Johan Commelin (Jul 25 2020 at 09:32):

@Scott Morrison How about the following (which is close to what Kenny says, but maybe a bit more explicit)

  1. O is a sheaf of rings. M is a presheaf valued in Ab. On top of that, one of the following:

4.(a) we have the data module (O U) (M U) for every U + the statement that the restriction maps are linear. (Note: The restriction maps will not be bundled linear maps automatically.)
4.(b) A morphism O \hom End(M)
4.(c) A morphism O × M → M

view this post on Zulip Scott Morrison (Jul 25 2020 at 09:32):

Will Kenny's version, or something close to it

  1. Think of the presheaf of rings O as a monoid object in presheaves of AddCommGroup, and think of a presheaf of modules as a module object for that monoid object

satisfy Kevin / Johan?

view this post on Zulip Johan Commelin (Jul 25 2020 at 09:35):

It all depends on the API. We need to get access to all the existing library on modules. In particular, we need module (O U) (M U), and lean should never have trouble inferring it. Also we need a way to talk about the restriction maps as (O U)-linear bundled homs.

view this post on Zulip Johan Commelin (Jul 25 2020 at 09:35):

And a good way to construct sheaves of modules.

view this post on Zulip Johan Commelin (Jul 25 2020 at 09:36):

So, whatever definition we choose, a great test would be to take a vector space V of real and see if we can turn functions X → V into a sheaf of modules over X → real.

view this post on Zulip Johan Commelin (Jul 25 2020 at 09:36):

If that is painless, I consider that a huge indicator of being on the right path.

view this post on Zulip Scott Morrison (Jul 25 2020 at 09:46):

Well, the restriction maps aren't exactly (O U)-linear maps, because the U is changing... I don't think we really have existing API covering that.

view this post on Zulip Johan Commelin (Jul 25 2020 at 09:50):

Well, if U < V in opens X, then you can view M U as an O V module via the restriction O V → O U, and then the restriction M V → M U should be O V-linear.

view this post on Zulip Johan Commelin (Jul 25 2020 at 09:51):

We will want to use that a lot. So we will need a way to access those maps as bundled homs (even if those bundled homs don't roll directly out of the definition, which I guess they won't, whatever we choose).

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:25):

The first test/challenge is to define the tensor product of presheaves of modules. Then tensor product of sheaves of modules. Then Picard groups

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:26):

Then Picard groups without universe bumping, but that's a question for the logicians

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:27):

I've just run into 100 sheep.

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:28):

The theorem we need is that tensor product is associative up to isomorphism

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:28):

Then we can make Picard monoids

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:29):

And the Picard group is I think the units of this monoid. So the goal should be the monoid of isomorphism classes of sheaves of modules

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:32):

It seems to me that the sheafification issue and the "make sure you have access to the module API" question are basically disjoint and perhaps the module one should be solved first

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:33):

The presheaf tensor product is nothing more than just taking tensor product on each open

view this post on Zulip Scott Morrison (Jul 25 2020 at 11:46):

Okay... the internal object route actually sounds pretty reasonable for all this. We'll show presheaf Ab X is symmetric monoidal. We'll think of O as a commutative monoid object internal to that. Anytime you have a commutative monoid in a symmetric (even just braided!) monoidal category, its category of module objects is monoidal.

view this post on Zulip Scott Morrison (Jul 25 2020 at 11:47):

So if we just define a presheaf of module objects to be a module object, we won't even need to transport this monoidal structure anywhere. :-)

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 11:51):

We should make sure we can do pushforwards and pullbacks along morphisms of ringed spaces, which are the same thing as morphisms of spaces equipped with a presheaf of rings

view this post on Zulip Scott Morrison (Jul 25 2020 at 12:08):

I think at the presheaf level pushforward has been in place for a while.

view this post on Zulip Scott Morrison (Jul 25 2020 at 12:08):

No pullback yet!

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 12:11):

Oh for pullbacks you need tensor again

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 12:12):

So the fundamental question is whether we can get a workable definition of presheaves of modules for which tensor product works

view this post on Zulip Scott Morrison (Jul 25 2020 at 12:12):

Sounds like someone should go add the definitions of braided and symmetric categories. :-)

view this post on Zulip Scott Morrison (Jul 25 2020 at 12:13):

Then commutative monoid objects in a braided category, then the tensor product on their module objects.

view this post on Zulip Scott Morrison (Jul 25 2020 at 12:13):

that should all be very formal, and hopefully not particularly painful.

view this post on Zulip Scott Morrison (Jul 25 2020 at 12:13):

(That said, it is exactly for this stuff that I originally wanted rewrite_search...)

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 13:13):

So how does all this work? Equality of types is troublesome in type theory, but equality of terms is fine. This is why we don't use the type module R because equality of R-modules is not the right idea, we instead introduce a new type M and have a typeclass module R M. However we can have the category of R-modules, that is a better thing to do somehow. So similarly a sheaf of rings on X shouldn't be a type, we should either put some kind of typeclass structure on a map from opens to rings, or make a category. But is it a good idea to make the typeclass first and then build the category on top?

view this post on Zulip Johan Commelin (Jul 25 2020 at 13:14):

I guess we're just firmly committing ourselves to not talking about equalities and only talk about isomorphisms instead.

view this post on Zulip Scott Morrison (Jul 25 2020 at 13:56):

I'm confused by your question, Kevin, but it's late, so perhaps I'll try again tomorrow.

A presheaf of rings on X is functor (opens X)^op \func Ring. That automatically receives a category instance, with morphisms natural tranformations. The category of sheaves is just defined as the induced category given by forgetting the sheaf condition.

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 14:04):

I'm saying that a presheaf of rings _could_ be a family of types and you could make a typeclass just like we do for modules

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 14:07):

And then you could bundle it to make the category

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 14:10):

And a sheaf of modules could similarly be another function M from opens to Type and then you have a typeclass forall U, abelian group (M U) and then forall U, module (R U) (M U) could be another typeclass

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 14:12):

Is it possible to bundle a typeclass which takes more than one type as input?

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 14:12):

Can we "bundle module"?


Last updated: May 11 2021 at 15:12 UTC