Cartan matrices for root systems

This file contains definitions and basic results about Cartan matrices of root pairings / systems.

Main definitions:

• RootPairing.Base.cartanMatrix: the Cartan matrix of a crystallographic root pairing, with respect to a base b.

def RootPairing.Base.cartanMatrixIn {ι : 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] (S : Type u_5) [CommRing S] [Algebra S R] {P : RootPairing ι R M N} [P.IsValuedIn S] (b : P.Base) : Matrix (↑b.support) (↑b.support) S

The Cartan matrix of a root pairing, taking values in S, with respect to a base b.

See also RootPairing.Base.cartanMatrix.

Equations

• RootPairing.Base.cartanMatrixIn S b = Matrix.of fun (i j : ↑b.support) => P.pairingIn S ↑i ↑j

theorem RootPairing.Base.cartanMatrixIn_def {ι : 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] (S : Type u_5) [CommRing S] [Algebra S R] {P : RootPairing ι R M N} [P.IsValuedIn S] (b : P.Base) (i j : ↑b.support) : cartanMatrixIn S b i j = P.pairingIn S ↑i ↑j

@[simp]

theorem RootPairing.Base.cartanMatrixIn_apply_same {ι : 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] (S : Type u_5) [CommRing S] [Algebra S R] {P : RootPairing ι R M N} [P.IsValuedIn S] (b : P.Base) [FaithfulSMul S R] (i : ↑b.support) : cartanMatrixIn S b i i = 2

@[reducible, inline]

abbrev RootPairing.Base.cartanMatrix {ι : 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} (b : P.Base) [P.IsCrystallographic] : Matrix ↑b.support ↑b.support ℤ

The Cartan matrix of a crystallographic root pairing, with respect to a base b.

Equations

• b.cartanMatrix = RootPairing.Base.cartanMatrixIn ℤ b

theorem RootPairing.Base.cartanMatrix_apply_same {ι : 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} (b : P.Base) [P.IsCrystallographic] [CharZero R] (i : ↑b.support) : b.cartanMatrix i i = 2

theorem RootPairing.Base.cartanMatrix_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} (b : P.Base) [P.IsCrystallographic] [CharZero R] [Finite ι] [NoZeroDivisors R] [NoZeroSMulDivisors R M] [NoZeroSMulDivisors R N] (i j : ↑b.support) (h : i ≠ j) : b.cartanMatrix i j ≤ 0