definition of sheaf of modules

Stream: maths

[Jujian Zhang]

I am trying to write down a definition of (pre)sheaf of modules. I can think of two ways of doing this:

1. be explicit about what the (pre)sheaf of ring is:

structure PresheafOfModules1 (X : Top) :=
(𝒪 : presheaf CommRing X)
(ℱ : presheaf AddCommGroup X)
[is_module : Π (U : (opens X)ᵒᵖ), module (𝒪.obj U) (ℱ.obj U)]
(res_compatible : Π (U V : (opens X)ᵒᵖ) (h : U ⟶ V) (r : 𝒪.obj U) (a: ℱ.obj U),
  ℱ.map h (r • a) = 𝒪.map h r • ℱ.map h a)

2. be implicit about what the ring is:

class PresheafOfModules2 {X : Top} (ℱ : @presheaf BundledModule BundledModule.is_cat X):=
(res_compatible :
  Π (U V : (opens X)ᵒᵖ) (h : U ⟶ V) (r : (ℱ.obj U).R) (m : (ℱ.obj U).M),
    (ℱ.map h).2 (r • m) = (r • (ℱ.map h).2 m))

Here bundled module is the category of pairs $(R, M)$ where $R$ is a ring and $M$ is an $R$-module.

Which way, if any, is a good definition? Or is there a better way.

[Johan Commelin]

Did you see https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/tensor.20product.20of.20sheaves/near/263012430?

[Johan Commelin]

(And the messages that follow it)

[Jujian Zhang]

I actually write restrict of scalars part and finished the bundled module category

[Jujian Zhang]

Could it be useful if I pr it, even if it didn't end up being used in defining sheaf of modules

[Jujian Zhang]

https://github.com/jjaassoonn/sheaf_of_modules

[Kevin Buzzard]

My guess is that nobody really knows which definition will be better, and we'll only find out once we start proving theorems about the idea.

[Kevin Buzzard]

My guess is that some stuff will be easier with one definition and some stuff will be easier with the other definition, and the real question will in some sense be whether the stuff which is easier with one definition is just completely horrible with the other definition, or whether it's not too bad.

[Andrew Yang]

Isn't the axiom in res_compatible part of the definition of what a hom in BundledModule is?

[Jujian Zhang]

Bundled module tells that r • (ℱ.map h).2 m) is actually (ℱ.map h).1 r • (ℱ.map h).2 m) but not saying that (ℱ.map h).2 (r • m) = (r • (ℱ.map h).2 m))

[Andrew Yang]

I may be missing something here, but given a map $(f, f') : (R, M) \to (S, N)$, the fact that $f' : M \to f^{*}N$ is a map of $R$-modules should tell you that $f'(r\cdot m) = r \cdot f'(m)$.

[Jujian Zhang]

You are absolutely right.

[Adam Topaz]

If you use the category you called BundledModule, you could just take presheaves resp. sheaves with values in that given category. I don't see why you need any further axioms. Then prove that the forgetful functor from that category to the category of rings preserves limits to obtain the forgetful functor from sheaves taking values in BundledModule to sheaves of rings.

[Jujian Zhang]

Yes.

[Adam Topaz]

docs#category_theory.Sheaf_compose

[Jujian Zhang]

Should I make a pr about bundledModule

[Andrew Yang]

I think this should be useful regardless of the final definition of sheaves of modules.

[Jujian Zhang]

Thank you. Sorry about the confusion. Let me pr bundled module

[Kevin Buzzard]

Note that linear_map is now precisely the morphism you want.

[Kevin Buzzard]

(I just read the most recent community blog post)

[Jujian Zhang]

I thought the explicit sheaf of ring definition is somewhat cumbersome exactly because the restriction map is just a map of abelian groups. But I forget that linear_map has map_smul

[Adam Topaz]

I think Kevin is referring to the fact that linear maps are now just a special case of a semilinear map

[Andrew Yang]

Regarding the definition of sheaves of modules, I would prefer the second one, especially after the recent advancements Adam has made in the sheaf library.

[Kevin Buzzard]

Adam: to my surprise, semilinear maps are now called linear_map.

[Adam Topaz]

@Jujian Zhang here is an approximation for how I would start the definition, with the new semilinear map stuff:

import algebra.category.Module.basic
import algebra.category.CommRing

universe u
structure BundledModule : Type (u+1) :=
(A : CommRing.{u})
(M : Module.{u} A)

structure BundledModule.hom (X Y : BundledModule) :=
(f : X.A ⟶ Y.A)
(g : X.M →ₛₗ[f] Y.M)

[Adam Topaz]

(I don't know whether you already have a definition of BundledModule)

[Adam Topaz]

You could generalize the universe levels, but I don't know how useful that would be.

[Kevin Buzzard]

I'll remark that Jujian and I have already discussed this issue a bit, and at some point he was having trouble with universes, and I already suggested that he used fewer than 4 :-)