## Stream: Is there code for X?

### Topic: algebra R (monoid_algebra R G)

#### 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?

#### 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. :-(

#### Johan Commelin (Apr 14 2020 at 08:32):

git reflog?

#### Johan Commelin (Apr 14 2020 at 08:32):

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

#### Kenny Lau (Apr 14 2020 at 08:34):

git does not do magic

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

#### 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.

#### 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!

#### 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.

#### Yury G. Kudryashov (Apr 15 2020 at 01:35):

Once we have an algebra instance, we have algebra_map

I see.

#### Yury G. Kudryashov (Apr 15 2020 at 01:36):

Or even better of_id which is an algebra homomorphism

#### 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?

#### Scott Morrison (Apr 15 2020 at 01:37):

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

#### 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.

#### Yury G. Kudryashov (Apr 15 2020 at 01:38):

I'm rewriting polynomials using monoid algebra

#### Yury G. Kudryashov (Apr 15 2020 at 01:38):

I'll PR it early next week

#### Yury G. Kudryashov (Apr 15 2020 at 01:39):

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