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 numberpin the chainβ - q • α, ..., β - α, β, β + α, ..., β + p • αRootPairing.chainTopCoeff: the natural numberqin 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_linearIndependent
{ι : 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])
:
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
Instances For
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
Instances For
theorem
RootPairing.chainTopCoeff_of_not_linearIndependent
{ι : 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])
:
theorem
RootPairing.chainBotCoeff_of_not_linearIndependent
{ι : 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])
:
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 : ℕ}
:
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 : ℕ}
:
theorem
RootPairing.one_le_chainTopCoeff_of_root_add_mem
{ι : 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]
(h : P.root i + P.root j ∈ Set.range ⇑P.root)
:
theorem
RootPairing.one_le_chainBotCoeff_of_root_add_mem
{ι : 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]
(h : P.root i - P.root j ∈ Set.range ⇑P.root)
:
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 : ℤ}
:
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 : ℤ}
:
@[simp]
theorem
RootPairing.chainTopCoeff_reflection_perm_left
{ι : 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 : ι}
:
@[simp]
theorem
RootPairing.chainBotCoeff_reflection_perm_left
{ι : 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 : ι}
:
@[simp]
theorem
RootPairing.chainTopCoeff_reflection_perm_right
{ι : 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 : ι}
:
@[simp]
theorem
RootPairing.chainBotCoeff_reflection_perm_right
{ι : 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 : ι}
:
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
Instances For
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
Instances For
@[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 : ι}
:
@[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 : ι}
:
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])
:
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])
:
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 : ι}
:
@[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 : ι}
:
theorem
RootPairing.chainBotCoeff_add_chainTopCoeff_eq_pairingIn_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 : ι}
(h : LinearIndependent R ![P.root i, P.root j])
:
theorem
RootPairing.chainBotCoeff_add_chainTopCoeff_le_three
{ι : 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]
:
theorem
RootPairing.chainBotCoeff_add_chainTopCoeff_le_two
{ι : 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.IsNotG2]
:
theorem
RootPairing.pairingIn_le_zero_of_root_add_mem
{ι : 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.IsNotG2]
(h : P.root i + P.root j ∈ Set.range ⇑P.root)
:
For a reduced, crystallographic, irreducible root pairing other than 𝔤₂, if the sum of two
roots is a root, they cannot make an acute angle.
To see that this lemma fails for 𝔤₂, let α (short) and β (long) be a base. Then the roots
α + β and 2α + β make an angle π / 3 even though 3α + 2β is a root. We can even witness as:
example (P : RootPairing ι R M N) [P.EmbeddedG2] :
P.pairingIn ℤ (EmbeddedG2.shortAddLong P) (EmbeddedG2.twoShortAddLong P) = 1 := by
simp
theorem
RootPairing.zero_le_pairingIn_of_root_sub_mem
{ι : 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.IsNotG2]
(h : P.root i - P.root j ∈ Set.range ⇑P.root)
:
theorem
RootPairing.chainBotCoeff_if_one_zero
{ι : 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.IsNotG2]
(h : P.root i + P.root j ∈ Set.range ⇑P.root)
:
For a reduced, crystallographic, irreducible root pairing other than 𝔤₂, if the sum of two
roots is a root, the bottom chain coefficient is either one or zero according to whether they are
perpendicular.
To see that this lemma fails for 𝔤₂, let α (short) and β (long) be a base. Then the roots
α and α + β provide a counterexample.
theorem
RootPairing.chainTopCoeff_if_one_zero
{ι : 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.IsNotG2]
(h : P.root i - P.root j ∈ Set.range ⇑P.root)
:
The proof of lemma 2.6 from Geck.
theorem
RootPairing.chainBotCoeff_mul_chainTopCoeff.aux_0
{ι : 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 k : ι}
[P.IsNotG2]
(hik_mem : P.root k + P.root i ∈ Set.range ⇑P.root)
:
theorem
RootPairing.chainBotCoeff_mul_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]
{b : P.Base}
{i j k l m : ι}
(hi : i ∈ b.support)
(hj : j ∈ b.support)
(hij : i ≠ j)
(h₁ : P.root k + P.root i = P.root l)
(h₂ : P.root k - P.root j = P.root m)
(h₃ : P.root k + P.root i - P.root j ∈ Set.range ⇑P.root)
[P.IsNotG2]
:
(chainBotCoeff i m + 1) * (chainTopCoeff j k + 1) = (chainTopCoeff j l + 1) * (chainBotCoeff i k + 1)
This is Lemma 2.6 from Geck.