Documentation

Mathlib.Algebra.Lie.Sl2

The Lie algebra sl₂ and its representations #

The Lie algebra sl₂ is the unique simple Lie algebra of minimal rank, 1, and as such occupies a distinguished position in the general theory. This file provides some basic definitions and results about sl₂.

Main definitions: #

structure IsSl2Triple {L : Type u_2} [LieRing L] (h : L) (e : L) (f : L) :

An sl₂ triple within a Lie ring L is a triple of elements h, e, f obeying relations which ensure that the Lie subalgebra they generate is equivalent to sl₂.

Instances For
    theorem IsSl2Triple.h_ne_zero {L : Type u_2} [LieRing L] {h : L} {e : L} {f : L} (self : IsSl2Triple h e f) :
    h 0
    theorem IsSl2Triple.lie_e_f {L : Type u_2} [LieRing L] {h : L} {e : L} {f : L} (self : IsSl2Triple h e f) :
    e, f = h
    theorem IsSl2Triple.lie_h_e_nsmul {L : Type u_2} [LieRing L] {h : L} {e : L} {f : L} (self : IsSl2Triple h e f) :
    h, e = 2 e
    theorem IsSl2Triple.lie_h_f_nsmul {L : Type u_2} [LieRing L] {h : L} {e : L} {f : L} (self : IsSl2Triple h e f) :
    h, f = -(2 f)
    theorem IsSl2Triple.symm {L : Type u_2} [LieRing L] {h : L} {e : L} {f : L} (ht : IsSl2Triple h e f) :
    IsSl2Triple (-h) f e
    @[simp]
    theorem IsSl2Triple.symm_iff {L : Type u_2} [LieRing L] {h : L} {e : L} {f : L} :
    theorem IsSl2Triple.lie_h_e_smul (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h : L} {e : L} {f : L} (t : IsSl2Triple h e f) :
    h, e = 2 e
    theorem IsSl2Triple.lie_lie_smul_f (R : Type u_1) {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {h : L} {e : L} {f : L} (t : IsSl2Triple h e f) :
    h, f = -(2 f)
    theorem IsSl2Triple.e_ne_zero {L : Type u_2} [LieRing L] {h : L} {e : L} {f : L} (t : IsSl2Triple h e f) :
    e 0
    theorem IsSl2Triple.f_ne_zero {L : Type u_2} [LieRing L] {h : L} {e : L} {f : L} (t : IsSl2Triple h e f) :
    f 0
    structure IsSl2Triple.HasPrimitiveVectorWith {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {h : L} {e : L} {f : L} (t : IsSl2Triple h e f) (m : M) (μ : R) :

    Given a representation of a Lie algebra with distinguished sl₂ triple, a vector is said to be primitive if it is a simultaneous eigenvector for the action of both h, e, and the eigenvalue for e is zero.

    Instances For
      theorem IsSl2Triple.HasPrimitiveVectorWith.ne_zero {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {h : L} {e : L} {f : L} {t : IsSl2Triple h e f} {m : M} {μ : R} (self : t.HasPrimitiveVectorWith m μ) :
      m 0
      theorem IsSl2Triple.HasPrimitiveVectorWith.lie_h {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {h : L} {e : L} {f : L} {t : IsSl2Triple h e f} {m : M} {μ : R} (self : t.HasPrimitiveVectorWith m μ) :
      h, m = μ m
      theorem IsSl2Triple.HasPrimitiveVectorWith.lie_e {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {h : L} {e : L} {f : L} {t : IsSl2Triple h e f} {m : M} {μ : R} (self : t.HasPrimitiveVectorWith m μ) :
      e, m = 0
      theorem IsSl2Triple.HasPrimitiveVectorWith.mk' {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h : L} {e : L} {f : L} [NoZeroSMulDivisors M] (t : IsSl2Triple h e f) (m : M) (μ : R) (ρ : R) (hm : m 0) (hm' : h, m = μ m) (he : e, m = ρ m) :
      t.HasPrimitiveVectorWith m μ

      Given a representation of a Lie algebra with distinguished sl₂ triple, a simultaneous eigenvector for the action of both h and e necessarily has eigenvalue zero for e.

      theorem IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h : L} {e : L} {f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) (n : ) :
      f, ((LieModule.toEnd R L M) f ^ n) m = ((LieModule.toEnd R L M) f ^ (n + 1)) m
      theorem IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h : L} {e : L} {f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) (n : ) :
      h, ((LieModule.toEnd R L M) f ^ n) m = (μ - 2 * n) ((LieModule.toEnd R L M) f ^ n) m
      theorem IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h : L} {e : L} {f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) (n : ) :
      e, ((LieModule.toEnd R L M) f ^ (n + 1)) m = ((n + 1) * (μ - n)) ((LieModule.toEnd R L M) f ^ n) m
      theorem IsSl2Triple.HasPrimitiveVectorWith.exists_nat {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h : L} {e : L} {f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) [IsNoetherian R M] [NoZeroSMulDivisors R M] [IsDomain R] [CharZero R] :
      ∃ (n : ), μ = n

      The eigenvalue of a primitive vector must be a natural number if the representation is finite-dimensional.

      theorem IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_ne_zero_of_eq_nat {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h : L} {e : L} {f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) [CharZero R] [NoZeroSMulDivisors R M] {n : } (hn : μ = n) {i : } (hi : i n) :
      ((LieModule.toEnd R L M) f ^ i) m 0
      theorem IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {h : L} {e : L} {f : L} {m : M} {μ : R} {t : IsSl2Triple h e f} (P : t.HasPrimitiveVectorWith m μ) [IsNoetherian R M] [NoZeroSMulDivisors R M] [IsDomain R] [CharZero R] {n : } (hn : μ = n) :
      ((LieModule.toEnd R L M) f ^ (n + 1)) m = 0