Inversion sets in a Weyl group

Relative to a base of a root pairing, the inversion set of a Weyl-group element consists of the positive roots that it sends to negative roots. This file gives the set-theoretic API for inversion sets and computes the inversion set of the identity and of a simple reflection.

These computations are the base cases for the root-level exchange step and the later identification of Coxeter length with the number of inversions.

Main definitions and results

• TauCeti.inversions is the set of positive roots sent to negative roots.
• TauCeti.inversions_one computes the inversion set of the identity.
• TauCeti.inversions_ofIdx computes the inversion set of a simple reflection.
• TauCeti.image_root_inversions identifies index-level inversions with vector roots.
• TauCeti.ncard_inversions_eq_ncard_vector_inversions identifies their cardinalities.

References

This file implements the inversion-set part of Layer 1 in TauCetiRoadmap/RepresentationTheory/RootSystems/README.md. The mathematical convention follows Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6.

def TauCeti.inversions {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (w : ↥P.weylGroup) : Set ι

The inversion set of w: the positive root indices that w sends to negative roots.

Equations

• TauCeti.inversions P b w = {i : ι | b.IsPos i ∧ ¬b.IsPos ((P.weylGroupToPerm w) i)}

@[simp]

theorem TauCeti.mem_inversions {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (w : ↥P.weylGroup) (i : ι) : i ∈ inversions P b w ↔ b.IsPos i ∧ ¬b.IsPos ((P.weylGroupToPerm w) i)

Membership in an inversion set means being positive and having negative image.

theorem TauCeti.inversions_eq_inter_preimage {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (w : ↥P.weylGroup) : inversions P b w = posRoots P b ∩ ⇑(P.weylGroupToPerm w) ⁻¹' negRoots P b

An inversion set is the intersection of the positive roots with the preimage of the negative roots.

theorem TauCeti.inversions_subset_posRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (w : ↥P.weylGroup) : inversions P b w ⊆ posRoots P b

Every inversion is a positive root.

theorem TauCeti.mapsTo_inversions_negRoots {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (w : ↥P.weylGroup) : Set.MapsTo (⇑(P.weylGroupToPerm w)) (inversions P b w) (negRoots P b)

The image of every inversion is a negative root.

theorem TauCeti.inversions_eq_empty_iff {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (w : ↥P.weylGroup) : inversions P b w = ∅ ↔ Set.MapsTo (⇑(P.weylGroupToPerm w)) (posRoots P b) (posRoots P b)

An element has no inversions exactly when it sends every positive root to a positive root.

theorem TauCeti.inversions_eq_posRoots_iff {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (w : ↥P.weylGroup) : inversions P b w = posRoots P b ↔ Set.MapsTo (⇑(P.weylGroupToPerm w)) (posRoots P b) (negRoots P b)

Every positive root is an inversion exactly when all positive roots are sent to negative roots.

theorem TauCeti.ncard_inversions_le {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (w : ↥P.weylGroup) [Finite ι] : (inversions P b w).ncard ≤ (posRoots P b).ncard

The number of inversions is at most the number of positive roots.

@[simp]

theorem TauCeti.inversions_one {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : inversions P b 1 = ∅

The identity Weyl-group element has no inversions.

theorem TauCeti.ncard_inversions_one {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) : (inversions P b 1).ncard = 0

The number of inversions of the identity is zero.

@[simp]

theorem TauCeti.inversions_ofIdx {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) : inversions P b (RootPairing.weylGroup.ofIdx P i) = {i}

A simple reflection has exactly its defining simple root as an inversion.

theorem TauCeti.ncard_inversions_ofIdx {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] {i : ι} (hi : i ∈ b.support) : (inversions P b (RootPairing.weylGroup.ofIdx P i)).ncard = 1

A simple reflection has one inversion.

theorem TauCeti.image_root_inversions {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (w : ↥P.weylGroup) : ⇑P.root '' inversions P b w = ⇑P.root '' posRoots P b ∩ {α : M | w • α ∈ ⇑P.root '' negRoots P b}

Index-level inversions identify with the positive vector roots sent to negative vector roots.

theorem TauCeti.ncard_inversions_eq_ncard_vector_inversions {ι : Type u} {R : Type v} {M : Type w} {N : Type x} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [CharZero R] (b : P.Base) (w : ↥P.weylGroup) : (inversions P b w).ncard = (⇑P.root '' posRoots P b ∩ {α : M | w • α ∈ ⇑P.root '' negRoots P b}).ncard

The number of index-level inversions equals the number of vector-root inversions.