The standard Borel subalgebra of gl n R, and the two nilpotent triangles

Order the index type n linearly. The upper triangular matrices form a Lie subalgebra TauCeti.upperTriangular R n of gl n R = Matrix n n R, and the strictly upper triangular matrices form a Lie subalgebra TauCeti.strictUpperTriangular R n inside it. This is the matrix unit positive system of gl n R: the raising operators are the matrix units Eᵢⱼ with i < j, and strictUpperTriangular R n is the span of those. Over a domain away from characteristic two, that span is the sum of the root spaces of the positive roots εᵢ - εⱼ, i < j, for the diagonal Cartan subalgebra TauCeti.diagonalCartan R n; without those hypotheses the root spaces can be larger (in characteristic two the root space of εᵢ - εⱼ also contains the lowering matrix unit Eⱼᵢ), as explained in the implementation notes below.

The two subalgebras fit together in the usual way. The upper triangular matrices are the direct sum of the diagonal ones and the strictly upper triangular ones (TauCeti.upperTriangular_toSubmodule_eq_sup and TauCeti.disjoint_diagonalCartan_strictUpperTriangular), which is the decomposition 𝔟 = 𝔥 ⊕ 𝔫⁺. The Borel subalgebra is self-normalizing (TauCeti.upperTriangular_normalizer_eq_self), and the bracket of any two upper triangular matrices is already strictly upper triangular (TauCeti.lie_mem_strictUpperTriangular), because the diagonal of a commutator of upper triangular matrices is the commutator of the diagonals and R is commutative. In particular the strictly upper triangular matrices are a Lie ideal of the Borel subalgebra, TauCeti.strictUpperTriangularIdeal.

On the other side of the diagonal, the strictly lower triangular matrices form the opposite nilpotent subalgebra TauCeti.strictLowerTriangular R n = 𝔫⁻, and together with the Borel subalgebra they exhaust gl n R (TauCeti.exists_mem_strictLowerTriangular_add_mem_upperTriangular). That triangular decomposition gl n R = 𝔫⁻ + 𝔟 is what reduces the stability of a submodule of a gl n R-module under all of gl n R to its stability under the two triangles, which is how the highest weight theory of Layer 9 uses this file.

Main definitions

• TauCeti.upperTriangular R n: the upper triangular matrices, as a LieSubalgebra R (Matrix n n R). This is the standard Borel subalgebra of gl n R.
• TauCeti.strictUpperTriangular R n: the strictly upper triangular matrices, as a LieSubalgebra R (Matrix n n R). This is the positive nilpotent ideal 𝔫⁺ of the standard Borel subalgebra.
• TauCeti.strictUpperTriangularIdeal R n: the same subalgebra, packaged as a Lie ideal of upperTriangular R n.
• TauCeti.strictLowerTriangular R n: the strictly lower triangular matrices, as a LieSubalgebra R (Matrix n n R). This is the opposite nilpotent subalgebra 𝔫⁻.

Main results

• TauCeti.lie_mem_strictUpperTriangular: the bracket of two upper triangular matrices is strictly upper triangular.
• TauCeti.exists_mem_strictLowerTriangular_add_mem_upperTriangular: the triangular decomposition gl n R = 𝔫⁻ + 𝔟, in the form the highest weight theory uses it.
• TauCeti.upperTriangular_toSubmodule_eq_sup and TauCeti.disjoint_diagonalCartan_strictUpperTriangular: the decomposition 𝔟 = 𝔥 ⊕ 𝔫⁺.
• TauCeti.upperTriangular_normalizer_eq_self: the Borel subalgebra is self-normalizing.
• TauCeti.strictUpperTriangular_toSubmodule_eq_iSup: 𝔫⁺ is spanned by the matrix units Eᵢⱼ with i < j, and, over a domain away from characteristic two, TauCeti.strictUpperTriangular_toSubmodule_eq_iSup_rootSpace reads this as the sum of the root spaces of the positive roots.
• 𝔫⁺ is a free module of finite rank over any commutative ring, the entries strictly above the diagonal being free coordinates: this is where the Module.Free and Module.Finite instances for TauCeti.strictUpperTriangular R n come from.

Implementation notes

𝔫⁺ is called here the positive nilpotent ideal of the Borel subalgebra, never its nilradical: for gl n R the two differ as soon as n is nonempty and R is nontrivial, because the nonzero scalar matrices are then central in gl n R and so span a further nilpotent ideal of upperTriangular R n outside strictUpperTriangular R n; for an empty index type, or over the trivial ring, gl n R is zero and the two agree. For a singleton index type this is the whole story: upperTriangular R n is then all of gl n R, which is abelian and hence its own nilradical, while strictUpperTriangular R n is zero. It is in sl n R, over a field whose characteristic does not divide the cardinality of n, that the strict upper triangle is the nilradical of the Borel: only under such a hypothesis are the scalar matrices really gone, since the trace of r • 1 is n • r, so when the characteristic divides the cardinality of n the nonzero scalar matrices are traceless and remain central in sl n R. What makes 𝔫⁺ the right object here regardless is that it is the span of the raising matrix units (TauCeti.strictUpperTriangular_toSubmodule_eq_iSup), which over a domain away from characteristic two is the sum of the positive root spaces (TauCeti.strictUpperTriangular_toSubmodule_eq_iSup_rootSpace), and which is what the highest weight theory downstream uses. The word nilpotent in the name records the standard terminology for 𝔫⁺; nilpotency itself is not proved below, because the highest weight targets this file serves are stated against the strict upper triangle as the set of raising operators rather than against a nilpotency bound.

The index type carries both [DecidableEq n], for the matrix units, and [LinearOrder n], which is what "upper triangular" refers to. The decidable equality stays a hypothesis of its own rather than being read off LinearOrder.toDecidableEq, exactly as in Mathlib's Matrix.BlockTriangular.det: the ring structure on Matrix n n R and the matrix units depend on it as data, so pinning it to the one the order carries would leave everything here inapplicable in the ambient [DecidableEq n] contexts of TauCeti.Algebra.Lie.GeneralLinear.Basic, .DiagonalCartan and .RootSpace, which this file continues and consumes. Upper triangularity is Mathlib's Matrix.BlockTriangular _ id, and TauCeti.upperTriangular is literally Mathlib's associative subalgebra Matrix.blockTriangularSubalgebra read as a Lie subalgebra along lieSubalgebraOfSubalgebra. Strict upper triangularity is not a Matrix.BlockTriangular condition for any block map, so TauCeti.strictUpperTriangular is spelled out. It is closed under the associative product (TauCeti.mul_mem_strictUpperTriangular) as well as under the bracket, and so is a nonunital associative subalgebra; but over a nontrivial R it does not contain 1 unless n is empty (over the trivial ring 1 = 0 lies in it for every n), so it is not a Mathlib Subalgebra, which is unital, and it cannot be read off one along lieSubalgebraOfSubalgebra the way TauCeti.upperTriangular is.

Everything here holds over an arbitrary commutative ring. The single exception is TauCeti.strictUpperTriangular_toSubmodule_eq_iSup_rootSpace, which identifies the individual summands with root spaces and so inherits the [IsDomain R] and (2 : R) ≠ 0 hypotheses of TauCeti.rootSpace_glWeightSub_eq_span: in characteristic two εᵢ - εⱼ = εⱼ - εᵢ, so the root space of a positive root also contains a lowering operator and is not contained in 𝔫⁺ at all.

As in TauCeti.Algebra.Lie.GeneralLinear.DiagonalCartan, none of Mathlib's LieAlgebra.IsKilling machinery is available for gl n R, whose Killing form is degenerate; in particular the positive system here is the matrix unit order rather than a LieAlgebra.IsKilling.rootSystem base.

References

This implements the matrix unit positive system of Layer 9 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md, the standing convention that the positive system of gl n is generated by the Matrix.single i j 1 with i < j, which the highest weight vectors of that layer are defined against. That layer states its highest weight vector target as "a simultaneous eigenvector of the diagonal killed by the strict upper triangle (IsGlHighestWeightVector)": the diagonal is TauCeti.diagonalCartan, and the strict upper triangle is TauCeti.strictUpperTriangular built here, so this file supplies the second of the two objects that statement is made from.

def TauCeti.upperTriangular (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] [LinearOrder n] : LieSubalgebra R (Matrix n n R)

The upper triangular matrices, as a Lie subalgebra of gl n R = Matrix n n R.

This is the standard Borel subalgebra of gl n R attached to the matrix unit positive system: it is the sum of the diagonal Cartan subalgebra and the span of the raising matrix units Eᵢⱼ with i < j, which over a domain away from characteristic two is the sum of the root spaces of the roots εᵢ - εⱼ with i < j.

Equations

• TauCeti.upperTriangular R n = lieSubalgebraOfSubalgebra R (Matrix n n R) (Matrix.blockTriangularSubalgebra R R id)

@[simp]

theorem TauCeti.mem_upperTriangular_iff_blockTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {A : Matrix n n R} : A ∈ upperTriangular R n ↔ A.BlockTriangular id

Membership in the Borel subalgebra is Mathlib's Matrix.BlockTriangular for the identity block map.

theorem TauCeti.mem_upperTriangular_iff {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {A : Matrix n n R} : A ∈ upperTriangular R n ↔ ∀ (i j : n), j < i → A i j = 0

The entrywise description of the Borel subalgebra.

theorem TauCeti.mul_mem_upperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {A B : Matrix n n R} (hA : A ∈ upperTriangular R n) (hB : B ∈ upperTriangular R n) : A * B ∈ upperTriangular R n

The Borel subalgebra is closed under the associative product.

theorem TauCeti.lie_apply_eq_zero_of_mem_upperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {A B : Matrix n n R} (hA : A ∈ upperTriangular R n) (hB : B ∈ upperTriangular R n) {i j : n} (hij : j ≤ i) : ⁅A, B⁆ i j = 0

The bracket of two upper triangular matrices vanishes on and below the diagonal.

def TauCeti.strictUpperTriangular (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] [LinearOrder n] : LieSubalgebra R (Matrix n n R)

The strictly upper triangular matrices, as a Lie subalgebra of gl n R = Matrix n n R.

This is the positive nilpotent ideal 𝔫⁺ of the standard Borel subalgebra TauCeti.upperTriangular R n: it is the span of the raising matrix units Eᵢⱼ with i < j, with no Cartan part, and over a domain away from characteristic two that is the sum of the root spaces of the roots εᵢ - εⱼ with i < j. It is not the nilradical of TauCeti.upperTriangular R n, which is in general larger; see the implementation notes of this file.

Equations

• TauCeti.strictUpperTriangular R n = { carrier := {A : Matrix n n R | ∀ (i j : n), j ≤ i → A i j = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_strictUpperTriangular_iff {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {A : Matrix n n R} : A ∈ strictUpperTriangular R n ↔ ∀ (i j : n), j ≤ i → A i j = 0

The entrywise description of 𝔫⁺.

theorem TauCeti.apply_diag_eq_zero_of_mem_strictUpperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {A : Matrix n n R} (hA : A ∈ strictUpperTriangular R n) (i : n) : A i i = 0

A strictly upper triangular matrix vanishes on the diagonal.

theorem TauCeti.strictUpperTriangular_le_upperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] : strictUpperTriangular R n ≤ upperTriangular R n

𝔫⁺ is contained in the Borel subalgebra.

theorem TauCeti.mul_mem_strictUpperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {A B : Matrix n n R} (hA : A ∈ strictUpperTriangular R n) (hB : B ∈ strictUpperTriangular R n) : A * B ∈ strictUpperTriangular R n

𝔫⁺ is closed under the associative product.

theorem TauCeti.lie_mem_strictUpperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {A B : Matrix n n R} (hA : A ∈ upperTriangular R n) (hB : B ∈ upperTriangular R n) : ⁅A, B⁆ ∈ strictUpperTriangular R n

The bracket of two upper triangular matrices is strictly upper triangular. So the derived subalgebra of the Borel subalgebra lies in 𝔫⁺; in particular 𝔫⁺ is a Lie ideal of the Borel subalgebra, TauCeti.strictUpperTriangularIdeal.

theorem TauCeti.diagonalCartan_le_upperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] : diagonalCartan R n ≤ upperTriangular R n

The diagonal Cartan subalgebra is contained in the Borel subalgebra.

Matrix units

theorem TauCeti.single_mem_upperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {i j : n} (hij : i ≤ j) (c : R) : Matrix.single i j c ∈ upperTriangular R n

The matrix unit Eᵢⱼ is upper triangular when i ≤ j.

theorem TauCeti.single_mem_strictUpperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {i j : n} (hij : i < j) (c : R) : Matrix.single i j c ∈ strictUpperTriangular R n

The matrix unit Eᵢⱼ is strictly upper triangular when i < j; these are the raising operators of the matrix unit positive system.

theorem TauCeti.single_mem_upperTriangular_iff {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {i j : n} {c : R} (hc : c ≠ 0) : Matrix.single i j c ∈ upperTriangular R n ↔ i ≤ j

A nonzero matrix unit Eᵢⱼ is upper triangular exactly when i ≤ j.

theorem TauCeti.single_mem_strictUpperTriangular_iff {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {i j : n} {c : R} (hc : c ≠ 0) : Matrix.single i j c ∈ strictUpperTriangular R n ↔ i < j

A nonzero matrix unit Eᵢⱼ is strictly upper triangular exactly when i < j.

def TauCeti.strictUpperTriangularIdeal (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] [LinearOrder n] : LieIdeal R ↥(upperTriangular R n)

The positive nilpotent ideal 𝔫⁺ of the standard Borel subalgebra of gl n R, as a Lie ideal of that Borel subalgebra. Its underlying set is TauCeti.strictUpperTriangular R n.

Equations

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

@[simp]

theorem TauCeti.mem_strictUpperTriangularIdeal_iff {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {A : ↥(upperTriangular R n)} : A ∈ strictUpperTriangularIdeal R n ↔ ↑A ∈ strictUpperTriangular R n

The decomposition 𝔟 = 𝔥 ⊕ 𝔫⁺

theorem TauCeti.sub_diagonal_diag_mem_strictUpperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {A : Matrix n n R} (hA : A ∈ upperTriangular R n) : A - Matrix.diagonal A.diag ∈ strictUpperTriangular R n

Subtracting its diagonal makes an upper triangular matrix strictly upper triangular.

theorem TauCeti.upperTriangular_toSubmodule_eq_sup {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] : (upperTriangular R n).toSubmodule = (diagonalCartan R n).toSubmodule ⊔ (strictUpperTriangular R n).toSubmodule

The Borel subalgebra is the sum of the diagonal Cartan subalgebra and 𝔫⁺: every upper triangular matrix is its diagonal plus a strictly upper triangular matrix.

theorem TauCeti.disjoint_diagonalCartan_strictUpperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] : Disjoint (diagonalCartan R n).toSubmodule (strictUpperTriangular R n).toSubmodule

The sum 𝔟 = 𝔥 ⊕ 𝔫⁺ is direct: a diagonal matrix with zero diagonal is zero.

The Borel subalgebra is self-normalizing

@[simp]

theorem TauCeti.upperTriangular_normalizer_eq_self (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] [LinearOrder n] : (upperTriangular R n).normalizer = upperTriangular R n

The standard Borel subalgebra of gl n R is self-normalizing.

𝔫⁺ as the span of the raising operators

theorem TauCeti.strictUpperTriangular_toSubmodule_eq_iSup (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] [LinearOrder n] : (strictUpperTriangular R n).toSubmodule = ⨆ (i : n), ⨆ (j : n), ⨆ (_ : i < j), R ∙ Matrix.single i j 1

𝔫⁺ is spanned by the raising matrix units Eᵢⱼ, i < j.

theorem TauCeti.strictUpperTriangular_toSubmodule_eq_iSup_rootSpace (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] [LinearOrder n] [IsDomain R] (h2 : 2 ≠ 0) : (strictUpperTriangular R n).toSubmodule = ⨆ (i : n), ⨆ (j : n), ⨆ (_ : i < j), ↑(LieAlgebra.rootSpace (diagonalCartan R n) ⇑(glWeightSub R n i j))

𝔫⁺ is the sum of the positive root spaces. Over a domain, away from characteristic two, the root space of εᵢ - εⱼ is the line spanned by Eᵢⱼ (TauCeti.rootSpace_glWeightSub_eq_span), so TauCeti.strictUpperTriangular_toSubmodule_eq_iSup says exactly that 𝔫⁺ is the sum of the root spaces of the positive roots εᵢ - εⱼ, i < j. Both hypotheses are needed: in characteristic two εᵢ - εⱼ = εⱼ - εᵢ, so that root space also contains the lowering operator Eⱼᵢ.

𝔫⁺ is free on the raising operators

instance TauCeti.instFreeSubtypeMatrixMemLieSubalgebraStrictUpperTriangular (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] [LinearOrder n] : Module.Free R ↥(strictUpperTriangular R n)

𝔫⁺ is a free module, on the raising matrix units Eᵢⱼ with i < j: the entries above the diagonal are free coordinates.

instance TauCeti.instFiniteSubtypeMatrixMemLieSubalgebraStrictUpperTriangular (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] [LinearOrder n] : Module.Finite R ↥(strictUpperTriangular R n)

𝔫⁺ is a finite module, the entries above the diagonal being finite in number.

The opposite nilpotent subalgebra 𝔫⁻

def TauCeti.strictLowerTriangular (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] [LinearOrder n] : LieSubalgebra R (Matrix n n R)

The strictly lower triangular matrices, as a Lie subalgebra of gl n R = Matrix n n R: those vanishing on and above the diagonal.

This is the opposite nilpotent subalgebra 𝔫⁻; it contains the lowering matrix units Eᵢⱼ with j < i (TauCeti.single_mem_strictLowerTriangular). It is TauCeti.strictUpperTriangular R n read for the reversed order on the index type, but that order lives on nᵒᵈ rather than on n, so it is spelled out here rather than transported. Its role is the triangular decomposition gl n R = 𝔫⁻ + 𝔟 of TauCeti.exists_mem_strictLowerTriangular_add_mem_upperTriangular: a submodule of a gl n R-module stable under 𝔫⁻ and under the Borel subalgebra is stable under all of gl n R.

Equations

• TauCeti.strictLowerTriangular R n = { carrier := {A : Matrix n n R | ∀ (i j : n), i ≤ j → A i j = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_strictLowerTriangular_iff {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {A : Matrix n n R} : A ∈ strictLowerTriangular R n ↔ ∀ (i j : n), i ≤ j → A i j = 0

The entrywise description of 𝔫⁻.

theorem TauCeti.single_mem_strictLowerTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] {i j : n} (hij : j < i) (c : R) : Matrix.single i j c ∈ strictLowerTriangular R n

A lowering matrix unit Eᵢⱼ, j < i, lies in 𝔫⁻.

theorem TauCeti.exists_mem_strictLowerTriangular_add_mem_upperTriangular {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [LinearOrder n] (A : Matrix n n R) : ∃ x ∈ strictLowerTriangular R n, ∃ y ∈ upperTriangular R n, x + y = A

The triangular decomposition gl n R = 𝔫⁻ + 𝔟: every matrix is the sum of its strictly lower triangular part and an upper triangular matrix.