Zulip Chat Archive

Stream: maths

Topic: Magma algebras


view this post on Zulip 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.

view this post on Zulip 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 : 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Mar 06 2021 at 21:56):

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

view this post on Zulip Oliver Nash (Mar 06 2021 at 22:01):

I was wondering if someone would ask!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Oliver Nash (Mar 07 2021 at 11:01):

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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Mar 07 2021 at 13:26):

In fact, the assumptions aren't even there!

view this post on Zulip Adam Topaz (Mar 07 2021 at 13:26):

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

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

all of which have left adjoints (by general universal algebra nonsense). The left adjoint MonoidSemiring\mathbf{Monoid} \to \mathbf{Semiring} is the monoid algebra (over N\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 N\mathbb{N}, but it can be generalized)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 07 2021 at 13:29):

No need for a new definition for magma_algebra

view this post on Zulip Adam Topaz (Mar 07 2021 at 13:30):

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

view this post on Zulip 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

view this post on Zulip 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)}⟩

view this post on Zulip Adam Topaz (Mar 07 2021 at 13:43):

Do we have something like this in mathlib?

view this post on Zulip Yakov Pechersky (Mar 07 2021 at 13:43):

docs#with_one.monoid

view this post on Zulip 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!

view this post on Zulip Adam Topaz (Mar 07 2021 at 14:04):

Do we even have nonassociative algebras in mathlib?

view this post on Zulip Eric Wieser (Mar 07 2021 at 14:40):

docs#algebra requires semiring which is associative

view this post on Zulip Damiano Testa (Mar 07 2021 at 14:40):

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

view this post on Zulip Oliver Nash (Mar 07 2021 at 16:37):

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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Oliver Nash (Mar 07 2021 at 17:22):

Thanks, I'll take a quick look now.

view this post on Zulip 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?

view this post on Zulip Oliver Nash (Mar 08 2021 at 17:14):

Thanks, I saw the merge. Nice!

view this post on Zulip 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