tensor product of sheaves

Stream: condensed mathematics

[Johan Commelin]

We'll need to be able to take tensor products of condensed abelian groups (and condensed $ℤ[T⁻¹]$-modules). I've created https://github.com/leanprover-community/lean-liquid/issues/76 to track this todo.

[Kevin Buzzard]

It's great that LTE is forcing us to develop category theory like this.

One thing I've never really got to the bottom of is how to do sheaves of modules over a sheaf of rings cleanly in dependent type theory -- a.k.a. an action of a sheaf of rings on a sheaf of groups. But will we need anything like this here?

[Johan Commelin]

Not really. We need it only for constant sheaves.

[Johan Commelin]

In fact, we need it for Ab and for {objects of Ab + distinguished endomorphism}.

[Johan Commelin]

The latter is of course equivalent to $ℤ[T⁻¹]$-modules.

[Adam Topaz]

@Kevin Buzzard I think one reasonable approach would be to consider sheaves taking values in the category of pairs $(A,M)$ with $A$ a ring and $M$ an $A$-module. If you compose with the forgetful functor $(A,M) \mapsto A$ that would give a functor from such sheaves to sheaves of rings, and we could then take something in the essential fiber of this functor over a given sheaf of rings.

[Adam Topaz]

I think this tensor product issue should be fairly straightforward to do. I'll give it a go once I finish getting the general version of the adjunction between sheaf categories into mathlib (which we'll need for the $S \mapsto \mathbb{Z}[S]$ functor)

[Johan Commelin]

I think the question about sheaves of modules over an arbitrary sheaf of rings is interesting, but let me say again that it isn't relevant to LTE.
That said, Adam, would your proposal be nice to work with in concrete examples? I would be inclined to copy the (long-winded and somewhat ugly) definition that appears in introductory courses: a sheaf of abelian groups, together with compatible module structures of the $𝒪(U)$ on the $F(U)$.

[Peter Scholze]

I'm almost certain that Adam's proposal is the "right" one (also in the sense that it will be the least painful to work with in practice).

[Johan Commelin]

Interesting!

[Kevin Buzzard]

This approach hadn't occurred to me before. The last time this issue was raised we ended up in some hairy discussion about how to get a presheaf to act on another presheaf. This way looks much nicer!

[Adam Topaz]

:wink: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Free.20stuff/near/209805136

[Adam Topaz]

As far as I can tell, we still don't have a def restrict_scalars {A B : CommRing} (f : A ⟶ B) : Module B ⥤ Module A in mathlib

[Eric Rodriguez]

no I remember making that as a way to mess with categories in mathlib and wondering if it was anywhere in mathlib

[Eric Rodriguez]

there's some code for it lying around somewhere

[Eric Rodriguez]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/messing.20around.20with.20categories

[Eric Rodriguez]

Probably what you were remembering Adam!