Zulip Chat Archive

Stream: Is there code for X?

Topic: algebra R (monoid_algebra R G)


view this post on Zulip Scott Morrison (Apr 14 2020 at 08:17):

@Yury G. Kudryashov, in your work on monoid_algebra recently, have you constructed the algebra R (monoid_algebra R G) instance?

view this post on Zulip Scott Morrison (Apr 14 2020 at 08:18):

I think I did this sometime last week, but I think I've accidentally deleted my branch. :-(

view this post on Zulip Johan Commelin (Apr 14 2020 at 08:32):

git reflog?

view this post on Zulip Johan Commelin (Apr 14 2020 at 08:32):

@Scott Morrison you can sometimes miraculously restore deleted branches...

view this post on Zulip Kenny Lau (Apr 14 2020 at 08:34):

git does not do magic

view this post on Zulip Scott Morrison (Apr 14 2020 at 09:58):

Actually my branch was still on github, even though I'd deleted it locally. It doesn't quite have what I wanted: it has the instance, but then a big comment about how it breaks polynomials. :-)

view this post on Zulip Yury G. Kudryashov (Apr 14 2020 at 17:37):

algebra instance universal property

view this post on Zulip Yury G. Kudryashov (Apr 14 2020 at 17:52):

I'm not sure if I picked up all useful lemmas from my polynomial branch. Unfortunately I will have no time for this for several days.

view this post on Zulip Scott Morrison (Apr 15 2020 at 01:25):

Oops... Serves me right for not doing a better job reviewing PRs. I duplicated some of this in #2412. It mostly looks like yours is better!

view this post on Zulip Scott Morrison (Apr 15 2020 at 01:33):

Oh, they are not the same, and I think the pushout of the two PRs may be even better. I separately define the ring_hom single_one.ring_hom : k →+* monoid_algebra k G, and use that in constructing the algebra instance, while you've inlined it into the algebra instance.

view this post on Zulip Yury G. Kudryashov (Apr 15 2020 at 01:35):

Once we have an algebra instance, we have algebra_map

view this post on Zulip Scott Morrison (Apr 15 2020 at 01:35):

I see.

view this post on Zulip Yury G. Kudryashov (Apr 15 2020 at 01:36):

Or even better of_id which is an algebra homomorphism

view this post on Zulip Scott Morrison (Apr 15 2020 at 01:37):

Did you consider doing the add_monoid_algebra version of this, so polynomial can just acquire its algebra instance from this file?

view this post on Zulip Scott Morrison (Apr 15 2020 at 01:37):

That's the only other thing I can see perhaps worth salvaging from my PR.

view this post on Zulip Scott Morrison (Apr 15 2020 at 01:38):

Unless there is a reason not to do it, I can try doing the requisite copy-pasting inside your PR.

view this post on Zulip Yury G. Kudryashov (Apr 15 2020 at 01:38):

I'm rewriting polynomials using monoid algebra

view this post on Zulip Yury G. Kudryashov (Apr 15 2020 at 01:38):

I'll PR it early next week

view this post on Zulip Yury G. Kudryashov (Apr 15 2020 at 01:39):

But it's worth having algebra instance for add monoid algebras anyway

view this post on Zulip Scott Morrison (Apr 15 2020 at 01:40):

So shall I add this to your PR?

view this post on Zulip Yury G. Kudryashov (Apr 15 2020 at 01:40):

Yes


Last updated: May 07 2021 at 21:10 UTC