Block-diagonal actions of general linear Lie algebras

The block-diagonal map sends a matrix A : Matrix ι ι R to the matrix with one copy of A for each element of an auxiliary finite type κ. Restricting the standard gl (ι × κ) action along this map gives a gl ι action on every exterior power of ι × κ → R.

Main definitions

• TauCeti.glBlockDiagonal: the block-diagonal map from gl ι to gl (ι × κ).
• TauCeti.glBlockDiagonalLieRingModule and TauCeti.glBlockDiagonalLieModule: the induced action on exterior powers of the standard module.

def TauCeti.glBlockDiagonal (R : Type u_1) [CommRing R] (ι : Type u_2) [DecidableEq ι] [Fintype ι] (κ : Type u_3) [DecidableEq κ] [Fintype κ] : Matrix ι ι R →ₗ⁅R⁆ Matrix (ι × κ) (ι × κ) R

The block-diagonal map from gl ι to gl (ι × κ), sending a matrix A to the block diagonal matrix with κ copies of A down the diagonal. On the standard module ι × κ → R this is the action of gl ι on the first coordinate alone.

Equations

• TauCeti.glBlockDiagonal R ι κ = (AlgHom.mk' ((Matrix.blockDiagonalRingHom ι κ R).comp (Pi.constRingHom κ (Matrix ι ι R))) ⋯).toLieHom

@[simp]

theorem TauCeti.glBlockDiagonal_apply (R : Type u_1) [CommRing R] (ι : Type u_2) [DecidableEq ι] [Fintype ι] (κ : Type u_3) [DecidableEq κ] [Fintype κ] (A : Matrix ι ι R) : (glBlockDiagonal R ι κ) A = Matrix.blockDiagonal fun (x : κ) => A

theorem TauCeti.glBlockDiagonal_single {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {κ : Type u_3} [DecidableEq κ] [Fintype κ] (s t : ι) : (glBlockDiagonal R ι κ) (Matrix.single s t 1) = ∑ c : κ, Matrix.single (s, c) (t, c) 1

The block-diagonal map takes a matrix unit of gl ι to the sum, over the auxiliary coordinate, of the matrix units of gl (ι × κ) that move a cell from row t to row s and leave its column alone.

@[instance_reducible]

noncomputable def TauCeti.glBlockDiagonalLieRingModule (R : Type u_1) [CommRing R] (ι : Type u_2) [DecidableEq ι] [Fintype ι] (κ : Type u_3) [DecidableEq κ] [Fintype κ] (N : ℕ) : LieRingModule (Matrix ι ι R) ↥(⋀[R]^N (ι × κ → R))

The bracket of gl ι on an exterior power of ι × κ → R, pulled back along the block-diagonal map from the standard gl (ι × κ)-action.

Equations

• TauCeti.glBlockDiagonalLieRingModule R ι κ N = LieRingModule.compLieHom (↥(⋀[R]^N (ι × κ → R))) (TauCeti.glBlockDiagonal R ι κ)

theorem TauCeti.glBlockDiagonalLieModule (R : Type u_1) [CommRing R] (ι : Type u_2) [DecidableEq ι] [Fintype ι] (κ : Type u_3) [DecidableEq κ] [Fintype κ] (N : ℕ) : LieModule R (Matrix ι ι R) ↥(⋀[R]^N (ι × κ → R))

The compatibility of that bracket with the R-module structures, making an exterior power of ι × κ → R a gl ι-module over R.

theorem TauCeti.gl_lie_blockDiagonal_def {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {κ : Type u_3} [DecidableEq κ] [Fintype κ] {N : ℕ} (A : Matrix ι ι R) (x : ↥(⋀[R]^N (ι × κ → R))) : ⁅A, x⁆ = ⁅(glBlockDiagonal R ι κ) A, x⁆

The gl ι-action on an exterior power of ι × κ → R is the gl (ι × κ)-action of the block-diagonal image.

theorem TauCeti.gl_lie_single {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {κ : Type u_3} [DecidableEq κ] [Fintype κ] {N : ℕ} (s t : ι) (x : ↥(⋀[R]^N (ι × κ → R))) : ⁅Matrix.single s t 1, x⁆ = ∑ c : κ, ⁅Matrix.single (s, c) (t, c) 1, x⁆

A matrix unit of gl ι acts on an exterior power of ι × κ → R as the sum, over the auxiliary coordinate, of the matrix units of gl (ι × κ) it is built from.