mutual types: ill-formed match/equation expression

Stream: new members

[Eric Wieser]

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)
with tensor_power.add_comm_monoid : Π n, add_comm_monoid (tensor_power n)
    | k := sorry

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

(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]

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]

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]

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

[Eric Wieser]

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

[Johan Commelin]

@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]

Making either or both of those changes does not help

[Eric Wieser]

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