Documentation

TauCeti.Algebra.Lie.GeneralLinear.Embedding

Corner embeddings of general linear Lie algebras #

An injection f : m ↪ n of finite index types embeds gl m in gl n as the matrices supported on the rows and columns in the range of f: a matrix A : Matrix m m R goes to the matrix with A a b in position (f a, f b) and zeros elsewhere. For Fin k ↪ Fin n given by Fin.castLE this is the upper-left corner gl k ⊆ gl n, and the chain of these corners gl 1 ⊆ gl 2 ⊆ ⋯ ⊆ gl n is the one along which Gelfand-Tsetlin theory restricts.

The map is conjugation A ↦ P * A * Pᵀ by the n × m matrix P of the embedding, whose column a is the standard basis vector at f a. Since f is injective, Pᵀ * P = 1, so this is multiplicative and in particular preserves commutators. It does not preserve the identity unless f is surjective, so it is a Lie algebra homomorphism but not an algebra homomorphism.

Main definitions #

Main results #

source
def TauCeti.glEmbedding (R : Type u_1) [CommRing R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : m ↪ n) :
Matrix m m R →ₗ⁅R⁆ Matrix n n R

The corner embedding gl m → gl n of an injection f : m ↪ n, sending a matrix A to the matrix with A a b in position (f a, f b) and zeros elsewhere.

Instances For
    source
    theorem TauCeti.glEmbedding_apply {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : m ↪ n) (A : Matrix m m R) :
    (glEmbedding R f) A = Matrix.submatrix 1 id ⇑f * A * Matrix.submatrix 1 (⇑f) id

    The corner embedding is conjugation by the n × m matrix of the injection, whose column a is the standard basis vector at f a.

    source
    @[simp]
    theorem TauCeti.glEmbedding_single {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : m ↪ n) (a b : m) (c : R) :
    (glEmbedding R f) (Matrix.single a b c) = Matrix.single (f a) (f b) c

    The corner embedding sends a matrix unit to the matrix unit at the image indices.

    source
    theorem TauCeti.glEmbedding_eq_sum_single {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : m ↪ n) (A : Matrix m m R) :
    (glEmbedding R f) A = ∑ a : m, ∑ b : m, Matrix.single (f a) (f b) (A a b)

    The corner embedding of A is the sum of the matrix units at the image indices, weighted by the entries of A.

    source
    @[simp]
    theorem TauCeti.glEmbedding_apply_apply {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : m ↪ n) (A : Matrix m m R) (a b : m) :
    (glEmbedding R f) A (f a) (f b) = A a b

    The entries of the corner embedding at the image indices are those of the source matrix.

    source
    theorem TauCeti.glEmbedding_apply_apply_of_notMem_range_left {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : m ↪ n) (A : Matrix m m R) {a : n} (ha : a ∉ Set.range ⇑f) (b : n) :
    (glEmbedding R f) A a b = 0

    The rows of the corner embedding outside the image of the injection vanish.

    source
    theorem TauCeti.glEmbedding_apply_apply_of_notMem_range_right {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : m ↪ n) (A : Matrix m m R) (a : n) {b : n} (hb : b ∉ Set.range ⇑f) :
    (glEmbedding R f) A a b = 0

    The columns of the corner embedding outside the image of the injection vanish.

    source
    theorem TauCeti.glEmbedding_injective {R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : m ↪ n) :
    Function.Injective ⇑(glEmbedding R f)

    The corner embedding is injective.

    source
    @[simp]
    theorem TauCeti.glEmbedding_refl {R : Type u_1} [CommRing R] {m : Type u_3} [Fintype m] [DecidableEq m] :
    glEmbedding R (Function.Embedding.refl m) = LieHom.id

    The corner embedding of the identity injection is the identity.

    source
    theorem TauCeti.glEmbedding_trans {R : Type u_1} [CommRing R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [Fintype l] [DecidableEq l] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (f : l ↪ m) (g : m ↪ n) :
    glEmbedding R (f.trans g) = (glEmbedding R g).comp (glEmbedding R f)

    The corner embedding of a composite of injections is the composite of the corner embeddings.