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.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.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.