extends has_scalar

Stream: Berkeley Lean Seminar

[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

[Patrick Massot]

I just discovered the existence of this stream in one of my periodic scans of hidden streams. I don't have any clue why such a question could be asked in such a secret stream when it could be in #maths

[Thomas Browning]

I'll put it there then

[Patrick Massot]

That will multiply the probability to get an answer by about 20 I think.

[Patrick Massot]

See?

[Thomas Browning]

Yes, thanks! (For future reference, apparently replacing "structure" with "class" fixes things)

[Kyle Miller]

Patrick Massot said:

I just discovered the existence of this stream in one of my periodic scans of hidden streams. I don't have any clue why such a question could be asked in such a secret stream when it could be in #maths

Sometimes it's nice testing a question among a group with a similar background. (We are right now having a Zoom session (1-2pm pacific time) where we're working on tutorials or projects for the seminar, and Zulip is much better than the Zoom chat.)

[Patrick Massot]

There is no problem having a dedicated stream, I was really commenting that kind of question.