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

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

[ 0  1 ]
[ 1  0 ].

Its standard Cartan subalgebra consists of the diagonal matrices diag(d, -d). This file bundles that subalgebra, proves that it is abelian and self-normalizing when 2 is regular, and gives its coordinate basis and dual coordinates. Over an algebraically closed field of characteristic not two, the existing finite-dimensional triangularizability instance therefore makes it a splitting Cartan subalgebra.

The self-normalizing argument is entrywise. If X normalizes every diag(d, -d), then the off-diagonal (a, b) entry of their bracket is (weight d b - weight d a) * X a b. Distinct indices in ι ⊕ ι have distinct weights when multiplication by 2 is injective, so every off-diagonal entry of X vanishes. Skew-adjointness then forces the two diagonal blocks to be negatives of one another.

Main definitions

• TauCeti.typeDDiagonalCartan: the diagonal Cartan subalgebra of LieAlgebra.Orthogonal.typeD ι K.
• TauCeti.typeDDiagonalEquiv: the coordinate equivalence (ι → K) ≃ₗ[K] typeDDiagonalCartan K ι.
• TauCeti.typeDDiagonalCartanBasis: its basis by the matrices with diagonal entries 1 and -1 in the paired positions.
• TauCeti.typeDWeightEquiv: the corresponding coordinate equivalence with the dual Cartan.
• TauCeti.typeDEpsilon: the coordinate functional εᵢ.

Main results

• TauCeti.typeDDiagonalCartan_normalizer_eq_self: the diagonal Cartan is self-normalizing.
• TauCeti.instIsCartanSubalgebraTypeDDiagonalCartan: it is a Cartan subalgebra.
• TauCeti.finrank_typeDDiagonalCartan: its dimension is Fintype.card ι.

References

The declaration order and coordinate API adapt the existing formal template in TauCeti.Algebra.Lie.GeneralLinear.DiagonalCartan to the split orthogonal subalgebra. This is the split type-D Cartan prerequisite for Layer 5 of the Spin-representations roadmap. See Fulton--Harris, Representation Theory, Lecture 20, for the coordinate model.

The diagonal matrices of type D

def TauCeti.typeDDiagonalValue {K : Type u} {ι : Type u_1} [Neg K] (d : ι → K) : ι ⊕ ι → K

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

Equations

• TauCeti.typeDDiagonalValue d = Sum.elim d (-d)

@[simp]

theorem TauCeti.typeDDiagonalValue_inl {K : Type u} {ι : Type u_1} [Neg K] (d : ι → K) (i : ι) : typeDDiagonalValue d (Sum.inl i) = d i

@[simp]

theorem TauCeti.typeDDiagonalValue_inr {K : Type u} {ι : Type u_1} [Neg K] (d : ι → K) (i : ι) : typeDDiagonalValue d (Sum.inr i) = -d i

def TauCeti.typeDDiagonalMatrix {K : Type u} {ι : Type u_1} [Neg K] [Zero K] [DecidableEq ι] (d : ι → K) : Matrix (ι ⊕ ι) (ι ⊕ ι) K

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

Equations

• TauCeti.typeDDiagonalMatrix d = Matrix.diagonal (TauCeti.typeDDiagonalValue d)

@[simp]

theorem TauCeti.typeDDiagonalMatrix_apply {K : Type u} {ι : Type u_1} [Neg K] [Zero K] [DecidableEq ι] (d : ι → K) (i j : ι ⊕ ι) : typeDDiagonalMatrix d i j = if i = j then typeDDiagonalValue d i else 0

theorem TauCeti.typeDDiagonalMatrix_mem_typeD {K : Type u} {ι : Type u_1} [CommRing K] [DecidableEq ι] [Fintype ι] (d : ι → K) : typeDDiagonalMatrix d ∈ LieAlgebra.Orthogonal.typeD ι K

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

The Cartan subalgebra and its coordinates

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

The diagonal matrices inside the split orthogonal Lie algebra of type D.

Equations

• TauCeti.typeDDiagonalCartan K ι = LieSubalgebra.comap (LieAlgebra.Orthogonal.typeD ι K).incl (TauCeti.diagonalCartan K (ι ⊕ ι))

@[simp]

theorem TauCeti.mem_typeDDiagonalCartan_iff_isDiag {K : Type u} {ι : Type u_1} [CommRing K] [DecidableEq ι] [Fintype ι] {A : ↥(LieAlgebra.Orthogonal.typeD ι K)} : A ∈ typeDDiagonalCartan K ι ↔ (↑A).IsDiag

Membership in the type-D diagonal Cartan means that the ambient matrix is diagonal.

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

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

Equations

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

@[simp]

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

@[simp]

theorem TauCeti.typeDDiagonalEquiv_symm_apply {K : Type u} {ι : Type u_1} [CommRing K] [DecidableEq ι] [Fintype ι] (A : ↥(typeDDiagonalCartan K ι)) (i : ι) : typeDDiagonalEquiv.symm A i = ↑↑A (Sum.inl i) (Sum.inl i)

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

Self-normalization

@[simp]

theorem TauCeti.typeDDiagonalMatrix_lie_apply {K : Type u} {ι : Type u_1} [CommRing K] [DecidableEq ι] [Fintype ι] (d : ι → K) (X : Matrix (ι ⊕ ι) (ι ⊕ ι) K) (a b : ι ⊕ ι) : ⁅typeDDiagonalMatrix d, X⁆ a b = (typeDDiagonalValue d a - typeDDiagonalValue d b) * X a b

The adjoint action of the matrix diag(d, -d) scales each matrix entry by the difference of its two coordinate weights.

theorem TauCeti.typeDDiagonalEquiv_lie_apply {K : Type u} {ι : Type u_1} [CommRing K] [DecidableEq ι] [Fintype ι] (d : ι → K) (X : ↥(LieAlgebra.Orthogonal.typeD ι K)) (a b : ι ⊕ ι) : ↑⁅typeDDiagonalEquiv d, X⁆ a b = (typeDDiagonalValue d a - typeDDiagonalValue d b) * ↑X a b

The adjoint action of the bundled Cartan element diag(d, -d) has the same entrywise normal form.

@[simp]

theorem TauCeti.lie_typeDDiagonalMatrix_apply {K : Type u} {ι : Type u_1} [CommRing K] [DecidableEq ι] [Fintype ι] (X : Matrix (ι ⊕ ι) (ι ⊕ ι) K) (d : ι → K) (a b : ι ⊕ ι) : ⁅X, typeDDiagonalMatrix d⁆ a b = (typeDDiagonalValue d b - typeDDiagonalValue d a) * X a b

Bracketing in the reverse order with the matrix diag(d, -d) scales each matrix entry by the reverse weight difference.

theorem TauCeti.lie_typeDDiagonalEquiv_apply {K : Type u} {ι : Type u_1} [CommRing K] [DecidableEq ι] [Fintype ι] (X : ↥(LieAlgebra.Orthogonal.typeD ι K)) (d : ι → K) (a b : ι ⊕ ι) : ↑⁅X, ↑(typeDDiagonalEquiv d)⁆ a b = (typeDDiagonalValue d b - typeDDiagonalValue d a) * ↑X a b

Bracketing in the reverse order with the bundled Cartan element diag(d, -d) has the same entrywise normal form.

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

The diagonal Cartan of type D is self-normalizing.

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

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

@[instance 100]

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

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

A basis and dual coordinates

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

The coordinate basis of the type-D diagonal Cartan.

Equations

• TauCeti.typeDDiagonalCartanBasis = Module.Basis.ofEquivFun TauCeti.typeDDiagonalEquiv.symm

@[simp]

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

@[simp]

theorem TauCeti.typeDDiagonalCartanBasis_repr_apply {K : Type u} {ι : Type u_1} [CommRing K] [DecidableEq ι] [Fintype ι] (A : ↥(typeDDiagonalCartan K ι)) (i : ι) : (typeDDiagonalCartanBasis.repr A) i = ↑↑A (Sum.inl i) (Sum.inl i)

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

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

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

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

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

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

Equations

• TauCeti.typeDWeightEquiv = TauCeti.typeDDiagonalCartanBasis.dualBasis.equivFun.symm

@[simp]

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

@[simp]

theorem TauCeti.typeDWeightEquiv_symm_apply {K : Type u} {ι : Type u_1} [CommRing K] [DecidableEq ι] [Fintype ι] (f : Module.Dual K ↥(typeDDiagonalCartan K ι)) (i : ι) : typeDWeightEquiv.symm f i = f (typeDDiagonalCartanBasis i)

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

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

Equations

• TauCeti.typeDEpsilon i = TauCeti.typeDDiagonalCartanBasis.dualBasis i

@[simp]

theorem TauCeti.typeDEpsilon_apply {K : Type u} {ι : Type u_1} [CommRing K] [DecidableEq ι] [Fintype ι] (i : ι) (A : ↥(typeDDiagonalCartan K ι)) : (typeDEpsilon i) A = ↑↑A (Sum.inl i) (Sum.inl i)

@[simp]

theorem TauCeti.typeDWeightEquiv_single {K : Type u} {ι : Type u_1} [CommRing K] [DecidableEq ι] [Fintype ι] (i : ι) : typeDWeightEquiv (Pi.single i 1) = typeDEpsilon i

The coordinate equivalence sends a standard coordinate vector to the corresponding coordinate functional.

@[simp]

theorem TauCeti.typeDWeightEquiv_symm_epsilon {K : Type u} {ι : Type u_1} [CommRing K] [DecidableEq ι] [Fintype ι] (i : ι) : typeDWeightEquiv.symm (typeDEpsilon i) = Pi.single i 1

In coordinates, the functional εᵢ is the standard coordinate vector at i.