## Stream: new members

### Topic: mutual types: ill-formed match/equation expression

#### Eric Wieser (Jul 20 2020 at 18:54):

I'm having an issue with the following, and the error message (ill-formed match/equations expression) is very short:

import linear_algebra.tensor_product

mutual def tensor_power, tensor_power.add_comm_monoid (R : Type) (V : Type) [comm_semiring R] [add_comm_group V] [semimodule R V]
with tensor_power : ℕ → Type
| 0 := R
| 1 := V
| (n + 1) :=
@tensor_product R _ V (tensor_power n) _ (tensor_power.add_comm_monoid n) _ sorry
-- haveI : semimodule R (tensor_power n) := tensor_power.semi_module n i,
-- exact tensor_product R V (tensor_power n)
| k := sorry


Is there a way to get a better diagnosis of what is going on?

#### Johan Commelin (Jul 20 2020 at 18:57):

@Sebastien Gouezel Did you already have something like this? You have multilinear maps, but maybe not tensor powers, right?

#### Johan Commelin (Jul 20 2020 at 18:58):

@Eric Wieser It might be a lot easier to define this via the monoidal structure on the category of modules over R.

#### Johan Commelin (Jul 20 2020 at 18:58):

But that's just an intuition. I've never tested it.

#### Johan Commelin (Jul 20 2020 at 18:58):

@Scott Morrison Do we have repeated tensor powers in the categorical framework already?

#### Johan Commelin (Jul 20 2020 at 18:59):

Johan Commelin said:

Eric Wieser It might be a lot easier to define this via the monoidal structure on the category of modules over R.

The reason being that all the typeclasses will be bundled, so you don't need the complicated mutual def construction.

#### Johan Commelin (Jul 20 2020 at 19:00):

(Aside: is there a reason you give the n = 1 case explicitly? It looks nice to have it defeq to V instead of V \tensor R, but it means that for proofs you will need to do an extra case, all the time (I guess).)

#### Sebastien Gouezel (Jul 20 2020 at 19:37):

Johan Commelin said:

Sebastien Gouezel Did you already have something like this? You have multilinear maps, but maybe not tensor powers, right?

I had something like that in a previous version of multilinear maps that was defined inductively (now, the current version is defined directly as multilinear maps from fin n to some space, so no induction needed). But it was simpler, as I could first define the type inductively, then the norm on it inductively. Here, it's more complicated as both things need to be defined together.

If mutual def doesn't work well, you can define a structure containing both the type and the add_comm_monoid structure on it, and define with normal induction this structure at rank n+1 when you have it at rank n.

#### Scott Morrison (Jul 21 2020 at 01:37):

Johan Commelin said:

Scott Morrison Do we have repeated tensor powers in the categorical framework already?

Unfortunately no. Monoidal categories are purely in terms of the binary tensor product.

#### Scott Morrison (Jul 21 2020 at 01:37):

But it should be zero problem to write a tensor power def, no mutual required!

#### Eric Wieser (Jul 21 2020 at 05:06):

This is all good advice, but it would be great if someone could tell me what my error message means!

#### Johan Commelin (Jul 21 2020 at 05:54):

@Eric Wieser I've never seen it before, but I see two things:

1. If you have a match on 0, and 1, then the remaining case is (n+2), not (n+1).
2. Does it help if you break
with tensor_power.add_comm_monoid : Π n, add_comm_monoid (tensor_power n)
| k := sorry


into 3 branches 0, 1, (n+2) as well, instead of only k?

#### Eric Wieser (Jul 21 2020 at 06:05):

Making either or both of those changes does not help

#### Eric Wieser (Jul 21 2020 at 06:07):

It looks like the issue is that tensor_power appears in the type of add_comm_monoid, not just the definition.

Last updated: May 13 2021 at 06:15 UTC