Invariance under homomorphisms of root pairings

A homomorphism f : P.Hom P₂ of root pairings consists of a linear map of weight spaces, its transpose on coweight spaces, and a bijection f.indexEquiv of the indexing sets, subject to f.weightMap (P.root i) = P₂.root (f.indexEquiv i). The index bijection preserves Cartan pairings and commutes with root reflections. When the weight map is injective, it also preserves and reflects root membership, additive relations between roots, linear independence, and the root-string coefficients RootPairing.chainTopCoeff and RootPairing.chainBotCoeff.

The weight map need not be surjective: these results also apply when the target has extra toral directions outside the span of its roots. An equivalence of root pairings supplies the injectivity hypothesis through g.bijective_weightMap.injective. Coefficient-valuedness is transported by RootPairing.Hom.isValuedIn; the root-string results likewise derive target finiteness from the index bijection. Only the source coefficient-valuedness and finiteness instances are required.

Mathlib's RootPairing.Hom.pairing gives the pairing in the coefficient ring. The invariance lemmas here also apply to combinatorial expressions in the index bijection, without introducing weight-space vectors.

Main results

• RootPairing.Hom.weightMap_mem_range_root_iff: the weight map carries roots to roots and nothing else to a root.
• RootPairing.Hom.isValuedIn: the target root pairing takes values in any coefficient ring in which the source root pairing takes values.
• RootPairing.Hom.pairingIn_indexEquiv: the index bijection preserves pairings valued in a coefficient subring.
• RootPairing.Hom.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.
• RootPairing.Hom.root_indexEquiv_eq_add_iff and RootPairing.Hom.root_indexEquiv_eq_sub_iff: it preserves and reflects the relations α = β + γ and α = β - γ between roots.
• RootPairing.Hom.linearIndependent_root_indexEquiv_iff: it preserves and reflects linear independence of a pair of roots.
• RootPairing.Hom.chainTopCoeff_indexEquiv and RootPairing.Hom.chainBotCoeff_indexEquiv: it preserves the two root-string coefficients.

These invariance facts show that an automorphism of a root system permutes the matrices of Geck's construction, as developed in TauCeti.LinearAlgebra.RootSystem.GeckConstruction.Symmetry.

References

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

theorem RootPairing.Hom.isValuedIn {ι : 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₂) (S : Type u_8) [CommRing S] [Algebra S R] [P.IsValuedIn S] : P₂.IsValuedIn S

A homomorphism of root pairings transports the property that all root-coroot pairings take values in a given coefficient ring.

@[simp]

theorem RootPairing.Hom.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₂} (f : P.Hom P₂) (S : Type u_8) [CommRing S] [Algebra S R] [FaithfulSMul S R] [P.IsValuedIn S] (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 RootPairing.Hom.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.

theorem RootPairing.Hom.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₂} (f : P.Hom P₂) (hf : Function.Injective ⇑f.weightMap) {m : M} : f.weightMap m ∈ Set.range ⇑P₂.root ↔ m ∈ Set.range ⇑P.root

A homomorphism of root pairings with injective weight map carries roots to roots, and carries nothing else to a root.

@[simp]

theorem RootPairing.Hom.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₂} (f : P.Hom P₂) (hf : Function.Injective ⇑f.weightMap) (k i j : ι) : P₂.root (f.indexEquiv k) = P₂.root (f.indexEquiv i) + P₂.root (f.indexEquiv j) ↔ P.root k = P.root i + P.root j

The index bijection of a homomorphism with injective weight map preserves and reflects the relation α = β + γ between roots.

@[simp]

theorem RootPairing.Hom.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₂} (f : P.Hom P₂) (hf : Function.Injective ⇑f.weightMap) (k j i : ι) : P₂.root (f.indexEquiv k) = P₂.root (f.indexEquiv j) - P₂.root (f.indexEquiv i) ↔ P.root k = P.root j - P.root i

The index bijection of a homomorphism with injective weight map preserves and reflects the relation α = β - γ between roots.

@[simp]

theorem RootPairing.Hom.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₂} (f : P.Hom P₂) (hf : Function.Injective ⇑f.weightMap) (i j : ι) : LinearIndependent R ![P₂.root (f.indexEquiv i), P₂.root (f.indexEquiv j)] ↔ LinearIndependent R ![P.root i, P.root j]

The index bijection of a homomorphism with injective weight map preserves and reflects linear independence of a pair of roots.

@[simp]

theorem RootPairing.Hom.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₂} (f : P.Hom P₂) (hf : Function.Injective ⇑f.weightMap) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (i j : ι) : chainTopCoeff (f.indexEquiv i) (f.indexEquiv j) = chainTopCoeff i j

The index bijection of a homomorphism with injective weight map preserves the number of times one may add P.root i to P.root j and stay among the roots.

@[simp]

theorem RootPairing.Hom.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₂} (f : P.Hom P₂) (hf : Function.Injective ⇑f.weightMap) [Finite ι] [CharZero R] [IsDomain R] [P.IsCrystallographic] (i j : ι) : chainBotCoeff (f.indexEquiv i) (f.indexEquiv j) = chainBotCoeff i j

The index bijection of a homomorphism with injective weight map preserves the number of times one may subtract P.root i from P.root j and stay among the roots.