# Zulip Chat Archive

## Stream: maths

### Topic: schemes over k

#### Scott Morrison (Sep 14 2020 at 03:48):

@Kenny Lau, @Johan Commelin, @Kevin Buzzard, I was wondering if before we go much further we should generalise the algebraic geometry files away from `CommRing`

to commutative algebras over some comm_ring `k`

(e.g. `int`

).

- it seems someone will want this anyway
- it should be cheap?
- it deftly avoids the annoying feature that at the moment we have tensor product of
`R`

-modules, but not of`add_comm_group`

s

#### Scott Morrison (Sep 14 2020 at 03:49):

The second question is whether we should just generalise all the way to monoid objects in some arbitrary monoidal category. The suggestion to handle sheaves of modules as module objects for an internal ring object in sheaves-of-abelian-groups would mean having to jump across that equivalence anyway...

#### Adam Topaz (Sep 14 2020 at 04:29):

Generalizations of schemes to symmetric monoidal categories (e.g. in the sense of Toen-Vaquie) don't always have underlying topological spaces, as far as I know. This might be a non-starter for some people. Perhaps there is there another construction you had in mind?

#### Scott Morrison (Sep 14 2020 at 04:49):

I guess I wasn't actually intending a particular generalisation, just an abstraction: to construct a sheaf of `CommMon_ (Module k)`

instead of a sheaf of `CommRing`

s.

#### Johan Commelin (Sep 14 2020 at 06:00):

Scott Morrison said:

Kenny Lau, Johan Commelin, Kevin Buzzard, I was wondering if before we go much further we should generalise the algebraic geometry files away from

`CommRing`

to commutative algebras over some comm_ring`k`

(e.g.`int`

).

- it seems someone will want this anyway

I completely agree

- it should be cheap?

Hopefully.

- it deftly avoids the annoying feature that at the moment we have tensor product of
`R`

-modules, but not of`add_comm_group`

s

But someone will want those anyway?

In general, I think the only solution is to have a huge API of compatibilities between the "big" category of ring/schemes and the "relative" categories of `k`

-algebra/schemes over a base (ring/scheme) and all the base change functors that come with them.

#### Kenny Lau (Sep 14 2020 at 07:46):

why do we need to tensor add_comm_groups?

#### Johan Commelin (Sep 14 2020 at 07:48):

why do we need the absolute category of schemes?

#### Kenny Lau (Sep 14 2020 at 07:48):

also:

```
import linear_algebra.tensor_product
universes u v
open_locale tensor_product
section
variables (M : Type u) [add_comm_group M] (N : Type v) [add_comm_group N]
#check M ⊗[ℤ] N
end
section
variables (M : Type u) [add_comm_monoid M] (N : Type v) [add_comm_monoid N]
#check M ⊗[ℕ] N
end
```

#### Scott Morrison (Sep 14 2020 at 09:40):

@Kenny Lau, I was trying to put together the `monoidal_category`

instance on `AddCommGroup`

, and while I found that what you show in your example works, it falls apart at the morphism level.

#### Scott Morrison (Sep 14 2020 at 09:41):

I was hoping I could almost copy and paste the `algebra/category/Module/monoidal.lean`

file over, mutatis mutandi, but without much success.

#### Scott Morrison (Sep 14 2020 at 09:42):

In the meantime I did manage to prove that you can transform a monoidal structure across an equivalence, but I haven't actually tried it out on `AddCommGroup ~ Module int`

.

Last updated: May 19 2021 at 02:10 UTC