Zulip Chat Archive
Stream: triage
Topic: issue #4013: properties of ring homomorphisms
Random Issue Bot (Dec 01 2020 at 14:24):
Today I chose issue 4013 for discussion!
properties of ring homomorphisms
Created by @Johan Commelin (@jcommelin) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 04 2021 at 14:29):
Today I chose issue 4013 for discussion!
properties of ring homomorphisms
Created by @Johan Commelin (@jcommelin) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Jan 04 2021 at 18:37):
It's most definitely still relevant, and a great guide to what we should be doing.
Random Issue Bot (Feb 07 2021 at 14:18):
Today I chose issue 4013 for discussion!
properties of ring homomorphisms
Created by @Johan Commelin (@jcommelin) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Nov 30 2021 at 14:19):
Today I chose issue 4013 for discussion!
properties of ring homomorphisms
Created by @Johan Commelin (@jcommelin) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Dec 24 2021 at 14:17):
Today I chose issue 4013 for discussion!
properties of ring homomorphisms
Created by @Johan Commelin (@jcommelin) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Andrew Yang (Dec 24 2021 at 16:16):
There sure are lots of todos.
Thanks to Kevin for pointing me here.
I think the base change stuff could definitely get some love now that the fibered products of schemes are on the way.
Kevin Buzzard (Dec 24 2021 at 17:27):
This is just pure ring theory and probably we have base change of ring morphisms along tensor products (I guess?)
Johan Commelin (Dec 24 2021 at 20:30):
nope, we don't really have that so far. There is a def tensor_product.map or something. But no API.
Kevin Buzzard (Dec 24 2021 at 21:16):
So what do we need -- pullback of finitely-generated is finitely-generated, pullback of flat is flat etc etc? Shall I try to get a PhD student interested?
Andrew Yang (Dec 24 2021 at 22:08):
Yes. I suppose most of the properties we will need in the near future are already on that list.
Though I think showing that some properties are local will also be helpful.
It would be great if someone works on these stuff.
But I'll probably end up doing them if they are not yet done when we need them.
Kevin Buzzard (Dec 24 2021 at 22:11):
@Andrew Yang I'll try to find someone to work on the issue. Can you edit the issue and add the properties which you want to be local and perhaps formalise exactly which form you'd like the lemmas to take?
Andrew Yang (Dec 24 2021 at 22:13):
Thanks! I'll do that tomorrow since it is too late in the night for me now.
Andrew Yang (Dec 26 2021 at 01:54):
Sorry for the delay, I'm away from home this weekend.
I've edited the issue and also included some thought on how it should be implemented.
Kevin Buzzard (Dec 26 2021 at 02:11):
This is great, I'll see if I can get someone working on it
Random Issue Bot (Feb 26 2022 at 14:13):
Today I chose issue 4013 for discussion!
properties of ring homomorphisms
Created by @Johan Commelin (@jcommelin) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 04 2023 at 14:09):
Today I chose issue 4013 for discussion!
properties of ring homomorphisms
Created by @Johan Commelin (@jcommelin) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC