algebra R (monoid_algebra R G)

Stream: Is there code for X?

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

git reflog?

[Johan Commelin]

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

[Kenny Lau]

git does not do magic

[Scott Morrison]

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. :-)

[Yury G. Kudryashov]

algebra instance universal property

[Yury G. Kudryashov]

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.

[Scott Morrison]

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!

[Scott Morrison]

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.

[Yury G. Kudryashov]

Once we have an algebra instance, we have algebra_map

[Scott Morrison]

I see.

[Yury G. Kudryashov]

Or even better of_id which is an algebra homomorphism

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Yury G. Kudryashov]

I'm rewriting polynomials using monoid algebra

[Yury G. Kudryashov]

I'll PR it early next week

[Yury G. Kudryashov]

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

[Scott Morrison]

So shall I add this to your PR?

[Yury G. Kudryashov]

Yes