Non commutative Finset.prod

Stream: new members

[Gaëtan Serré]

Hello, is it possible to define a product over a finite, noncommutative group:

import Mathlib

open BigOperators

-- Fails because G is not commutative.
def generative_subgroup  {α : Type} [G : Group (Fintype α)] (G' : Subgroup (Fintype α)) := ∀ (g : Fintype α), ∃ (S : Finset G'), ∏ g' in S, g' = g

I saw that docs#Finset.prod depends on fold operations on lists, that return the same result when applied to lists that are permutation of each others (hence to necessity of commutativity). Is there a "fold" depending on the order of operations or do I have to define my own operator on Finset?

[Richard Copley]

I think List.prod is the closest thing. To illustrate why there isn't a noncommutative product defined using Finset, suppose that there were:

import Mathlib.Data.Finset.Basic

example {α : Type*} [Monoid α]
    (MyNoncommProd : (s : Finset ℕ) → (f : ℕ → α) → α) (f : ℕ → α) :
    MyNoncommProd {1, 2} f = MyNoncommProd {2, 1} f := by
  rw [Finset.pair_comm 1 2]

[Gaëtan Serré]

Ok I get what you mean, thanks a lot!

[Gaëtan Serré]

Moreover, I think docs#List.prod is much more adapted to what I want to do next anyway

[Richard Copley]

That's what is usually used. See the definition of ExteriorAlgebra.ιMulti (in "Mathlib.LinearAlgebra.ExteriorAlgebra.Basic"), for example.

[Richard Copley]

Or more directly, MultilinearMap.mkPiAlgebraFin in Mathlib.LinearAlgebra.Multilinear.Basic

[Gaëtan Serré]

Oh I see! Thanks a lot for the references

[Eric Wieser]

docs#Finset.noncommProd is related, but probably not helpful here

[Gaëtan Serré]

Good to know, thanks anyway!