The diagonal Cartan subalgebra of the split orthogonal Lie algebra of type B

Mathlib's LieAlgebra.Orthogonal.typeB ι K is the Lie algebra of matrices skew-adjoint for the split symmetric form with matrix

[ 2  0  0 ]
[ 0  0  1 ]
[ 0  1  0 ].

Its standard Cartan subalgebra consists of the matrices diag(0, d, -d). This file bundles that subalgebra, proves that it is abelian and self-normalizing, and gives its coordinate basis and dual coordinates. The regularity of 2 is needed only for self-normalization: it distinguishes the two opposite coordinate weights.

Main definitions

• TauCeti.typeBDiagonalCartan: the diagonal Cartan subalgebra of LieAlgebra.Orthogonal.typeB ι K.
• TauCeti.typeBDiagonalEquiv: the coordinate equivalence (ι → K) ≃ₗ[K] typeBDiagonalCartan K ι.
• TauCeti.typeBDiagonalCartanBasis: its basis by the matrices with diagonal entries 1 and -1 in paired positions.
• TauCeti.typeBWeightEquiv: the corresponding coordinate equivalence with the dual Cartan.
• TauCeti.typeBEpsilon: the coordinate functional εᵢ.

Main results

• TauCeti.typeBDiagonalCartan_normalizer_eq_self: the diagonal Cartan is self-normalizing.
• TauCeti.instIsCartanSubalgebraTypeBDiagonalCartan: it is a Cartan subalgebra.
• TauCeti.finrank_typeBDiagonalCartan: its dimension is Fintype.card ι.

References

The construction follows Fulton--Harris, Representation Theory, Lecture 20. Its declaration order and coordinate API follow TauCeti.Algebra.Lie.GeneralLinear.DiagonalCartan and the type-D analogue in TauCeti#4356. This is the split type-B Cartan prerequisite for Layer 5 of the Spin-representations roadmap.

The diagonal matrices of type B

def TauCeti.typeBDiagonalValue {K : Type u} [CommRing K] {ι : Type u_1} (d : ι → K) : Unit ⊕ ι ⊕ ι → K

The weight of a coordinate in the standard type-B module: zero on the middle coordinate, d i on the first copy of ι, and -d i on the second.

Equations

• TauCeti.typeBDiagonalValue d = Sum.elim 0 (Sum.elim d (-d))

@[simp]

theorem TauCeti.typeBDiagonalValue_inl {K : Type u} [CommRing K] {ι : Type u_1} (d : ι → K) (i : Unit) : typeBDiagonalValue d (Sum.inl i) = 0

@[simp]

theorem TauCeti.typeBDiagonalValue_inr_inl {K : Type u} [CommRing K] {ι : Type u_1} (d : ι → K) (i : ι) : typeBDiagonalValue d (Sum.inr (Sum.inl i)) = d i

@[simp]

theorem TauCeti.typeBDiagonalValue_inr_inr {K : Type u} [CommRing K] {ι : Type u_1} (d : ι → K) (i : ι) : typeBDiagonalValue d (Sum.inr (Sum.inr i)) = -d i

def TauCeti.typeBDiagonalMatrix {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] (d : ι → K) : Matrix (Unit ⊕ ι ⊕ ι) (Unit ⊕ ι ⊕ ι) K

The ambient matrix diag(0, d, -d) in the split type-B model.

Equations

• TauCeti.typeBDiagonalMatrix d = Matrix.diagonal (TauCeti.typeBDiagonalValue d)

@[simp]

theorem TauCeti.typeBDiagonalMatrix_apply {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] (d : ι → K) (i j : Unit ⊕ ι ⊕ ι) : typeBDiagonalMatrix d i j = if i = j then typeBDiagonalValue d i else 0

theorem TauCeti.typeBDiagonalMatrix_mem_diagonalCartan {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (d : ι → K) : typeBDiagonalMatrix d ∈ diagonalCartan K (Unit ⊕ ι ⊕ ι)

Every diag(0, d, -d) lies in the ambient diagonal Cartan subalgebra of matrices.

theorem TauCeti.typeBDiagonalMatrix_mem_typeB {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (d : ι → K) : typeBDiagonalMatrix d ∈ LieAlgebra.Orthogonal.typeB ι K

Every diag(0, d, -d) is skew-adjoint for the split type-B form.

The Cartan subalgebra and its coordinates

def TauCeti.typeBDiagonalCartan (K : Type u) [CommRing K] (ι : Type u_1) [DecidableEq ι] [Fintype ι] : LieSubalgebra K ↥(LieAlgebra.Orthogonal.typeB ι K)

The explicit diagonal matrices diag(0, d, -d) inside the split orthogonal Lie algebra of type B.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.mem_typeBDiagonalCartan_iff {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] {A : ↥(LieAlgebra.Orthogonal.typeB ι K)} : A ∈ typeBDiagonalCartan K ι ↔ ∃ (d : ι → K), ↑A = typeBDiagonalMatrix d

Membership in the type-B diagonal Cartan is an explicit diag(0, d, -d) presentation.

def TauCeti.typeBDiagonalEquiv {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] : (ι → K) ≃ₗ[K] ↥(typeBDiagonalCartan K ι)

The coordinate equivalence from ι-tuples to the type-B diagonal Cartan.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.coe_typeBDiagonalEquiv_apply {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (d : ι → K) : ↑(typeBDiagonalEquiv d) = ⟨typeBDiagonalMatrix d, ⋯⟩

@[simp]

theorem TauCeti.typeBDiagonalEquiv_symm_apply {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (A : ↥(typeBDiagonalCartan K ι)) (i : ι) : typeBDiagonalEquiv.symm A i = ↑↑A (Sum.inr (Sum.inl i)) (Sum.inr (Sum.inl i))

instance TauCeti.instIsLieAbelianSubtypeMatrixSumUnitMemLieSubalgebraTypeBTypeBDiagonalCartan {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] : IsLieAbelian ↥(typeBDiagonalCartan K ι)

Self-normalization

theorem TauCeti.lie_typeBDiagonalEquiv_apply {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (X : ↥(LieAlgebra.Orthogonal.typeB ι K)) (d : ι → K) (a b : Unit ⊕ ι ⊕ ι) : ↑⁅X, ↑(typeBDiagonalEquiv d)⁆ a b = (typeBDiagonalValue d b - typeBDiagonalValue d a) * ↑X a b

Bracketing with diag(0, d, -d) scales each matrix entry by the difference of its two coordinate weights.

theorem TauCeti.mem_typeBDiagonalCartan_iff_isDiag {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (h2 : IsRegular 2) {A : ↥(LieAlgebra.Orthogonal.typeB ι K)} : A ∈ typeBDiagonalCartan K ι ↔ (↑A).IsDiag

When multiplication by 2 is injective, membership in the type-B diagonal Cartan is equivalent to being diagonal as an ambient matrix. Skew-adjointness then forces the middle entry to vanish and the two remaining diagonal blocks to be opposite.

@[simp]

theorem TauCeti.typeBDiagonalCartan_normalizer_eq_self (K : Type u) [CommRing K] (ι : Type u_1) [DecidableEq ι] [Fintype ι] (h2 : IsRegular 2) : (typeBDiagonalCartan K ι).normalizer = typeBDiagonalCartan K ι

The diagonal Cartan of type B is self-normalizing when multiplication by 2 is injective.

instance TauCeti.instIsCartanSubalgebraTypeBDiagonalCartan (K : Type u) [CommRing K] (ι : Type u_1) [DecidableEq ι] [Fintype ι] [h2 : Fact (IsRegular 2)] : (typeBDiagonalCartan K ι).IsCartanSubalgebra

The diagonal matrices form a Cartan subalgebra of the split orthogonal Lie algebra of type B: they are abelian, hence nilpotent, and self-normalizing.

@[instance 100]

instance TauCeti.instIsCartanSubalgebraTypeBDiagonalCartanOfNoZeroDivisors (K : Type u) [CommRing K] (ι : Type u_1) [DecidableEq ι] [Fintype ι] [NoZeroDivisors K] [NeZero 2] : (typeBDiagonalCartan K ι).IsCartanSubalgebra

Over a domain, nonvanishing of 2 supplies the regularity needed by the type-B Cartan instance.

A basis and dual coordinates

noncomputable def TauCeti.typeBDiagonalCartanBasis {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] : Module.Basis ι K ↥(typeBDiagonalCartan K ι)

The coordinate basis of the type-B diagonal Cartan.

Equations

• TauCeti.typeBDiagonalCartanBasis = Module.Basis.ofEquivFun TauCeti.typeBDiagonalEquiv.symm

@[simp]

theorem TauCeti.coe_typeBDiagonalCartanBasis_apply {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) : ↑(typeBDiagonalCartanBasis i) = ⟨typeBDiagonalMatrix (Pi.single i 1), ⋯⟩

@[simp]

theorem TauCeti.typeBDiagonalCartanBasis_repr_apply {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (A : ↥(typeBDiagonalCartan K ι)) (i : ι) : (typeBDiagonalCartanBasis.repr A) i = ↑↑A (Sum.inr (Sum.inl i)) (Sum.inr (Sum.inl i))

instance TauCeti.instFreeSubtypeMatrixSumUnitMemLieSubalgebraTypeBTypeBDiagonalCartan {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] : Module.Free K ↥(typeBDiagonalCartan K ι)

instance TauCeti.instFiniteSubtypeMatrixSumUnitMemLieSubalgebraTypeBTypeBDiagonalCartan {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] : Module.Finite K ↥(typeBDiagonalCartan K ι)

theorem TauCeti.finrank_typeBDiagonalCartan {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] [StrongRankCondition K] : Module.finrank K ↥(typeBDiagonalCartan K ι) = Fintype.card ι

The type-B diagonal Cartan has dimension Fintype.card ι.

noncomputable def TauCeti.typeBWeightEquiv {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] : (ι → K) ≃ₗ[K] Module.Dual K ↥(typeBDiagonalCartan K ι)

Coordinates on the type-B Cartan are also coordinates on its dual.

Equations

• TauCeti.typeBWeightEquiv = TauCeti.typeBDiagonalEquiv.trans TauCeti.typeBDiagonalCartanBasis.toDualEquiv

@[simp]

theorem TauCeti.typeBWeightEquiv_apply {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (mu : ι → K) (A : ↥(typeBDiagonalCartan K ι)) : (typeBWeightEquiv mu) A = ∑ i : ι, mu i * ↑↑A (Sum.inr (Sum.inl i)) (Sum.inr (Sum.inl i))

@[simp]

theorem TauCeti.typeBWeightEquiv_symm_apply {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (f : Module.Dual K ↥(typeBDiagonalCartan K ι)) (i : ι) : typeBWeightEquiv.symm f i = f (typeBDiagonalCartanBasis i)

noncomputable def TauCeti.typeBEpsilon {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) : Module.Dual K ↥(typeBDiagonalCartan K ι)

The coordinate functional εᵢ on the type-B diagonal Cartan.

Equations

• TauCeti.typeBEpsilon i = TauCeti.typeBWeightEquiv (Pi.single i 1)

@[simp]

theorem TauCeti.typeBEpsilon_apply {K : Type u} [CommRing K] {ι : Type u_1} [DecidableEq ι] [Fintype ι] (i : ι) (A : ↥(typeBDiagonalCartan K ι)) : (typeBEpsilon i) A = ↑↑A (Sum.inr (Sum.inl i)) (Sum.inr (Sum.inl i))