sheaves of modules

Stream: maths

[Scott Morrison]

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.

[Kenny Lau]

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

[Kenny Lau]

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

[Johan Commelin]

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

4. 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

[Scott Morrison]

Will Kenny's version, or something close to it

4. 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?

[Johan Commelin]

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.

[Johan Commelin]

And a good way to construct sheaves of modules.

[Johan Commelin]

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.

[Johan Commelin]

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

[Scott Morrison]

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.

[Johan Commelin]

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.

[Johan Commelin]

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).

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I've just run into 100 sheep.

[Kevin Buzzard]

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

[Kevin Buzzard]

Then we can make Picard monoids

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Scott Morrison]

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.

[Scott Morrison]

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. :-)

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

No pullback yet!

[Kevin Buzzard]

Oh for pullbacks you need tensor again

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Kevin Buzzard]

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?

[Johan Commelin]

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

[Scott Morrison]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

And then you could bundle it to make the category

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Can we "bundle module"?