## Stream: maths

### Topic: Magma algebras

#### Oliver Nash (Mar 06 2021 at 21:43):

Rather ironically, having previously wondered if Mathlib's generalisation of a group algebra to a monoid algebra was necessary, I now find myself wanting to generalise it further to a raw magma algebra.

#### Oliver Nash (Mar 06 2021 at 21:44):

Of course very little is true at this level of generality, basically just the following:

import algebra.monoid_algebra

universes u v

noncomputable theory

namespace magma_algebra

variables (R : Type u) (X : Type v) [comm_semiring R] [has_mul X]

open finsupp

def magma_algebra := X →₀ R

instance : semimodule R (magma_algebra R X) := finsupp.semimodule X R

instance : has_mul (magma_algebra R X) :=
⟨λ a b, a.sum $λ m₁ t₁, b.sum$ λ m₂ t₂, single (m₁ * m₂) (t₁ * t₂)⟩

def mul_bilinear : magma_algebra R X →ₗ[R] magma_algebra R X →ₗ[R] magma_algebra R X :=
{ to_fun    := λ a,
{ to_fun := λ b, a * b,
map_smul' := sorry,
map_smul' := sorry, }, }

end magma_algebra


#### Oliver Nash (Mar 06 2021 at 21:46):

In other words we get a (in general) non-unital, (in general) non-associative algebra. Note that we don't have a bundled typeclass for these.

#### Oliver Nash (Mar 06 2021 at 21:50):

So I think what I'd like to do is a slight refactor of our monoid algebras to factor them through something along the lines of the above. Any objections / comments?

#### Bryan Gin-ge Chen (Mar 06 2021 at 21:56):

Out of curiosity, what are you planning to use these for?

#### Oliver Nash (Mar 06 2021 at 22:01):

I was wondering if someone would ask!

#### Oliver Nash (Mar 06 2021 at 22:02):

I want to construct free Lie algebras and the standard construction is to build them as a quotient of the magma algebra of the free magma of a type.

#### Oliver Nash (Mar 06 2021 at 22:03):

I was delighted to see that we actually have free magmas so it looks like I can get this to work.

#### Oliver Nash (Mar 06 2021 at 22:06):

(Given a type X and a commutative ring R, there is a much easier construction that constructs the free Lie algebra FL(R, X) as the Lie subalgebra generated by X inside the free associative algebra F(X, R) but it only works with some assumptions on R, so I don't want to use it.)

#### Oliver Nash (Mar 06 2021 at 22:07):

I believe I could also just construct FL(R, X) directly as a quotient of a custom inductive type like we have for F(X) but I figured I'd try the standard construction first.

#### Adam Topaz (Mar 07 2021 at 00:10):

I would suggest the following route: define the free monoid on a magma, then the magma algebra as the monojd algebra associated to that!

#### Oliver Nash (Mar 07 2021 at 11:01):

I would suggest the following route: define the free monoid on a magma, then the magma algebra as the monojd algebra associated to that!

I can't quite seem to make sense of this. Could you spell it out a bit more?

#### Oliver Nash (Mar 07 2021 at 12:54):

I've sketched out how this might look if I push ahead here: https://github.com/leanprover-community/mathlib/pull/6571

#### Eric Wieser (Mar 07 2021 at 13:25):

Is the api the same as src#monoid_algebra? If so, can you just relax the typeclass assumptions on the latter?

#### Eric Wieser (Mar 07 2021 at 13:26):

In fact, the assumptions aren't even there!

#### Adam Topaz (Mar 07 2021 at 13:26):

@Oliver Nash What I had in mind is the following: Let $\mathbf{Semiring}$ resp. $\mathbf{Monoid}$ resp. $\mathbf{Magma}$ denote the categories of semirings resp. monoids resp. magmas.
There are forgetful functors

$\mathbf{Semiring} \to \mathbf{Monoid} \to \mathbf{Magma}$

all of which have left adjoints (by general universal algebra nonsense). The left adjoint $\mathbf{Monoid} \to \mathbf{Semiring}$ is the monoid algebra (over $\mathbb{N}$, but this can be generalized if you consider algebras as well), and the left adjoint from magmas to monoids is what I mean by "the free monoid on a magma". The composition of these two left adjoints is the left adjoint of the composition, which is the so-called "magma algebra" (again over $\mathbb{N}$, but it can be generalized)

#### Adam Topaz (Mar 07 2021 at 13:27):

However if you need an explicit description of the magma algebra as a finsupp like in your code, then that's a different story and it's probably better to make an explicit construction as you did.

#### Eric Wieser (Mar 07 2021 at 13:28):

I think docs#monoid_algebra.has_mul has an unnecessary monoid assumption that can be relaxed to has_mul

#### Eric Wieser (Mar 07 2021 at 13:29):

No need for a new definition for magma_algebra

#### Adam Topaz (Mar 07 2021 at 13:30):

Not true... The 1 in the monoid must become the 1 in the algebra

#### Adam Topaz (Mar 07 2021 at 13:31):

So you first need to add a 1 in some free way, then make the algebra, and in this case, yes I agree with you @Eric Wieser

#### Adam Topaz (Mar 07 2021 at 13:43):

Here's a silly way to "attach a one" to a type with has_mul:

variables (α : Type*) [has_mul α]

def with_one := option α

instance : has_one (with_one α) := ⟨none⟩

instance : has_mul (with_one α) :=
⟨λ x y, do {X ← x, Y ← y, return (X * Y)}⟩


#### Adam Topaz (Mar 07 2021 at 13:43):

Do we have something like this in mathlib?

#### Yakov Pechersky (Mar 07 2021 at 13:43):

docs#with_one.monoid

#### Adam Topaz (Mar 07 2021 at 14:03):

Oh wait... I now realize that the magma algebra need not be associative. Ignore everything I said!

#### Adam Topaz (Mar 07 2021 at 14:04):

Do we even have nonassociative algebras in mathlib?

#### Eric Wieser (Mar 07 2021 at 14:40):

docs#algebra requires semiring which is associative

#### Damiano Testa (Mar 07 2021 at 14:40):

Aren't Lie algebras (barely) non-associative?

#### Oliver Nash (Mar 07 2021 at 16:37):

Do we even have nonassociative algebras in mathlib?

We do not. We do have Lie algebras as Damiano mentioned but these are not set up as a special type of non-associative algebra (obviously, since we don't have such a notion). In particular, algebra and lie_algebra most recent common ancestor is has_scalar!

Note also that Lie algebra multiplication is encoded using the has_bracket typeclass rather than has_mul, though we should be able to meta-program-away any awkwardness associated with this.

#### Oliver Nash (Mar 07 2021 at 16:40):

As I've worked on Lie algebras, I have occasionally considered whether we might need to unify with associative algebras, presumably via a general not-necessarily-associative, not-necessarily-unital algebra. So far the only compelling case has been for derivations and this is part of the reason I have avoided defining them for Lie algebras for now.

#### Oliver Nash (Mar 07 2021 at 16:42):

Eric Wieser said:

I think docs#monoid_algebra.has_mul has an unnecessary monoid assumption that can be relaxed to has_mul

Agreed, in the sense that it is unnecessary in order to define the convolution multiplication; that is essentially my point in seeking to define these magma algebras.

#### Oliver Nash (Mar 07 2021 at 16:51):

Eric Wieser said:

No need for a new definition for magma_algebra

Basically I agree and indeed in my candidate PR I reuse the definition for the convolution multiplication so I don't actually make a new definition. On the other hand, I am creating a new name magma_algebra because I want to avoid having to call the magma_algebra a monoid_algebra.

#### Oliver Nash (Mar 07 2021 at 16:51):

I hope to have a little more time later today. Perhaps the best thing to do if for me to turn that PR into a genuine proposal and seek feedback there?

#### Eric Wieser (Mar 07 2021 at 16:55):

I just created #6572 with the refactor I was suggesting. I'm sure it doesn't go all the way to what you're after, but it seems like a sensible cleanup anyway

#### Oliver Nash (Mar 07 2021 at 17:22):

Thanks, I'll take a quick look now.

#### Eric Wieser (Mar 08 2021 at 17:05):

My PR is merged, so you should now be good to go on splitting out magma_algebra.

It seems to me what you're actually missing is some kind of algebra_without_one typeclass which has smul_mul_assoc and mul_smul_comm fields?

#### Oliver Nash (Mar 08 2021 at 17:14):

Thanks, I saw the merge. Nice!

#### Oliver Nash (Mar 08 2021 at 17:15):

I do plan to continue now. In the meantime I bit the bullet and put together a proposal for non-associative algebras https://github.com/leanprover-community/mathlib/pull/6591 which I think is approximately what you're describing. I guess I'll wait and see how that is received. It's just one possible way to set things up.

Last updated: May 11 2021 at 16:22 UTC