Chains of roots

Given roots α and β, the α-chain through β is the set of roots of the form α + z • β for an integer z. This is known as a "root chain" and also a "root string". For linearly independent roots in finite crystallographic root pairings, these chains are always unbroken, i.e., of the form: β - q • α, ..., β - α, β, β + α, ..., β + p • α for natural numbers p, q, and the length, p + q is at most 3.

Main definitions / results:

• RootPairing.chainTopCoeff: the natural number p in the chain β - q • α, ..., β - α, β, β + α, ..., β + p • α
• RootPairing.chainTopCoeff: the natural number q in the chain β - q • α, ..., β - α, β, β + α, ..., β + p • α
• RootPairing.root_add_zsmul_mem_range_iff: every chain is an interval (aka unbroken).
• RootPairing.chainBotCoeff_add_chainTopCoeff_le: every chain has length at most three.

theorem RootPairing.setOf_root_add_zsmul_eq_Icc_of_linInd {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} (h : LinearIndependent R ![P.root i, P.root j]) : ∃ q ≤ 0, ∃ p ≥ 0, {z : ℤ | P.root j + z • P.root i ∈ Set.range ⇑P.root} = Set.Icc q p

Note that it is often more convenient to use RootPairing.root_add_zsmul_mem_range_iff than to invoke this lemma directly.

def RootPairing.chainTopCoeff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] (i j : ι) : ℕ

If α = P.root i and β = P.root j are linearly independent, this is the value p ≥ 0 where β - q • α, ..., β - α, β, β + α, ..., β + p • α is the α-chain through β.

In the absence of linear independence, it takes a junk value.

Equations

• RootPairing.chainTopCoeff i j = if h : LinearIndependent R ![P.root i, P.root j] then ⋯.choose.toNat else 0

def RootPairing.chainBotCoeff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] (i j : ι) : ℕ

If α = P.root i and β = P.root j are linearly independent, this is the value q ≥ 0 where β - q • α, ..., β - α, β, β + α, ..., β + p • α is the α-chain through β.

In the absence of linear independence, it takes a junk value.

Equations

• RootPairing.chainBotCoeff i j = if h : LinearIndependent R ![P.root i, P.root j] then (-⋯.choose).toNat else 0

theorem RootPairing.chainTopCoeff_of_not_linInd {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} (h : ¬LinearIndependent R ![P.root i, P.root j]) : chainTopCoeff i j = 0

theorem RootPairing.chainBotCoeff_of_not_linInd {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} (h : ¬LinearIndependent R ![P.root i, P.root j]) : chainBotCoeff i j = 0

theorem RootPairing.root_add_nsmul_mem_range_iff_le_chainTopCoeff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} (h : LinearIndependent R ![P.root i, P.root j]) {n : ℕ} : P.root j + n • P.root i ∈ Set.range ⇑P.root ↔ n ≤ chainTopCoeff i j

theorem RootPairing.root_sub_nsmul_mem_range_iff_le_chainBotCoeff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} (h : LinearIndependent R ![P.root i, P.root j]) {n : ℕ} : P.root j - n • P.root i ∈ Set.range ⇑P.root ↔ n ≤ chainBotCoeff i j

theorem RootPairing.root_add_zsmul_mem_range_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} (h : LinearIndependent R ![P.root i, P.root j]) {z : ℤ} : P.root j + z • P.root i ∈ Set.range ⇑P.root ↔ z ∈ Set.Icc (-↑(chainBotCoeff i j)) ↑(chainTopCoeff i j)

theorem RootPairing.root_sub_zsmul_mem_range_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} (h : LinearIndependent R ![P.root i, P.root j]) {z : ℤ} : P.root j - z • P.root i ∈ Set.range ⇑P.root ↔ z ∈ Set.Icc (-↑(chainTopCoeff i j)) ↑(chainBotCoeff i j)

@[simp]

theorem RootPairing.chainTopCoeff_relfection_perm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} : chainTopCoeff ((P.reflection_perm i) i) j = chainBotCoeff i j

@[simp]

theorem RootPairing.chainBotCoeff_relfection_perm {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} : chainBotCoeff ((P.reflection_perm i) i) j = chainTopCoeff i j

def RootPairing.chainTopIdx {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] (i j : ι) : ι

If α = P.root i and β = P.root j are linearly independent, this is the index of the root β + p • α where β - q • α, ..., β - α, β, β + α, ..., β + p • α is the α-chain through β.

In the absence of linear independence, it takes a junk value.

Equations

• RootPairing.chainTopIdx i j = if h : LinearIndependent R ![P.root i, P.root j] then Exists.choose ⋯ else j

def RootPairing.chainBotIdx {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] (i j : ι) : ι

If α = P.root i and β = P.root j are linearly independent, this is the index of the root β - q • α where β - q • α, ..., β - α, β, β + α, ..., β + p • α is the α-chain through β.

In the absence of linear independence, it takes a junk value.

Equations

• RootPairing.chainBotIdx i j = if h : LinearIndependent R ![P.root i, P.root j] then Exists.choose ⋯ else j

@[simp]

theorem RootPairing.root_chainTopIdx {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} : P.root (chainTopIdx i j) = P.root j + chainTopCoeff i j • P.root i

@[simp]

theorem RootPairing.root_chainBotIdx {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} : P.root (chainBotIdx i j) = P.root j - chainBotCoeff i j • P.root i

theorem RootPairing.chainBotCoeff_sub_chainTopCoeff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} (h : LinearIndependent R ![P.root i, P.root j]) : ↑(chainBotCoeff i j) - ↑(chainTopCoeff i j) = P.pairingIn ℤ j i

theorem RootPairing.chainTopCoeff_sub_chainBotCoeff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} (h : LinearIndependent R ![P.root i, P.root j]) : ↑(chainTopCoeff i j) - ↑(chainBotCoeff i j) = -P.pairingIn ℤ j i

theorem RootPairing.chainCoeff_chainTopIdx_aux {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} : chainBotCoeff i (chainTopIdx i j) = chainBotCoeff i j + chainTopCoeff i j ∧ chainTopCoeff i (chainTopIdx i j) = 0

@[simp]

theorem RootPairing.chainBotCoeff_chainTopIdx {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} : chainBotCoeff i (chainTopIdx i j) = chainBotCoeff i j + chainTopCoeff i j

@[simp]

theorem RootPairing.chainTopCoeff_chainTopIdx {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} : chainTopCoeff i (chainTopIdx i j) = 0

theorem RootPairing.chainBotCoeff_add_chainTopCoeff_le {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [CharZero R] [IsDomain R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [P.IsCrystallographic] {i j : ι} [P.IsReduced] : chainBotCoeff i j + chainTopCoeff i j ≤ 3