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