MultilinearMapClass?

Stream: mathlib4

[Yury G. Kudryashov]

I've started looking into adding MultilinearMapClass to avoid code duplication between docs#MultilinearMap, docs#AlternatingMap and their Continuous* versions. The first obstacle is that docs#MultilinearMap.map_add doesn't needs the scalars ring, so we can't have it as a lemma for MultilinearMapClass. Which way is better?

• leave it as is;
• add MultiadditiveMap and MultiadditiveMapClass;
• add MultiadditiveMapClass, postpone adding MultiadditiveMap until we need it.

While writing this, I've realized that we have a projection from docs#SemilinearMapClass to docs#AddMonoidHomClass and it works. Why? Doesn't Lean start searching for SemilinearMapClass ?σ M N with unknown R, S, and σ : R →+* S whenever it needs AddMonoidHomClass, which should fail?

[Eric Wieser]

I think it works because all the arguments to the MapClasses are outParams

[Eric Wieser]

That is, if you know the bundled type, there is only one possible domain, codomain, and relevant ring,

[Eric Wieser]

Either 2 or 3 sounds fine to me

[Yury G. Kudryashov]

Does it mean that I have 1 more option:

• make map_update_add a lemma about MultilinearMapClass?

[Eric Wieser]

Yes, I think so

[Eric Wieser]

Maybe that makes more sense in the short term

[Yury G. Kudryashov]

I think I'll go this way, then we can add MultiadditiveMapClass/MultiadditiveMap whenever we need it.

[Yury G. Kudryashov]

I want to rename docs#MultilinearMap.map_smul (about f (update m i (c • x))) to _root_.map_update_smul. How should I call docs#MultilinearMap.map_update_smul ? It's about f (update (c • m) i x).

[Yury G. Kudryashov]

map_smul_update? Something else?

[Ruben Van de Velde]

Map update smul left/right?

[Eric Wieser]

map_smul_update or map_update_smul' or Ruben"s suggestions all seem fine to me