Zulip Chat Archive

Stream: maths

Topic: isomorphism theorems


view this post on Zulip Kevin Buzzard (Sep 03 2018 at 09:04):

I need what is apparently called the "fourth isomorphism theorem" for R-modules, R a commutative ring. Of course more generally we will need all the isomorphism theorems for groups and R-modules, plus various extra bits and bobs. I might do some of this today in a coding session with the undergraduates. I propose doing the thing I actually want, which is that if RR is a general ring (commutativity not necessary) and NN is a sub-RR-module of the RR-module MM then there's a canonical order-preserving bijection between submodules of M/NM/N and submodules of MM containing NN. My proposal is that I write this code at about 2pm today UK time so before then perhaps I should have a clue about the best way to say this. Here are some dumb questions.

The reason I want this is that I want that a quotient module of a Noetherian module is Noetherian. Because Noetherian modules are not yet in mathlib, but they are in mathlib-community, am I right in thinking I should be doing this work in a fork of the mathlib-community repo?

What should this file be called? fourth_isomorphism_theorem.lean sounds daft. Should it just be tagged onto quotient_module.lean in linear_algebra? I don't know how much more commutative algebra should up in this directory -- this stuff is not linear algebra any more.

Those of us who care about Galois insertions might now point out that the result I want is perhaps something to do with Galois insertions or Galois connections. Currently my instinct is to completely ignore all of this because I don't see what it buys us. I'd be interested in opinions. My proposal is to write an equiv between the type of submodules of M/N and the type of submodules of M containing N and then prove that it is order-preserving. Now my (good) understanding of equiv tells me exactly what I should be proving about the constructions. But my (poor) understanding of lattices doesn't tell me exactly what I should be proving about the order: I mean -- I know I should be proving that the constructions in each direction preserve inclusion, but should I be proving that some map is some morphism of lattices, or something?

My goal is that a quotient module of a Noetherian module is Noetherian, and I want the proof to be "this set is well-founded, by definition of Noetherian module, and hence this subset is well-founded, so we're done". What structures should I be using to formalise this statement in order for it to be mathlib-ready?

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

Gaargh. I've checked out the noetherian branch of community mathlib and it doesn't build. order/conditionally_complete_lattice.lean has a problem in line 128 for example:

/--Adding a point to a set preserves its boundedness above.-/
@[simp] lemma bdd_above_insert : bdd_above (insert a s)  bdd_above s :=
show bdd_above (insert a s)  bdd_above s, from bdd_above_subset (by simp),
 show bdd_above s  bdd_above (insert a s), by rw[insert_eq]; finish

->

α : Type u,
_inst_1 : semilattice_sup α,
s : set α,
a : α
⊢ bdd_above s → bdd_above (insert a s)
conditionally_complete_lattice.lean:131:62: error

solve1 tactic failed, focused goal has not been solved
state:
α : Type u,
_inst_1 : semilattice_sup α,
s : set α,
a : α,
a_1 : bdd_above s,
a_2 : ¬bdd_above (insert a s)
⊢ false

(finish is failing). Is there an easy fix for this?

view this post on Zulip Kenny Lau (Sep 03 2018 at 11:01):

finish [bdd_above_insert]?

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:03):

but there are 100 errors

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:03):

so I'd rather find out what's going on

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:05):

Maybe your olean files aren't matching with this branch? Did you try a recompile from scratch?

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:06):

maybe I messed up. I thought I'd done exactly that

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:07):

I've removed all the olean files and am trying again

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:08):

Dumb question: if I clone a lean repo, make all the .olean files, and then checkout a different branch, do all the .olean files magically disappear?

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:21):

Nope. They are in .gitignore. So git doesn't touch them.

view this post on Zulip Johannes Hölzl (Sep 03 2018 at 11:22):

Also, Lean should know which olean files to rebuild. But sometimes it happens that a olean file is flying around were the corresponding lean file was removed. This produces strange results sometimes...

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:22):

So if you are on a very recent mathlib:master, and you've built. Then you checkout noetherian which is a couple of days old, then you get olean-files that are too new.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:22):

no there are still errors.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:23):

I removed all .olean files and the noetherian branch does not compile. Is this to do with "This branch is 2 commits ahead, 37 commits behind leanprover:master."?

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:23):

Is there a magic merge type command I can type to rebase or whatever the right word is?

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:23):

With noetherian checked out, you could try git merge master.

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:24):

There shouldn't be any conflicts.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:24):

git merge master reports already up to date and nothing seemed to happen.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:25):

It would be really nice to get a working noetherian.lean by 2pm

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:25):

I can happily dump the entire repo and clone again.

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:25):

Give me 2 minutes

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:27):

git checkout master
git pull
git checkout noetherian
git merge master
git push origin noetherian

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:27):

Can you checkout noetherian and git pull origin noetherian?

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:28):

I'm building using nightly-2018-06-21. Is this an issue?

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:28):

I just cloned again from github

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:29):

I'll also rebuild. But this machine is not the fastest in the world.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:33):

Will switching lean version change the behaviour of finish?

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:34):

I'm glad your version of 2pm is still 90 minutes away...

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:34):

Oh!

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:34):

I might have found my erro

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:34):

r

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:35):

I think I just don't understand branches. Maybe I thought I had pulled but I hadn't pulled.

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:36):

Does my little log of shell commands make sense to you?

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:36):

I just cloned the repo again

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:37):

I pushed a commit that merges the latest master into noetherian

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:42):

Woohow... I'm also getting boatloads of errors.

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:42):

Did I break the system?

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:44):

which version of Lean are you using?

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:45):

Whatever elan gave me. I think/hope the most recent. Let me check.

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:45):

Lean (version 3.4.1, commit 17fe3decaf8a, Release)

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:47):

Everything is complaining that data/set/basic.lean uses sorry.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:49):

so data/set/basic.lean works fine in regular mathlib but I have an error in community mathlib

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:51):

@[simp] theorem insert_diff_singleton {a : α} {s : set α} :
  insert a (s \ {a}) = insert a s :=
by simp [insert_eq, union_diff_self]

takes an age to compile and then I get a deterministic time-out

view this post on Zulip Johannes Hölzl (Sep 03 2018 at 11:52):

what does git status say? Are there any changed files?

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:57):

I only just cloned

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:57):

buzzard@ebony:~/lean-projects/mathlib-community$ git status
On branch noetherian
Your branch is up-to-date with 'origin/noetherian'.
nothing to commit, working directory clean
buzzard@ebony:~/lean-projects/mathlib-community$

view this post on Zulip Johan Commelin (Sep 03 2018 at 11:57):

The latest commit on the noetherian branch is a merging in master. I just did that.

view this post on Zulip Scott Morrison (Sep 03 2018 at 11:58):

@Johan Commelin, rebasing might have been better than merging. :-) (Says someone who only learnt to rebase last week.)

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:58):

The issue existed before the merge

view this post on Zulip Scott Morrison (Sep 03 2018 at 11:58):

I noticed the noetherian branch was broken, too.

view this post on Zulip Scott Morrison (Sep 03 2018 at 11:58):

Sorry, should have said something!

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 11:58):

is the master branch broken?

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 12:00):

[of community-mathlib]

view this post on Zulip Scott Morrison (Sep 03 2018 at 12:01):

no, it's good

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 12:01):

which version of Lean are you using?

view this post on Zulip Scott Morrison (Sep 03 2018 at 12:01):

I'm guessing the culprit is Mario's changes data/set/basic

view this post on Zulip Scott Morrison (Sep 03 2018 at 12:02):

What are these "versions" of which you speak? I use elan, so running lean automatically runs whichever version each respository says it needs. :-)

view this post on Zulip Scott Morrison (Sep 03 2018 at 12:03):

Looking at the leanpkg.toml for mathlib, that's 3.4.1

view this post on Zulip Johan Commelin (Sep 03 2018 at 12:05):

Ok, what should we do?

view this post on Zulip Johan Commelin (Sep 03 2018 at 12:05):

Can we still rebase?

view this post on Zulip Johan Commelin (Sep 03 2018 at 12:05):

Then we can use a built latest master branch, and look at the 5 changes or so, that are introduced by noetherian

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 12:06):

Oh I can work around this, I don't need it to compile. I will just work with mathlib master and not use the Noetherian branch.

view this post on Zulip Johan Commelin (Sep 03 2018 at 12:06):

Sure, but you want to work on noetherian modules, right?

view this post on Zulip Johan Commelin (Sep 03 2018 at 12:06):

So you want the TFAE theorem

view this post on Zulip Johan Commelin (Sep 03 2018 at 12:07):

And that is on the noetherian branch, and it depends on changes to data/set/basic.lean that seem to cause wreckage.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 12:07):

right

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 12:08):

so I'll just not have noetherian modules and I can still do the thing I was planning on doing, which was proving the 4th isomorphism theorem for R-modules

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 12:08):

we just don't get the application

view this post on Zulip Johan Commelin (Sep 03 2018 at 12:08):

@Johannes Hölzl @Scott Morrison would it be ok to rewrite history on this branch?

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 12:08):

It's OK, I have changed my plans

view this post on Zulip Scott Morrison (Sep 03 2018 at 12:08):

fine with me :-)

view this post on Zulip Johan Commelin (Sep 03 2018 at 12:08):

And you don't get the lattice structure and all the other foundational stuff that Mario did.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 12:09):

I don't need this stuff right now

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 12:09):

I just need it at some point

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 12:09):

it's no longer time-critical

view this post on Zulip Johannes Hölzl (Sep 03 2018 at 12:09):

Should I rebase it?

view this post on Zulip Johan Commelin (Sep 03 2018 at 12:09):

Yes please.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 12:09):

I don't mind either way

view this post on Zulip Johan Commelin (Sep 03 2018 at 12:09):

Throw away my merge commit.

view this post on Zulip Johannes Hölzl (Sep 03 2018 at 12:16):

just a second I need to fix some stuff which broke by Marios data/set/basic.lean changes

view this post on Zulip Johannes Hölzl (Sep 03 2018 at 12:32):

noetherian is now rebased and fixes the problems with the simp set. But maybe we just shouldn't add singleton_union and union_singleton to the simp set...

view this post on Zulip Johan Commelin (Sep 03 2018 at 12:46):

Thanks a lot!

view this post on Zulip Johan Commelin (Sep 03 2018 at 12:46):

@Kevin Buzzard A fresh clone should repair your issues.

view this post on Zulip Kenny Lau (Sep 03 2018 at 12:48):

A clone of Kevin Buzzard arrives with a wrench

view this post on Zulip Johan Commelin (Sep 03 2018 at 15:20):

@Kevin Buzzard What did you end up doing?

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

import linear_algebra.quotient_module

open is_submodule

local attribute [instance] quotient_rel

definition module.correspondence_theorem (R : Type*) [ring R] (M : Type*) [module R M]
  (N : set M) [is_submodule N] :
{Xbar : set (quotient M N) // is_submodule Xbar}  {X : set M // is_submodule X  N  X} :=
{ to_fun := λ Xbar, quotient.mk ⁻¹' Xbar.1,
    @@is_submodule.preimage _ _ _ Xbar.2 _ (is_linear_map_quotient_mk N),
    λ n Hn,begin
      show quotient.mk n  Xbar.val,
      have : n = 0,
        apply quotient.sound,
        show n - 0  N,
        simpa,
      rw this,
      haveI := Xbar.property,
      show (0 : quotient M N)  Xbar.val,
      exact @is_submodule.zero _ _ _ _ Xbar.val _,
end⟩⟩,
  inv_fun := λ X, ((quotient.mk '' X.val) : set (quotient M N)),
    by haveI := X.2.1; exact is_submodule.image (is_linear_map_quotient_mk N),
  left_inv := λ Pbar,_⟩,subtype.eq $ set.image_preimage_eq quotient.exists_rep,
  right_inv := λ P,HP, subtype.eq $ set.ext $ λ x,begin
    intro H,
    have H2 :  (y : M), y  P  y  x,
      simpa using H,
    rcases H2 with y,H3,H4,
    rw quotient_rel_eq at H4,
    have H5 : y - (y - x)  P,
      refine @is_submodule.sub _ _ _ _ _ HP.1 _ _ H3 _, -- fixing type class inference issues
      exact HP.2 H4, -- goal still x ∈ P.val, but H5 is y - (y - x) ∈ P.val
    convert H5, -- goal is now x = y - (y - x)
    simp, -- solves this
  end
  ,by apply set.subset_preimage_image,
}

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

4th isomorphism theorem!

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 16:03):

I spent about an hour talking about the mathematics (some of the audience had not seen quotient groups before) and then about an hour writing the code, although I would never have done it if Chris hadn't shown up and occasionally made comments like "oh you need to put local attribute [instance] quotient_rel".

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 16:05):

It's only a bijection between the sets, but checking that it's inclusion-preserving will be trivial because this is just a diagram chase using functions, not using the module properties at all. Note the excessive number of @s in the proof; this is apparently (according to @Chris Hughes ) because Chris has figured out how to make type class inference work OK for quotient structures, but quotient modules haven't been through his filter yet.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 16:05):

Chris -- what needs doing?

view this post on Zulip Johan Commelin (Sep 03 2018 at 16:09):

Ok, that's really cool! So this was basically a very successful live Lean coding session in front of students!

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 16:12):

to_fun was particularly painful. There are tricks here which would have made my life a lot easier, someone just needs to take the tricks from quotient groups and apply them here.

view this post on Zulip Johan Commelin (Sep 03 2018 at 16:17):

So, how far are we from showing that quotient of Noetherian is Noetherian?

view this post on Zulip Johan Commelin (Sep 03 2018 at 16:17):

By now it is math-trivial...

view this post on Zulip Johan Commelin (Sep 03 2018 at 16:18):

But in Lean? We need that a suitable sublattice of a well-founded lattice is well-founded. And we need to glue everything.

view this post on Zulip Chris Hughes (Sep 03 2018 at 16:18):

Very easy. I think it's just an application of inv_image_wf with the isomorphism.

view this post on Zulip Chris Hughes (Sep 03 2018 at 16:19):

But you also need S \sub T \iff f S \sub f T

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 16:31):

I'm just doing that now. I just used tidy for the first time :grinning:

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 16:33):

In fact both inclusions are by tidy

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 17:26):

OK dumb question: where is the construction which gives a module from a submodule?

view this post on Zulip Johan Commelin (Sep 03 2018 at 17:27):

https://github.com/leanprover/mathlib/blob/master/linear_algebra/subtype_module.lean

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 17:27):

Thanks.

view this post on Zulip Johan Commelin (Sep 03 2018 at 17:28):

This could potentially be subtype_instanced

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 17:41):

so now I find myself proving that a submodule of a submodule is a submodule :-/

view this post on Zulip Johan Commelin (Sep 03 2018 at 17:45):

Yes... that is really annoying.

view this post on Zulip Johan Commelin (Sep 03 2018 at 17:46):

In the end we'll want some lattice inclusion for that part of the story as well. And it seems you are already proving it.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 19:37):

tidy is just pwning a lot of these goals. It's just a lot of chasing trivialities around and perhaps tidy is just the thing for it.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 19:37):

Yes, my goal before I go to bed today is to prove that submodules and quotient modules of Noetherian modules are Noetherian.

view this post on Zulip Johan Commelin (Sep 03 2018 at 19:38):

Do you check what kind of proofs tidy generates? Or do you just write by tidy and move on?

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 20:26):

I write by tidy and then observe that in contrast to Scott I am unable to immediately see what proofs it generates, so I am forced to move on.

view this post on Zulip Patrick Massot (Sep 03 2018 at 20:28):

you could use the hole command to see what it does

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 20:48):

I need some advice. I have f : equiv X Y between two types both of which have `le. I have proved a <= b -> f a <= f b and c <= d -> f.symm c <= f.symm d (so f is an equivalence of preorders). I now want to deduce a < b <-> f a < f b` and I just wrote a boring proof of this. I feel like I'm missing some trick.

view this post on Zulip Chris Hughes (Sep 03 2018 at 21:02):

This is the least boring proof I could come up with

import data.equiv.basic
variables {α : Type*} {β : Type*} [preorder α] [preorder β]

example (f : α  β) (hf :  a b, a  b  f a  f b)
  (hf' :  a b, a  b  f.symm a  f.symm b) :  a b, a < b  f a < f b :=
have  a b, a  b  f a  f b, from λ a b,
hf a b, λ h, by rw [ equiv.inverse_apply_apply f a,  equiv.inverse_apply_apply f b];
  exact hf' (f a) (f b) h,
λ a b, by simp [lt_iff_le_not_le, this]

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 21:29):

I am wondering now if this proof should be generated by a tactic. I have beefed up my f to an equivalence of sets-equipped-with-le and then anything that I can define in a reasonable way just using le should be the same on both sides.

view this post on Zulip Mario Carneiro (Sep 03 2018 at 22:22):

You should use the theorems about order isomorphisms

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 22:30):

right.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 22:31):

I am drowning in trivialities, switching between your is_submodule M, the subtype {X : set M // is_submodule X}, and related subtypes such as {X : set M // is_submodule X \and X \sub N}.

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 22:32):

furthermore there is a hot tub full of teenage girls about 10 metres from me and they're getting really loud

view this post on Zulip Kevin Buzzard (Sep 03 2018 at 22:32):

I think it might be about time to tell my daughter to quieten down a bit. I can't really think straight any more

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

OK sanity restored (they're all asleep). @Mario Carneiro or @Patrick Massot I need advice -- mostly about management of code . I have proved subs of Noeth mods are Noeth and I have essentially proved quotients of Noeth mods are Noeth. Currently the proofs are horrible, it was getting harder and harder to work last night and some lemmas are called temp_name etc so I don't even feel it's ready to PR. But I have momentum and I'd like to finish the job. Currently in the noetherian branch of community mathlib (which I am actively working on) there's a bunch of stuff at the beginning of noetherian.lean which Mario wrote and which has nothing to do with Noetherian stuff -- it sets up a new type submodule R M which is the R-submodules of the R-module M. Mario set it up as a structure but it has precisely the structure of a subtype, it's the subsets of M with some property. The...whatever they're called...are called N.s (the subset) and N.sub (the proof it's a submodule) rather than N.val and N.property. Which is preferable and why? I propose moving this stuff somewhere else, because I want to use this language in the correspondence theorem. The proof that subquotients of Noetherian things are Noetherian naturally uses this submodule lattice all over the place but I want to use the same language for the correspondence theorem. Currently I've moved the definition of submodule to submodule.lean in linear_algebra even though it's not linear algebra in my opinion -- this is absolutely commutative ring theory. My main organisational problem is that I now want to prove things like "there's an injective map submodule R (quotient M N) -> submodule R M which I've proved in some sense -- I have a Lean theorem saying some interpretation of this -- but I am convinced I'm not using the right language. Mario proved submodule R M (see how much easier it is to understand if you use maths notation rather than alpha beta?) is a partial order so now I seem to want to prove theorems about order embeddings, and use the fact that if X -> Y is an order embedding then the order on X is induced from the order of Y somehow. Where do I look for this theorem and the relevant definitions -- are these theorems about orders, or semi-bot-sup-lattices, or what? Should this go into yet another file, called submodule_order.lean or does it all go in submodule.lean -- should this file be in ring theory or linear algebra, etc etc?

What I'm trying to say is: the maths is now in Lean, but it's not in a good state. When I was writing the schemes repo I would just dump it all in and move on. But Scott and others have convinced me that this is not a good long term plan, so I now want to spend just an hour or two making it as mathlib-ready as I can before actually PR'ing it. If anyone has any comments on (a) the merits of creating random new files like submodule.lean and where they should go or (b) the abstract theorem I should be proving about the relationship between the partial orders submodule R (quotient M N) and submodule R M (there's an injective map from the left to the right which preserves the order relation; this must already be a concept in Lean) then I'd be grateful to hear them. I am reluctant to put any more commutative ring theory into linear_algebra by the way.

view this post on Zulip Kenny Lau (Sep 04 2018 at 08:43):

did you sleep?

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 08:43):

I did. The joys of earplugs.

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 08:43):

I've just spent 2 hours tidying up though

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 08:45):

Kenny do you know what kind of Lean structure I have? I have two partial orders X and Y, an injection X -> Y, and a proof that a <= b iff f a <= f b. Furthermore (although I don't know if this is relevant) if f a <= d <= f b then there exists c such that f c = d.

view this post on Zulip Kenny Lau (Sep 04 2018 at 08:46):

I don't even know what kind of mathematical structure you have

view this post on Zulip Patrick Massot (Sep 04 2018 at 08:47):

Do you know about https://github.com/leanprover/mathlib/blob/master/order/order_iso.lean?

view this post on Zulip Patrick Massot (Sep 04 2018 at 08:48):

It seems to be exactly the file you want

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 08:49):

right -- thanks. I've never looked at that file I don't think. This is exactly why I asked here :-)

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 08:49):

Aah so that's the meaning of the symbol ≼o which I've seen several times before :-)

view this post on Zulip Scott Morrison (Sep 04 2018 at 08:51):

Your PR should also certainly create a whole new folder commutative_algebra. It's time!

view this post on Zulip Kevin Buzzard (Sep 04 2018 at 08:58):

Thanks Scott. OK so current proposal: new directory commutative_algebra, move file noetherian.lean into it, leave current files about modules where they are, nonsense about order embeddings in a file called something like module_order.lean(is this a bad name?) perhaps in ring_theory (because this part works for general rings), and now short proofs that subquotients of Noetherian modules are Noetherian ends up in Noetherian.lean. Hmm. Maybe even this part should be done for general rings; the theory very quickly becomes a commutative-ring-only theory, but this very basic part seems to work in general (we are doing "Noetherian left modules" I suspect, but I don't think it's an unreasonable convention to have "all modules over a non-comm ring, if not stated otherwise, are left modules" -- I think that's the current convention anyway.

view this post on Zulip Kevin Buzzard (Sep 05 2018 at 19:11):

The 4th isomorphism theorem needed some rewriting after Chris' changes to quotient modules. What is really striking now is that the theorem is still pretty much the same, but the complete proof that the correspondence is order-preserving is by tidy. Commutative algebra comes with a whole bunch of diagram chases and my intial impression is that tidy seems like it will be a really useful tool. I don't know if Mario is worried that compile times will go through the roof though...

import ring_theory.submodule
import linear_algebra.quotient_module -- I propose moving this to ring_theory
import tactic.tidy
import order.order_iso

open is_submodule
open quotient_module

definition module.correspondence_equiv (R) [ring R] (M) [module R M] (N : set M) [is_submodule N] :
(has_le.le : submodule R (quotient M N)  submodule R (quotient M N)  Prop) o
(has_le.le : {X : submodule R M // N  X}  {X : submodule R M // N  X}  Prop) := {
  to_fun := λ Xbar, submodule.pullback (mk : M  (quotient M N))
    (is_linear_map_quotient_mk N) Xbar,λ n Hn,begin
      show n  Xbar.s,
      haveI := Xbar.sub,
      have : ((0 : M) : quotient M N)  Xbar.s,
        exact @is_submodule.zero _ _ _ _ Xbar.s _,
      suffices : (n : quotient M N) = (0 : M),
        rwa this,
      rw quotient_module.eq,
      simp [Hn],
    end,
  inv_fun := λ X, submodule.pushforward mk (is_linear_map_quotient_mk N) X.val,
  left_inv := λ P, submodule.eq $ set.image_preimage_eq quotient_module.quotient.exists_rep,
  right_inv := λ P,HP, subtype.eq $ begin
    show submodule.pullback mk _ (submodule.pushforward mk _ P) = P,
    ext x,
    split,swap,apply set.subset_preimage_image,
    rintro y,Hy,Hyx,
    change (y : quotient M N) = x at Hyx,
    rw quotient_module.eq at Hyx,
    suffices : y - (y - x)  P,
      simpa,
    haveI := P.sub,
    exact is_submodule.sub Hy (HP Hyx),
  end,
  ord := by tidy, -- I love you Scott Morrison
}

view this post on Zulip Johan Commelin (Sep 05 2018 at 19:12):

Well, tidy can also tell you the proof. That will shave a bit of time off future compiles.

view this post on Zulip Johan Commelin (Sep 05 2018 at 19:12):

Use the hole command, Luke!

view this post on Zulip Kevin Buzzard (Sep 05 2018 at 19:14):

ord := begin intros a b, dsimp at *, simp at *, fsplit, work_on_goal 0 { intros a_1 a_2 a_3, simp at *, solve_by_elim }, intros a_1 a_2 a_3, induction a_2, work_on_goal 0 { simp at *, solve_by_elim }, refl end, -- I love you Scott Morrison

view this post on Zulip Kevin Buzzard (Sep 05 2018 at 19:14):

Should I use that proof instead? I am tempted to change the comment to "this proof brought to you by tidy"

view this post on Zulip Patrick Massot (Sep 05 2018 at 19:15):

I don't think we want that kind of proof in mathlib

view this post on Zulip Patrick Massot (Sep 05 2018 at 19:15):

But it should be very easy to clean

view this post on Zulip Patrick Massot (Sep 05 2018 at 19:16):

or else you can leave by tidy

view this post on Zulip Patrick Massot (Sep 05 2018 at 19:16):

we already have proofs by tidy (somewhat hidden by autoparam)

view this post on Zulip Johan Commelin (Sep 05 2018 at 19:16):

If you leave tidy there, what does the profiler say?

view this post on Zulip Johan Commelin (Sep 05 2018 at 19:17):

I guess it is pretty fast.

view this post on Zulip Johan Commelin (Sep 05 2018 at 19:17):

And the proof looks a lot more readable to me if it is just tidy (-;


Last updated: May 06 2021 at 18:20 UTC