Submodules : Structure VS Class

Stream: new members

[Ken Lee]

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]

because you want (s : submodule R M)

[Kevin Buzzard]

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]

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

[Ken Lee]

@Kenny Lau why do you not want membership instead?

@Kevin Buzzard are structures bundled or unbundled?

[Kenny Lau]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Ken Lee]

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

[Kenny Lau]

s is a submodule of M

[Kenny Lau]

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

[Kevin Buzzard]

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]

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]

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

[Ken Lee]

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

[Kevin Buzzard]

Right.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

oh, perhaps this is not true?

[Ken Lee]

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]

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

[Kevin Buzzard]

Oh I remember

[Kevin Buzzard]

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

[Ken Lee]

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

yes, of course, sorry.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kenny Lau]

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]

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