# Zulip Chat Archive

## Stream: new members

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

#### Johan Commelin (Jul 21 2020 at 06:19):

Hmm... I'm sorry that I can't really help you.

#### Johan Commelin (Jul 21 2020 at 06:19):

I don't have experience with mutual defs

#### Reid Barton (Jul 21 2020 at 12:38):

Eric Wieser said:

It looks like the issue is that

`tensor_power`

appears in the type of`add_comm_monoid`

, not just the definition.

Yes, I think this means the desugaring would produce a definition which appears in its own type, which is not possible

#### Scott Morrison (Jul 21 2020 at 12:53):

```
import algebra.category.Module.monoidal
import algebra.category.CommRing.basic
open category_theory
variables {C : Type*} [category C] [monoidal_category C]
def tensor_power (X : C) : ℕ → C
| 0 := 𝟙_ C
| (n+1) := X ⊗ tensor_power n
example {R : CommRing} (M : Module R) : Module R := tensor_power M 17
-- And if you want to do this with unbundled objects:
universes u
variables (R : Type u) [comm_ring R] (M : Type u) [add_comm_group M] [module R M]
def foo : Type u :=
(tensor_power (Module.of R M) 17 : Module R)
instance : add_comm_group (foo R M) := by { delta foo1, apply_instance, }
instance : module R (foo R M) := by { delta foo1, apply_instance, }
```

#### Eric Wieser (Jul 21 2020 at 13:14):

I'm a bit confused by that example. For one, I don't see any import of tensor_product.

My bigger concern is it seems like everything is defined twice, once in `category`

and once not. How should I pick between them? Is there a plan to unify at some later point?

#### Scott Morrison (Jul 21 2020 at 13:43):

`import algebra.category.Module.monoidal`

transitively imports `linear_algebra.tensor_product`

. This is defeq to what you want.

#### Scott Morrison (Jul 21 2020 at 13:43):

You're right that there is becoming worrying amounts of duplication, but in fact this isn't part of it.

#### Eric Wieser (Jul 21 2020 at 13:48):

The other worrying part is that I don't know any category theory...

#### Kevin Buzzard (Jul 21 2020 at 14:41):

But this is a concrete category so you can just think of it as some sort of overlay on top of the stuff you know

#### Utensil Song (Jul 21 2020 at 15:24):

I only know basic category theory (that is, covering about half of the concepts in https://www.youtube.com/watch?v=1NUc-ZNC_2s ) but if we only scratch the surface (like using it to define `tensor_power`

) we'll manage. Plus, category_theory in lean seems to have good automation.

B.T.W. Clifford Algebra can be defined categorically too, see 1.2 in PG course on Spin Geometry - Lecture 1: Clifford algebras: basic notions.

Last updated: Dec 20 2023 at 11:08 UTC