Zulip Chat Archive

Stream: general

Topic: non-unital sub(semi)rings

Jireh Loreaux (Apr 20 2022 at 19:56):

I'm ready to define non-unital sub(semi)rings. Is there anything I should know about the current sub(semi)ring API which is outdated or deprecated? Otherwise I am planning to base my work on that.

Kevin Buzzard (Apr 20 2022 at 22:12):

The deprecated stuff is hopefully all in src/deprecated nowadays

Yaël Dillies (Apr 20 2022 at 22:13):

And Scott is about to delete it!

Jireh Loreaux (Apr 20 2022 at 23:41):

Sorry, I think what I mean is the parallel of the hom refactor. There the refactor is not complete and even the parts that are still have vestiges of the old format. I'm not sure if there is any similarity with the set_like stuff.

Eric Wieser (Apr 21 2022 at 05:35):

I think @Anne Baanen is in the middle of such a refactor, but is away from lean at the moment

Anne Baanen (Apr 21 2022 at 08:25):

Thanks for the ping! I was ill last week but slowly doing better. The current state is indeed that there are still some vestiges of the old approach around, especially for subobjects. But you should be able to already use the new set_like subclasses like docs#mul_mem_class and docs#add_submonoid_class.

Anne Baanen (Apr 21 2022 at 08:28):

Essentially, if you copy the current subsemiring definition and make sure to remove the instances that directly reference subsemiring, rather than subsemiring_class then you should be up to date with the refactor.

Eric Wieser (Apr 21 2022 at 10:22):

Glad to hear you're doing a bit better! I was indeed thinking of #11759 when I remarked it was in progress.

Jireh Loreaux (Apr 21 2022 at 12:36):

Got it, thanks! I suspected something like this must be the case.

Last updated: Dec 20 2023 at 11:08 UTC