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) [CommRing S] [LinearOrder S] [IsStrictOrderedRing 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 : ι) [IsDomain 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_isCrystal_of_isRed {ι : 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 : ι) [IsDomain R] [P.IsReduced] : (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.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' {ι : 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 : ι) [IsDomain R] [P.IsReduced] (hij : P.root i ≠ P.root j) (hij' : P.root i ≠ -P.root j) : (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)}

theorem RootPairing.RootPositiveForm.rootLength_le_of_pairingIn_eq {ι : 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] [IsDomain R] (B : RootPositiveForm ℤ P) {i j : ι} (hij : P.pairingIn ℤ i j = -1 ∨ P.pairingIn ℤ i j = 1) : B.rootLength i ≤ B.rootLength j

theorem RootPairing.RootPositiveForm.rootLength_lt_of_pairingIn_notMem {ι : 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] [IsDomain R] (B : RootPositiveForm ℤ P) {i j : ι} (hne : P.root i ≠ P.root j) (hne' : P.root i ≠ -P.root j) (hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}) : B.rootLength j < B.rootLength i

theorem RootPairing.pairingIn_pairingIn_mem_set_of_length_eq {ι : 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 : ι} [IsDomain R] {B : P.InvariantForm} (len_eq : (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)) : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(0, 0), (1, 1), (-1, -1), (2, 2), (-2, -2)}

theorem RootPairing.pairingIn_pairingIn_mem_set_of_length_eq_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] {i j : ι} [IsDomain R] {B : P.InvariantForm} (len_eq : (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j)) (ne : i ≠ j) (ne' : P.root i ≠ -P.root j) : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(0, 0), (1, 1), (-1, -1)}

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) [CharZero R] [P.IsCrystallographic] (i j : ι) [IsDomain 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 : ι} [IsDomain R] (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 : ι} [IsDomain R] (h : P.pairingIn ℤ i j < 0) (h' : P.root i ≠ -P.root j) : P.root i + P.root j ∈ Set.range ⇑P.root

If two roots make an obtuse angle then their sum is a root (provided it is not zero).

See RootPairing.pairingIn_le_zero_of_root_add_mem for a partial converse.

theorem RootPairing.pairingIn_eq_zero_of_add_notMem_of_sub_notMem {ι : 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 : ι} [IsDomain R] (hp : i ≠ j) (hn : P.root i ≠ -P.root j) (h_add : P.root i + P.root j ∉ Set.range ⇑P.root) (h_sub : P.root i - P.root j ∉ Set.range ⇑P.root) : P.pairingIn ℤ i j = 0

theorem RootPairing.pairing_eq_zero_of_add_notMem_of_sub_notMem {ι : 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 : ι} [IsDomain R] (hp : i ≠ j) (hn : P.root i ≠ -P.root j) (h_add : P.root i + P.root j ∉ Set.range ⇑P.root) (h_sub : P.root i - P.root j ∉ Set.range ⇑P.root) : P.pairing i j = 0

theorem RootPairing.exists_coroot_sub_coroot_eq_zsmul {ι : 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 : ι} [IsDomain R] {k : ι} (hk : P.root k = P.root j - P.root i) (hij : P.pairingIn ℤ i j ≤ 0) : ∃ (n : ℤ), 2 ≤ n ∧ P.coroot j - P.coroot i = n • P.coroot k

theorem RootPairing.root_sub_root_notMem_range' {ι : 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 : ι} [IsDomain R] (f : Module.Dual ℤ ↥(P.corootSpan ℤ)) (hf : f (P.corootSpanMem ℤ j) - f (P.corootSpanMem ℤ i) = 1) (hij : P.pairingIn ℤ i j ≤ 0) : P.root j - P.root i ∉ Set.range ⇑P.root

theorem RootPairing.root_sub_root_notMem_range {ι : 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] [IsDomain R] {s : Finset ι} (h₀ : LinearIndepOn ℤ ⇑P.coroot ↑s) (h₃ : ∀ (k : ι), P.coroot k ∈ Submodule.span ℤ (⇑P.coroot '' ↑s)) {i j : ↥s} (hij : P.pairingIn ℤ ↑i ↑j ≤ 0) : P.root ↑j - P.root ↑i ∉ Set.range ⇑P.root

theorem RootPairing.exists_pos_pairingIn {ι : 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 : ι} [IsDomain R] {s : Finset ι} (h₀ : LinearIndepOn ℤ ⇑P.root ↑s) (h₁ : (↑s).Pairwise fun (i j : ι) => P.pairingIn ℤ i j ≤ 0) {c : ↥s → ℤ} (hc : ∑ k : ↥s, c k • P.root ↑k = P.root i) (hc₀ : ¬c ≤ 0) : ∃ (j : ↥s), 0 < c j ∧ 0 < P.pairingIn ℤ i ↑j

theorem RootPairing.root_mem_submodule_iff_of_add_mem_invtSubmodule {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] {i j : ι} {K : Type u_5} [Field K] [NeZero 2] [Module K M] [Module K N] {P : RootPairing ι K M N} (q : ↥P.invtRootSubmodule) (hij : P.root i + P.root j ∈ Set.range ⇑P.root) : P.root i ∈ ↑q ↔ P.root j ∈ ↑q

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] [IsDomain R] [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] [IsDomain R] [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 {ι : 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] [IsDomain R] [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 : ι} [IsDomain R] [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.forall_pairing_eq_swap_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] [IsDomain R] [P.IsReduced] [P.IsIrreducible] : (∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 2 * P.pairing j i ∨ P.pairing j i = 2 * P.pairing i j) ∨ ∀ (i j : ι), P.pairing i j = P.pairing j i ∨ P.pairing i j = 3 * P.pairing j i ∨ P.pairing j i = 3 * P.pairing i j

theorem RootPairing.forall_pairingIn_eq_swap_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] [IsDomain R] [P.IsReduced] [P.IsIrreducible] : (∀ (i j : ι), P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨ P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j) ∨ ∀ (i j : ι), P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨ P.pairingIn ℤ i j = 3 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 3 * P.pairingIn ℤ i j