Lean doesn't know how to extend two `smul`s

Stream: new members

[Hanting Zhang]

Hi, I've been working with some representation stuff, and when trying to define a subrepresentation I get this:

import linear_algebra.basic
import algebra.monoid_algebra
import algebra.module.basic

universes u v w

class representation (k : Type u) (G : Type v) (M : Type w)
  [semiring k] [monoid G] [add_comm_monoid M]
  [semimodule k M] extends distrib_mul_action G M : Type (max u v w) :=
(smul_smul :  ∀ (g : G) (r : k) (m : M), g • (r • m) = r • (g • m))

variables (k : Type u) (G : Type v) (M : Type w)
variables [semiring k] [monoid G] [add_comm_monoid M]
variables [semimodule k M] [distrib_mul_action G M]

set_option old_structure_cmd true

class subrepresentation [representation k G M] extends submodule k M, sub_mul_action G M
-- invalid 'structure' header, field 'smul_mem'' from 'sub_mul_action' has already been declared with a different type

So Lean is unhappy with the implementation detail that two smuls from the G-action and the k scalar multiplication are called the same thing. Is there any way to tell Lean to use different names?

[Kevin Buzzard]

Instead of extending you can just extend one thing, add the fields of the other thing (changing the bad name appropriately), and then define the structure projection yourself if and when you need it.

[Hanting Zhang]

Is there any preference for which one I should extend? Or does it not matter?

[Kevin Buzzard]

I think it doesn't matter. I should add that I learnt about this stuff earlier today for the first time, so I am not really an expert.

[Hanting Zhang]

Also, I was wondering if I should still be using set_option old_structure_cmd true, since you seemed to be getting rid of all them.

[Hanting Zhang]

Ah, I guess I will wait for someone who knows better to tell me how this works then

[Kevin Buzzard]

If my understanding of your problem is correct, the old structure command won't help you. That's for when you extend two things which both have a smul_mem' but they're the same thing.

[Kevin Buzzard]

I think this will be fine:

structure subrepresentation [representation k G M] extends submodule k M :=
(group_smul_mem' : ∀ (c : G) {x : M}, x ∈ carrier → c • x ∈ carrier)

Note structure not class: a typical representation will have more than one subrepresentation.

[Hanting Zhang]

Oh, thank you! I had your exact copy of code with class instead of structure; that mistake would not have been fun to fix later

[Kevin Buzzard]

I think this is better:

class representation (k : Type u) (G : Type v) (M : Type w)
  [semiring k] [monoid G] [add_comm_monoid M]
  [semimodule k M] [distrib_mul_action G M] : Type (max u v w) :=
(smul_smul :  ∀ (g : G) (r : k) (m : M), g • (r • m) = r • (g • m))

I think that you shouldn't extend stuff with fewer variables (like e.g. semimodule k M does not extend add_comm_monoid M, it asks for it)

[Kevin Buzzard]

As I say, I don't really understand why.

[Hanting Zhang]

Hmm, ok, I will keep that in mind. Thank you again for your help!

[Eric Wieser]

If you extend something with fewer arguments, then the instance derived.to_base : base is a dangerous instance with an unrestricted argument