The Serre presentation: generators, relations, and the universal property

Mathlib's Matrix.ToLieAlgebra R CM is the Lie algebra presented by Serre's relations for a matrix CM of integers: the quotient of the free Lie algebra on the generators Hᵢ, Eᵢ, Fᵢ by the Lie ideal CartanMatrix.Relations.toIdeal generated by

⁅Hᵢ, Hⱼ⁆, ⁅Eᵢ, Fᵢ⁆ - Hᵢ, ⁅Eᵢ, Fⱼ⁆ (i ≠ j), ⁅Hᵢ, Eⱼ⁆ - CMᵢⱼ • Eⱼ, ⁅Hᵢ, Fⱼ⁆ + CMᵢⱼ • Fⱼ, (ad Eᵢ) ^ (-CMᵢⱼ).toNat ⁅Eᵢ, Eⱼ⁆, (ad Fᵢ) ^ (-CMᵢⱼ).toNat ⁅Fᵢ, Fⱼ⁆.

That definition is all Mathlib records: the generators of the presented algebra are not named, the relations are not known to hold in it, and nothing maps out of it. This file supplies those three things, which is what makes the presentation usable.

The generators TauCeti.serreH, TauCeti.serreE and TauCeti.serreF are the images of the free generators. The relations they satisfy are collected in the predicate TauCeti.IsSerreSystem, one field per displayed relator, and TauCeti.isSerreSystem_serre proves that the generators of the presented algebra form such a system — the "only if" direction of the presentation. The converse is TauCeti.serreLift: any Serre system in any Lie algebra L is the image of the generators under a homomorphism out of Matrix.ToLieAlgebra R CM, and by TauCeti.serre_hom_ext that homomorphism is the only one with those values. The symmetries of Serre's relations are recorded as stability properties of TauCeti.IsSerreSystem — under reindexing the families along an injective map of index sets and under the signed exchange of the raising and lowering families — since they are statements about an arbitrary Serre system rather than about the presented algebra. Finally TauCeti.lieSpan_serreGenerators_eq_top records that the three families generate the presented algebra as a Lie subalgebra.

Nothing here assumes that CM is a Cartan matrix, since none of it needs to: the presented algebra is defined for an arbitrary matrix of integers, and the universal property is a statement about the relators rather than about the geometry behind them. Accordingly no statement below mentions a root system: TauCeti.serreH, TauCeti.serreE and TauCeti.serreF are named after the free generators Hᵢ, Eᵢ, Fᵢ they are the images of, and reading them as a coroot and a pair of simple root vectors of a split semisimple Lie algebra needs the identification of the presented algebra with one, which is not proved here (see the Roadmap section below).

Main definitions

• TauCeti.serreMk: the quotient map presenting Matrix.ToLieAlgebra R CM.
• TauCeti.serreH, TauCeti.serreE, TauCeti.serreF: the generators of the presented algebra.
• TauCeti.IsSerreSystem: three families of elements of a Lie algebra satisfying Serre's relations for CM.
• TauCeti.serreLift: the homomorphism out of Matrix.ToLieAlgebra R CM determined by a Serre system.

Main results

• TauCeti.isSerreSystem_serre: the generators of Matrix.ToLieAlgebra R CM are a Serre system, with the individual relations available as TauCeti.lie_serreH_serreH and its companions.
• TauCeti.serreLift_serreH, TauCeti.serreLift_serreE, TauCeti.serreLift_serreF and TauCeti.serre_hom_ext: TauCeti.serreLift sends the generators to the given Serre system, and is the unique homomorphism doing so; TauCeti.serre_equiv_ext is the same extensionality principle for equivalences out of the presented algebra.
• TauCeti.IsSerreSystem.changeScalars: a Serre system over one base ring is one over any other base ring for which the same Lie ring has a Lie-algebra structure.
• TauCeti.IsSerreSystem.map, TauCeti.IsSerreSystem.submatrix, TauCeti.IsSerreSystem.perm and TauCeti.IsSerreSystem.neg_swap: Serre systems are preserved by Lie homomorphisms, reindexing, and the signed exchange of the raising and lowering families.
• TauCeti.serreLift_eq_id: lifting the generators along their own Serre system is the identity.
• TauCeti.lieSpan_serreGenerators_eq_top: the generators generate the presented algebra.

Roadmap

This is a prerequisite for the Chevalley--Demazure construction, Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, which builds the split reductive group scheme over ℤ of a pinned root datum from a Chevalley basis and the Kostant ℤ-form of the enveloping algebra of the corresponding split semisimple Lie algebra. The Serre presentation of the pinned Cartan matrix is the explicit carrier of that Lie algebra, and the generators named here are the ones a Chevalley basis of it starts from. Consumed in turn by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md. The presentation theorem identifying the presented algebra with a concrete split semisimple Lie algebra is a separate target, Layer 7 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md; it consumes TauCeti.serreLift to build its comparison map, and is not begun here.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6
• J.P. Serre, Complex Semisimple Lie Algebras, chapter VI, appendix

The generators

noncomputable def TauCeti.serreMk {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) : FreeLieAlgebra R (CartanMatrix.Generators B) →ₗ⁅R⁆ Matrix.ToLieAlgebra R CM

The quotient map presenting Matrix.ToLieAlgebra R CM as the free Lie algebra on the Serre generators modulo the Lie ideal generated by Serre's relations.

Equations

• TauCeti.serreMk R CM = (CartanMatrix.Relations.toIdeal R CM).mkQ

@[simp]

theorem TauCeti.ker_serreMk {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) : (serreMk R CM).ker = CartanMatrix.Relations.toIdeal R CM

The kernel of the presentation map is the Lie ideal generated by Serre's relations.

theorem TauCeti.serreMk_surjective {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) : Function.Surjective ⇑(serreMk R CM)

Every element of the presented algebra is the class of an element of the free Lie algebra.

theorem TauCeti.serreMk_eq_zero_of_mem_toSet {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {x : FreeLieAlgebra R (CartanMatrix.Generators B)} (hx : x ∈ CartanMatrix.Relations.toSet R CM) : (serreMk R CM) x = 0

A relator of Serre's presentation becomes zero in the presented algebra.

noncomputable def TauCeti.serreH {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i : B) : Matrix.ToLieAlgebra R CM

The generator Hᵢ of Matrix.ToLieAlgebra R CM, the image of the free generator Hᵢ.

Equations

• TauCeti.serreH R CM i = (TauCeti.serreMk R CM) (FreeLieAlgebra.of R (CartanMatrix.Generators.H i))

noncomputable def TauCeti.serreE {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i : B) : Matrix.ToLieAlgebra R CM

The generator Eᵢ of Matrix.ToLieAlgebra R CM, the image of the free generator Eᵢ.

Equations

• TauCeti.serreE R CM i = (TauCeti.serreMk R CM) (FreeLieAlgebra.of R (CartanMatrix.Generators.E i))

noncomputable def TauCeti.serreF {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i : B) : Matrix.ToLieAlgebra R CM

The generator Fᵢ of Matrix.ToLieAlgebra R CM, the image of the free generator Fᵢ.

Equations

• TauCeti.serreF R CM i = (TauCeti.serreMk R CM) (FreeLieAlgebra.of R (CartanMatrix.Generators.F i))

@[simp]

theorem TauCeti.serreMk_of_H {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i : B) : (serreMk R CM) (FreeLieAlgebra.of R (CartanMatrix.Generators.H i)) = serreH R CM i

The quotient map sends the free generator Hᵢ to TauCeti.serreH.

@[simp]

theorem TauCeti.serreMk_of_E {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i : B) : (serreMk R CM) (FreeLieAlgebra.of R (CartanMatrix.Generators.E i)) = serreE R CM i

The quotient map sends the free generator Eᵢ to TauCeti.serreE.

@[simp]

theorem TauCeti.serreMk_of_F {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i : B) : (serreMk R CM) (FreeLieAlgebra.of R (CartanMatrix.Generators.F i)) = serreF R CM i

The quotient map sends the free generator Fᵢ to TauCeti.serreF.

The relators lie in the defining ideal

Each of the six families of relators of CartanMatrix.Relations.toSet is a range, and membership in the union is recorded once here so that the relations below read off from a single lemma. These are proof-local plumbing: the relations themselves, below, are the public statement.

Serre's relations in the presented algebra

@[simp]

theorem TauCeti.lie_serreH_serreH {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i j : B) : ⁅serreH R CM i, serreH R CM j⁆ = 0

Serre's relation ⁅Hᵢ, Hⱼ⁆ = 0: the generators Hᵢ commute.

@[simp]

theorem TauCeti.lie_serreE_serreF_self {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i : B) : ⁅serreE R CM i, serreF R CM i⁆ = serreH R CM i

Serre's relation ⁅Eᵢ, Fᵢ⁆ = Hᵢ.

@[simp]

theorem TauCeti.lie_serreE_serreF_of_ne {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {i j : B} (hij : i ≠ j) : ⁅serreE R CM i, serreF R CM j⁆ = 0

Serre's relation ⁅Eᵢ, Fⱼ⁆ = 0 for i ≠ j.

@[simp]

theorem TauCeti.lie_serreH_serreE {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i j : B) : ⁅serreH R CM i, serreE R CM j⁆ = CM i j • serreE R CM j

Serre's relation ⁅Hᵢ, Eⱼ⁆ = CMᵢⱼ • Eⱼ.

@[simp]

theorem TauCeti.lie_serreH_serreF {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i j : B) : ⁅serreH R CM i, serreF R CM j⁆ = -(CM i j • serreF R CM j)

Serre's relation ⁅Hᵢ, Fⱼ⁆ = -(CMᵢⱼ • Fⱼ).

@[simp]

theorem TauCeti.ad_pow_lie_serreE_serreE {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i j : B) : ((LieAlgebra.ad R (Matrix.ToLieAlgebra R CM)) (serreE R CM i) ^ (-CM i j).toNat) ⁅serreE R CM i, serreE R CM j⁆ = 0

The higher Serre relation on the E's: (ad Eᵢ) ^ (-CMᵢⱼ).toNat ⁅Eᵢ, Eⱼ⁆ = 0.

@[simp]

theorem TauCeti.ad_pow_lie_serreF_serreF {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i j : B) : ((LieAlgebra.ad R (Matrix.ToLieAlgebra R CM)) (serreF R CM i) ^ (-CM i j).toNat) ⁅serreF R CM i, serreF R CM j⁆ = 0

The higher Serre relation on the F's: (ad Fᵢ) ^ (-CMᵢⱼ).toNat ⁅Fᵢ, Fⱼ⁆ = 0.

Serre systems and the universal property

structure TauCeti.IsSerreSystem {B : Type u_1} (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {L : Type u_3} [LieRing L] [LieAlgebra R L] (H E F : B → L) : Prop

Three families H, E, F of elements of a Lie algebra form a Serre system for the matrix CM when they satisfy Serre's relations for CM. The fields are in bijection with the six families of relators generating CartanMatrix.Relations.toIdeal, the ⁅E, F⁆ family being split into its diagonal and off-diagonal halves.

• lie_H_H (i j : B) : ⁅H i, H j⁆ = 0

  The Hᵢ commute.

• lie_E_F_self (i : B) : ⁅E i, F i⁆ = H i

  ⁅Eᵢ, Fᵢ⁆ is Hᵢ.

• lie_E_F_of_ne (i j : B) : i ≠ j → ⁅E i, F j⁆ = 0

  Eᵢ and Fⱼ commute for i ≠ j.

• lie_H_E (i j : B) : ⁅H i, E j⁆ = CM i j • E j

  Eⱼ is an eigenvector of ad Hᵢ of eigenvalue CMᵢⱼ.

• lie_H_F (i j : B) : ⁅H i, F j⁆ = -(CM i j • F j)

  Fⱼ is an eigenvector of ad Hᵢ of eigenvalue -CMᵢⱼ.

• ad_pow_lie_E_E (i j : B) : ((LieAlgebra.ad R L) (E i) ^ (-CM i j).toNat) ⁅E i, E j⁆ = 0

  The higher Serre relation on the E's.

• ad_pow_lie_F_F (i j : B) : ((LieAlgebra.ad R L) (F i) ^ (-CM i j).toNat) ⁅F i, F j⁆ = 0

  The higher Serre relation on the F's.

theorem TauCeti.isSerreSystem_serre {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) : IsSerreSystem R CM (serreH R CM) (serreE R CM) (serreF R CM)

The generators of Matrix.ToLieAlgebra R CM are a Serre system for CM.

Stability of Serre systems

Serre's relations are stable under reindexing the three families along an injective map of index sets, provided the matrix is reindexed the same way, and under the signed exchange of the raising and lowering families. Both are statements about an arbitrary Serre system in an arbitrary Lie algebra; applied to the generators of the presented algebra they give its automorphisms, in TauCeti/Algebra/Lie/Presentation/Serre/Automorphism.lean.

theorem TauCeti.IsSerreSystem.map {B : Type u_1} {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} {L' : Type u_4} [LieRing L'] [LieAlgebra R L'] (h : IsSerreSystem R CM H E F) (f : L →ₗ⁅R⁆ L') : IsSerreSystem R CM (⇑f ∘ H) (⇑f ∘ E) (⇑f ∘ F)

The image of a Serre system under a Lie algebra homomorphism is a Serre system.

theorem TauCeti.IsSerreSystem.changeScalars {B : Type u_1} {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} {S : Type u_4} [CommRing S] [LieAlgebra S L] (h : IsSerreSystem R CM H E F) : IsSerreSystem S CM H E F

A Serre system over one base ring transfers to any other base ring for which the same Lie ring has a Lie-algebra structure.

theorem TauCeti.IsSerreSystem.submatrix {B : Type u_1} {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} {B' : Type u_4} {f : B' → B} (hf : Function.Injective f) (h : IsSerreSystem R CM H E F) : IsSerreSystem R (CM.submatrix f f) (H ∘ f) (E ∘ f) (F ∘ f)

Reindexing a Serre system along an injective map of index sets gives a Serre system for the matrix reindexed the same way.

theorem TauCeti.IsSerreSystem.perm {B : Type u_1} {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} {σ : Equiv.Perm B} (h : IsSerreSystem R CM H E F) (hσ : CM.submatrix ⇑σ ⇑σ = CM) : IsSerreSystem R CM (H ∘ ⇑σ) (E ∘ ⇑σ) (F ∘ ⇑σ)

Reindexing a Serre system along a permutation σ of the index set that preserves the matrix gives a Serre system for the same matrix.

theorem TauCeti.IsSerreSystem.neg_swap {B : Type u_1} {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} (h : IsSerreSystem R CM H E F) : IsSerreSystem R CM (fun (i : B) => -H i) (fun (i : B) => -F i) fun (i : B) => -E i

Negating the Cartan family of a Serre system and exchanging its raising and lowering families, again with a sign, gives a Serre system for the same matrix. This is the symmetry of Serre's relations behind the Chevalley involution.

The universal property

noncomputable def TauCeti.serreLift {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} (h : IsSerreSystem R CM H E F) : Matrix.ToLieAlgebra R CM →ₗ⁅R⁆ L

The homomorphism out of Matrix.ToLieAlgebra R CM determined by a Serre system: the universal property of the presentation.

Equations

• TauCeti.serreLift h = (CartanMatrix.Relations.toIdeal R CM).liftQ ((FreeLieAlgebra.lift R) (TauCeti.serreGeneratorMap✝ H E F)) ⋯

@[simp]

theorem TauCeti.serreLift_serreH {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} (h : IsSerreSystem R CM H E F) (i : B) : (serreLift h) (serreH R CM i) = H i

The homomorphism determined by a Serre system sends Hᵢ to H i.

@[simp]

theorem TauCeti.serreLift_serreE {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} (h : IsSerreSystem R CM H E F) (i : B) : (serreLift h) (serreE R CM i) = E i

The homomorphism determined by a Serre system sends Eᵢ to E i.

@[simp]

theorem TauCeti.serreLift_serreF {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} (h : IsSerreSystem R CM H E F) (i : B) : (serreLift h) (serreF R CM i) = F i

The homomorphism determined by a Serre system sends Fᵢ to F i.

theorem TauCeti.serreH_ne_zero {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} (h : IsSerreSystem R CM H E F) {i : B} (hi : H i ≠ 0) : serreH R CM i ≠ 0

A nonzero Cartan element in a Serre system has a nonzero preimage among the presented Cartan generators.

theorem TauCeti.serreE_ne_zero {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} (h : IsSerreSystem R CM H E F) {i : B} (hi : E i ≠ 0) : serreE R CM i ≠ 0

A nonzero raising element in a Serre system has a nonzero preimage among the presented raising generators.

theorem TauCeti.serreF_ne_zero {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} (h : IsSerreSystem R CM H E F) {i : B} (hi : F i ≠ 0) : serreF R CM i ≠ 0

A nonzero lowering element in a Serre system has a nonzero preimage among the presented lowering generators.

theorem TauCeti.linearIndependent_serreH {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} (h : IsSerreSystem R CM H E F) (hH : LinearIndependent R H) : LinearIndependent R (serreH R CM)

Linear independence of the Cartan family of a Serre system lifts to the presented Cartan generators.

theorem TauCeti.serre_hom_ext {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {g₁ g₂ : Matrix.ToLieAlgebra R CM →ₗ⁅R⁆ L} (hH : ∀ (i : B), g₁ (serreH R CM i) = g₂ (serreH R CM i)) (hE : ∀ (i : B), g₁ (serreE R CM i) = g₂ (serreE R CM i)) (hF : ∀ (i : B), g₁ (serreF R CM i) = g₂ (serreF R CM i)) : g₁ = g₂

Two homomorphisms out of Matrix.ToLieAlgebra R CM agreeing on the generators are equal.

theorem TauCeti.serre_hom_ext_iff {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {g₁ g₂ : Matrix.ToLieAlgebra R CM →ₗ⁅R⁆ L} : g₁ = g₂ ↔ (∀ (i : B), g₁ (serreH R CM i) = g₂ (serreH R CM i)) ∧ (∀ (i : B), g₁ (serreE R CM i) = g₂ (serreE R CM i)) ∧ ∀ (i : B), g₁ (serreF R CM i) = g₂ (serreF R CM i)

theorem TauCeti.serre_equiv_ext {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {g₁ g₂ : Matrix.ToLieAlgebra R CM ≃ₗ⁅R⁆ L} (hH : ∀ (i : B), g₁ (serreH R CM i) = g₂ (serreH R CM i)) (hE : ∀ (i : B), g₁ (serreE R CM i) = g₂ (serreE R CM i)) (hF : ∀ (i : B), g₁ (serreF R CM i) = g₂ (serreF R CM i)) : g₁ = g₂

Two equivalences out of Matrix.ToLieAlgebra R CM agreeing on the generators are equal.

theorem TauCeti.serre_equiv_ext_iff {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {g₁ g₂ : Matrix.ToLieAlgebra R CM ≃ₗ⁅R⁆ L} : g₁ = g₂ ↔ (∀ (i : B), g₁ (serreH R CM i) = g₂ (serreH R CM i)) ∧ (∀ (i : B), g₁ (serreE R CM i) = g₂ (serreE R CM i)) ∧ ∀ (i : B), g₁ (serreF R CM i) = g₂ (serreF R CM i)

theorem TauCeti.eq_serreLift {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} {h : IsSerreSystem R CM H E F} {g : Matrix.ToLieAlgebra R CM →ₗ⁅R⁆ L} (hH : ∀ (i : B), g (serreH R CM i) = H i) (hE : ∀ (i : B), g (serreE R CM i) = E i) (hF : ∀ (i : B), g (serreF R CM i) = F i) : g = serreLift h

TauCeti.serreLift is the unique homomorphism sending the generators to a given Serre system.

theorem TauCeti.serreLift_surjective {B : Type u_1} [DecidableEq B] {R : Type u_2} [CommRing R] {CM : Matrix B B ℤ} {L : Type u_3} [LieRing L] [LieAlgebra R L] {H E F : B → L} (h : IsSerreSystem R CM H E F) (hspan : LieSubalgebra.lieSpan R L (Set.range E ∪ Set.range F) = ⊤) : Function.Surjective ⇑(serreLift h)

A Serre system whose raising and lowering families generate the ambient Lie algebra presents it: the homomorphism it determines is surjective.

@[simp]

theorem TauCeti.serreLift_eq_id {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) : serreLift ⋯ = LieHom.id

Lifting the generators of Matrix.ToLieAlgebra R CM along their own Serre system returns the identity.

theorem TauCeti.lieSpan_serreGenerators_eq_top {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) : LieSubalgebra.lieSpan R (Matrix.ToLieAlgebra R CM) (Set.range (serreH R CM) ∪ Set.range (serreE R CM) ∪ Set.range (serreF R CM)) = ⊤

The generators TauCeti.serreH, TauCeti.serreE and TauCeti.serreF generate Matrix.ToLieAlgebra R CM as a Lie subalgebra.