Reduced root pairings

This file contains basic definitions and results related to reduced root pairings.

Main definitions:

• RootPairing.IsReduced: A root pairing is said to be reduced if two linearly dependent roots are always related by a sign.
• RootPairing.linInd_iff_coxeterWeight_ne_four: for a finite root pairing, two roots are linearly independent iff their Coxeter weight is not four.

def RootPairing.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) : Prop

A root pairing is said to be reduced if any linearly dependent pair of roots is related by a sign.

Equations

• P.IsReduced = ∀ (i j : ι), ¬LinearIndependent R ![P.root i, P.root j] → P.root i = P.root j ∨ P.root i = -P.root j

theorem RootPairing.isReduced_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) : P.IsReduced ↔ ∀ (i j : ι), i ≠ j → ¬LinearIndependent R ![P.root i, P.root j] → P.root i = -P.root j

theorem RootPairing.infinite_of_linInd_coxeterWeight_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) {i j : ι} [NeZero 2] [NoZeroSMulDivisors ℤ M] (hl : LinearIndependent R ![P.root i, P.root j]) (hc : P.coxeterWeight i j = 4) : Infinite ι

theorem RootPairing.pairing_smul_root_eq_of_not_linInd {ι : 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) {i j : ι} [NeZero 2] [NoZeroSMulDivisors R M] (h : ¬LinearIndependent R ![P.root i, P.root j]) : P.pairing j i • P.root i = 2 • P.root j

theorem RootPairing.coxeterWeight_ne_four_of_linearIndependent {ι : 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) {i j : ι} [Finite ι] [NeZero 2] [NoZeroSMulDivisors ℤ M] (hl : LinearIndependent R ![P.root i, P.root j]) : P.coxeterWeight i j ≠ 4

theorem RootPairing.linearIndependent_iff_coxeterWeight_ne_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) {i j : ι} [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] : LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeight i j ≠ 4

theorem RootPairing.coxeterWeight_eq_four_iff_not_linearIndependent {ι : 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) {i j : ι} [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] : P.coxeterWeight i j = 4 ↔ ¬LinearIndependent R ![P.root i, P.root j]

@[simp]

theorem RootPairing.pairing_two_two_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) (i j : ι) [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] : P.pairing i j = 2 ∧ P.pairing j i = 2 ↔ i = j

@[simp]

theorem RootPairing.pairing_neg_two_neg_two_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) (i j : ι) [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] : P.pairing i j = -2 ∧ P.pairing j i = -2 ↔ P.root i = -P.root j

theorem RootPairing.pairing_one_four_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) (i j : ι) [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] (h2 : IsSMulRegular R 2) : P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = 2 • P.root i

theorem RootPairing.pairing_neg_one_neg_four_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) (i j : ι) [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] (h2 : IsSMulRegular R 2) : P.pairing i j = -1 ∧ P.pairing j i = -4 ↔ P.root j = -2 • P.root i

@[simp]

theorem RootPairing.pairing_one_four_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) (i j : ι) [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] [NoZeroDivisors R] : P.pairing i j = 1 ∧ P.pairing j i = 4 ↔ P.root j = 2 • P.root i

@[simp]

theorem RootPairing.pairing_neg_one_neg_four_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) (i j : ι) [Finite ι] [CharZero R] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] [NoZeroDivisors R] : P.pairing i j = -1 ∧ P.pairing j i = -4 ↔ P.root j = -2 • P.root i