Magma algebras

Stream: maths

[Oliver Nash]

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]

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 : add_comm_monoid (magma_algebra R X) := finsupp.add_comm_monoid

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_add' := sorry,
    map_smul' := sorry,
  map_add'  := sorry,
  map_smul' := sorry, }, }

end magma_algebra

[Oliver Nash]

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]

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]

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

[Oliver Nash]

I was wondering if someone would ask!

[Oliver Nash]

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]

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

[Oliver Nash]

(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]

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]

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]

Adam Topaz said:

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]

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

[Eric Wieser]

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

[Eric Wieser]

In fact, the assumptions aren't even there!

[Adam Topaz]

@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]

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]

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

[Eric Wieser]

No need for a new definition for magma_algebra

[Adam Topaz]

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

[Adam Topaz]

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]

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]

Do we have something like this in mathlib?

[Yakov Pechersky]

docs#with_one.monoid

[Adam Topaz]

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

[Adam Topaz]

Do we even have nonassociative algebras in mathlib?

[Eric Wieser]

docs#algebra requires semiring which is associative

[Damiano Testa]

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

[Oliver Nash]

Adam Topaz said:

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]

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]

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]

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]

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]

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]

Thanks, I'll take a quick look now.

[Eric Wieser]

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]

Thanks, I saw the merge. Nice!

[Oliver Nash]

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.