RootPairing definition

Stream: mathlib4

[Scott Carnahan]

Does the following alternative definition of docs#RootPairing seem reasonable? I thought it might remove the necessity of choice when, e.g., considering the permutation action of the Weyl group on the type that indexes roots:

structure RootPairing extends PerfectPairing R M N :=
  root : ι ↪ M
  coroot : ι ↪ N
  root_coroot_two : ∀ i, toLin (root i) (coroot i) = 2
  reflection_perm : ι → (ι ≃ ι)
  reflection_perm_root : ∀ i j,
    (preReflection (root i) (toLin.flip (coroot i))) (root j) = root ((reflection_perm i) j)
  reflection_perm_coroot : ∀ i j,
    (preReflection (coroot i) (toLin (root i))) (coroot j) = coroot ((reflection_perm i) j)

[Scott Carnahan]

As far as I can tell, the two definitions are "mathematically equivalent". (edit 1 week later: this is wrong)

[Johan Commelin]

Re "I thought"... do I understand correctly that you still think that?

[Kevin Buzzard]

Nice question! Of course you can check that they're equivalent by checking you can write code which bijects the two structures :-)

[Johan Commelin]

So the "new stuff" is that you are explicitly registering reflection_perm, right? And afaict it should be easy to build an "old" root pairing from your new defn. And in the other direction, theory indicates that it works. But I don't think we have the permutation action of Weyl groups yet. So I'm not sure we can carry out Kevin's exercise...

[Scott Carnahan]

Yes, I still think that.

[Johan Commelin]

Minor comment: do you need the .toFun bits in the last 2 axioms?

[Scott Carnahan]

Yes, I was writing API for the permutation action, and getting very frustrated.

[Scott Carnahan]

No, it seems .toFun was unnecessary. Editing.

[Johan Commelin]

Somewhat major question: can we easily convince ourselves that propositionally reflection_perm is determined by the other axioms?

[Johan Commelin]

cc @Oliver Nash who probably has something to say about this thread (-;

[Scott Carnahan]

We have docs#RootPairing.bijOn_reflection_root which says reflection induces bijections on the images under the injection root, but nothing about lifting the bijection to the indexing type (I'm still don't know an elegant way to do this - I used lots of choose and choose_spec).

[Andrew Yang]

Maybe docs#Function.Embedding.toEquivRange can give a good spelling of the lift?

[Andrew Yang]

Or docs#Equiv.ofInjective

[Oliver Nash]

I think Scott's suggestion is excellent and very much in the spirit of the rest of the definition of docs#RootPairing in which I took the view that the most convenient thing to do was to include uniquely-determined data and provide extensionality lemmas in the case that someone needed to take advantage of this uniqueness.

Of course it's not necessary to change the definitions, but I worked quite hard before I landed on the current design and my memory of previous iterations (which involved moderate use of docs#Classical.choose_spec amongst other things) makes it easy to believe that this extension is a good idea.

[Oliver Nash]

Unfortunately I do not have time to help with this refactor but I'd certainly be interested to see it attempted, and I would be surprised if it is not an improvement (even though I am already quite pleased with our current design).

[Scott Carnahan]

Thank you for the comments. I will attempt a refactor.

[Scott Carnahan]

It turns out the two definitions are not mathematically equivalent - the condition reflection_perm_coroot does not necessarily follow from the old definition in general.
They are equivalent for finite root systems in characteristic zero.
In the infinite case, the affine sl2 root pairing gives a counterexample. If we start with a pairing satisfying the new definition, then precomposing coroot with a suitable permutation of ι yields a structure that breaks the new definition but still satisfies the old definition.

[Johan Commelin]

@Scott Carnahan Interesting! I cannot infer from your message whether you think that is a feature or a bug of the new definition :wink:
Or should we have both?

[Scott Carnahan]

I think this means the new definition is preferable. Alternatively, I was too careless making a PR that removed the finiteness hypothesis in the old definition.

[Johan Commelin]

Ok, sounds good. I will happily review a PR that upgrades mathlib to the new definition.

[Oliver Nash]

The new definition is definitely the "right" one if we want to support infinite and positive-characteristic root systems (which we do).

With the benefit of hindsight, good evidence for this is the fact that docs#RootSystem.coroot_eq_coreflection_of_root_eq demands [Finte ι] and [CharZero R]. Moreover, your affine-sl2-based example shows [Finte ι] is necessary (and it wouldn't be too hard to find an example showing [CharZero R] is too).

[Scott Carnahan]

@Johan Commelin Thank you for offering! #13917
Please let me know if I am trying to do too much in one PR.

[Oliver Nash]

Thanks for doing this. I'll review it this evening.

[Oliver Nash]

@Scott Carnahan I decided to push up a commit of my own to #13917. I hope this is OK! Unfortunately this does mean we'll need a new reviewer to get this merged.

My main motivation was to add the alternate constructor RootPairing.mk'.

Mathematically, the main content is that if:

1. the roots / coroots are finite, and
2. we are in characteristic zero, and
3. there is no torsion,

then requiring that the root / coroots are stable under reflections / coreflections is sufficient to ensure that the _same family of permuations_ is induced on both roots and coroots.

I've never seen root data / systems set up to require this _same family of permutations_ property by definition: it's always a corollary, so I think it is important to provide these additional constructors which show that your very nice definition which requires it by definition is equivalent in the presence of 1, 2, 3.

[Oliver Nash]

I wonder has anyone worked these details out before. It seems root systems / data provide a good example of the phenomenon where naive weakening of the hypotheses leads to nonsense and axioms which are invisible in the usual cases need to be added to exclude pathologies in general.

[Johan Commelin]

I will try to find time to review this today. (Sorry for the late responses, the past 10 days have been hectic.)