Invariant forms along root strings

This file records how an invariant bilinear form changes between consecutive roots in a root string. It also shows that any integer-valued length function symmetrizing the Cartan integers is quadratic along integral root relations. The results are the root-system calculation behind the integrality of Chevalley structure constants.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §25.2.
• R. W. Carter, Simple Groups of Lie Type, §4.1.

This advances the Chevalley-basis input to the explicit Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, consumed by milestone L0 of the CFSGStatement roadmap.

theorem RootPairing.length_of_root_eq_add_zsmul {I : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module ℤ M] [AddCommGroup N] [Module ℤ N] (P : RootPairing I ℤ M N) (length : I → ℤ) (hsym : ∀ (α β : I), length α * P.pairing β α = length β * P.pairing α β) (α β γ : I) (n : ℤ) (h : P.root γ = P.root β + n • P.root α) : length γ = length β + n * length α * P.pairing β α + n ^ 2 * length α

A symmetrizing integer-valued length function is quadratic along integral root relations.

theorem RootPairing.pairing_mem_neg_one_zero_one_of_length_eq {I : Type u_1} {M : Type u_2} {N : Type u_3} [Finite I] [AddCommGroup M] [Module ℤ M] [Module.IsTorsionFree ℤ M] [AddCommGroup N] [Module ℤ N] {P : RootPairing I ℤ M N} (length : I → ℤ) (hsym : ∀ (α β : I), length α * P.pairing β α = length β * P.pairing α β) (α β : I) (hpair : |P.pairing β α| ≤ 2) (hαpos : 0 < length α) (hαβ : length α = length β) (hne : β ≠ α) (hneg : P.root β ≠ -P.root α) : P.pairing β α ∈ {-1, 0, 1}

Distinct non-opposite roots of equal positive length have Cartan pairing -1, 0, or 1 when that pairing has absolute value at most two.

theorem RootPairing.not_root_eq_add_nsmul_of_length_eq_of_two_le {I : Type u_1} {M : Type u_2} {N : Type u_3} [Finite I] [AddCommGroup M] [Module ℤ M] [Module.IsTorsionFree ℤ M] [AddCommGroup N] [Module ℤ N] {P : RootPairing I ℤ M N} (length : I → ℤ) (hsym : ∀ (α β : I), length α * P.pairing β α = length β * P.pairing α β) (α β γ : I) (n : ℕ) (hpair : |P.pairing β α| ≤ 2) (hαpos : 0 < length α) (hαβ : length α = length β) (hγ : length γ < 3 * length α) (hneg : P.root β ≠ -P.root α) (hn : 2 ≤ n) (h : P.root γ = P.root β + ↑n • P.root α) : False

An equal-length root string through non-opposite roots has no term two or more steps in the positive direction when the resulting root has length less than three times theirs.

theorem RootPairing.pairing_eq_zero_of_short_add_short_eq_long {I : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module ℤ M] [AddCommGroup N] [Module ℤ N] {P : RootPairing I ℤ M N} (length : I → ℤ) (hsym : ∀ (α β : I), length α * P.pairing β α = length β * P.pairing α β) (α β γ : I) (hα : length α = 1) (hβ : length β = 1) (hγ : length γ = 2) (h : P.root γ = P.root β + P.root α) : P.pairing β α = 0

If two roots of length one add to a root of length two, their Cartan pairing is zero.

theorem RootPairing.n_eq_one_and_pairing_eq_neg_one_and_length_eq_one_of_short_add_nsmul_long {I : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module ℤ M] [AddCommGroup N] [Module ℤ N] {P : RootPairing I ℤ M N} (length : I → ℤ) (hsym : ∀ (α β : I), length α * P.pairing β α = length β * P.pairing α β) (α β γ : I) (n : ℕ) (hpair : |P.pairing α β| ≤ 2) (hα : length α = 2) (hβ : length β = 1) (hγ : length γ = 1 ∨ length γ = 2) (hn : 0 < n) (h : P.root γ = P.root β + ↑n • P.root α) : n = 1 ∧ P.pairing β α = -1 ∧ length γ = 1

A positive root string from a root of length one in a length-two direction has at most one step, and that step again has length one.

theorem RootPairing.chainBotCoeff_eq_one_of_short_add_short_eq_long {I : Type u_1} {M : Type u_2} {N : Type u_3} [Finite I] [AddCommGroup M] [Module ℤ M] [AddCommGroup N] [Module ℤ N] {P : RootPairing I ℤ M N} [P.IsCrystallographic] [P.IsReduced] (length : I → ℤ) (hsym : ∀ (α β : I), length α * P.pairing β α = length β * P.pairing α β) (α β γ : I) (hlength : ∀ (δ : I), P.root δ = P.root β + 2 • P.root α → length δ = 1 ∨ length δ = 2) (hα : length α = 1) (hβ : length β = 1) (hγ : length γ = 2) (h : P.root γ = P.root β + P.root α) : chainBotCoeff α β = 1

If two roots of length one add to a root of length two, and every root at the next positive string position has length one or two, their descending chain coefficient is one.

theorem RootPairing.pairings_of_long_add_two_short {I : Type u_1} {M : Type u_2} {N : Type u_3} [AddCommGroup M] [Module ℤ M] [AddCommGroup N] [Module ℤ N] {P : RootPairing I ℤ M N} (length : I → ℤ) (hsym : ∀ (α β : I), length α * P.pairing β α = length β * P.pairing α β) (α β γ : I) (hα : length α = 1) (hβ : length β = 2) (hγ : length γ = 1 ∨ length γ = 2) (h : P.root γ = P.root β + 2 • P.root α) : P.pairing β α = -2 ∧ P.pairing α β = -1 ∧ length γ = 2

If adding twice a length-one root to a length-two root gives a root, the endpoint has length two and the two Cartan pairings are -2 and -1.

theorem RootPairing.exists_short_midpoint_of_long_add_two_short {I : Type u_1} {M : Type u_2} {N : Type u_3} [Finite I] [AddCommGroup M] [Module ℤ M] [Module.IsTorsionFree ℤ M] [AddCommGroup N] [Module ℤ N] {P : RootPairing I ℤ M N} [P.IsCrystallographic] [P.IsReduced] (length : I → ℤ) (hsym : ∀ (α β : I), length α * P.pairing β α = length β * P.pairing α β) (α β γ : I) (hα : length α = 1) (hβ : length β = 2) (hγ : length γ = 1 ∨ length γ = 2) (h : P.root γ = P.root β + 2 • P.root α) : ∃ (δ : I), P.root δ = P.root β + P.root α ∧ length δ = 1 ∧ chainBotCoeff α β = 0 ∧ chainTopCoeff α β = 2 ∧ chainBotCoeff α δ = 1 ∧ chainTopCoeff α δ = 1

A two-step root string from a length-two root in a length-one direction has a length-one midpoint, and its chain coefficients are zero, two, one, and one.

theorem RootPairing.chainBotCoeff_eq_zero_of_add_of_length_eq {I : Type u_1} {M : Type u_2} {N : Type u_3} [Finite I] [AddCommGroup M] [Module ℤ M] [AddCommGroup N] [Module ℤ N] {P : RootPairing I ℤ M N} [P.IsCrystallographic] (length : I → ℤ) (hsym : ∀ (α β : I), length α * P.pairing β α = length β * P.pairing α β) (α β γ : I) (hαpos : 0 < length α) (hminus : ∀ (δ : I), P.root δ = P.root β + -1 • P.root α → length δ ≤ 2) (hβpos : 0 < length β) (hβγ : length β = length γ) (h : P.root γ = P.root β + P.root α) : chainBotCoeff α β = 0

A root edge whose source and target have the same positive length has no descending root when every possible predecessor has length at most two.

theorem RootPairing.chainBotCoeff_comm_of_root_add_mem {I : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite I] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing I R M N} [P.IsCrystallographic] [P.IsReduced] {i j : I} (hadd : P.root i + P.root j ∈ Set.range ⇑P.root) : chainBotCoeff i j = chainBotCoeff j i

The lower endpoint of the root string through two roots is symmetric when their sum is a root.

theorem RootPairing.InvariantForm.apply_root_self_eq_of_root_add_of_pairing_eq_zero {I : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite I] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing I R M N} [P.IsCrystallographic] [P.IsReduced] (B : P.InvariantForm) {i j k : I} (hk : P.root k = P.root i + P.root j) (hij₀ : P.pairing i j = 0) : (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)

Two orthogonal roots whose sum is a root have the same squared length in every invariant form.

theorem RootPairing.InvariantForm.chainTopCoeff_mul_apply_root_self_eq {I : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite I] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing I R M N} [P.IsCrystallographic] [P.IsReduced] (B : P.InvariantForm) {i j k : I} (hk : P.root k = P.root i + P.root j) : ↑(chainTopCoeff i j) * (B.form (P.root k)) (P.root k) = ↑(chainBotCoeff i j + 1) * (B.form (P.root j)) (P.root j)

Along a root string, the squared lengths of two consecutive roots have the ratio of the corresponding raising coefficients. If γ = α + β, then

q (γ, γ) = (p + 1) (β, β),

where p = chainBotCoeff α β and q = chainTopCoeff α β.