Zulip Chat Archive

Stream: maths

Topic: extends has_scalar


view this post on Zulip 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

view this post on Zulip Kenny Lau (Jun 23 2020 at 20:40):

maybe make them class instead of structure

view this post on Zulip Thomas Browning (Jun 23 2020 at 20:40):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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_scalars and so these must be unbundled as they are.

view this post on Zulip Oliver Nash (Jun 23 2020 at 21:59):

Good luck!


Last updated: May 06 2021 at 18:20 UTC