Definition of presheaf of modules

Stream: maths

[Jujian Zhang]

I was experimenting with definition of presheaves of modules following stack project 6.6. I came up with two formalizations

1. presheaves of modules are a functor with values in BundledModule, see #10724, i.e. then if 𝓕 is a presheaf of modules, aka, (opens X)ᵒᵖ ⥤ BunledModule, then 𝓕 ⋙ BundledModule.forget_to_Ring is a presheaf of ring and 𝓕 ⋙ BundledModule.forget_to_Ab is a presheaf of abelian groups. The nice thing about this approach is that, for any opens $U$, $\mathcal F(U)$ is automatically $\mathcal O(U)$-module and restriction map is automatically compatible with scalar multiplication. But this definition will make category of presheaves of module over a presheaf of ring $\mathcal O$ difficult, because then the category needs to be defined as
   {𝓕 | 𝓕 ⋙ BundledModule.forget_to_Ring = 𝓞} with equalities of functor flowing around. And I think the sheaf condition would be presumably "wrong", because that would actually imply 𝓕 ⋙ BundledModule.forget_to_Ring is a sheaf as well.

2. given a presheaf of rings 𝓞, define presheaf of modules over 𝓞 as

structure presheaf_of_module
(self : presheaf Ab X)
[module : ∀ (U : opens X), module (𝓞.obj (op U)) (self.obj (op U))]
(compatible : ∀ {U V : opens X} (inc : op U ⟶ op V) (r : 𝓞.obj (op U)) (m : self.obj (op U)),
   self.map inc (r • m) = 𝓞.map inc r • self.map inc m)

structure sheaf_of_module extends presheaf_of_module 𝓞 :=
(is_sheaf : presheaf.is_sheaf self)

see #12186 this link.

Now the problem with this approach is that

• then presheaf of module is not literally a presheaf in mathlib's sense
• (common to both approaches, I think) given a morphism f : 𝓞1 ⟶ 𝓞2 between presheaves of ring, defining restriction and extension of presheaf of modules by f is cumbersome, because lean's class inference cannot "see through f".

[Johan Commelin]

I think Adam was a big fan of (1).

[Reid Barton]

The equality in (1) seems quite awkward. I think in order to work with it directly, you would basically need to create an API for it that looked like (2) anyways.

[Reid Barton]

The DTT-natural way to say this would probably be using https://ncatlab.org/nlab/show/displayed+category, which is basically an abstraction of (2), I think

[Reid Barton]

I would suggest first thinking about all the operations you will want to support--I guess there are a lot: sheafification of presheaves of O-modules, (co)limits, restriction and extension of scalars, closed monoidal structure, pullback/pushforward between ringed sites

[Johan Commelin]

I was thinking of this https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/tensor.20product.20of.20sheaves/near/263012430 and the discussion following it

[Reid Barton]

OK so "essential fiber" means we have a ring+module and an isomorphism of its ring to O. That's better in some respects (and maybe not worse in any respects since = is so awkward anyways). But it still leaves a lot to be desired, for example, even to define the direct sum of two objects of this category you will need to make use of those isomorphisms already to define +

[Reid Barton]

Ah not to define +, but to define the action of the "wrong" copy of O on one (or both) of the summands

[Reid Barton]

Johan you asked me once why HoTT people think definitional equality is so important--here is an example. I don't think it will be pleasant to work in the category of "modules over a ring equipped with an isomorphism to R".

[Jujian Zhang]

Using the second approach, I have defined the restriction and extension functor and close of finishing their adjunction.

[Adam Topaz]

With approach 2, you would have to replicate literally everything we have about sheafification.

[Adam Topaz]

Here is a non-(pre)sheafy way I see to make approach 1 work in practice:

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

universe u

structure BundledModule :=
(R : CommRing.{u})
(M : Module.{u} R)

structure Module' (A : CommRing.{u}) :=
(M : BundledModule.{u})
(e : M.R ≅ A)

namespace Module'

instance (A : CommRing.{u}) : has_coe_to_sort (Module'.{u} A) (Type u) :=
⟨λ M, M.M.M⟩

instance (A : CommRing.{u}) (M : Module' A) : module A M :=
begin
  haveI : algebra A M.M.R := M.e.inv.to_algebra,
  change module A (restrict_scalars A M.M.R M),
  apply_instance,
end

end Module'

[Adam Topaz]

Essentially, set up the correct instances for your object so you can work with them as we usually work with modules from mathlib.

[Reid Barton]

Now you can't use the original restriction maps of the presheaf directly so you also need an API for those... and you end up at (2)

[Reid Barton]

So maybe the answer is "both", and you use (1) abstractly to prove that existence of sheafififcation

[Adam Topaz]

Reid Barton said:

Now you can't use the original restriction maps of the presheaf directly so you also need an API for those... and you end up at (2)

There may be a way to convince the scalar_tower stuff to make this fairly quick?"

[Kevin Buzzard]

Just to be clear -- Jujian has made extensive experiments with both approaches in the links he posts above.

[Jujian Zhang]

Adam Topaz said:

Here is a non-(pre)sheafy way I see to make approach 1 work in practice:

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

universe u

structure BundledModule :=
(R : CommRing.{u})
(M : Module.{u} R)

structure Module' (A : CommRing.{u}) :=
(M : BundledModule.{u})
(e : M.R ≅ A)

namespace Module'

instance (A : CommRing.{u}) : has_coe_to_sort (Module'.{u} A) (Type u) :=
⟨λ M, M.M.M⟩

instance (A : CommRing.{u}) (M : Module' A) : module A M :=
begin
  haveI : algebra A M.M.R := M.e.inv.to_algebra,
  change module A (restrict_scalars A M.M.R M),
  apply_instance,
end

end Module'

I haven't thought about this Module' approach.

If to use this approach, do we see a possibility in which we use approach 1, but avoid equality of functor when defining sheaf of modules over some given sheaf of rings?

[Adam Topaz]

Use isomorphism instead of equality.

[Adam Topaz]

I.e. "sheafify" this definition:

structure Module' (A : CommRing.{u}) :=
(M : BundledModule.{u})
(e : M.R ≅ A)

[Adam Topaz]

My concern with approach (2) is that whenever there is some categorical thing you want to do, you would have to make some bespoke construction that only really applies to your structure, and doesn't really fit in with the rest of the Sheaf/functor library. I think that would get old REALLY fast.

[Reid Barton]

I don't really understand how that doesn't also apply to (1), though

[Reid Barton]

What constructions do you get on (1) for free?

[Reid Barton]

For example, one obvious milestone would be to prove that the category of O-modules is abelian

[Adam Topaz]

BundledModule is a sufficiently nice concrete category, so you get sheafification for free. BundledModule has (co)limits, so you get (co)limits of sheaves of BundledModules for free. The forgetful functors to Ab and CommRing preserve limits, so you get the forgetful functors from sheaves of BundledModules to Sheaves of Ab and/or CommRing for free (this allows you define (1) in the first place in the case of sheaves).

[Reid Barton]

But the colimits of bundled modules aren't the colimits you want--they will have some kind of colimit in the ring part too.

[Reid Barton]

You need some kind of fiberwise colimit and now it is another custom construction

[Adam Topaz]

Hmm... I thought there may be a way to use the isomorphism to make this work without a custom construction. Let me think.

[Reid Barton]

For sheafification specifically, I think it does work, but you need some argument to verify it (something like forgetting to rings preserves limits and colimits)

[Reid Barton]

I mean that tells you that sheafifying a presheaf of O-modules gives you another O-module, but I guess you still have to check that it has the right universal property

[Jujian Zhang]

I verified that for any L : J ⥤ BundledModule, denote R to be L forget to ring and M to be L forget to abelian group, then lim M is a lim R-module, but couldn't prove (lim R, lim M) has the universal property. (because I can only get a group homomorphism instead of linear map)

[Adam Topaz]

Bah... I'm ready to throw my hands up and say that we should work internally in the Sheaf topos.

[Kevin Buzzard]

Can you explain what that means?

[Adam Topaz]

Roughly what I mean is one of the following two approaches:

Approach (3): Work with sheaves of sets, and define Ring-objects and Module-objects over such Ring-objects, inside of the category of sheaves of sets.

Approach (3'): Work with sheaves of abelian groups, define the monoidal structure, and use that to define Ring-objects (as monoid objects) and modules over them.

[Adam Topaz]

Of course these approaches come with their own problems.

[Adam Topaz]

Okay, now I really don't know what the best approach would be! It's an interesting problem to think about!

[Adam Topaz]

Reid Barton said:

But the colimits of bundled modules aren't the colimits you want--they will have some kind of colimit in the ring part too.

Considering this: Let me just think about modules for a moment (the case of (pre)sheaves should be similar): Suppose I have a diagram J : I ⥤ Module' A where Module' is the category of BunledModules with an isomorphism to A on the ring level (as in the code above).
Let F : Module' A ⥤ BundledModule be the forgetful functor, and consider the colimit of J ⋙ F, say M.
I suppose this is a module over the colimit of J ⋙ F ⋙ R where R : BundledModule ⥤ CommRing is the forgetful functor. Now, the isomorphisms used in the definition of Module' A give us a morphism from the colimit of J ⋙ F ⋙ R to A in the category of commutative rings. If I then base-change along this morphism, I suppose that should be the colimit of the original J.

(NB. I don't have a complete proof of this, but I think I convinced myself that this is true in the case of coproducts)

[Joël Riou]

At some point, anyway, it shall make sense to develop notions of group-objects, etc, in general monoidal categories, whether the monoidal structure is given by the categorical product (e.g. group schemes are group-objects in a category of S-schemes), or any other monoidal structure...

[Johan Commelin]

It's probably a good idea to keep sheaves of modules and group schemes in mind at the same time, when thinking about this problem. As you say, they could benefit from similar approaches.

[Jujian Zhang]

Adam Topaz said:

I.e. "sheafify" this definition:

structure Module' (A : CommRing.{u}) :=
(M : BundledModule.{u})
(e : M.R ≅ A)

@Adam Topaz Were you thinking about something like this:

universe u

variables {T : Top.{u}}

structure presheaf_of_module (𝓞 : presheaf CommRing T) :=
(self : presheaf BundledModule T)
(e : self ⋙ BundledModule.forget_to_Ring ≅ 𝓞)

If so, I think this approach is weird because, for 𝓕 : presheaf_of_module 𝓞, (𝓕 .obj U).M is not an 𝓞.obj U module, rather a (𝓕 .obj U).R module. I don't think class inference can pick up e and use it to synthesize what we want.

[Adam Topaz]

@Jujian Zhang see https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Definition.20of.20presheaf.20of.20modules/near/272815916

[Adam Topaz]

specifically this part:

instance (A : CommRing.{u}) : has_coe_to_sort (Module'.{u} A) (Type u) :=
⟨λ M, M.M.M⟩

instance (A : CommRing.{u}) (M : Module' A) : module A M :=
begin
  haveI : algebra A M.M.R := M.e.inv.to_algebra,
  change module A (restrict_scalars A M.M.R M),
  apply_instance,
end

[Junyan Xu]

The essential fiber could alternatively be defined as { f : structured_arrow 𝓞 forget // is_iso f } but I'm not in favor of the approach. What @Jujian Zhang has done is essentially defining the restriction/extension (lax) functors from presheaf CommRing X to Cat (short of showing they're adjoint), and after that we could show that the Grothendieck constructions applied to these functors are isomorphic to the presheaf BundledModule category, and transition freely between them. (Working with the presheaf of abelian groups and its sheafification should be nice enough, but if we can somehow use the bundled presheaf category to automatically put module structures on abelian groups and verify compatibilit in constructions, that would even be better.)

Here are some mathlib API that #12186 failed to use, which seems to make it longer than necessary:
docs#module.comp_hom (or docs#restrict_scalars.module), docs#linear_map.restrict_scalars, docs#tensor_product.left_module, docs#linear_map.base_change, docs#linear_map.compatible_smul, docs#tensor_product.algebra_tensor_module.lift.equiv (more general than the hom_equiv of the restriction-extension adjunction but I can't find a simpler version), docs#category_theory.adjunction.mk_of_hom_equiv

[Junyan Xu]

Various constructions involving O-modules (e.g. tensor product, and those in abelian category axioms) could be abstracted into the following: module categories with restriction of scalars can be seen as a (strict) functor module : CommRing ⥤ Cat; whenever we have a (oplax) natural transformation from "module^n" to module, i.e. a functor (module R)^n ⥤ module R for each comm ring R that "commutes" with restriction of scalars, we get a functor from O-modules^n to O-modules (the natural transformation could be made strict for direct sum, kernel, image etc. but not for tensor products!).

[Jujian Zhang]

Thanks for pointing out the useful lemmas and apis. Though I don’t fully understand all the terminologies, am I correct to assume that you are suggesting to build two versions of (pre)sheaf of modules in parallel and prove the two versions are isomorphic and choose whichever version that is more convenient to do some specific construction, for example shefification using functor into bundled module etc.

[Jack J Garzella]

Adam Topaz said:

Roughly what I mean is one of the following two approaches:

Approach (3): Work with sheaves of sets, and define Ring-objects and Module-objects over such Ring-objects, inside of the category of sheaves of sets.

Approach (3'): Work with sheaves of abelian groups, define the monoidal structure, and use that to define Ring-objects (as monoid objects) and modules over them.

Adam Topaz said:

Of course these approaches come with their own problems.

Can someone explain what the drawbacks to such an approach would be?

Surely it gets rid of the "category-is-hard" and "sheafification-is-hard" problems from before. I assume approaching it this way would make it much harder (at least, at first) to prove basic results. However, this seems like the most natural approach for a Bourbaki-style exposition in my (admittedly biased) opinion.

One a less subjective note, developing a theory of group/ring/module/monoid objects in an arbitrary category (not to mention groupoids in a category) will be quite useful as this is a suuuuuuper common perspective in cutting-edge research. I.e. buzzwords like group schemes, etale equivalence relations, ring spectra, etc. Might we end up having to go to this module-object approach eventually anyway?

[Adam Topaz]

The difficulty is that if you have a sheaf of modules $M$ over a sheaf of rings $\mathcal{O}$ and $U$ is open, then you want $M(U)$ to be a module over $\mathcal{O}(U)$ in the usual sense!

[Adam Topaz]

of course if you go with the internal objects approach, you could introduce the appropriate instances on such things, but that requires additional work and additional API.

[Adam Topaz]

In the ideal world, we would have all the definitions, and a robust API that would let us go back-and-forth between any two definitions you chose.

[Jack J Garzella]

Ok, maybe I'll try this definition out and see what happens

[Adam Topaz]

If you want to try to define monoid objects in sheaves on a site, and identify those with sheaves of monoids, that would be a very good test case!

[Adam Topaz]

We already have monoid objects in a monoidal category, but we don't have the monoidal structure on sheaves

[Adam Topaz]

Adam Topaz said:

...but we don't have the monoidal structure on sheaves

well, we do, it's just the cartesian structure in this case, so you should be good to go

[Adam Topaz]

docs#Mon_

[Adam Topaz]

There we go!

[Reid Barton]

That will give you sheaves of monoids

[Reid Barton]

Oh this is as a test case, carry on!

[Adam Topaz]

Well, anyway we should choose a single-sorted thing as our first test case before jumping into modules

[Reid Barton]

Right, I was thinking of rings

[Jack J Garzella]

Adam Topaz said:

Adam Topaz said:

...but we don't have the monoidal structure on sheaves

well, we do, it's just the cartesian structure in this case, so you should be good to go

So, I'm having trouble finding an instance of has_finite_products or has_products on any of the sheaf categories. Do you know if Lean has this somewhere? (also is there is a standard way to see if something has an instance somewhere? my method so far is searching on github)

[Jack J Garzella]

Adam Topaz said:

If you want to try to define monoid objects in sheaves on a site, and identify those with sheaves of monoids, that would be a very good test case!

Is there a standard thing that we want to mean by "identify" here? I.e. some possibilities show an equivalence of categories between monoid objects in the category of sheaves and sheaves of monoids, or give some sort of function that takes a monoid object in the category of sheaves and gives a sheaf of monoids and then give an inverse, or is there some more mathlibby way?

[Matt Diamond]

is there is a standard way to see if something has an instance somewhere?

do you mean starting from a specific structure and trying to figure out if it instantiates a specific class somehow? or do you mean starting from a class and finding a list of structures that instantiate it?

re: the latter, each class has an "Instances of this typeclass" list below it in the mathlib docs

[Andrew Yang]

Searching in the documentation for "sheaf has_limits_of_shape" gives docs#category_theory.Sheaf.category_theory.limits.has_limits_of_shape

[Andrew Yang]

I think showing the equivalence of the two categories is the right way to go?