-
Notifications
You must be signed in to change notification settings - Fork 298
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(algebra/lie/cartan_subalgebra): define Cartan subalgebras #6385
Closed
Closed
Changes from all commits
Commits
Show all changes
14 commits
Select commit
Hold shift + click to select a range
73936e0
feat(algebra/lie/nilpotent): basic facts about nilpotent Lie algebras
ocfnash 902887e
Update src/algebra/lie/nilpotent.lean
ocfnash 2254349
Update src/algebra/lie/nilpotent.lean
ocfnash 2dd28d9
Suggestions from CR
ocfnash 307a81c
Additional simp tag
ocfnash f96f680
Golf proof of `map_bracket_eq` using `map_bracket_le`
ocfnash 943864c
Add missing doc string
ocfnash b93a1c3
feat(algebra/lie/cartan_subalgebra): define Cartan subalgebras
ocfnash 140775d
Resolve merge conflict
ocfnash 8bbe328
Update src/algebra/lie/cartan_subalgebra.lean
ocfnash 9a0ad54
CR suggestions
ocfnash a4cced3
Drop now-redundant hypothesis from `le_normalizer_of_ideal`
ocfnash cc7a320
Implicit carrier types for `is_cartan_subalgebra`
ocfnash ab268b4
Explicitly mark `is_cartan_subalgebra` as `Prop`-valued
ocfnash File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,92 @@ | ||
/- | ||
Copyright (c) 2021 Oliver Nash. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Oliver Nash | ||
-/ | ||
import algebra.lie.nilpotent | ||
|
||
/-! | ||
# Cartan subalgebras | ||
|
||
Cartan subalgebras are one of the most important concepts in Lie theory. We define them here. | ||
The standard example is the set of diagonal matrices in the Lie algebra of matrices. | ||
|
||
## Main definitions | ||
|
||
* `lie_subalgebra.normalizer` | ||
* `lie_subalgebra.le_normalizer_of_ideal` | ||
* `lie_subalgebra.is_cartan_subalgebra` | ||
|
||
## Tags | ||
|
||
lie subalgebra, normalizer, idealizer, cartan subalgebra | ||
-/ | ||
|
||
universes u v w w₁ w₂ | ||
|
||
variables {R : Type u} {L : Type v} | ||
variables [comm_ring R] [lie_ring L] [lie_algebra R L] (H : lie_subalgebra R L) | ||
|
||
namespace lie_subalgebra | ||
|
||
/-- The normalizer of a Lie subalgebra `H` is the set of elements of the Lie algebra whose bracket | ||
with any element of `H` lies in `H`. It is the Lie algebra equivalent of the group-theoretic | ||
normalizer (see `subgroup.normalizer`) and is an idealizer in the sense of abstract algebra. -/ | ||
def normalizer : lie_subalgebra R L := | ||
{ carrier := { x : L | ∀ (y : L), (y ∈ H) → ⁅x, y⁆ ∈ H }, | ||
zero_mem' := λ y hy, by { rw zero_lie y, exact H.zero_mem, }, | ||
add_mem' := λ z₁ z₂ h₁ h₂ y hy, by { rw add_lie, exact H.add_mem (h₁ y hy) (h₂ y hy), }, | ||
smul_mem' := λ t y hy z hz, by { rw smul_lie, exact H.smul_mem t (hy z hz), }, | ||
lie_mem' := λ z₁ z₂ h₁ h₂ y hy, by | ||
{ rw lie_lie, exact H.sub_mem (h₁ _ (h₂ y hy)) (h₂ _ (h₁ y hy)), }, } | ||
|
||
lemma mem_normalizer_iff (x : L) : x ∈ H.normalizer ↔ ∀ (y : L), (y ∈ H) → ⁅x, y⁆ ∈ H := iff.rfl | ||
|
||
lemma le_normalizer : H ≤ H.normalizer := | ||
begin | ||
rw le_def, intros x hx, | ||
simp only [submodule.mem_coe, mem_coe_submodule, coe_coe, mem_normalizer_iff] at ⊢ hx, | ||
intros y, exact H.lie_mem hx, | ||
end | ||
|
||
/-- A Lie subalgebra is an ideal of its normalizer. -/ | ||
lemma ideal_in_normalizer : ∀ (x y : L), x ∈ H.normalizer → y ∈ H → ⁅x,y⁆ ∈ H := | ||
begin | ||
simp only [mem_normalizer_iff], | ||
intros x y h, exact h y, | ||
end | ||
|
||
/-- The normalizer of a Lie subalgebra `H` is the maximal Lie subalgebra in which `H` is a Lie | ||
ideal. -/ | ||
lemma le_normalizer_of_ideal {N : lie_subalgebra R L} | ||
(h : ∀ (x y : L), x ∈ N → y ∈ H → ⁅x,y⁆ ∈ H) : N ≤ H.normalizer := | ||
begin | ||
intros x hx, | ||
rw mem_normalizer_iff, | ||
exact λ y, h x y hx, | ||
end | ||
|
||
/-- A Cartan subalgebra is a nilpotent, self-normalizing subalgebra. -/ | ||
class is_cartan_subalgebra : Prop := | ||
(nilpotent : lie_algebra.is_nilpotent R H) | ||
(self_normalizing : H.normalizer = H) | ||
|
||
end lie_subalgebra | ||
|
||
@[simp] lemma lie_ideal.normalizer_eq_top {R : Type u} {L : Type v} | ||
[comm_ring R] [lie_ring L] [lie_algebra R L] (I : lie_ideal R L) : | ||
(I : lie_subalgebra R L).normalizer = ⊤ := | ||
begin | ||
ext x, simp only [lie_subalgebra.mem_normalizer_iff, lie_subalgebra.mem_top, iff_true], | ||
intros y hy, exact I.lie_mem hy, | ||
end | ||
|
||
open lie_ideal | ||
|
||
/-- A nilpotent Lie algebra is its own Cartan subalgebra. -/ | ||
instance lie_algebra.top_is_cartan_subalgebra_of_nilpotent [lie_algebra.is_nilpotent R L] : | ||
lie_subalgebra.is_cartan_subalgebra ⊤ := | ||
{ nilpotent := | ||
by { rwa lie_algebra.nilpotent_iff_equiv_nilpotent lie_subalgebra.top_equiv_self, }, | ||
self_normalizing := | ||
by { rw [← top_coe_lie_subalgebra, normalizer_eq_top, top_coe_lie_subalgebra], }, } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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.
IMO Lie and Cartan should be uppercase here.
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.
I generally agree with capitalising names but I've been consistently sticking to pure lowercase for these
Tags
across 15+ files so I'm reluctant to make this file the odd one out!Of course if someone wants to submit a PR capitalising all the names in
Tags
insrc/algebra/lie/*.lean
then that would be fine by me :-)