# Zulip Chat Archive

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

algebra instance universal property

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

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

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

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

So shall I add this to your PR?

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

Yes

Last updated: May 07 2021 at 21:10 UTC