Automorphisms of a Serre presentation

Two families of automorphisms of Matrix.ToLieAlgebra R CM are visible in Serre's presentation itself, and both are constructed here from the universal property in TauCeti/Algebra/Lie/Presentation/Serre.lean.

The first family comes from the symmetries of the matrix: a permutation σ of the index set with CM.submatrix σ σ = CM reindexes the generators, and TauCeti.serreDiagramAut is the resulting automorphism Hᵢ ↦ H_{σ i}, Eᵢ ↦ E_{σ i}, Fᵢ ↦ F_{σ i}. When CM is the Cartan matrix of a Dynkin diagram these are the diagram (or graph) automorphisms; the permutations themselves are already pinned in TauCeti/LinearAlgebra/RootSystem/DiagramPermutations.lean, whose entrywise invariance lemmas supply the hypothesis CM.submatrix σ σ = CM through Matrix.ext.

The second is the Chevalley involution TauCeti.serreChevalleyInvolution, which exchanges the raising and lowering generators with a sign: Hᵢ ↦ -Hᵢ, Eᵢ ↦ -Fᵢ, Fᵢ ↦ -Eᵢ. It exists because Serre's relations are invariant under that exchange, and it is an involution because the exchange is. The two families commute (TauCeti.serreChevalleyInvolution_comm_serreDiagramAut).

Both are instances of one observation, recorded with the predicate itself in TauCeti/Algebra/Lie/Presentation/Serre.lean as stability properties of TauCeti.IsSerreSystem: a Serre system in any Lie algebra stays a Serre system after reindexing along an injective map of index sets (TauCeti.IsSerreSystem.submatrix, of which reindexing along a symmetry of the matrix is the special case TauCeti.IsSerreSystem.perm) or after the signed exchange (TauCeti.IsSerreSystem.neg_swap). Stated at that generality they also give the naturality of the two automorphisms — TauCeti.serreLift_comp_serreDiagramAut and TauCeti.serreLift_comp_serreChevalleyInvolution — which say that any realisation of the presentation transports them, and are how a downstream identification of the presented algebra with a concrete split semisimple Lie algebra will carry them across.

Nothing here assumes that CM is a Cartan matrix, matching TauCeti/Algebra/Lie/Presentation/Serre.lean: the constructions are statements about the relators.

Main definitions

• TauCeti.serreDiagramAut: the automorphism of Matrix.ToLieAlgebra R CM induced by a permutation of the index set preserving CM.
• TauCeti.serreChevalleyInvolution: the Chevalley involution of Matrix.ToLieAlgebra R CM.

Main results

• TauCeti.serreDiagramAut_serreH and its companions, TauCeti.serreChevalleyInvolution_serreH and its companions: the values on the generators, together with the uniqueness statements TauCeti.eq_serreDiagramAut and TauCeti.eq_serreChevalleyInvolution.
• TauCeti.serreDiagramAut_refl, TauCeti.serreDiagramAut_trans and TauCeti.serreDiagramAut_symm: the diagram automorphisms follow the group law of the permutations, which for the hypothesis itself is TauCeti.submatrix_perm_refl, TauCeti.submatrix_perm_trans and TauCeti.submatrix_perm_symm.
• TauCeti.serreDiagramAut_iterate_eq_id: a power relation on the indexing permutation induces the same iterate relation on its diagram automorphism.
• TauCeti.serreChevalleyInvolution_involutive: the Chevalley involution squares to the identity.
• TauCeti.serreChevalleyInvolution_comm_serreDiagramAut: it commutes with every diagram automorphism.
• TauCeti.serreLift_comp_serreDiagramAut and TauCeti.serreLift_comp_serreChevalleyInvolution: naturality against an arbitrary Serre system.

Implementation notes

The hypothesis that σ preserves CM is carried as the equation CM.submatrix σ σ = CM rather than as a new predicate: it is the Mathlib spelling, its entrywise form CM (σ i) (σ j) = CM i j holds by rfl, and the group law of such permutations is Matrix.submatrix_submatrix. That group law is TauCeti.submatrix_perm_refl, TauCeti.submatrix_perm_trans and TauCeti.submatrix_perm_symm of TauCeti/LinearAlgebra/Matrix/Submatrix.lean, so a composite automorphism builds the hypothesis it needs for Equiv.refl B, σ.trans τ or σ.symm rather than demanding it from the caller; proof irrelevance makes a caller's own proof interchangeable with the one built here.

Equalities of the automorphisms themselves are proved with TauCeti.serre_equiv_ext, the equivalence-level extensionality principle of the presentation, so that no proof here has to descend to the underlying homomorphisms by hand.

Roadmap

Both automorphisms are prerequisites for the pinned Chevalley--Demazure group schemes, Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, which asks for the split reductive group scheme over ℤ to be built "via a Chevalley basis and the Kostant ℤ-form of the enveloping algebra". The Serre presentation of TauCeti/Algebra/Lie/Presentation/Serre.lean is the explicit carrier of the Lie algebra that construction starts from, and the two automorphisms are the two symmetries of it that construction uses.

The Chevalley involution is the immediate one: the classical normalisation of a Chevalley basis picks the root vectors x α and x (-α) compatibly by transporting them along an automorphism acting as h ↦ -h on the Cartan subalgebra and exchanging the raising and lowering root vectors with a sign, and that choice is what forces the structure constants of opposite pairs of roots to match up as N (-α, -β) = -N (α, β) (Humphreys §25.2, Carter §4.1). Integrality of the structure constants is a separate matter, coming from the root-string argument once the basis is normalised this way; the involution is what makes the two halves of the basis consistent, not what clears denominators. TauCeti.serreChevalleyInvolution is that automorphism on the presented algebra, and TauCeti.serreLift_comp_serreChevalleyInvolution is what will carry it to any concrete split semisimple Lie algebra identified with the presentation.

The diagram automorphisms are the second: a pinning is what makes "the" graph automorphism well defined, and on the Chevalley--Demazure side the graph automorphism of the group scheme is obtained by descending the one that permutes the divided powers of the generators in the Kostant ℤ-form, which is TauCeti.serreDiagramAut on the underlying Lie algebra. Consumed in turn by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md, whose twisted groups of Lie type are the fixed points of a Steinberg endomorphism built from a graph automorphism of the ambient pinned group.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6
• J.E. Humphreys, Introduction to Lie Algebras and Representation Theory, sections 14.2 and 25.2
• R.W. Carter, Simple Groups of Lie Type, section 4.1

The diagram automorphisms

A permutation of the index set preserving the matrix acts on the presented algebra by permuting the generators.

noncomputable def TauCeti.serreDiagramAut {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) : Matrix.ToLieAlgebra R CM ≃ₗ⁅R⁆ Matrix.ToLieAlgebra R CM

The automorphism of Matrix.ToLieAlgebra R CM induced by a permutation σ of the index set preserving CM: it sends the generator of index i to the generator of index σ i, in each of the three families. For a Cartan matrix this is a diagram automorphism.

Equations

• TauCeti.serreDiagramAut R CM hσ = { toLieHom := TauCeti.serreDiagramHom✝ R CM hσ, invFun := ⇑(TauCeti.serreDiagramHom✝ R CM ⋯), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.serreDiagramAut_serreH {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) (i : B) : (serreDiagramAut R CM hσ) (serreH R CM i) = serreH R CM (σ i)

The diagram automorphism of σ sends Hᵢ to H_{σ i}.

@[simp]

theorem TauCeti.serreDiagramAut_serreE {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) (i : B) : (serreDiagramAut R CM hσ) (serreE R CM i) = serreE R CM (σ i)

The diagram automorphism of σ sends Eᵢ to E_{σ i}.

@[simp]

theorem TauCeti.serreDiagramAut_serreF {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) (i : B) : (serreDiagramAut R CM hσ) (serreF R CM i) = serreF R CM (σ i)

The diagram automorphism of σ sends Fᵢ to F_{σ i}.

theorem TauCeti.eq_serreDiagramAut {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} {hσ : CM.submatrix ⇑σ ⇑σ = CM} {g : Matrix.ToLieAlgebra R CM →ₗ⁅R⁆ Matrix.ToLieAlgebra R CM} (hH : ∀ (i : B), g (serreH R CM i) = serreH R CM (σ i)) (hE : ∀ (i : B), g (serreE R CM i) = serreE R CM (σ i)) (hF : ∀ (i : B), g (serreF R CM i) = serreF R CM (σ i)) : g = (serreDiagramAut R CM hσ).toLieHom

TauCeti.serreDiagramAut is the unique homomorphism permuting the generators along σ.

@[simp]

theorem TauCeti.serreDiagramAut_refl {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) : serreDiagramAut R CM ⋯ = LieEquiv.refl

The identity permutation induces the identity automorphism.

@[simp]

theorem TauCeti.serreDiagramAut_trans {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {σ τ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) (hτ : CM.submatrix ⇑τ ⇑τ = CM) : (serreDiagramAut R CM hσ).trans (serreDiagramAut R CM hτ) = serreDiagramAut R CM ⋯

Diagram automorphisms compose along the composition of permutations.

@[simp]

theorem TauCeti.serreDiagramAut_symm {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) : (serreDiagramAut R CM hσ).symm = serreDiagramAut R CM ⋯

The inverse of a diagram automorphism is the diagram automorphism of the inverse permutation.

theorem TauCeti.serreDiagramAut_iterate_eq_id {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) {n : ℕ} (hn : σ ^ n = 1) : (⇑(serreDiagramAut R CM hσ))^[n] = id

A diagram automorphism has order dividing the order of its indexing permutation. If σ ^ n = 1, then applying the corresponding Serre automorphism n times is the identity.

This is stated using Function.iterate because endomorphism LieEquivs do not carry a group instance.

@[simp]

theorem TauCeti.serreLift_comp_serreDiagramAut {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] {σ : Equiv.Perm B} {H E F : B → L} (h : IsSerreSystem R CM H E F) (hσ : CM.submatrix ⇑σ ⇑σ = CM) : (serreLift h).comp (serreDiagramAut R CM hσ).toLieHom = serreLift ⋯

Naturality: any Serre system realising the presentation transports the diagram automorphism to the reindexed system.

The Chevalley involution

noncomputable def TauCeti.serreChevalleyInvolution {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) : Matrix.ToLieAlgebra R CM ≃ₗ⁅R⁆ Matrix.ToLieAlgebra R CM

The Chevalley involution of Matrix.ToLieAlgebra R CM: the automorphism Hᵢ ↦ -Hᵢ, Eᵢ ↦ -Fᵢ, Fᵢ ↦ -Eᵢ exchanging the raising and lowering generators with a sign.

Equations

• TauCeti.serreChevalleyInvolution R CM = { toLieHom := TauCeti.serreChevalleyHom✝ R CM, invFun := ⇑(TauCeti.serreChevalleyHom✝ R CM), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.serreChevalleyInvolution_serreH {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i : B) : (serreChevalleyInvolution R CM) (serreH R CM i) = -serreH R CM i

The Chevalley involution sends Hᵢ to -Hᵢ.

@[simp]

theorem TauCeti.serreChevalleyInvolution_serreE {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i : B) : (serreChevalleyInvolution R CM) (serreE R CM i) = -serreF R CM i

The Chevalley involution sends Eᵢ to -Fᵢ.

@[simp]

theorem TauCeti.serreChevalleyInvolution_serreF {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (i : B) : (serreChevalleyInvolution R CM) (serreF R CM i) = -serreE R CM i

The Chevalley involution sends Fᵢ to -Eᵢ.

theorem TauCeti.eq_serreChevalleyInvolution {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {g : Matrix.ToLieAlgebra R CM →ₗ⁅R⁆ Matrix.ToLieAlgebra R CM} (hH : ∀ (i : B), g (serreH R CM i) = -serreH R CM i) (hE : ∀ (i : B), g (serreE R CM i) = -serreF R CM i) (hF : ∀ (i : B), g (serreF R CM i) = -serreE R CM i) : g = (serreChevalleyInvolution R CM).toLieHom

TauCeti.serreChevalleyInvolution is the unique homomorphism exchanging the raising and lowering generators with a sign.

@[simp]

theorem TauCeti.serreChevalleyInvolution_serreChevalleyInvolution {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) (x : Matrix.ToLieAlgebra R CM) : (serreChevalleyInvolution R CM) ((serreChevalleyInvolution R CM) x) = x

Applying the Chevalley involution twice returns the original element.

theorem TauCeti.serreChevalleyInvolution_involutive {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) : Function.Involutive ⇑(serreChevalleyInvolution R CM)

The Chevalley involution is an involution.

@[simp]

theorem TauCeti.serreChevalleyInvolution_symm {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) : (serreChevalleyInvolution R CM).symm = serreChevalleyInvolution R CM

The Chevalley involution is its own inverse.

theorem TauCeti.serreChevalleyInvolution_comm_serreDiagramAut {B : Type u_1} [DecidableEq B] (R : Type u_2) [CommRing R] (CM : Matrix B B ℤ) {σ : Equiv.Perm B} (hσ : CM.submatrix ⇑σ ⇑σ = CM) : (serreChevalleyInvolution R CM).trans (serreDiagramAut R CM hσ) = (serreDiagramAut R CM hσ).trans (serreChevalleyInvolution R CM)

The Chevalley involution commutes with every diagram automorphism: both composites send Hᵢ to -H_{σ i}, Eᵢ to -F_{σ i} and Fᵢ to -E_{σ i}.

@[simp]

theorem TauCeti.serreLift_comp_serreChevalleyInvolution {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) : (serreLift h).comp (serreChevalleyInvolution R CM).toLieHom = serreLift ⋯

Naturality: any Serre system realising the presentation transports the Chevalley involution to the signed exchange of that system.