Zulip Chat Archive

Stream: new members

Topic: Submodules : Structure VS Class


view this post on Zulip Ken Lee (Dec 01 2019 at 18:21):

Why are submodules of a module a structure consisting of a set with properties of the set
rather than just a class of sets satisfying the properties?

view this post on Zulip Kenny Lau (Dec 01 2019 at 18:22):

because you want (s : submodule R M)

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:22):

There are two ways of doing it -- they're called bundled or unbundled, and neither is perfect, but bundled is better (in Lean at least).

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:23):

Stuff like intersections etc all still work because you can make all the notation apply for submodules as well as subsets.

view this post on Zulip Ken Lee (Dec 01 2019 at 18:26):

@Kenny Lau why do you not want membership instead?

@Kevin Buzzard are structures bundled or unbundled?

view this post on Zulip Kenny Lau (Dec 01 2019 at 18:26):

because (s : set M) (hs : s \in submodules R M) is clumsy

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:26):

bundled means the set is a field of the structure, so submodules are currently bundled.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:27):

It's harder to get your head around it at first, but once you do you'll see that it works really nicely.

view this post on Zulip Kenny Lau (Dec 01 2019 at 18:28):

one advantage is that with (s : submodule R M) you can write s.add_mem

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:28):

For example given a map of RR-modules MNM\to N you get maps submodule R M -> submodule R N and submodule R N -> submodule R M

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:29):

Note in contrast that groups are unbundled -- we write G : Type then _inst_1 : group G.

view this post on Zulip Ken Lee (Dec 01 2019 at 18:30):

@Kenny Lau I don't follow. s is a subset of M and s is in a submodule of M?

view this post on Zulip Kenny Lau (Dec 01 2019 at 18:30):

s is a submodule of M

view this post on Zulip Kenny Lau (Dec 01 2019 at 18:31):

s.add_mem is x \in s \to y \in s \to x + y \in s

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:31):

If you didn't mean that then whatever you meant you will have s : set M and then another thing as well to indicate it's a submodule. With teh bundled approach it's just one term.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:32):

Type class inference works fine for _inst_1 : group G but it might be pushing it a bit too far to get submodules to work. I think they had enough trouble getting modules to work the way we wanted them to.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:33):

But enough about the disadvantages of the unbundled approach -- the point is that the bundled approach seems to work really nicely.

view this post on Zulip Ken Lee (Dec 01 2019 at 18:33):

I think I see it, do you mean instead of writing (s : set M) [submodule R s], you just write (s : submodule R M)?

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:33):

Right.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:34):

and then there will probably be a coercion to the set, but you don't need it anyway because there will be a has_mem instance for elements of s.

view this post on Zulip Ken Lee (Dec 01 2019 at 18:37):

similarly, if you want to intersect submodules, you have to first prove has_intersect instance?

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:37):

I imagine that if you just try it, it will work.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:38):

Because is notation for has_inter.inter and the instance will be defined for you.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:40):

oh, perhaps this is not true?

view this post on Zulip Ken Lee (Dec 01 2019 at 18:40):

Sorry, I meant when it was first defined in math lib, did someone have to prove it?
i.e. every time I define "subobject" of an object using structures, would I have to prove these has_inter, has_union etc ?

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:40):

sure! But union of two submodules isn't a submodule in general.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:40):

Oh I remember

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:41):

you should think of them as a lattice, so probably you have to use lattice notation.

view this post on Zulip Ken Lee (Dec 01 2019 at 18:42):

sure! But union of two submodules isn't a submodule in general.

yes, of course, sorry.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:42):

On the other hand you could just imagine the submodule generated by two submodules, and I bet that's what \lub does

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:42):

import algebra.module linear_algebra.basic

variables {R : Type*} [ring R] (M : Type*) [add_comm_group M] [module R M]

#check  A B : submodule R M, A  B -- fails
#check  A B : submodule R M, A  B -- works

view this post on Zulip Ken Lee (Dec 01 2019 at 18:44):

then does it make sense to ask whether two submodules are equal?

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:44):

There is a whole theory of general types with <= (inclusion, in this case) and (intersection, in this case), called lattice theory. Lattice is an overused word and to make matters worse mathematicians hardly ever use it in this context. But submodules form a lattice.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:45):

then does it make sense to ask whether two submodules are equal?

Probably there is an extensionality lemma saying that two submodules are equal iff the underlying sets are equal.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:46):

If you want to learn how to use modules then because of @Rob Lewis 's documentation push you will find that the first 50 lines of linear_algebra/basic.lean might be of some use to you!

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:48):

oh wow, submodules are even a complete lattice. I think that's one of the best kinds of lattice.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:50):

https://github.com/leanprover-community/mathlib/blob/177ccedb21ca423105081e4a20778a34f3ee356f/src/linear_algebra/basic.lean#L405

Not only that, just afterwards they're proved to be an add_comm_monoid, which will mean that you will be able to add them up too.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:52):

I am slightly surprised that there's not just some general piece of nonsense which gives you add comm monoids from certain kinds of lattices. But anyway the moral is that you should use lattice notation when working with submodules, i.e. not \subseteq and not \cap.

view this post on Zulip Kevin Buzzard (Dec 01 2019 at 18:53):

and you have 1800 lines of lemmas in linear_algebra.basic to help you along your way.

view this post on Zulip Kenny Lau (Dec 01 2019 at 19:12):

There is a whole theory of general types with <= (inclusion, in this case) and (intersection, in this case), called lattice theory. Lattice is an overused word and to make matters worse mathematicians hardly ever use it in this context. But submodules form a lattice.

To make it worse, "complete lattice" means something completely different in Neukirch

view this post on Zulip Kenny Lau (Dec 01 2019 at 19:12):

a lattice is a discrete subgroup of R^n and a complete lattice is one whose R-span is R^n


Last updated: May 14 2021 at 00:42 UTC