feat(algebra/module): Add Jordan-Hölders lattice for modules #17226
Conversation
MadPidgeon
added
awaiting-review
MadPidgeon
changed the title
| structure is_maximal (x z : α) : Prop := | ||
| (lt : x < z) | ||
| (bot_or_top : ∀ {y}, x ≤ y → y ≤ z → (y = x ∨ y = z)) |
There was a problem hiding this comment.
I think this is the same notion as covby; perhaps @YaelDillies can confirm
There was a problem hiding this comment.
Yep, this is exactly x ⋖ z (import order.cover).
There was a problem hiding this comment.
Thanks, I will try to replace is_maximal by covby tomorrow!
There was a problem hiding this comment.
I have a version now which uses covby. I am not sure where to leave the additional lemmas, nor what their correct name should be.
There was a problem hiding this comment.
Please also conform to the style guidelines (see examples there, though contemporary mathlib uses λ more often than assume):
When defining instances, opening and closing braces are not alone on their line.
When new goals arise as side conditions or steps, they are enclosed in focussing braces and indented (except possibly the last goal, if its proof is much longer than the proofs of the other goals). Braces are not alone on their line.
| is_maximal_inf_left_of_is_maximal_sup := λ {A B} h₁ h₂, by { | ||
| rw covby_iff_quot_is_simple (inf_le_left : A ⊓ B ≤ A), | ||
| haveI h := (covby_iff_quot_is_simple (le_sup_right : B ≤ A ⊔ B)).mp h₂, | ||
| apply is_simple_module.congr (linear_map.quotient_inf_equiv_sup_quotient A B) }, |
There was a problem hiding this comment.
This should be proved for modular lattices.
There was a problem hiding this comment.
In fact, this is already a theorem. See inf_covby_of_covby_sup_of_covby_sup_left
There was a problem hiding this comment.
Here is a start to show that a modular lattice is upper/lower semimodular: modular_semimodular_lattice
mathlib-dependent-issues-bot
added
blocked-by-other-PR
|
This PR/issue depends on: |
|
Oh I just noticed, this PR was opened from another repo. Could you please reopen this PR from the mathlib repository? You can ask for writing permissions on Zulip. |
|
I think you can change the branch after you create a branch in the leanprover-community repo, and there's no need to open another PR. |
|
Hmm, seems you can only change the to-branch but not the from-branch. Never mind then! |
YaelDillies
removed
the
awaiting-review
wcovby_iff_le_and_eq_or_eq#17262