extends has_scalar

Stream: maths

[Thomas Browning]

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]

maybe make them class instead of structure

[Thomas Browning]

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

[Kyle Miller]

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]

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]

@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]

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]

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.

[Oliver Nash]

Good luck!