## Stream: maths

### Topic: sheaves of modules

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

#### 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

#### 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

#### 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

#### 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?

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

#### Johan Commelin (Jul 25 2020 at 09:35):

And a good way to construct sheaves of modules.

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

#### Johan Commelin (Jul 25 2020 at 09:36):

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

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

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

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

#### 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

#### Kevin Buzzard (Jul 25 2020 at 11:26):

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

#### Kevin Buzzard (Jul 25 2020 at 11:27):

I've just run into 100 sheep.

#### Kevin Buzzard (Jul 25 2020 at 11:28):

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

#### Kevin Buzzard (Jul 25 2020 at 11:28):

Then we can make Picard monoids

#### 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

#### 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

#### Kevin Buzzard (Jul 25 2020 at 11:33):

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

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

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

#### 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

#### Scott Morrison (Jul 25 2020 at 12:08):

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

No pullback yet!

#### Kevin Buzzard (Jul 25 2020 at 12:11):

Oh for pullbacks you need tensor again

#### 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

#### Scott Morrison (Jul 25 2020 at 12:12):

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

#### Scott Morrison (Jul 25 2020 at 12:13):

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

#### Scott Morrison (Jul 25 2020 at 12:13):

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

#### Scott Morrison (Jul 25 2020 at 12:13):

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

#### 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?

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

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

#### 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

#### Kevin Buzzard (Jul 25 2020 at 14:07):

And then you could bundle it to make the category

#### 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

#### Kevin Buzzard (Jul 25 2020 at 14:12):

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

#### Kevin Buzzard (Jul 25 2020 at 14:12):

Can we "bundle module"?

Last updated: May 11 2021 at 15:12 UTC