Stream: general

Topic: Compact elements of lattices & f.g. submodules

Chase Meadors (Jan 15 2021 at 23:08):

Hey all! I was surprised to find recently that Lean doesn't seem to know that a finitely generated module has a maximal submodule (although it does know this for Noetherian modules).
Well, I went down a rabbit hole and ended up making a small project out of that, and proved it more generally by way of defining compact elements in (complete) lattices, showing such elements always cover something below them. Then you can get that a submodule is f.g. iff it's compact (and same for other f.g. algebraic substructures).
Highlights include the defn of compact and the equivalence of the two definitions here,

def compact {α : Type} [has_le α] [has_Sup α] (k : α) :=
∀ S : set α, S.nonempty → directed_on (≤) S → k ≤ Sup S → ∃ x : α, x ∈ S ∧ k ≤ x,

theorem compact_def {α : Type} [decidable_eq α] [complete_lattice α] (k : α) :
compact k ↔ ∀ S : set α, k ≤ Sup S → ∃ F : finset α, ↑F ⊆ S ∧ k ≤ F.sup id


And the main theorems

theorem exists_maximal_of_compact {α : Type} [complete_lattice α] (k : α) (hk : compact k) :
∀ b : α, b < k → ∃ m ∈ set.Ico b k, ∀ x ∈ set.Ico b k, m ≤ x → x = m

theorem submodule_compact_iff_fg (S : submodule R M) (h : S.fg) : compact S


This was mainly an exercise to do something non-trivial in Lean, but I would be interested in contributing this if there's any interest. I expect there's a lot of clean up and things to do before it's ready for a PR, so I wanted to ask (1) is there any interest in this enough to work on contributing it, and (2) what are some of those things to do to get something up to mathlib standards?

Alex J. Best (Jan 15 2021 at 23:27):

Hi Chase, this certainly sounds interesting to me, I'd encourage you to PR this. A few things to do to get it to mathlib standards are to:

• Check that all the linters are happy (type #lint at the bottom of each file you changed)
• Check out the style guide https://leanprover-community.github.io/contribute/style.html and naming conventions for lemmas and make sure those are conformed to https://leanprover-community.github.io/contribute/naming.html
• Make sure any documentation follows the developed style https://leanprover-community.github.io/contribute/doc.html
• Make sure all lemmas etc. are in good places, its quite tempting to lump everything in one file when developing something new, but in the end things should be in a logical file for the sort of object they deal with.
• Remove any stray commented out code and random #check blah type lines you may have added when writing
• If you've done all this (or even if you haven't) feel free to open a PR and then add the awaiting-review tag when you're ready, people will undoubtedly have more comments but thats part of the process too!

Chase Meadors (Jan 16 2021 at 00:12):

Thanks a lot! I'll get to work on that soon

Aaron Anderson (Jan 16 2021 at 01:10):

@Oliver Nash and I have recently been expanding the lattice library, with some related PRs currently in the pipeline

Aaron Anderson (Jan 16 2021 at 01:14):

The main file that you should look at, if you haven’t, is order.complete_well_founded.lean

Aaron Anderson (Jan 16 2021 at 01:15):

Which essentially shows that a complete lattice is well-founded iff all elements are compact, but without quite defining “compact elements”

Aaron Anderson (Jan 16 2021 at 01:22):

I totally think that definition belongs in mathlib, and we should edit that file to use it.

Chase Meadors (Jan 16 2021 at 01:39):

Thanks Aaron; that file's pretty recent so I didn't have it - I'll definitely take a look. I'll see if some of what I've done can fit in or around there.

Aaron Anderson (Jan 16 2021 at 02:05):

Oh, also, there's certainly some relation between your lemma exists_maximal_of_compact and the definition is_coatomic in #5588.

Johan Commelin (Jan 16 2021 at 04:00):

@Chase Meadors besides the checklist from Alex, there is also https://leanprover-community.github.io/contribute/index.html that gives an overview of the PR lifecycle.
Could you please give a rought estimate of how many lines of code you have added/changed? For example using

git diff --stat master...


Oliver Nash (Jan 16 2021 at 12:59):

@Chase Meadors This is great news! I look forward to seeing the definition of compact lattice elements land in Mathlib. These results will be useful and as @Aaron Anderson mentions, it will allow you to refine the results we recently introduced here.

Chase Meadors (Jan 17 2021 at 00:29):

Thanks @Aaron Anderson @Oliver Nash I'll be away this weekend but I'll take a look at this soon; I'll message you if I have ideas or questions.
@Johan Commelin I only have about 7 theorems comprising about 200 LOC, but I did everything in a scratch file and hadn't decided where to put things yet. It sounds like I should check for some overlap with the areas Aaron and Oliver mentioned before deciding what to contribute.

Oliver Nash (Jan 17 2021 at 09:52):

Enjoy your weekend away!

Last updated: May 14 2021 at 00:42 UTC