Zulip Chat Archive

Stream: maths

Topic: has_emptyc


view this post on Zulip Thomas Browning (Jul 14 2020 at 21:44):

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

view this post on Zulip Reid Barton (Jul 14 2020 at 21:49):

{} is notation for the empty collection!

view this post on Zulip Kyle Miller (Jul 14 2020 at 21:50):

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?

view this post on Zulip Reid Barton (Jul 14 2020 at 21:51):

Well, Lean doesn't seem to agree

view this post on Zulip Reid Barton (Jul 14 2020 at 21:51):

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

view this post on Zulip Thomas Browning (Jul 14 2020 at 21:52):

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

view this post on Zulip Reid Barton (Jul 14 2020 at 21:53):

I think that's right

view this post on Zulip Kyle Miller (Jul 14 2020 at 21:54):

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).

view this post on Zulip Thomas Browning (Jul 14 2020 at 21:55):

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

view this post on Zulip Reid Barton (Jul 14 2020 at 21:56):

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.

view this post on Zulip Kyle Miller (Jul 14 2020 at 21:57):

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).

view this post on Zulip Reid Barton (Jul 14 2020 at 21:59):

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

view this post on Zulip Thomas Browning (Jul 14 2020 at 22:01):

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")


Last updated: May 09 2021 at 11:09 UTC