dependent mulSupport

Stream: Is there code for X?

[Kevin Buzzard]

I'm working with a restricted product of groups but the same question would arise for a product of groups $\prod_i G_i$; I care about the support of an element $g$, i.e. $\{i\in I\mid g(i)\ne1\}.$ I remembered we had docs#Function.mulSupport but it doesn't apply because $g$ is a dependent function. Do we have dependent mulSupport?

[Etienne Marion]

I'm pretty sure we don't. There are many Function.foo which do not have a dependent version although it could.

[Etienne Marion]

@loogle ∀ _, One _

[loogle]

:search: AddOpposite.instOne, MulOpposite.instOne, and 181 more

[Etienne Marion]

This does not yield anything I think.

[Kevin Buzzard]

FWIW I need this to show that a Hecke algebra commutes; I have some restricted product group G and a subgroup U, and I want to prove that some Hecke operators [UgU] and [UhU] commute, but g and h are supported at different places in the product so the decomposition of the double coset into single cosets can also be made with cosets reps supported at different places and these automatically commute, but I had to make a bunch of API for dependent mulsupport first.

[Eric Wieser]

What breaks if we generalize Function.support?

[Yaël Dillies]

A lot of things probably. Elaboration of Pi.mulSingle is very brittle. See how many Pi.single (M := _) there are in the library

[Eric Wieser]

That's quite different though, as the argument becomes dependent not the return type