Zulip Chat Archive

Stream: maths

Topic: schemes over k


view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Sep 14 2020 at 07:46):

why do we need to tensor add_comm_groups?

view this post on Zulip Johan Commelin (Sep 14 2020 at 07:48):

why do we need the absolute category of schemes?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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