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

1. it seems someone will want this anyway
2. it should be cheap?
3. it deftly avoids the annoying feature that at the moment we have tensor product of R-modules, but not of add_comm_groups

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

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

1. it seems someone will want this anyway

I completely agree

1. it should be cheap?

Hopefully.

1. it deftly avoids the annoying feature that at the moment we have tensor product of R-modules, but not of add_comm_groups

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