has_emptyc

Stream: maths

[Thomas Browning]

So I'm trying to show that something is a module. I was able to show that it's a semimodule, but when I try to give it a module structure:

instance : module 𝕜 (hom G 𝕜 V W) := { }

I get this goal:

failed to synthesize type class instance for
[some stuff]
⊢ has_emptyc (module 𝕜 (hom G 𝕜 V W))

What is this has_emptyc thing? I thought that a semimodule over a ring (here k is a field) was automatically a module:

abbreviation module (R : Type u) (M : Type v) [ring R] [add_comm_group M] :=
semimodule R M

[Reid Barton]

{} is notation for the empty collection!

[Kyle Miller]

I think Thomas was aiming for the empty structure so that he could see which fields needed to be implemented. I've used { } before for this -- why is it the empty collection here?

[Reid Barton]

Well, Lean doesn't seem to agree

[Reid Barton]

maybe because module is not a structure, but an abbreviation?

[Thomas Browning]

So do I just not need to bother giving a module structure, since I've already given a semi_module structure?

[Reid Barton]

I think that's right

[Kyle Miller]

You probably just need to make sure you have all the instances in the definition of module. Like add_comm_group (hom G 𝕜 V W).

[Thomas Browning]

I have all that (it was needed when giving the semimodule structure)

[Reid Barton]

If you really needed to, I think you can write something like { semimodule . } to make it clear to Lean that you want to write a structure literal, and for which kind of structure.

[Kyle Miller]

Oh, I see, the only difference is module requires there to be a ring 𝕜 instance, which you probably already have because it's a field (knowing what you're working on).

[Reid Barton]

Indeed, as recently discussed, we could probably just remove module and rename semimodule to module.

[Thomas Browning]

Actually, one thing that works is just this:

instance : add_comm_group (hom G 𝕜 V W) := {
[do a bunch of stuff]
}

instance : module 𝕜 (hom G 𝕜 V W) := {
[do a bunch of stuff]
}

(previously I had "semimodule" instead of "module")