# Zulip Chat Archive

## Stream: maths

### Topic: extends has_scalar

#### Thomas Browning (Jun 23 2020 at 20:37):

In the following code:

```
import algebra.module
-- From https://github.com/fpvandoorn/group-representations/blob/master/src/group_theory/representation/basic.lean
structure G_module (G : Type*) [group G] (M : Type*) [add_comm_group M] extends has_scalar G M :=
(id : ∀ m : M, (1 : G) • m = m)
(mul : ∀ g h : G, ∀ m : M, g • (h • m) = (g * h) • m)
(linear : ∀ g : G, ∀ m n : M, g • (m + n) = g • m + g • n)
-- A vector space and G-module whose action is 𝕜-linear
structure representation (G : Type*) [group G] (𝕜 : Type*) [field 𝕜] (V : Type*) [add_comm_group V] [module 𝕜 V] extends G_module G V :=
(lin : ∀ k : 𝕜, ∀ v : V, ∀ g : G, g • (k • v) = k • (g • v))
definition stable (G : Type*) [group G] (𝕜 : Type*) [field 𝕜]
(V : Type*) [add_comm_group V] [module 𝕜 V] [representation G 𝕜 V]
(W : submodule 𝕜 V) : Prop :=
∀ g : G, ∀ (v ∈ W), ((g • (v : V)) ∈ W)
```

Lean doesn't like the expression `g • (v : V)`

because it can't figure out why `has_scalar G V`

I find this strange since `representation G 𝕜 V`

extends `G_module G V`

which extends `has_scalar G V`

#### Kenny Lau (Jun 23 2020 at 20:40):

maybe make them `class`

instead of `structure`

#### Thomas Browning (Jun 23 2020 at 20:40):

ah, that does the trick. What's the difference?

#### Kyle Miller (Jun 23 2020 at 20:42):

Is it considered to be OK to have classes with multiple possible instances for the same types? There are many different G-module structures, and studying all of them is important for representation theory. Maybe, here, one can assume each representation has a different M.

#### Kyle Miller (Jun 23 2020 at 21:02):

Thomas Browning If wanted to do it with structures, this works:

```
import algebra.module
-- From https://github.com/fpvandoorn/group-representations/blob/master/src/group_theory/representation/basic.lean
structure G_module (G : Type*) [group G] (M : Type*) [add_comm_group M] [has_scalar G M] :=
(id : ∀ m : M, (1 : G) • m = m)
(mul : ∀ g h : G, ∀ m : M, g • (h • m) = (g * h) • m)
(linear : ∀ g : G, ∀ m n : M, g • (m + n) = g • m + g • n)
-- A vector space and G-module whose action is 𝕜-linear
structure representation (G : Type*) [group G] (𝕜 : Type*) [field 𝕜] (V : Type*) [add_comm_group V] [module 𝕜 V] [has_scalar G V] :=
(mod : G_module G V)
(lin : ∀ k : 𝕜, ∀ v : V, ∀ g : G, g • (k • v) = k • (g • v))
definition stable (G : Type*) [group G] (𝕜 : Type*) [field 𝕜]
(V : Type*) [add_comm_group V] [module 𝕜 V] [has_scalar G V] [representation G 𝕜 V]
(W : submodule 𝕜 V) : Prop :=
∀ g : G, ∀ (v ∈ W), ((g • (v : V)) ∈ W)
```

The issue seems to be that, while `G_module`

extended `has_scalar`

, this does not provide a `has_scalar`

instance for Lean's class resolution.

#### Kyle Miller (Jun 23 2020 at 21:13):

@Thomas Browning I might go with class, and maybe combine `G_module`

and `representation`

into a `G_representation`

(unless you plan on working with `G_modules`

):

```
import algebra.module
class G_representation (G : Type*) [group G] (𝕜 : Type*) [field 𝕜] (V : Type*) [add_comm_group V] [has_scalar G V] [module 𝕜 V] :=
(id : ∀ m : V, (1 : G) • m = m)
(action : ∀ g h : G, ∀ m : V, g • (h • m) = (g * h) • m)
(dist : ∀ g : G, ∀ m n : V, g • (m + n) = g • m + g • n)
(scalar_comm : ∀ k : 𝕜, ∀ v : V, ∀ g : G, g • (k • v) = k • (g • v))
section
variables (G : Type*) [group G] (𝕜 : Type*) [field 𝕜] (V : Type*) [add_comm_group V] [has_scalar G V] [module 𝕜 V]
def stable [G_representation G 𝕜 V] (W : submodule 𝕜 V) :=
∀ g : G, ∀ (v ∈ W), ((g • (v : V)) ∈ W)
end
```

(I don't understand the finer details of when to extend a class or not.)

#### Oliver Nash (Jun 23 2020 at 21:55):

This thread touches on a two points that took me longer than I would have liked to get to grips with. Firstly on the "finer details of when to extend a class or not" I will try to explain with the following snippet:

```
namespace bundled_vs_unbundled
class foo (X : Type*) := (x : X)
class bundled_bar (X Y : Type*) extends foo X := (y : Y)
class unbundled_bar (X Y : Type*) [foo X] := (y : Y)
-- Some differences already visible:
#print unbundled_bar
#print bundled_bar
def works : bundled_bar ℕ ℕ :=
{ x := 37,
y := 23, }
-- Key difference: we need a foo instance already in hand in order to create an instance in the unbundled case
def fails : unbundled_bar ℕ ℕ :=
{ x := 37,
y := 23, }
instance : foo ℕ := { x := 37 }
def works' : unbundled_bar ℕ ℕ := { y := 23 }
end bundled_vs_unbundled
```

#### Oliver Nash (Jun 23 2020 at 21:59):

Secondly, due to a limitation of the Lean 3 typeclass search problem, you should never extend a class with strictly fewer carrier types. Since `G_representation`

has three carrier types (`G`

, `𝕜`

, `V`

) it cannot extend either of the two `has_scalar`

s and so these must be unbundled as they are.

#### Oliver Nash (Jun 23 2020 at 21:59):

Good luck!

Last updated: May 06 2021 at 18:20 UTC