Structural lemmas about finite crystallographic root pairings

In this file we gather basic lemmas necessary for the classification of finite crystallographic root pairings.

Main results:

• RootPairing.coxeterWeightIn_mem_set_of_isCrystallographic: the Coxeter weights of a finite crystallographic root pairing belong to the set {0, 1, 2, 3, 4}.
• RootPairing.root_sub_root_mem_of_pairingIn_pos: if α ≠ β are both roots of a finite crystallographic root pairing, and the pairing of α with β is positive, then α - β is also a root.
• RootPairing.root_add_root_mem_of_pairingIn_neg: if α ≠ -β are both roots of a finite crystallographic root pairing, and the pairing of α with β is negative, then α + β is also a root.

theorem RootPairing.coxeterWeightIn_le_four {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] (S : Type u_5) [LinearOrderedCommRing S] [Algebra S R] [FaithfulSMul S R] [Module S M] [IsScalarTower S R M] [P.IsValuedIn S] (i j : ι) : P.coxeterWeightIn S i j ≤ 4

SGA3 XXI Prop. 2.3.1

theorem RootPairing.coxeterWeightIn_mem_set_of_isCrystallographic {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [P.IsCrystallographic] (i j : ι) : P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}

theorem RootPairing.pairingIn_pairingIn_mem_set_of_isCrystallographic {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [P.IsCrystallographic] (i j : ι) [NoZeroDivisors R] : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4), (-4, -1), (-1, -4), (2, 2), (-2, -2)}

theorem RootPairing.pairingIn_pairingIn_mem_set_of_isCrystallographic_of_isReduced {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [P.IsCrystallographic] (i j : ι) [NoZeroDivisors R] [P.IsReduced] [NoZeroSMulDivisors R M] : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (2, 2), (-2, -2)}

theorem RootPairing.coxeterWeightIn_eq_zero_iff {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [P.IsCrystallographic] (i j : ι) [NoZeroDivisors R] : P.coxeterWeightIn ℤ i j = 0 ↔ P.pairingIn ℤ i j = 0

theorem RootPairing.root_sub_root_mem_of_pairingIn_pos {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [P.IsCrystallographic] {i j : ι} [NoZeroDivisors R] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] (h : 0 < P.pairingIn ℤ i j) (h' : i ≠ j) : P.root i - P.root j ∈ Set.range ⇑P.root

theorem RootPairing.root_add_root_mem_of_pairingIn_neg {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (P : RootPairing ι R M N) [Finite ι] [CharZero R] [P.IsCrystallographic] {i j : ι} [NoZeroDivisors R] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] (h : P.pairingIn ℤ i j < 0) (h' : P.root i ≠ -P.root j) : P.root i + P.root j ∈ Set.range ⇑P.root

theorem RootPairing.InvariantForm.apply_eq_or_aux {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [P.IsCrystallographic] [NoZeroDivisors R] [NoZeroSMulDivisors R M] [P.IsReduced] (B : P.InvariantForm) (i j : ι) (h : P.pairingIn ℤ i j ≠ 0) : (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j) ∨ (B.form (P.root i)) (P.root i) = 2 * (B.form (P.root j)) (P.root j) ∨ (B.form (P.root i)) (P.root i) = 3 * (B.form (P.root j)) (P.root j) ∨ (B.form (P.root j)) (P.root j) = 2 * (B.form (P.root i)) (P.root i) ∨ (B.form (P.root j)) (P.root j) = 3 * (B.form (P.root i)) (P.root i)

theorem RootPairing.InvariantForm.apply_eq_or {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [P.IsCrystallographic] [NoZeroDivisors R] [NoZeroSMulDivisors R M] [P.IsReduced] (B : P.InvariantForm) [P.IsIrreducible] (i j : ι) : (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j) ∨ (B.form (P.root i)) (P.root i) = 2 * (B.form (P.root j)) (P.root j) ∨ (B.form (P.root i)) (P.root i) = 3 * (B.form (P.root j)) (P.root j) ∨ (B.form (P.root j)) (P.root j) = 2 * (B.form (P.root i)) (P.root i) ∨ (B.form (P.root j)) (P.root j) = 3 * (B.form (P.root i)) (P.root i)

Relative of lengths of roots in a reduced irreducible finite crystallographic root pairing are very constrained.

theorem RootPairing.InvariantForm.exists_apply_eq_or_aux {R : Type u_2} [CommRing R] [CharZero R] [NoZeroDivisors R] {x y z : R} (hij : x = 2 * y ∨ x = 3 * y ∨ y = 2 * x ∨ y = 3 * x) (hik : x = 2 * z ∨ x = 3 * z ∨ z = 2 * x ∨ z = 3 * x) (hjk : y = 2 * z ∨ y = 3 * z ∨ z = 2 * y ∨ z = 3 * y) : x = 0 ∧ y = 0 ∧ z = 0

theorem RootPairing.InvariantForm.exists_apply_eq_or {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [P.IsCrystallographic] [NoZeroDivisors R] [NoZeroSMulDivisors R M] [P.IsReduced] (B : P.InvariantForm) [P.IsIrreducible] [Nonempty ι] : ∃ (i : ι) (j : ι), ∀ (k : ι), (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨ (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

A reduced irreducible finite crystallographic root system has roots of at most two different lengths.

theorem RootPairing.InvariantForm.apply_eq_or_of_apply_ne {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [P.IsCrystallographic] {i j : ι} [NoZeroDivisors R] [NoZeroSMulDivisors R M] [P.IsReduced] (B : P.InvariantForm) [P.IsIrreducible] (h : (B.form (P.root i)) (P.root i) ≠ (B.form (P.root j)) (P.root j)) (k : ι) : (B.form (P.root k)) (P.root k) = (B.form (P.root i)) (P.root i) ∨ (B.form (P.root k)) (P.root k) = (B.form (P.root j)) (P.root j)

theorem RootPairing.Base.pairingIn_le_zero_of_ne {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [P.IsCrystallographic] [NoZeroDivisors R] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] (b : P.Base) {i j : ι} (hij : i ≠ j) (hi : i ∈ b.support) (hj : j ∈ b.support) : P.pairingIn ℤ i j ≤ 0

theorem RootPairing.Base.root_sub_root_mem_of_mem_of_mem {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [P.IsCrystallographic] [NoZeroDivisors R] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] (b : P.Base) (i j k : ι) (hij : i ≠ j) (hi : i ∈ b.support) (hj : j ∈ b.support) (hk : P.root k + P.root i - P.root j ∈ Set.range ⇑P.root) (hkj : k ≠ j) (hk' : P.root k + P.root i ∈ Set.range ⇑P.root) : P.root k - P.root j ∈ Set.range ⇑P.root

This is Lemma 2.5 (a) from Geck.

theorem RootPairing.Base.root_add_root_mem_of_mem_of_mem {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootPairing ι R M N} [Finite ι] [CharZero R] [P.IsCrystallographic] [NoZeroDivisors R] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] (b : P.Base) (i j k : ι) (hij : i ≠ j) (hi : i ∈ b.support) (hj : j ∈ b.support) (hk : P.root k + P.root i - P.root j ∈ Set.range ⇑P.root) (hkj : P.root k ≠ -P.root i) (hk' : P.root k - P.root j ∈ Set.range ⇑P.root) : P.root k + P.root i ∈ Set.range ⇑P.root

This is Lemma 2.5 (b) from Geck.