New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(Order/Hom): prove disjoint from order embedding #12223
Conversation
I golfed your proofs (I hope, without loss of readability). LGTM |
🚀 Pull request has been placed on the maintainer queue by urkud. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
This adds 3 lemmas which state that if you have an order embedding `f` such that `f a₁` and `f a₂` are disjoint/codisjoint/complements, then the same holds for `a₁` and `a₂`. *Motivation*: For a project described [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Derivations.20on.20Lie.20algebras), I wanted to know that if two Lie ideals are complements as submodules, then they are complements as Lie ideals too. I realized that the correct level of generality was probably in the `Order.Hom.Basic` file. *Caveats*: I am very much open to golfing/naming/redesign suggestions. Within the modified file, there was already a `Disjoint.map_orderIso` result, but it requires an `OrderIso` (not just a one-way embedding) and it requires a `SemilatticeInf` (whereas my version just uses `PartialOrder`). Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Pull request successfully merged into master. Build succeeded: |
Thank you very much for the golfing and the fast merging. The proofs indeed look much better. |
This adds 3 lemmas which state that if you have an order embedding `f` such that `f a₁` and `f a₂` are disjoint/codisjoint/complements, then the same holds for `a₁` and `a₂`. *Motivation*: For a project described [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Derivations.20on.20Lie.20algebras), I wanted to know that if two Lie ideals are complements as submodules, then they are complements as Lie ideals too. I realized that the correct level of generality was probably in the `Order.Hom.Basic` file. *Caveats*: I am very much open to golfing/naming/redesign suggestions. Within the modified file, there was already a `Disjoint.map_orderIso` result, but it requires an `OrderIso` (not just a one-way embedding) and it requires a `SemilatticeInf` (whereas my version just uses `PartialOrder`). Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
This adds 3 lemmas which state that if you have an order embedding `f` such that `f a₁` and `f a₂` are disjoint/codisjoint/complements, then the same holds for `a₁` and `a₂`. *Motivation*: For a project described [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Derivations.20on.20Lie.20algebras), I wanted to know that if two Lie ideals are complements as submodules, then they are complements as Lie ideals too. I realized that the correct level of generality was probably in the `Order.Hom.Basic` file. *Caveats*: I am very much open to golfing/naming/redesign suggestions. Within the modified file, there was already a `Disjoint.map_orderIso` result, but it requires an `OrderIso` (not just a one-way embedding) and it requires a `SemilatticeInf` (whereas my version just uses `PartialOrder`). Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
This adds 3 lemmas which state that if you have an order embedding `f` such that `f a₁` and `f a₂` are disjoint/codisjoint/complements, then the same holds for `a₁` and `a₂`. *Motivation*: For a project described [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Derivations.20on.20Lie.20algebras), I wanted to know that if two Lie ideals are complements as submodules, then they are complements as Lie ideals too. I realized that the correct level of generality was probably in the `Order.Hom.Basic` file. *Caveats*: I am very much open to golfing/naming/redesign suggestions. Within the modified file, there was already a `Disjoint.map_orderIso` result, but it requires an `OrderIso` (not just a one-way embedding) and it requires a `SemilatticeInf` (whereas my version just uses `PartialOrder`). Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
This adds 3 lemmas which state that if you have an order embedding
f
such thatf a₁
andf a₂
are disjoint/codisjoint/complements, then the same holds fora₁
anda₂
.Motivation: For a project described here, I wanted to know that if two Lie ideals are complements as submodules, then they are complements as Lie ideals too. I realized that the correct level of generality was probably in the
Order.Hom.Basic
file.Caveats: I am very much open to golfing/naming/redesign suggestions. Within the modified file, there was already a
Disjoint.map_orderIso
result, but it requires anOrderIso
(not just a one-way embedding) and it requires aSemilatticeInf
(whereas my version just usesPartialOrder
).