feat: add Wanted statement for the classification of root systems - #43068
feat: add Wanted statement for the classification of root systems#43068ocfnash wants to merge 2 commits into
Wanted statement for the classification of root systems#43068Conversation
PR summary e1cd5cdfc1Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
1d73cd1 to
3c6925c
Compare
This is partly motivated by seeing somewhat less ergonomic versions of these results land in Tau Ceti. These constructions and proofs could probably be provided in a couple of weeks by an expert. (NB: I do not have any plans to carry out this work in the near or distant future). Furthermore since we already have a complete reduction of the classification of Lie algebras to root systems, this would finish both classifications.
3c6925c to
cf1a443
Compare
faenuccio
left a comment
faenuccio
left a comment
There was a problem hiding this comment.
Thanks! I left some comments; I was also suggesting at a certain point the creation of a dedicated PR label (like Wanted or something) to indicate the kind of contribution.
| public import Mathlib.LinearAlgebra.RootSystem.OfBilinear | ||
|
|
||
| /-! | ||
| # The classification of root systems. |
There was a problem hiding this comment.
Could you add a small description for the un-initiated, perhaps with a (precise) reference?
|
|
||
| variable | ||
| {ι : Type*} [Finite ι] | ||
| {K : Type*} [Field K] [CharZero K] |
There was a problem hiding this comment.
Why not over an arbitrary CommRing R? People can weaken the theorem_wanted if they can't get to the full one immediately, but since the library is crafter to accommodate this it seems a pity. Or am I missing something?
| {N : Type*} [AddCommGroup N] [Module K N] | ||
| {P : RootPairing ι K M N} | ||
|
|
||
| def Base.HasCM {n : Type*} [P.IsCrystallographic] (bs : P.Base) (A : Matrix n n ℤ) := |
There was a problem hiding this comment.
Why not a structure fixing e? I understand that this would not really be unique (because of the permutation), but it would be easier to access for the API, no?
|
|
||
| -/ | ||
|
|
||
| theorem_wanted Base.hasCM_A_or_B_or_C_or_D_or_E_or_F_or_G |
There was a problem hiding this comment.
Doesn't this call for a definition of "classical groups", or something? It would probably just be an inductive type with the list of gadgets, but at least this statement would be nicer. Something like
| A (n : ℕ) → ClassicalGroupOrWhatever
|...
| E6 : ClassicalGroupOrWhatever
|...
does it make sense?
| instance_wanted : (❰a❱ K M N n).IsIrreducible | ||
| instance_wanted : (❰a❱ K M N n).IsValuedIn ℤ | ||
| instance_wanted : (❰a❱ K M N n).IsRootSystem | ||
| theorem_wanted a_hasCM_a : ∀ bs : (❰a❱ K M N n).Base, bs.HasCM (CartanMatrix.A n) |
There was a problem hiding this comment.
Actually only the instance_wanted : (❰a❱ K M N n).IsValuedIn ℤ is needed for the theorem, right? It might be worth it to section the file so that if someone feels like embarking on proving it, they don't need to prove reduceness/irreducibility.
ocfnash
added
the
awaiting-author
| {N : Type*} [AddCommGroup N] [Module K N] | ||
| {P : RootPairing ι K M N} | ||
|
|
||
| def Base.HasCM {n : Type*} [P.IsCrystallographic] (bs : P.Base) (A : Matrix n n ℤ) := |
There was a problem hiding this comment.
Rather annoyingly, an abelian variety "has CM" (aka "has complex multiplication") if its endomorphism ring is large in some precise sense, and this is a standard abbreviation in the area. Can we not face HasCartanMatrix?
|
|
||
| -/ | ||
|
|
||
| theorem_wanted Base.hasCM_A_or_B_or_C_or_D_or_E_or_F_or_G |
There was a problem hiding this comment.
It occurred to me that the current statement is not ideal for a different reason: this should really be a result about matrices and not use the language of root systems at all. The right statement is:
theorem_wanted Matrix.IsFiniteCartan.exists_A_or_B_or_C_or_D_or_E_or_F_or_G
{ι : Type*} [Fintype ι] [DecidableEq ι]
(M : Matrix ι ι ℤ) (hM : M.IsFiniteCartan) (hM' : M.IsIndecomposable) :
(∃ n e, M.reindex e e = CartanMatrix.A n) ∨
(∃ n e, M.reindex e e = CartanMatrix.B n) ∨
(∃ n e, M.reindex e e = CartanMatrix.C n) ∨
(∃ n e, M.reindex e e = CartanMatrix.D n) ∨
(∃ e, M.reindex e e = CartanMatrix.E 6) ∨
(∃ e, M.reindex e e = CartanMatrix.E 7) ∨
(∃ e, M.reindex e e = CartanMatrix.E 8) ∨
(∃ e, M.reindex e e = CartanMatrix.F₄) ∨
(∃ e, M.reindex e e = CartanMatrix.G₂)This needs #43121 so I'll return to this work once that is (hopefully!) in master.
3 participants
This is partly motivated by seeing somewhat less ergonomic versions of these results land in Tau Ceti.
Note that since we already have a complete reduction of the classification of Lie algebras to root systems, this would finish both classifications.
These constructions and proofs could probably be provided in a couple of weeks by an expert. I do not have any plans to carry out this work in the near or distant future and one goal of this PR is to invite others to implement this plan.