Zulip Chat Archive

Stream: maths

Topic: noetherian modules


view this post on Zulip Johan Commelin (Aug 31 2018 at 11:32):

What are the next steps for noetherian modules?
1. We want to prove that if M is noetherian, then so are all its submodules and quotients.
2. This suggests that we might quickly want is_noetherian to be a class.
3. To prove (1) we want to show that a linear map M -> N induces an order preserving map submodule R M -> submodule R N.

view this post on Zulip Johan Commelin (Aug 31 2018 at 11:33):

The map induced map in (3) is injective if M -> N is an inclusion or quotient map.

view this post on Zulip Johan Commelin (Aug 31 2018 at 11:37):

Is this induced map an example of (one side of) a Galois connection? And is it useful to know this?

view this post on Zulip Reid Barton (Aug 31 2018 at 11:41):

There are actually three maps forming two Galois connections I think

view this post on Zulip Johan Commelin (Aug 31 2018 at 11:42):

Taking image, taking inverse image, and ...?

view this post on Zulip Reid Barton (Aug 31 2018 at 11:42):

Whatever the right adjoint to the inverse image is

view this post on Zulip Reid Barton (Aug 31 2018 at 11:43):

The biggest submodule whose inverse image is contained in the original one

view this post on Zulip Reid Barton (Aug 31 2018 at 11:43):

I guess it's not useful

view this post on Zulip Johan Commelin (Aug 31 2018 at 11:45):

Right, so you have N' \sub N, and then you'dd take the image of f^{-1} N' \cap M?

view this post on Zulip Johan Commelin (Aug 31 2018 at 11:45):

Scratch that, that's nonsense

view this post on Zulip Reid Barton (Aug 31 2018 at 11:45):

Start with a submodule of M

view this post on Zulip Johan Commelin (Aug 31 2018 at 11:45):

Right,

view this post on Zulip Johan Commelin (Aug 31 2018 at 11:45):

Call it M', and put \cap M' in my formula

view this post on Zulip Reid Barton (Aug 31 2018 at 11:46):

It's those n whose inverse image is a subset of M'. I think

view this post on Zulip Reid Barton (Aug 31 2018 at 11:48):

You have it for just a map of sets also.

view this post on Zulip Reid Barton (Aug 31 2018 at 11:48):

It has a forall where the direct image has an exists

view this post on Zulip Johannes Hölzl (Aug 31 2018 at 11:49):

Yeah, sets and filters also have this strange right adjoint to preimage. I don't know if this is useful anywhere...

view this post on Zulip Reid Barton (Aug 31 2018 at 11:49):

Actually, now I think it doesn't exist for submodules

view this post on Zulip Reid Barton (Aug 31 2018 at 11:50):

Because the inverse image of zero might not be zero

view this post on Zulip Reid Barton (Aug 31 2018 at 11:50):

So the inverse image map doesn't preserve the empty sup

view this post on Zulip Reid Barton (Aug 31 2018 at 11:50):

So it can't have a right adjoint

view this post on Zulip Reid Barton (Aug 31 2018 at 11:51):

So ignore everything I said.

view this post on Zulip Reid Barton (Aug 31 2018 at 11:52):

Direct and inverse image of submodules should be a Galois connection though

view this post on Zulip Johan Commelin (Aug 31 2018 at 11:53):

Right, and I guess this is a general fact about subobjects in algebraic concrete categories...

view this post on Zulip Johan Commelin (Aug 31 2018 at 11:53):

So it would be cool if we could either deduce it from such a general fact, or have a subtype_galois_connection tactic (-;

view this post on Zulip Reid Barton (Aug 31 2018 at 12:03):

I guess we can start with the complete lattice of subobjects tactic and the span Galois insertion tactic

view this post on Zulip Johannes Hölzl (Aug 31 2018 at 12:05):

A galois_connection tactic would be nice, but I don't see how it should work. To prove that something is free (e.g. span, generator etc) is not for free.

view this post on Zulip Johan Commelin (Aug 31 2018 at 12:06):

No, I didn't mean that one. I meant the direct/inverse image connection.

view this post on Zulip Johan Commelin (Aug 31 2018 at 12:06):

That one is usually just a follow-your-nose result.

view this post on Zulip Reid Barton (Aug 31 2018 at 12:08):

You can take the intersection of all the subobjects which contain the given set. Basically get the complete lattice structure from the intersection instead

view this post on Zulip Reid Barton (Aug 31 2018 at 12:08):

But then in a particular case, you will probably want a more explicit description of the generated subobject.

view this post on Zulip Johan Commelin (Aug 31 2018 at 12:09):

Mario would say that we shouldn't automate this, but just go for it (-;

view this post on Zulip Reid Barton (Aug 31 2018 at 12:10):

Does the subobject instance tactic work for R-modules? Does it understand that the structure is module R?

view this post on Zulip Johan Commelin (Aug 31 2018 at 12:12):

this instance is already in mathlib

view this post on Zulip Johan Commelin (Aug 31 2018 at 12:12):

I didn't test the tactic, because that is not yet in mathlib

view this post on Zulip Johan Commelin (Aug 31 2018 at 12:12):

linear_algebra.subtype_module

view this post on Zulip Mario Carneiro (Aug 31 2018 at 12:18):

A galois_connection tactic would be nice, but I don't see how it should work. To prove that something is free (e.g. span, generator etc) is not for free.

span is not free when presented in a "constructive" way, i.e. linear combinations of elements in the set, but it is free given the Moore collection axioms. A Moore collection is a set of sets that is closed under arbitrary intersection (let's call these things closed sets). This enables the definition of a closure operator that is the span (i.e. the intersection of all closed sets containing S), and then there is some work to show that this operator has a constructive interpretation using an inductive family or what have you. Any algebraically presented subobject family like is_subgroup or is_submodule, where the assumptions all say "if these things are in the subgroup then these other things are in the subgroup", is a Moore collection, and there is a formulaic proof of such.

view this post on Zulip Mario Carneiro (Aug 31 2018 at 12:21):

This approach seems like a way to automate this, but it does not go via the galois connection, since that approach brings in the details of the constructive definition of span (here I mean constructive in the mathematician's sense) which are not as uniform

view this post on Zulip Reid Barton (Aug 31 2018 at 12:23):

Right so there are three definitions of, say, the submodule of M generated by a set S.

view this post on Zulip Reid Barton (Aug 31 2018 at 12:23):

1 is the intersection of the submodules containing S.

view this post on Zulip Mario Carneiro (Aug 31 2018 at 12:24):

If a Moore collection is generated by the closure with respect to a (possibly infinite) family of finite arity operators, then it is an algebraic closure system (ACS), which has still more properties for free. Almost all of the algebraic sub-things are ACSs

view this post on Zulip Reid Barton (Aug 31 2018 at 12:24):

2 is the set of elements which can be built up from S from the operations of a module, i.e., we define an inductive type of trees which are expressions in the language of R-modules.

view this post on Zulip Reid Barton (Aug 31 2018 at 12:25):

3 is the one in terms of linear combinations.

view this post on Zulip Mario Carneiro (Aug 31 2018 at 12:25):

(2) seems like an inductive definition that is amenable to automation in the same sense as I have suggested

view this post on Zulip Reid Barton (Aug 31 2018 at 12:26):

1 and 2 are automatable. 3 is not, you have to think of something which is a good "normal form" (roughly) and then prove a special theorem.

view this post on Zulip Reid Barton (Aug 31 2018 at 12:33):

I guess it probably doesn't matter much which definition we choose or whether the definitions are consistent between different kinds of structures

view this post on Zulip Mario Carneiro (Aug 31 2018 at 12:37):

If we want a one-line setup of the collection, the complete lattice, the span operator and the galois connection, it would be best to take one of the uniform versions as the definition, and leave the nonuniform version as a theorem to be proven separately

view this post on Zulip Reid Barton (Aug 31 2018 at 12:37):

I should look into this Moore system stuff. It sounds related to locally presentable categories (a locally finitely presentable category is the category of models of a finitary essentially algebraic theory) and there are some theorems about subobjects in them, though usually I don't care so much about those theorems.

view this post on Zulip Mario Carneiro (Aug 31 2018 at 12:38):

I learned about it first through metamath, see http://us.metamath.org/mpeuni/df-mre.html and http://us.metamath.org/mpeuni/df-acs.html which have some links to references. Wikipedia doesn't seem to have anything on it

view this post on Zulip Johannes Hölzl (Aug 31 2018 at 12:42):

Yeah, I should have looked into them the first time you mentioned them. I like the Examples section in https://ncatlab.org/nlab/show/Moore+closure :

What are examples? Better to ask what isn't an example!

view this post on Zulip Reid Barton (Aug 31 2018 at 12:49):

I see, so it looks a lot more general than subobjects in an algebraic theory.

view this post on Zulip Mario Carneiro (Aug 31 2018 at 12:52):

oh, looks like the WP reference is https://en.wikipedia.org/wiki/Closure_operator

view this post on Zulip Mario Carneiro (Aug 31 2018 at 12:53):

"finitary closure operator" in that article corresponds to what I called an ACS

view this post on Zulip Scott Morrison (Sep 01 2018 at 09:22):

Does anyone know why the noetherian branch isn't compiling?

view this post on Zulip Scott Morrison (Sep 01 2018 at 09:24):

@Chris Hughes, @Kenny Lau, what are the prospects of getting tensor products of commutative rings into mathlib?

view this post on Zulip Kenny Lau (Sep 01 2018 at 09:25):

I wrote half the file a month ago

view this post on Zulip Patrick Massot (Sep 01 2018 at 09:33):

is_add_group_hom is now in mathlib

view this post on Zulip Patrick Massot (Sep 01 2018 at 09:35):

https://github.com/leanprover/mathlib/commit/afd1c063638d611fda65db7499ccbd7257c90870

view this post on Zulip Patrick Massot (Sep 01 2018 at 09:36):

What is the current state of quotient groups by the way?

view this post on Zulip Chris Hughes (Sep 01 2018 at 09:51):

Kevin's stuff got merged. There's about 100 lines of the basic facts.

view this post on Zulip Scott Morrison (Sep 01 2018 at 09:51):

@Chris Hughes can you point me to it?

view this post on Zulip Patrick Massot (Sep 01 2018 at 09:51):

I was thinking of the left_cosets vs group_quotient issue

view this post on Zulip Patrick Massot (Sep 01 2018 at 09:51):

I think we have two competing versions

view this post on Zulip Chris Hughes (Sep 01 2018 at 09:52):

Everything's quotient_group.quotient now.

view this post on Zulip Patrick Massot (Sep 01 2018 at 09:52):

left_cosets disappeared?

view this post on Zulip Chris Hughes (Sep 01 2018 at 09:52):

Yes.

view this post on Zulip Patrick Massot (Sep 01 2018 at 09:52):

That's good news, but again something to be changed in Kenny's tensor product file

view this post on Zulip Chris Hughes (Sep 01 2018 at 09:52):

but quotient_group includes quotient by non normal subgroups

view this post on Zulip Chris Hughes (Sep 01 2018 at 09:53):

@Scott Morrison It's in group_theory/quotient_group

view this post on Zulip Scott Morrison (Sep 01 2018 at 09:55):

@Chris Hughes, oh, oops, I thought you were talking about tensor products of rings. :-)

view this post on Zulip Patrick Massot (Sep 01 2018 at 09:55):

couldn't we call this group.quotient instead of quotient_group? The later really looks like the quotient is a group

view this post on Zulip Scott Morrison (Sep 01 2018 at 09:55):

@Kenny Lau, are you going to PR that stuff on tensor products? I'd like to be able to use it!

view this post on Zulip Chris Hughes (Sep 01 2018 at 09:58):

I think group.quotient is a better name.

view this post on Zulip Kenny Lau (Sep 01 2018 at 12:52):

@Kenny Lau, are you going to PR that stuff on tensor products? I'd like to be able to use it!

give me some time

view this post on Zulip Kenny Lau (Sep 02 2018 at 12:28):

Tensor product PR: https://github.com/leanprover/mathlib/pull/303

view this post on Zulip Kenny Lau (Sep 02 2018 at 12:28):

@Scott Morrison further feature request?

view this post on Zulip Kenny Lau (Sep 02 2018 at 12:28):

@Patrick Massot you might be interested

view this post on Zulip Patrick Massot (Sep 02 2018 at 12:53):

thanks Kenny!

view this post on Zulip Patrick Massot (Sep 02 2018 at 18:16):

Kenny's tensor product is merged! I'm really super excited by the idea of mathlib taking advantage of Kenny's proving power!

view this post on Zulip Kevin Buzzard (Sep 02 2018 at 18:18):

rofl I was reviewing it

view this post on Zulip Kenny Lau (Sep 02 2018 at 18:19):

it's alright Kevin, I may still have things to add there anyway

view this post on Zulip Kenny Lau (Sep 02 2018 at 18:19):

I may prove the dimension theorem, and then I would prove that the dimension of tensor is the product of the dimension

view this post on Zulip Johannes Hölzl (Sep 02 2018 at 18:24):

@Kevin Buzzard was I too fast merging it? Any suggestions?

view this post on Zulip Kevin Buzzard (Sep 02 2018 at 18:25):

nothing serious. I'll finish my review. I am trying to get into the habit of reviewing mathlib PRs where the mathematics relates to the perfectoid project.

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 21:42):

@Mario Carneiro just to let you know I am still working on the Noetherian branch of community mathlib. I have a proof that subs and quotients of Noeth are Noeth but it's currently broken as I fiddle with it to try and make things more general and reasonable. I'm sure there will still be lots of work to do when I finally make the PR, hopefully tomorrow. Admin got the better of me today, that and the fact that I kept having little insights about how to do things a little better than they were done before.

view this post on Zulip Kevin Buzzard (Sep 05 2018 at 10:58):

OK so I pushed the proof that a sub of a Noetherian module is Noetherian to community-mathlib, the Noetherian branch. I spent some time proving order embeddings which I could have probably avoided. I'd appreciate any feedback on the push. Am I supposed to open a PR to mathlib? I have littered my PR with comments, which of course will have to go in the end, but they're just to flag things I wasn't sure about or to explain what I was trying to do.

I also have a proof that quotients of Noetherian modules are Noetherian, but I was waiting for Chris' quotient module PR to be accepted -- I see that it was accepted an hour ago so I'll work on quotient modules later.


Last updated: May 12 2021 at 07:17 UTC