mutual defs: ill-formed match/equation expression

Stream: new members

[Johan Commelin]

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

[Johan Commelin]

I don't have experience with mutual defs

[Reid Barton]

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]

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]

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]

import algebra.category.Module.monoidal transitively imports linear_algebra.tensor_product. This is defeq to what you want.

[Scott Morrison]

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

[Eric Wieser]

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

[Kevin Buzzard]

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]

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.