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.
• RootPairing.Base.induction_on_cartanMatrix: an induction principle expressing the connectedness of the Dynkin diagram of an irreducible root pairing.

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 { x : ι // x ∈ b.support } { x : ι // x ∈ 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.

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 : { x : ι // x ∈ 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 : { x : ι // x ∈ 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 : { x : ι // x ∈ 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 ι] : ((cartanMatrixIn S b).map ⇑(algebraMap S R) * Matrix.diagonal fun (i : { x : ι // x ∈ 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 { x : ι // x ∈ b.support } { x : ι // x ∈ b.support } ℤ

The Cartan matrix of a crystallographic root pairing, with respect to a base 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 : { x : ι // x ∈ b.support }) : b.cartanMatrix i i = 2

theorem RootPairing.Base.cartanMatrix_apply_eq_zero_iff_pairing {ι : 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 j : { x : ι // x ∈ b.support }} : b.cartanMatrix i j = 0 ↔ P.pairing ↑i ↑j = 0

theorem RootPairing.Base.cartanMatrix_apply_eq_zero_iff_symm {ι : 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] [IsDomain R] {i j : { x : ι // x ∈ b.support }} : b.cartanMatrix i j = 0 ↔ b.cartanMatrix j i = 0

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

theorem RootPairing.Base.cartanMatrix_eq_neg_chainTopCoeff {ι : 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] [IsDomain R] [Finite ι] {i j : { x : ι // x ∈ b.support }} (hij : i ≠ j) : b.cartanMatrix i j = -↑(chainTopCoeff ↑j ↑i)

theorem RootPairing.Base.cartanMatrix_apply_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} (b : P.Base) [P.IsCrystallographic] [CharZero R] [IsDomain R] [Finite ι] {i j : { x : ι // x ∈ b.support }} (hij : i ≠ j) : b.cartanMatrix i j = 0 ↔ P.root ↑i + P.root ↑j ∉ Set.range ⇑P.root

theorem RootPairing.Base.abs_cartanMatrix_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] {P : RootPairing ι R M N} (b : P.Base) [P.IsCrystallographic] [CharZero R] [IsDomain R] [Finite ι] [DecidableEq ι] {i j : { x : ι // x ∈ b.support }} : |b.cartanMatrix i j| = (if i = j then 4 else 0) - b.cartanMatrix i j

@[simp]

theorem RootPairing.Base.cartanMatrix_map_abs {ι : 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] [IsDomain R] [Finite ι] [DecidableEq ι] : b.cartanMatrix.map abs = 4 - b.cartanMatrix

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

theorem RootPairing.Base.induction_on_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] [CharZero R] [IsDomain R] [Finite ι] [P.IsReduced] [P.IsIrreducible] (p : { x : ι // x ∈ b.support } → Prop) {i j : { x : ι // x ∈ b.support }} (hi : p i) (hp : ∀ (i j : { x : ι // x ∈ b.support }), p i → b.cartanMatrix j i ≠ 0 → p j) : p j

A characterisation of the connectedness of the Dynkin diagram for irreducible root pairings.

theorem RootPairing.Base.injective_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] [CharZero R] [IsDomain R] [Finite ι] {P : RootSystem ι R M N} [P.IsCrystallographic] (b : P.Base) : Function.Injective fun (i : ι) (k : { x : ι // x ∈ b.support }) => P.pairingIn ℤ i ↑k