What an equivalence of root pairings preserves

An equivalence g : P.Equiv P₂ of root pairings consists of a linear equivalence of weight spaces, its transpose on coweight spaces, and a bijection g.indexEquiv of the indexing sets, subject to g.weightMap (P.root i) = P₂.root (g.indexEquiv i). This file collects the combinatorial data that the index bijection therefore preserves: which elements of the weight space are roots, the integral Cartan pairings, the negation of an index, additive relations between roots, and the root-string coefficients RootPairing.chainTopCoeff and RootPairing.chainBotCoeff.

Mathlib's RootPairing.Hom.pairing already gives the pairing in the coefficient ring. Everything else here is new, and each statement is about the index bijection alone, so it applies to a combinatorial expression in which no weight-space vector occurs.

Main results

• TauCeti.weightMap_mem_range_root_iff: the weight map carries roots to roots and nothing else to a root.
• TauCeti.pairingIn_indexEquiv: the index bijection preserves pairings valued in a coefficient subring.
• TauCeti.indexEquiv_reflectionPerm: it commutes with RootPairing.reflectionPerm, and therefore with the negation of an index, which is RootPairing.reflectionPerm i i by definition and is rewritten to that form by the simp lemma RootPairing.indexNeg_neg.
• TauCeti.root_indexEquiv_eq_add_iff and TauCeti.root_indexEquiv_eq_sub_iff: it preserves and reflects the relations α = β + γ and α = β - γ between roots.
• TauCeti.linearIndependent_root_indexEquiv_iff: it preserves and reflects linear independence of a pair of roots.
• TauCeti.chainTopCoeff_indexEquiv and TauCeti.chainBotCoeff_indexEquiv: it preserves the two root-string coefficients.

Roadmap

These are the invariance facts consumed by TauCeti/LinearAlgebra/RootSystem/GeckConstruction/Symmetry.lean, which uses them to show that an automorphism of a root system permutes the matrices of Geck's construction. That is a step of Layer 9, "pinned Chevalley--Demazure group schemes over ℤ", of TauCetiRoadmap/ReductiveGroups/README.md.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Ch. VI, §1.

theorem TauCeti.weightMap_mem_range_root_iff {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P.Equiv P₂) {m : M} : (↑g).weightMap m ∈ Set.range ⇑P₂.root ↔ m ∈ Set.range ⇑P.root

An equivalence of root pairings carries roots to roots, and carries nothing else to a root.

This is not a simp lemma: Set.mem_range is itself @[simp], so both sides are already reducible to their existential forms and the simpNF linter rejects the annotation.

@[simp]

theorem TauCeti.pairingIn_indexEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} (S : Type u_8) [CommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] [P₂.IsValuedIn S] (f : P.Hom P₂) (i j : ι) : P₂.pairingIn S (f.indexEquiv i) (f.indexEquiv j) = P.pairingIn S i j

The index bijection of a homomorphism of root pairings preserves the pairing valued in a coefficient subring.

@[simp]

theorem TauCeti.indexEquiv_reflectionPerm {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} (f : P.Hom P₂) (i j : ι) : f.indexEquiv ((P.reflectionPerm i) j) = (P₂.reflectionPerm (f.indexEquiv i)) (f.indexEquiv j)

The index bijection of a homomorphism of root pairings commutes with root reflections.

@[simp]

theorem TauCeti.root_indexEquiv_eq_add_iff {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P.Equiv P₂) (k i j : ι) : P₂.root ((↑g).indexEquiv k) = P₂.root ((↑g).indexEquiv i) + P₂.root ((↑g).indexEquiv j) ↔ P.root k = P.root i + P.root j

The index bijection of an equivalence of root pairings preserves and reflects the relation α = β + γ between roots.

@[simp]

theorem TauCeti.root_indexEquiv_eq_sub_iff {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P.Equiv P₂) (k j i : ι) : P₂.root ((↑g).indexEquiv k) = P₂.root ((↑g).indexEquiv j) - P₂.root ((↑g).indexEquiv i) ↔ P.root k = P.root j - P.root i

The index bijection of an equivalence of root pairings preserves and reflects the relation α = β - γ between roots.

@[simp]

theorem TauCeti.linearIndependent_root_indexEquiv_iff {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P.Equiv P₂) (i j : ι) : LinearIndependent R ![P₂.root ((↑g).indexEquiv i), P₂.root ((↑g).indexEquiv j)] ↔ LinearIndependent R ![P.root i, P.root j]

The index bijection of an equivalence of root pairings preserves and reflects linear independence of a pair of roots.

@[simp]

theorem TauCeti.chainTopCoeff_indexEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P.Equiv P₂) [Finite ι] [Finite ι₂] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P₂.IsCrystallographic] (i j : ι) : RootPairing.chainTopCoeff ((↑g).indexEquiv i) ((↑g).indexEquiv j) = RootPairing.chainTopCoeff i j

The index bijection of an equivalence of root pairings preserves the number of steps one may add α to β and stay among the roots.

@[simp]

theorem TauCeti.chainBotCoeff_indexEquiv {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} (g : P.Equiv P₂) [Finite ι] [Finite ι₂] [CharZero R] [IsDomain R] [P.IsCrystallographic] [P₂.IsCrystallographic] (i j : ι) : RootPairing.chainBotCoeff ((↑g).indexEquiv i) ((↑g).indexEquiv j) = RootPairing.chainBotCoeff i j

The index bijection of an equivalence of root pairings preserves the number of steps one may subtract α from β and stay among the roots.