schemes over k

Stream: maths

[Scott Morrison]

@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]

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]

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]

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]

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

2. it should be cheap?

Hopefully.

3. 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]

why do we need to tensor add_comm_groups?

[Johan Commelin]

why do we need the absolute category of schemes?

[Kenny Lau]

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]

@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]

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]

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.