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.
• RootPairing.Base.cartanMatrix_nondegenerate: the Cartan matrix is non-degenerate.

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.algebraMap_cartanMatrixIn_apply {ι : 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) : (algebraMap S R) (cartanMatrixIn S b i j) = P.pairing ↑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

theorem RootPairing.Base.cartanMatrixIn_mul_diagonal_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] (S : Type u_5) [CommRing S] [Algebra S R] {P : RootSystem ι R M N} [P.IsValuedIn S] (B : P.InvariantForm) (b : P.Base) [DecidableEq ι] [Fintype ↑b.support] : ((cartanMatrixIn S b).map ⇑(algebraMap S R) * Matrix.diagonal fun (i : ↑b.support) => (B.form (P.root ↑i)) (P.root ↑i)) = 2 • (BilinForm.toMatrix b.toWeightBasis) B.form

theorem RootPairing.Base.cartanMatrixIn_nondegenerate {ι : 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] [IsDomain R] [NeZero 2] [FaithfulSMul S R] [IsDomain S] {P : RootSystem ι R M N} [P.IsValuedIn S] [Fintype ι] [P.IsAnisotropic] (b : P.Base) : (cartanMatrixIn S b).Nondegenerate

@[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 ι] [IsDomain R] (i j : ↑b.support) (h : i ≠ j) : b.cartanMatrix i j ≤ 0

theorem RootPairing.Base.cartanMatrix_mem_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 ι] [IsDomain R] {i j : ↑b.support} (hij : i ≠ j) : b.cartanMatrix i j ∈ {-3, -2, -1, 0}

theorem RootPairing.Base.cartanMatrix_nondegenerate {ι : 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] [CharZero R] [Finite ι] [IsDomain R] {P : RootSystem ι R M N} [P.IsCrystallographic] (b : P.Base) : b.cartanMatrix.Nondegenerate