## Stream: Is there code for X?

### Topic: Products of non-commutative monoids

#### Eric Wieser (Mar 14 2021 at 15:06):

What's the canonical spelling of the product of a sequence of non-commutative elements?

def prod' {M ι : Type*} [monoid M] (f : ι → M) (l : list ι) : M := (l.map f).prod


Would it make sense to introduce notation for this?

notation ∏⃑ binders  in  l ,  r:(scoped:67 f, list.prod \$ list.map f l) := r

#check (∏⃑ i in [1, 2, 3], i*i)


#### Kevin Buzzard (Mar 14 2021 at 15:45):

Do people do this?

#### Eric Wieser (Mar 14 2021 at 15:45):

Write that notation(which I largely made up), or take the product of a sequence of non-commutative elements?

#### Eric Wieser (Mar 14 2021 at 15:47):

It would allow stating things like star (∏⃑ i in l, f i) = ∏⃑ i in l.reverse, star (f i), for instance (the n-ary docs#star_mul)

#### Kevin Buzzard (Mar 14 2021 at 15:53):

Noncommutative finite products. You can state a lemma but does anyone want to use it? If people do then fair enough

#### Eric Wieser (Mar 14 2021 at 15:56):

The motivation was making the statement of docs#clifford_algebra.involute_prod_map_ι more readable

#### Eric Wieser (Mar 14 2021 at 15:57):

The lemma itself primarily exists as a "look human, this definition is the one you would hand-wave", rather than actually being useful in a proof

#### Eric Wieser (Mar 14 2021 at 15:57):

Which makes it all the more useful to have some sort of reasonable notation for it

#### Kevin Buzzard (Mar 14 2021 at 15:58):

Right. My feeling is just that list.prod is a CS thing, lists are everywhere in computer science, but in maths we often just use sets

#### Kevin Buzzard (Mar 14 2021 at 16:00):

If you need it then you could give it one of those fish notations that we don't use in maths :-) >=>-> or whatever

#### Eric Wieser (Mar 14 2021 at 16:01):

Yeah, I'm not tied to list specifically here. Just something like take the product of f(i) from i = 0 to n would be enough, for non-commutative f(i)

#### Eric Wieser (Mar 14 2021 at 16:01):

Summing over finset.range doesn't work for that

#### Kevin Buzzard (Mar 14 2021 at 16:02):

I guess I'm saying that one has to draw a line somewhere when making an API and I usually draw the line before anything involving list.prod. But if you want it then all I ask is that you don't steal a notation mathematicians might want to use for something else

#### Patrick Massot (Mar 14 2021 at 16:36):

I don't understand what Kevin is saying. Certainly we want product of lists of elements in non-commutative groups.

#### Kevin Buzzard (Mar 14 2021 at 16:41):

I guess I just live in a commutative world.

#### Patrick Massot (Mar 14 2021 at 16:43):

By the way, Bourbaki answers Eric's question on Page 3 of their chapter 1 of algebra .

#### Eric Wieser (Mar 14 2021 at 16:44):

In that they introduce notation?

image.png

#### Patrick Massot (Mar 14 2021 at 16:48):

Note for Kevin: as you can see from the very bottom of the page, this comes before defining associativity of a composition law. The definition of commutativity comes two sections later...

#### Eric Wieser (Mar 14 2021 at 16:49):

If I'm reading that correctly, that implies that we should probably just reuse the finset notation, perhaps via a has_sum class?

#### Patrick Massot (Mar 14 2021 at 16:50):

I'm not claiming anything regarding mathlib, I try to convince Kevin this isn't computer science.

#### Eric Wieser (Mar 14 2021 at 16:54):

well, it's possibly computer science if we use lists, the Bourbaki definition is closer to

def prod' {M ι : Type*} [monoid M] [linear_order ι] (f : ι → M) (s : finset ι) : M :=
((s.sort (≤)).map f).prod


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

Which hides the lists under the API

#### Patrick Massot (Mar 14 2021 at 17:10):

They assume ι is finite and equipped with a linear order.

#### Damiano Testa (Mar 14 2021 at 18:13):

I have seen the description below of the fundamental group of a (connected, orientable) surface of genus $g$ fairly often, so I would welcome a "non-commutative product"!

$\pi_1(S_g)$ = (free group on $2g$ generators $a_1, b_1,\ldots , a_g, b_g$) / $\prod [a_i, b_i]$

#### Kevin Buzzard (Mar 14 2021 at 18:59):

OK I'm now sold on the idea.

#### Adam Topaz (Mar 14 2021 at 19:17):

Here's the most computer sciency way I can think of to state "associativity" :smile: :

import algebra

example {M : Type*} [monoid M] (ls : list (list M)) :
(ls.map list.prod).prod = (mjoin ls).prod := sorry


#### Adam Topaz (Mar 14 2021 at 19:18):

(It looks like this lemma is missing from mathlib BTW)

#### Julian Külshammer (Mar 14 2021 at 19:24):

This is definitely on the list of things I found a strange commutativity assumption when looking through mathlib. I would claim that if pressed most mathematicians would define a product of x1 to xn via a list and not only in the commutative setting via some counting of how many times xi appears like it is done in mathlib. There are results in mathlib which would be true for arbitrary rings if the product notation would be defined via lists instead.

#### Adam Topaz (Mar 14 2021 at 19:31):

Actually, forget what I said above, this is docs#list.prod_join (just using join as opposed to mjoin)

#### Patrick Massot (Mar 14 2021 at 20:18):

This is a fight I lost many years ago. I never really understood why.

#### Bryan Gin-ge Chen (Mar 14 2021 at 21:40):

We could definitely use more API to make working with big operators over lists more convenient. Right now everything is in terms of finsets only because no one has put in the work to duplicate the lemmas for lists and multisets.

#### Patrick Massot (Mar 14 2021 at 21:45):

The fight I lost a long time ago was to start with the non-commutative case and deduce the commutative case from there.

#### Kevin Buzzard (Mar 14 2021 at 22:36):

We had to make some sacrifices. In analysis we did it properly. I wanted to do differentiable functions of one variable but lots of people wanted to do it properly. As a result we have a very impressive and robust theory of topological vector spaces, all manner of integrals, and we just proved FTC and can now integrate sin(x) from 0 to pi and can prove the sphere is a manifold. I am only too aware of how impressive this is but it does not sell our prover. In algebra we just got on with making a pile of commutative algebra and then all of a sudden we had schemes, and, a year later, perfectoid spaces. Now we need to go back and refactor stuff but it put Lean on the map. It's swings and roundabouts maybe?

#### Scott Morrison (Mar 15 2021 at 06:09):

Patrick Massot said:

The fight I lost a long time ago was to start with the non-commutative case and deduce the commutative case from there.

Is it really too late? I remember back then being skeptical of taking the Coq version as gospel, but obviously our current approach is terrible. :-)

#### Kevin Buzzard (Mar 15 2021 at 06:29):

No surely it's not too late. I would imagine that it's just some plumbing at the bottom. I would propose ideal meaning "left ideal" in the non-commutative case.

#### Scott Morrison (Mar 15 2021 at 06:43):

@Kevin Buzzard, I think Patrick was referring to big_operators, not ideal.

#### Scott Morrison (Mar 15 2021 at 06:44):

But yes, I'd be happy if ideal meant "left ideal".

#### Julian Külshammer (Mar 15 2021 at 06:44):

I don't know how it is in other areas, but I feel that it is more standard to have ideal mean two-sided ideal.

#### Julian Külshammer (Mar 15 2021 at 07:32):

A few days ago I made a list collecting the changes that I thought would be needed for mathlib with respect to commutativity. Feel free to comment or expand: https://github.com/leanprover-community/mathlib/projects/10

#### Julian Külshammer (Mar 15 2021 at 07:36):

I think the first step (which probably is also helpful in the commutative setting) would be to get R-S bimodules into mathlib. Then one could use this to split the uses of left ideal and two-sided ideal in the noncommutative setting (independent of which one gets to be called ideal). Note that bi-ideal is not a term used for this structure (googling said it is used for something else). I would think that in most cases in mathlib now, the correct generalisation is to replace commutative ideal by two-sided ideal.

#### Johan Commelin (Mar 15 2021 at 07:37):

@Julian Külshammer Thanks for doing this!

Last updated: May 17 2021 at 15:13 UTC