## Stream: new members

### Topic: Submodules : Structure VS Class

#### 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?

#### Kenny Lau (Dec 01 2019 at 18:22):

because you want (s : submodule R M)

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

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

#### Ken Lee (Dec 01 2019 at 18:26):

@Kenny Lau why do you not want membership instead?

@Kevin Buzzard are structures bundled or unbundled?

#### Kenny Lau (Dec 01 2019 at 18:26):

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

#### Kevin Buzzard (Dec 01 2019 at 18:26):

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

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

#### Kenny Lau (Dec 01 2019 at 18:28):

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

#### Kevin Buzzard (Dec 01 2019 at 18:28):

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

#### Kevin Buzzard (Dec 01 2019 at 18:29):

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

#### 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?

#### Kenny Lau (Dec 01 2019 at 18:30):

s is a submodule of M

#### Kenny Lau (Dec 01 2019 at 18:31):

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

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

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

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

#### 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)?

Right.

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

#### Ken Lee (Dec 01 2019 at 18:37):

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

#### Kevin Buzzard (Dec 01 2019 at 18:37):

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

#### Kevin Buzzard (Dec 01 2019 at 18:38):

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

#### Kevin Buzzard (Dec 01 2019 at 18:40):

oh, perhaps this is not true?

#### 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 ?

#### Kevin Buzzard (Dec 01 2019 at 18:40):

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

Oh I remember

#### Kevin Buzzard (Dec 01 2019 at 18:41):

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

#### Ken Lee (Dec 01 2019 at 18:42):

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

yes, of course, sorry.

#### 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

#### 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


#### Ken Lee (Dec 01 2019 at 18:44):

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

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

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

#### 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!

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

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

#### 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$.

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

#### 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

#### 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