The three-dimensional Heisenberg Lie algebra

The Heisenberg Lie algebra is the strictly upper triangular 3 × 3 matrices, that is, TauCeti.strictUpperTriangular R (Fin 3), and TauCeti.heisenberg is that Lie subalgebra of gl 3 R under its traditional name. It is free of rank three on the matrix units

x = E₀₁, y = E₁₂, z = E₀₂,

whose only nonzero bracket is ⁅x, y⁆ = z. Everything below comes out of one computation, TauCeti.lie_eq_smul_heisenbergZ: the bracket of two strictly upper triangular 3 × 3 matrices is a multiple of the corner z, with the 2 × 2 determinant of their two superdiagonal entries as its coefficient. Every iterated bracket ⁅⁅A, B⁆, C⁆ vanishes, so z is central and the algebra is nilpotent of class at most two — of class exactly two over a nontrivial ring, where ⁅x, y⁆ = z ≠ 0 (TauCeti.heisenbergZ_ne_zero) — with ⁅L, L⁆ and the centre both equal to the line R ∙ z.

This is the standard two-step nilpotent Lie algebra, and it separates the two faithfulness questions. Its centre is nonzero, so the adjoint representation is not faithful (TauCeti.not_isFaithful_self_heisenberg); a faithful finite-dimensional representation of it must therefore come from somewhere else, and the defining action on R³ supplies one, which needs no statement here: LieModule.IsFaithful R (heisenberg R) (Fin 3 → R) is an instance for every Lie subalgebra of gl 3 R, from Mathlib/Algebra/Lie/Matrix.lean. The Heisenberg Lie algebra also pins down the indexing of the powers of the augmentation ideal U⁺(L) of TauCeti/Algebra/Lie/UniversalEnveloping/Augmentation.lean: the central generator z is a single bracket, so it lands in the square (U⁺)² and not merely in U⁺ itself (TauCeti.ι_heisenbergZ_mem_augmentation_toIdeal_sq).

Main definitions

• TauCeti.heisenberg: the three-dimensional Heisenberg Lie algebra over R, as the Lie subalgebra TauCeti.strictUpperTriangular R (Fin 3) of gl 3 R.
• TauCeti.heisenbergX, TauCeti.heisenbergY, TauCeti.heisenbergZ: its standard generators E₀₁, E₁₂ and E₀₂.
• TauCeti.heisenbergEquivFun and TauCeti.heisenbergBasis: the coordinate isomorphism heisenberg R ≃ₗ[R] (Fin 3 → R) reading off the three superdiagonal and corner entries, and the basis (x, y, z) it produces, whose three vectors are TauCeti.heisenbergBasis_zero, TauCeti.heisenbergBasis_one and TauCeti.heisenbergBasis_two, and whose coordinates are those three entries again (TauCeti.heisenbergBasis_equivFun).

Main results

• TauCeti.lie_eq_smul_heisenbergZ: the bracket is a multiple of the corner generator, with an explicit coefficient. The defining relation TauCeti.lie_heisenbergX_heisenbergY and the centrality TauCeti.heisenbergZ_lie, TauCeti.lie_heisenbergZ of z — which together are the whole bracket table — are its special cases.
• TauCeti.lie_lie_heisenberg_eq_zero, its simp-normal companion TauCeti.lie_lie_heisenberg_eq_zero' and TauCeti.lie_mem_center_heisenberg: an iterated bracket vanishes, so every bracket is central.
• TauCeti.heisenbergBasis: the Heisenberg Lie algebra is a free module of rank three, and TauCeti.finrank_heisenberg reads finrank R (heisenberg R) = 3 off that basis over a ring satisfying the strong rank condition.
• TauCeti.center_heisenberg_toSubmodule_eq_span_heisenbergZ and TauCeti.lowerCentralSeries_heisenberg_one_toSubmodule_eq_span_heisenbergZ: the centre and the derived subalgebra are both the line R ∙ z, and TauCeti.lowerCentralSeries_heisenberg_two is the vanishing of the next term, which makes the Heisenberg Lie algebra nilpotent of class at most two, and of class exactly two over a nontrivial ring.
• TauCeti.not_isFaithful_self_heisenberg: the adjoint representation is not faithful, in contrast with the defining action on R³, which is faithful by instance inference.
• TauCeti.ι_heisenbergZ_mem_augmentation_toIdeal_sq: the central generator lies in the square of the augmentation ideal of U(L).

Implementation notes

TauCeti.heisenberg is an abbreviation rather than a new type: the Heisenberg Lie algebra is the strict upper triangle of gl 3 R, and every fact about TauCeti.strictUpperTriangular — that it is a Lie subalgebra, spanned by the raising matrix units, closed under the associative product — is meant to apply to it unchanged. What this file adds is the three-dimensional arithmetic, which the general n does not have: for n = 3, and only there, a bracket is a multiple of a single fixed matrix unit.

The Module.Free and Module.Finite instances are not proved here. The strict upper triangle is free on the raising matrix units for every finite ordered index type, so TauCeti/Algebra/Lie/GeneralLinear/Borel.lean carries both instances at general n, exactly as TauCeti/Algebra/Lie/Sl2/Basic.lean takes its instances from TauCeti/Algebra/Lie/GeneralLinear/Finrank.lean; TauCeti.heisenbergBasis is here to name the three generators and to count them.

Everything is stated over an arbitrary commutative ring. [Nontrivial R] appears only where a generator is claimed to be nonzero, and [StrongRankCondition R] only for the rank computation, as in TauCeti/Algebra/Lie/Sl2/Basic.lean. Mathlib does not register LieRing.ofAssociativeRing as a global instance, so, as in Mathlib/Algebra/Lie/Classical.lean and in TauCeti/Algebra/Lie/GeneralLinear/Borel.lean, it is a local instance here.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory (1972), §1.2 and §17.

@[reducible, inline]

abbrev TauCeti.heisenberg (R : Type u_1) [CommRing R] : LieSubalgebra R (Matrix (Fin 3) (Fin 3) R)

The three-dimensional Heisenberg Lie algebra over R: the strictly upper triangular 3 × 3 matrices, as a Lie subalgebra of gl 3 R = Matrix (Fin 3) (Fin 3) R.

It is free of rank three on the matrix units x = E₀₁, y = E₁₂ and z = E₀₂ (TauCeti.heisenbergBasis), whose only nonzero bracket is ⁅x, y⁆ = z.

Equations

• TauCeti.heisenberg R = TauCeti.strictUpperTriangular R (Fin 3)

def TauCeti.heisenbergX (R : Type u_1) [CommRing R] : ↥(heisenberg R)

The generator x = E₀₁ of the Heisenberg Lie algebra.

Equations

• TauCeti.heisenbergX R = ⟨Matrix.single 0 1 1, ⋯⟩

def TauCeti.heisenbergY (R : Type u_1) [CommRing R] : ↥(heisenberg R)

The generator y = E₁₂ of the Heisenberg Lie algebra.

Equations

• TauCeti.heisenbergY R = ⟨Matrix.single 1 2 1, ⋯⟩

def TauCeti.heisenbergZ (R : Type u_1) [CommRing R] : ↥(heisenberg R)

The central generator z = E₀₂ of the Heisenberg Lie algebra, the bracket ⁅x, y⁆.

Equations

• TauCeti.heisenbergZ R = ⟨Matrix.single 0 2 1, ⋯⟩

@[simp]

theorem TauCeti.coe_heisenbergX (R : Type u_1) [CommRing R] : ↑(heisenbergX R) = Matrix.single 0 1 1

@[simp]

theorem TauCeti.coe_heisenbergY (R : Type u_1) [CommRing R] : ↑(heisenbergY R) = Matrix.single 1 2 1

@[simp]

theorem TauCeti.coe_heisenbergZ (R : Type u_1) [CommRing R] : ↑(heisenbergZ R) = Matrix.single 0 2 1

Coordinates

theorem TauCeti.eq_smul_heisenbergX_add_smul_heisenbergY_add_smul_heisenbergZ {R : Type u_1} [CommRing R] (A : ↥(heisenberg R)) : A = ↑A 0 1 • heisenbergX R + ↑A 1 2 • heisenbergY R + ↑A 0 2 • heisenbergZ R

The entries of a strictly upper triangular 3 × 3 matrix expand it in the three matrix units E₀₁, E₁₂ and E₀₂.

@[simp]

theorem TauCeti.smul_heisenbergZ_eq_zero_iff {R : Type u_1} [CommRing R] {c : R} : c • heisenbergZ R = 0 ↔ c = 0

A multiple of the central generator vanishes only for a vanishing coefficient: reading off the corner entry recovers the coefficient.

theorem TauCeti.heisenbergZ_ne_zero {R : Type u_1} [CommRing R] [Nontrivial R] : heisenbergZ R ≠ 0

The central generator is nonzero over a nontrivial ring.

The bracket

theorem TauCeti.lie_eq_smul_heisenbergZ {R : Type u_1} [CommRing R] (A B : ↥(heisenberg R)) : ⁅A, B⁆ = (↑A 0 1 * ↑B 1 2 - ↑B 0 1 * ↑A 1 2) • heisenbergZ R

The bracket of the Heisenberg Lie algebra is a multiple of its central generator. The coefficient is the 2 × 2 determinant of the two superdiagonal entries, so the whole bracket structure of the strict upper triangle in size three is one 2 × 2 determinant.

@[simp]

theorem TauCeti.lie_heisenbergX_heisenbergY {R : Type u_1} [CommRing R] : ⁅heisenbergX R, heisenbergY R⁆ = heisenbergZ R

The defining relation of the Heisenberg Lie algebra: ⁅x, y⁆ = z.

@[simp]

theorem TauCeti.lie_heisenbergY_heisenbergX {R : Type u_1} [CommRing R] : ⁅heisenbergY R, heisenbergX R⁆ = -heisenbergZ R

The defining relation of the Heisenberg Lie algebra, in the opposite order: ⁅y, x⁆ = -z.

@[simp]

theorem TauCeti.heisenbergZ_lie {R : Type u_1} [CommRing R] (A : ↥(heisenberg R)) : ⁅heisenbergZ R, A⁆ = 0

The central generator commutes with everything.

@[simp]

theorem TauCeti.lie_heisenbergZ {R : Type u_1} [CommRing R] (A : ↥(heisenberg R)) : ⁅A, heisenbergZ R⁆ = 0

The central generator commutes with everything, on the other side.

theorem TauCeti.lie_lie_heisenberg_eq_zero {R : Type u_1} [CommRing R] (A B C : ↥(heisenberg R)) : ⁅⁅A, B⁆, C⁆ = 0

An iterated bracket of length three vanishes: the Heisenberg Lie algebra is nilpotent of class at most two.

This is deliberately not a @[simp] lemma: Mathlib's lie_lie is itself @[simp] and rewrites ⁅⁅A, B⁆, C⁆ into ⁅A, ⁅B, C⁆⁆ - ⁅B, ⁅A, C⁆⁆, so the left-hand side here is not in simp-normal form and the simpNF linter rejects the tag. The simp-normal form of the statement is TauCeti.lie_lie_heisenberg_eq_zero', which is what closes such a goal by simp.

@[simp]

theorem TauCeti.lie_lie_heisenberg_eq_zero' {R : Type u_1} [CommRing R] (A B C : ↥(heisenberg R)) : ⁅A, ⁅B, C⁆⁆ = 0

An iterated bracket of length three vanishes, in the right-nested simp-normal form that Mathlib's lie_lie rewrites ⁅⁅A, B⁆, C⁆ into.

theorem TauCeti.lie_mem_center_heisenberg {R : Type u_1} [CommRing R] (A B : ↥(heisenberg R)) : ⁅A, B⁆ ∈ LieAlgebra.center R ↥(heisenberg R)

A bracket lies in the centre of the Heisenberg Lie algebra.

Coordinates, as a basis

def TauCeti.heisenbergEquivFun (R : Type u_1) [CommRing R] : ↥(heisenberg R) ≃ₗ[R] Fin 3 → R

The coordinate isomorphism of the Heisenberg Lie algebra: a strictly upper triangular 3 × 3 matrix is its two superdiagonal entries together with its corner entry.

Equations

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

@[simp]

theorem TauCeti.heisenbergEquivFun_apply {R : Type u_1} [CommRing R] (A : ↥(heisenberg R)) : (heisenbergEquivFun R) A = ![↑A 0 1, ↑A 1 2, ↑A 0 2]

@[simp]

theorem TauCeti.heisenbergEquivFun_symm_apply {R : Type u_1} [CommRing R] (v : Fin 3 → R) : (heisenbergEquivFun R).symm v = v 0 • heisenbergX R + v 1 • heisenbergY R + v 2 • heisenbergZ R

noncomputable def TauCeti.heisenbergBasis (R : Type u_1) [CommRing R] : Module.Basis (Fin 3) R ↥(heisenberg R)

The standard basis of the Heisenberg Lie algebra, the matrix units x = E₀₁, y = E₁₂ and z = E₀₂; see TauCeti.heisenbergBasis_apply. In particular the Heisenberg Lie algebra is a free R-module of rank three.

Equations

• TauCeti.heisenbergBasis R = Module.Basis.ofEquivFun (TauCeti.heisenbergEquivFun R)

theorem TauCeti.heisenbergBasis_apply {R : Type u_1} [CommRing R] (k : Fin 3) : (heisenbergBasis R) k = ![heisenbergX R, heisenbergY R, heisenbergZ R] k

@[simp]

theorem TauCeti.heisenbergBasis_zero (R : Type u_1) [CommRing R] : (heisenbergBasis R) 0 = heisenbergX R

The first standard basis vector of the Heisenberg Lie algebra is x = E₀₁.

@[simp]

theorem TauCeti.heisenbergBasis_one (R : Type u_1) [CommRing R] : (heisenbergBasis R) 1 = heisenbergY R

The second standard basis vector of the Heisenberg Lie algebra is y = E₁₂.

@[simp]

theorem TauCeti.heisenbergBasis_two (R : Type u_1) [CommRing R] : (heisenbergBasis R) 2 = heisenbergZ R

The third standard basis vector of the Heisenberg Lie algebra is the central z = E₀₂.

@[simp]

theorem TauCeti.heisenbergBasis_equivFun (R : Type u_1) [CommRing R] : (heisenbergBasis R).equivFun = heisenbergEquivFun R

The coordinates of the standard basis are the three entries read off by TauCeti.heisenbergEquivFun.

@[simp]

theorem TauCeti.finrank_heisenberg (R : Type u_1) [CommRing R] [StrongRankCondition R] : Module.finrank R ↥(heisenberg R) = 3

The Heisenberg Lie algebra has rank three: finrank R (heisenberg R) = 3, over a commutative ring satisfying the strong rank condition, which is what counting the three basis vectors of TauCeti.heisenbergBasis needs.

The centre and the lower central series

theorem TauCeti.center_heisenberg_toSubmodule_eq_span_heisenbergZ (R : Type u_1) [CommRing R] : ↑(LieAlgebra.center R ↥(heisenberg R)) = R ∙ heisenbergZ R

The centre of the Heisenberg Lie algebra is the line spanned by its central generator.

theorem TauCeti.lowerCentralSeries_heisenberg_one_toSubmodule_eq_span_heisenbergZ (R : Type u_1) [CommRing R] : ↑(LieModule.lowerCentralSeries R (↥(heisenberg R)) (↥(heisenberg R)) 1) = R ∙ heisenbergZ R

The derived subalgebra of the Heisenberg Lie algebra is the line spanned by its central generator, and so coincides with its centre.

theorem TauCeti.lowerCentralSeries_heisenberg_two (R : Type u_1) [CommRing R] : LieModule.lowerCentralSeries R (↥(heisenberg R)) (↥(heisenberg R)) 2 = ⊥

The Heisenberg Lie algebra is nilpotent of class at most two: the second term of its lower central series vanishes. Over a nontrivial ring the class is exactly two, the first term being the nonzero line R ∙ z (TauCeti.lowerCentralSeries_heisenberg_one_toSubmodule_eq_span_heisenbergZ, TauCeti.heisenbergZ_ne_zero).

instance TauCeti.instIsNilpotentHeisenberg (R : Type u_1) [CommRing R] : LieModule.IsNilpotent ↥(heisenberg R) ↥(heisenberg R)

Faithfulness

theorem TauCeti.not_isLieAbelian_heisenberg (R : Type u_1) [CommRing R] [Nontrivial R] : ¬IsLieAbelian ↥(heisenberg R)

The Heisenberg Lie algebra is not abelian.

theorem TauCeti.not_isFaithful_self_heisenberg (R : Type u_1) [CommRing R] [Nontrivial R] : ¬LieModule.IsFaithful R ↥(heisenberg R) ↥(heisenberg R)

The adjoint representation of the Heisenberg Lie algebra is not faithful: it kills the central generator. The defining action on R³ is faithful — LieModule.IsFaithful R (heisenberg R) (Fin 3 → R) is an instance for every Lie subalgebra of gl 3 R, from Mathlib/Algebra/Lie/Matrix.lean — so this is a property of the adjoint representation and not of the algebra.

The augmentation ideal

theorem TauCeti.ι_heisenbergZ_mem_augmentation_toIdeal_sq (R : Type u_1) [CommRing R] : (UniversalEnvelopingAlgebra.ι R) (heisenbergZ R) ∈ (HopfIdeal.augmentation R (UniversalEnvelopingAlgebra R ↥(heisenberg R))).toIdeal ^ 2

The central generator of the Heisenberg Lie algebra lies in the square of the augmentation ideal of its universal enveloping algebra, being the single bracket ⁅x, y⁆. This is the indexing convention of TauCeti.UniversalEnvelopingAlgebra.ι_mem_augmentation_toIdeal_pow_of_mem_lowerCentralSeries, whose n-th term of the lower central series lands in the (n + 1)-st power: z belongs to the first term, not the zeroth.