Renumbering the nodes of a Lie algebra basis

A LieAlgebra.Basis ι H is a Chevalley-style presentation of a Lie algebra: a Cartan matrix indexed by ι, three families h, e, f of elements indexed by ι, and the relations between them. Nothing in the structure depends on which index type is used, so a bijection ι ≃ ι' transports the whole package.

This is what lets a construction whose index set arises from the construction itself — Geck's, for instance, whose nodes are the support of a base, a subtype of the root index type — be read against an index type fixed in advance, such as Fin n in a pinned Bourbaki numbering. The Cartan matrix is renumbered by Matrix.submatrix, so the entry at renumbered nodes is by definition the entry at the corresponding original nodes and no reindexed copy of the matrix has to be compared with the original one.

Main definitions

• LieAlgebra.Basis.reindex: the basis obtained by renumbering the nodes along a bijection.

def LieAlgebra.Basis.reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {L : Type u_4} [Finite ι] [Finite ι'] [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} (b : Basis ι H) (σ : ι ≃ ι') : Basis ι' H

Renumber the nodes of a Lie algebra basis along a bijection. The Cartan matrix is renumbered by Matrix.submatrix, and each of the three families of elements is precomposed with the bijection.

Equations

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

@[simp]

theorem LieAlgebra.Basis.reindex_A {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {L : Type u_4} [Finite ι] [Finite ι'] [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} (b : Basis ι H) (σ : ι ≃ ι') : (b.reindex σ).A = b.A.submatrix ⇑σ.symm ⇑σ.symm

Reindexing transports the Cartan matrix along the given equivalence.

@[simp]

theorem LieAlgebra.Basis.reindex_h {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {L : Type u_4} [Finite ι] [Finite ι'] [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} (b : Basis ι H) (σ : ι ≃ ι') : (b.reindex σ).h = b.h ∘ ⇑σ.symm

Reindexing precomposes the Cartan generators with the given equivalence.

@[simp]

theorem LieAlgebra.Basis.reindex_e {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {L : Type u_4} [Finite ι] [Finite ι'] [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} (b : Basis ι H) (σ : ι ≃ ι') : (b.reindex σ).e = b.e ∘ ⇑σ.symm

Reindexing precomposes the raising generators with the given equivalence.

@[simp]

theorem LieAlgebra.Basis.reindex_f {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {L : Type u_4} [Finite ι] [Finite ι'] [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} (b : Basis ι H) (σ : ι ≃ ι') : (b.reindex σ).f = b.f ∘ ⇑σ.symm

Reindexing precomposes the lowering generators with the given equivalence.