Documentation

TauCeti.LinearAlgebra.RootSystem.Isomorphism

Root systems of the same Dynkin type are isomorphic #

The Cartan-Killing classification has two halves. One is combinatorial: the Cartan matrix of a base of an irreducible reduced crystallographic finite root system is, after relabelling the nodes, one of the standard matrices TauCeti.DynkinType.cartanMatrix. The other is the rigidity statement that the type is a complete invariant, and this file supplies it: two root systems carrying bases of the same Dynkin type are isomorphic as root pairings.

Nothing here re-proves rigidity. Mathlib's RootPairing.Base.equivOfCartanMatrixEq already builds an isomorphism from a relabelling matching the two Cartan matrices, and TauCeti.HasCartanType.exists_supportEquiv_cartanMatrix_eq is what supplies such a relabelling: two bases of type t are each labelled by the nodes of t, and composing the two labellings identifies their supports compatibly with the Cartan matrices.

Main results #

References #

This file proves nonempty_equiv_of_hasCartanType, the final isomorphism step of Layer 5 of TauCetiRoadmap/RepresentationTheory/RootSystems/README.md, following the target signature in TauCetiRoadmap/RepresentationTheory/RootSystems/Suggested.lean. See Bourbaki, Lie Groups and Lie Algebras, Chapters 4-6, chapter VI, §4, and Humphreys, Introduction to Lie Algebras and Representation Theory, §11.1, for the isomorphism theorem in the classical language.

source
@[simp]
theorem TauCeti.equivOfCartanMatrixEq_indexEquiv_apply {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} [CharZero R] [IsDomain R] [Finite ι] [Finite ι₂] [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] [P₂.IsRootSystem] [P₂.IsCrystallographic] [P₂.IsReduced] (b : P.Base) (b₂ : P₂.Base) (e : ↥b.support ≃ ↥b₂.support) (he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j) (i : ↥b.support) :
(↑(b.equivOfCartanMatrixEq b₂ e he)).indexEquiv ↑i = ↑(e i)

The root-index equivalence constructed from a relabelling of equal Cartan matrices restricts to that relabelling on the chosen simple roots.

Mathlib constructs the equivalence on all root indices by transporting the roots through the linear equivalence between the two simple-root bases. This theorem exposes the resulting value on a simple root, so consumers do not have to unfold that construction.

source
@[simp]
theorem TauCeti.equivOfCartanMatrixEq_coweightEquiv_symm_apply_coroot {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} [CharZero R] [IsDomain R] [Finite ι] [Finite ι₂] [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] [P₂.IsRootSystem] [P₂.IsCrystallographic] [P₂.IsReduced] (b : P.Base) (b₂ : P₂.Base) (e : ↥b.support ≃ ↥b₂.support) (he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j) (i : ↥b.support) :
(b.equivOfCartanMatrixEq b₂ e he).coweightEquiv.symm (P.coroot ↑i) = P₂.coroot ↑(e i)

The covariant inverse coweight equivalence constructed from equal Cartan matrices sends a chosen simple coroot to the simple coroot selected by the supplied relabelling.

source
@[simp]
theorem TauCeti.map_equivOfCartanMatrixEq {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} [CharZero R] [IsDomain R] [Finite ι] [Finite ι₂] [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] [P₂.IsRootSystem] [P₂.IsCrystallographic] [P₂.IsReduced] (b : P.Base) (b₂ : P₂.Base) (e : ↥b.support ≃ ↥b₂.support) (he : ∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j) :
b.map (b.equivOfCartanMatrixEq b₂ e he) = b₂

Transporting a base along the root-system equivalence constructed from equal Cartan matrices gives the target base exactly. Thus the construction remembers the supplied simple-root relabelling as an equivalence of based root systems.

source
theorem TauCeti.nonempty_equiv_of_hasCartanType {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {M : Type u_4} {N : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N} {P₂ : RootPairing ι₂ R M₂ N₂} [CharZero R] [IsDomain R] [Finite ι] [Finite ι₂] [P.IsRootSystem] [P.IsCrystallographic] [P.IsReduced] [P₂.IsRootSystem] [P₂.IsCrystallographic] [P₂.IsReduced] (b : P.Base) (b₂ : P₂.Base) (t : DynkinType) (h : HasCartanType P b t) (h₂ : HasCartanType P₂ b₂ t) :
Nonempty (P.Equiv P₂)

Two root systems carrying bases of the same Cartan type are isomorphic. This is the rigidity half of the Cartan-Killing classification: the Dynkin type is not merely an invariant of a finite reduced crystallographic root system, it is a complete one.

Only the existence of an isomorphism is asserted. The isomorphism produced depends on the two labellings of the supports by the nodes of t, which TauCeti.HasCartanType quantifies existentially, so there is no canonical choice to name; a caller that needs one destructures the two HasCartanType witnesses and applies RootPairing.Base.equivOfCartanMatrixEq itself.