Documentation

TauCeti.Algebra.Lie.NormTwoShell.Basic

The signed Lie algebra of the norm-two shell of an even lattice #

Let B : Matrix I I ℤ be the Gram matrix of the lattice Q = I → ℤ, with pairing ⟪a, b⟫ = a ⬝ᵥ B *ᵥ b, and let Φ = B.normTwoShell be its vectors of norm two. When B is the Cartan matrix of a simply laced Dynkin diagram, possibly disconnected, Φ is its root system and the construction below is the Frenkel--Kac construction of the corresponding simply laced Lie algebra over ℤ; no comparison with other constructions of that Lie algebra is made here. Its carrier ShellLieAlgebra B is Q × (Φ →₀ ℤ): a Cartan vector H_h for each h : Q (ShellLieAlgebra.cartan) and a root vector x_a for each a ∈ Φ (ShellLieAlgebra.root), which together give an integral basis (ShellLieAlgebra.basis). The bracket (ShellLieAlgebra.bracketBilin) is the bilinear map with ⁅H_h, H_k⁆ = 0, ⁅H_h, x_a⁆ = ⟪h, a⟫ x_a, and on root vectors (ShellLieAlgebra.rootBracket)

where ε(a, b) = (-1) ^ (B.orderedSignForm a b) is the ordered sign of Matrix.SignCover B.

The sign ε uses only the strictly lower triangular part of B, so ε(a, a) is not normalized to (-1) ^ (⟪a, a⟫ / 2). Correspondingly the opposite bracket ⁅x_a, x_(-a)⁆ is ε(a, -a) H_a, not -H_a: the vector x_(-a) indexed by -a ∈ Φ is a section vector, not the vector of the inverse lift of a to the cover.

The bracket is antisymmetric and alternating as soon as B is symmetric with even diagonal (ShellLieAlgebra.lie_skew, ShellLieAlgebra.lie_self): interchanging a and b changes ε by (-1) ^ ⟪a, b⟫. For B positive definite with even diagonal it satisfies the Jacobi identity over ℤ (ShellLieAlgebra.lie_jacobi), so it is a Lie ring (ShellLieAlgebra.lieRing) and hence a Lie algebra over ℤ. Positive definiteness confines the pairing of two roots that are neither equal nor opposite to {-1, 0, 1}, and the proof is a case analysis on these pairings for three root vectors, in which no division by 2 occurs.

Main definitions #

Main results #

References #

source
def Matrix.ShellLieAlgebra {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) :
Type u_1

The carrier Q × (Φ →₀ ℤ) of the signed Lie algebra of the norm-two shell Φ of an integer Gram matrix B on Q = I → ℤ: a Cartan part Q and a free root part with basis indexed by Φ. The bracket is Matrix.ShellLieAlgebra.bracketBilin.

Instances For
    source
    @[instance_reducible]
    noncomputable instance Matrix.ShellLieAlgebra.instAddCommGroup {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) :
    AddCommGroup B.ShellLieAlgebra
    source
    noncomputable def Matrix.ShellLieAlgebra.equivProd {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) :
    B.ShellLieAlgebra ≃ₗ[ℤ] (I → ℤ) × (↑B.normTwoShell →₀ ℤ)

    The identification of ShellLieAlgebra B with the product Q × (Φ →₀ ℤ) defining it.

    Instances For
      source
      noncomputable def Matrix.ShellLieAlgebra.cartan {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) :
      (I → ℤ) →ₗ[ℤ] B.ShellLieAlgebra

      The Cartan vector H_h of a lattice vector h, as a linear map Q →ₗ[ℤ] ShellLieAlgebra B.

      Instances For
        source
        noncomputable def Matrix.ShellLieAlgebra.root {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) (a : ↑B.normTwoShell) :
        B.ShellLieAlgebra

        The root vector x_a of a vector a of the norm-two shell.

        Instances For
          source
          @[simp]
          theorem Matrix.ShellLieAlgebra.equivProd_cartan {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) (h : I → ℤ) :
          (equivProd B) ((cartan B) h) = (h, 0)
          source
          theorem Matrix.ShellLieAlgebra.cartan_injective {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) :
          Function.Injective ⇑(cartan B)

          The Cartan embedding is injective.

          source
          @[simp]
          theorem Matrix.ShellLieAlgebra.equivProd_root {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) (a : ↑B.normTwoShell) :
          (equivProd B) (root B a) = (0, Finsupp.single a 1)
          source
          theorem Matrix.ShellLieAlgebra.equivProd_snd_eq_zero_iff {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) (x : B.ShellLieAlgebra) :
          ((equivProd B) x).2 = 0 ↔ x = (cartan B) ((equivProd B) x).1

          Vanishing of the root component is equivalent to being the recovered Cartan vector.

          source
          noncomputable def Matrix.ShellLieAlgebra.basis {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) :
          Module.Basis (I ⊕ ↑B.normTwoShell) ℤ B.ShellLieAlgebra

          The integral basis of ShellLieAlgebra B: the Cartan vectors H_(αᵢ) of the coordinate vectors αᵢ = Pi.single i 1, followed by the root vectors x_a.

          Instances For
            source
            @[simp]
            theorem Matrix.ShellLieAlgebra.basis_inl {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) [DecidableEq I] (i : I) :
            (basis B) (Sum.inl i) = (cartan B) (Pi.single i 1)
            source
            @[simp]
            theorem Matrix.ShellLieAlgebra.basis_inr {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) (a : ↑B.normTwoShell) :
            (basis B) (Sum.inr a) = root B a
            source
            instance Matrix.ShellLieAlgebra.instFreeInt {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) :
            Module.Free ℤ B.ShellLieAlgebra

            The signed shell Lie algebra is free over ℤ, with basis Matrix.ShellLieAlgebra.basis.

            source
            instance Matrix.ShellLieAlgebra.instFiniteIntOfFiniteElemForallNormTwoShell {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) [Finite ↑B.normTwoShell] :
            Module.Finite ℤ B.ShellLieAlgebra

            The signed shell Lie algebra is finite over ℤ when its norm-two shell is finite, as it is for a positive definite B (Matrix.PosDef.finite_normTwoShell).

            source
            theorem Matrix.ShellLieAlgebra.cartan_add_sum_root_eq {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) [Fintype ↑B.normTwoShell] (x : B.ShellLieAlgebra) :
            (cartan B) ((equivProd B) x).1 + ∑ a : ↑B.normTwoShell, ((equivProd B) x).2 a • root B a = x

            Every element x of ShellLieAlgebra B is the sum H_h + ∑_(a ∈ Φ) c_a x_a of the Cartan vector of its Cartan part h and the root vectors weighted by its root coefficients c.

            source
            @[simp]
            theorem Matrix.ShellLieAlgebra.basis_repr_cartan_inl {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) (h : I → ℤ) (i : I) :
            ((basis B).repr ((cartan B) h)) (Sum.inl i) = h i

            A Cartan vector has its original lattice coordinates in the Cartan part of the shell basis.

            source
            @[simp]
            theorem Matrix.ShellLieAlgebra.basis_repr_root {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) (a : ↑B.normTwoShell) :
            (basis B).repr (root B a) = Finsupp.single (Sum.inr a) 1

            The coordinates of an integral root vector in the Cartan-and-root basis.

            source
            @[simp]
            theorem Matrix.ShellLieAlgebra.basis_repr_cartan_inr {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) (h : I → ℤ) (a : ↑B.normTwoShell) :
            ((basis B).repr ((cartan B) h)) (Sum.inr a) = 0

            The coordinates of an integral Cartan vector vanish on every root index.

            source
            noncomputable def Matrix.ShellLieAlgebra.rootBracket {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) [LinearOrder I] (a b : ↑B.normTwoShell) :
            B.ShellLieAlgebra

            The bracket ⁅x_a, x_b⁆ of two root vectors: ε(a, b) x_(a + b) if a + b is in the norm-two shell, ε(a, b) H_a if a + b = 0, and 0 otherwise, where ε(a, b) is the ordered sign (B.orderedSignForm a b).negOnePow.

            Instances For
              source
              @[simp]
              theorem Matrix.ShellLieAlgebra.rootBracket_of_mem {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] {a b : ↑B.normTwoShell} (h : ↑a + ↑b ∈ B.normTwoShell) :
              rootBracket B a b = ((B.orderedSignForm ↑a) ↑b).negOnePow • root B ⟨↑a + ↑b, h⟩

              The bracket of two root vectors whose sum is in the norm-two shell.

              source
              @[simp]
              theorem Matrix.ShellLieAlgebra.rootBracket_of_add_eq_zero {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] {a b : ↑B.normTwoShell} (h : ↑a + ↑b = 0) :
              rootBracket B a b = ((B.orderedSignForm ↑a) ↑b).negOnePow • (cartan B) ↑a

              The bracket of two opposite root vectors.

              source
              @[simp]
              theorem Matrix.ShellLieAlgebra.rootBracket_of_notMem_of_add_ne_zero {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] {a b : ↑B.normTwoShell} (h : ↑a + ↑b ∉ B.normTwoShell) (h' : ↑a + ↑b ≠ 0) :
              rootBracket B a b = 0

              Two root vectors whose sum is neither in the norm-two shell nor zero have bracket zero.

              source
              @[simp]
              theorem Matrix.ShellLieAlgebra.basis_repr_rootBracket_inl {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (a b : ↑B.normTwoShell) (i : I) :
              ((basis B).repr (rootBracket B a b)) (Sum.inl i) = if ↑a + ↑b = 0 then ↑((B.orderedSignForm ↑a) ↑b).negOnePow * ↑a i else 0

              Only opposite roots contribute to the Cartan coordinates of a root bracket.

              source
              @[simp]
              theorem Matrix.ShellLieAlgebra.basis_repr_rootBracket_inr {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (a b c : ↑B.normTwoShell) :
              ((basis B).repr (rootBracket B a b)) (Sum.inr c) = if ↑a + ↑b = ↑c then ↑((B.orderedSignForm ↑a) ↑b).negOnePow else 0

              The coefficient of x_c in a root bracket is its ordered sign exactly when the two roots sum to c.

              source
              theorem Matrix.ShellLieAlgebra.rootBracket_eq_zero_of_nonneg {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (hB : B.IsSymm) {a b : ↑B.normTwoShell} (h : 0 ≤ ↑a ⬝ᵥ B.mulVec ↑b) :
              rootBracket B a b = 0

              For a symmetric B, two root vectors whose roots have nonnegative pairing have bracket zero: the sum of the roots then has norm at least 4.

              source
              noncomputable def Matrix.ShellLieAlgebra.bracketBilin {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) [LinearOrder I] :
              B.ShellLieAlgebra →ₗ[ℤ] B.ShellLieAlgebra →ₗ[ℤ] B.ShellLieAlgebra

              The bracket of ShellLieAlgebra B, as the bilinear map determined on the integral basis by ⁅H_h, H_k⁆ = 0, ⁅H_h, x_b⁆ = ⟪h, b⟫ x_b, ⁅x_a, H_k⁆ = -⟪k, a⟫ x_a and ⁅x_a, x_b⁆ = rootBracket B a b.

              Instances For
                source
                @[instance_reducible]
                noncomputable instance Matrix.ShellLieAlgebra.instBracket {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) [LinearOrder I] :
                Bracket B.ShellLieAlgebra B.ShellLieAlgebra

                The bracket of ShellLieAlgebra B is Matrix.ShellLieAlgebra.bracketBilin. It is a Lie bracket for positive definite B with even diagonal, see Matrix.ShellLieAlgebra.lieRing.

                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.bracketBilin_apply_apply {I : Type u_1} [Fintype I] (B : Matrix I I ℤ) [LinearOrder I] (x y : B.ShellLieAlgebra) :
                ((bracketBilin B) x) y = ⁅x, y⁆
                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.add_lie {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (x y z : B.ShellLieAlgebra) :
                ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.lie_add {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (x y z : B.ShellLieAlgebra) :
                ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.smul_lie {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (n : ℤ) (x y : B.ShellLieAlgebra) :
                ⁅n • x, y⁆ = n • ⁅x, y⁆
                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.lie_smul {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (n : ℤ) (x y : B.ShellLieAlgebra) :
                ⁅x, n • y⁆ = n • ⁅x, y⁆
                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.cartan_lie_cartan {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (h k : I → ℤ) :
                ⁅(cartan B) h, (cartan B) k⁆ = 0

                Cartan vectors commute.

                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.cartan_lie_root {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (h : I → ℤ) (b : ↑B.normTwoShell) :
                ⁅(cartan B) h, root B b⁆ = (h ⬝ᵥ B.mulVec ↑b) • root B b

                The Cartan vector H_h acts on the root vector x_b by the pairing ⟪h, b⟫.

                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.equivProd_cartan_lie_snd {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (h : I → ℤ) (x : B.ShellLieAlgebra) (a : ↑B.normTwoShell) :
                ((equivProd B) ⁅(cartan B) h, x⁆).2 a = h ⬝ᵥ B.mulVec ↑a * ((equivProd B) x).2 a

                The coefficient of a root in a Cartan bracket is its root pairing times its coefficient.

                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.root_lie_cartan {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (a : ↑B.normTwoShell) (k : I → ℤ) :
                ⁅root B a, (cartan B) k⁆ = -((k ⬝ᵥ B.mulVec ↑a) • root B a)

                The bracket ⁅x_a, H_k⁆ = -⟪k, a⟫ x_a.

                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.root_lie_root {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (a b : ↑B.normTwoShell) :
                ⁅root B a, root B b⁆ = rootBracket B a b

                The bracket of two root vectors is their root bracket.

                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.zero_lie {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (y : B.ShellLieAlgebra) :
                ⁅0, y⁆ = 0
                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.lie_zero {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (x : B.ShellLieAlgebra) :
                ⁅x, 0⁆ = 0
                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.neg_lie {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (x y : B.ShellLieAlgebra) :
                ⁅-x, y⁆ = -⁅x, y⁆
                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.lie_neg {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (x y : B.ShellLieAlgebra) :
                ⁅x, -y⁆ = -⁅x, y⁆
                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.units_smul_lie {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (u : ℤˣ) (x y : B.ShellLieAlgebra) :
                ⁅u • x, y⁆ = u • ⁅x, y⁆
                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.lie_units_smul {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (u : ℤˣ) (x y : B.ShellLieAlgebra) :
                ⁅x, u • y⁆ = u • ⁅x, y⁆
                source
                @[simp]
                theorem Matrix.ShellLieAlgebra.cartan_lie_rootBracket {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (h : I → ℤ) (a b : ↑B.normTwoShell) :
                ⁅(cartan B) h, rootBracket B a b⁆ = (h ⬝ᵥ B.mulVec (↑a + ↑b)) • rootBracket B a b

                The Cartan weight of a root bracket. The bracket of two root vectors has weight the sum of their roots.

                source
                theorem Matrix.ShellLieAlgebra.rootBracket_swap {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (hB : B.IsSymm) (hdiag : ∀ (i : I), Even (B i i)) (a b : ↑B.normTwoShell) :
                rootBracket B b a = -rootBracket B a b

                Antisymmetry of the root bracket, for a symmetric B with even diagonal: interchanging the two roots changes the ordered sign exactly when the roots pair to an odd integer.

                source
                theorem Matrix.ShellLieAlgebra.lie_skew {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (hB : B.IsSymm) (hdiag : ∀ (i : I), Even (B i i)) (x y : B.ShellLieAlgebra) :
                ⁅y, x⁆ = -⁅x, y⁆

                Antisymmetry of the bracket, for a symmetric B with even diagonal.

                source
                theorem Matrix.ShellLieAlgebra.lie_self {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (hB : B.IsSymm) (hdiag : ∀ (i : I), Even (B i i)) (x : B.ShellLieAlgebra) :
                ⁅x, x⁆ = 0

                The bracket is alternating, for a symmetric B with even diagonal.

                The Jacobi identity #

                source
                theorem Matrix.ShellLieAlgebra.lie_jacobi {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (hB : B.PosDef) (hdiag : ∀ (i : I), Even (B i i)) (x y z : B.ShellLieAlgebra) :
                ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0

                The Jacobi identity, for a positive definite B with even diagonal.

                source
                theorem Matrix.ShellLieAlgebra.leibniz_lie {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (hB : B.PosDef) (hdiag : ∀ (i : I), Even (B i i)) (x y z : B.ShellLieAlgebra) :
                ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆

                The Leibniz form of the Jacobi identity, for a positive definite B with even diagonal.

                source
                @[instance_reducible]
                noncomputable def Matrix.ShellLieAlgebra.lieRing {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] (hB : B.PosDef) (hdiag : ∀ (i : I), Even (B i i)) :
                LieRing B.ShellLieAlgebra

                The signed Lie ring of the norm-two shell of a positive definite integer matrix B with even diagonal. Install it locally from explicit hypotheses, or use instLieRingOfFact when the hypotheses are available as typeclass facts.

                Instances For
                  source
                  @[instance_reducible]
                  noncomputable instance Matrix.ShellLieAlgebra.instLieRingOfFact {I : Type u_1} [Fintype I] {B : Matrix I I ℤ} [LinearOrder I] [hB : Fact B.PosDef] [hev : Fact (∀ (i : I), Even (B i i))] :
                  LieRing B.ShellLieAlgebra

                  The signed shell Lie ring, with positivity and evenness supplied as typeclass facts.