Products of non-commutative monoids

Stream: Is there code for X?

[Eric Wieser]

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]

Do people do this?

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Kevin Buzzard]

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]

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]

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]

Summing over finset.range doesn't work for that

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

I guess I just live in a commutative world.

[Patrick Massot]

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

[Eric Wieser]

In that they introduce notation?

[Patrick Massot]

image.png

[Patrick Massot]

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]

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]

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

[Eric Wieser]

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]

Which hides the lists under the API

[Patrick Massot]

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

[Damiano Testa]

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]

OK I'm now sold on the idea.

[Adam Topaz]

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]

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

[Julian Külshammer]

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]

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

[Patrick Massot]

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

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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]

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

[Scott Morrison]

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

[Julian Külshammer]

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]

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]

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]

@Julian Külshammer Thanks for doing this!