Documentation

TauCeti.LinearAlgebra.RootSystem.SimplyConnectedRootDatum.C.Classical

Classical coordinates on the pinned type Cₙ lattices #

The pinned type Cₙ datum TauCeti.DynkinType.typeCSimplyConnectedRootDatum writes its character lattice in the fundamental-weight basis and its cocharacter lattice in the simple-coroot basis. Both lattices are also the classical lattice ℤ ^ n with standard basis e₀, …, e_{n-1}, because the simple coroots eᵢ - eᵢ₊₁ and e_{n-1} of Cₙ form a basis of it. This file makes that identification explicit, in the form a concrete group with diagonal torus 𝔾ₘⁿ consumes.

The change of coordinates on characters sends λ to its pairings (⟨λ, e_a⟩)_a with the classical basis, and the one on cocharacters sends μ to (⟨e_a, μ⟩)_a. They send the families TauCeti.DynkinType.TypeC.weight and TauCeti.DynkinType.TypeC.coweight to the standard basis vectors and carry the pinned dot-product pairing to the classical one. Both are integral with integral inverse, since the matrices of the two families are inverse transposes of one another by TauCeti.DynkinType.TypeC.weight_dotProduct_coweight.

Main definitions #

Main results #

References #

N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate III.

source
noncomputable def TauCeti.DynkinType.TypeC.classicalWeightEquiv (n : ℕ) :
(Fin n → ℤ) ≃ₗ[ℤ] Fin n → ℤ

Classical coordinates on the pinned type Cₙ character lattice. A character λ, written in the fundamental-weight basis, is sent to its pairings (⟨λ, e_a⟩)_a with the classical basis.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def TauCeti.DynkinType.TypeC.classicalCoweightEquiv (n : ℕ) :
    (Fin n → ℤ) ≃ₗ[ℤ] Fin n → ℤ

    Classical coordinates on the pinned type Cₙ cocharacter lattice. A cocharacter μ, written in the simple-coroot basis, is sent to its pairings (⟨e_a, μ⟩)_a with the classical basis.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.DynkinType.TypeC.classicalWeightEquiv_apply {n : ℕ} (x : Fin n → ℤ) (a : Fin n) :
      (classicalWeightEquiv n) x a = x ⬝ᵥ coweight n ↑a

      The a-th classical coordinate of a character is its pairing with e_a.

      source
      @[simp]
      theorem TauCeti.DynkinType.TypeC.classicalCoweightEquiv_apply {n : ℕ} (y : Fin n → ℤ) (a : Fin n) :
      (classicalCoweightEquiv n) y a = weight n ↑a ⬝ᵥ y

      The a-th classical coordinate of a cocharacter is the pairing of e_a with it.

      source
      @[simp]
      theorem TauCeti.DynkinType.TypeC.classicalWeightEquiv_weight {n : ℕ} (a : Fin n) :
      (classicalWeightEquiv n) (weight n ↑a) = Pi.single a 1

      The character e_a has the a-th standard basis vector as classical coordinates.

      source
      @[simp]
      theorem TauCeti.DynkinType.TypeC.classicalCoweightEquiv_coweight {n : ℕ} (a : Fin n) :
      (classicalCoweightEquiv n) (coweight n ↑a) = Pi.single a 1

      The cocharacter e_a has the a-th standard basis vector as classical coordinates.

      source
      @[simp]
      theorem TauCeti.DynkinType.TypeC.classicalWeightEquiv_symm_single {n : ℕ} (a : Fin n) :
      (classicalWeightEquiv n).symm (Pi.single a 1) = weight n ↑a

      The a-th standard basis vector of classical coordinates is the character e_a.

      source
      @[simp]
      theorem TauCeti.DynkinType.TypeC.classicalCoweightEquiv_symm_single {n : ℕ} (a : Fin n) :
      (classicalCoweightEquiv n).symm (Pi.single a 1) = coweight n ↑a

      The a-th standard basis vector of classical coordinates is the cocharacter e_a.

      source
      @[simp]
      theorem TauCeti.DynkinType.TypeC.classicalWeightEquiv_dotProduct_classicalCoweightEquiv {n : ℕ} (x y : Fin n → ℤ) :
      (classicalWeightEquiv n) x ⬝ᵥ (classicalCoweightEquiv n) y = x ⬝ᵥ y

      The classical coordinates preserve the pairing. The pinned dot product of a character and a cocharacter is the dot product of their classical coordinates.