Compact elements of lattices & f.g. submodules

Stream: general

[Chase Meadors]

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]

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]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Chase Meadors]

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]

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

[Johan Commelin]

@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]

@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]

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]

Enjoy your weekend away!