Products of Lie modules

Mathlib gives the product of two Lie algebras its Lie ring structure (Mathlib/Algebra/Lie/Prod.lean) and the direct sum of a family of Lie modules its Lie module structure (Mathlib/Algebra/Lie/DirectSum.lean), but not the binary product of two Lie modules over a fixed Lie algebra. This file supplies it: for L-modules M and N, the componentwise bracket makes M × N an L-module, and the four maps fst, snd, inl, inr are morphisms of L-modules.

The binary product is what an argument comparing two Lie modules of different types needs: the direct sum ⨁ i, M i of a family forces all the summands into one universe, whereas M × N does not. The first consumer is the uniqueness of the irreducible highest weight module of a given weight, which compares two such modules by cutting out the graph of an isomorphism inside their product.

Main definitions

• Ado.LieModuleHom.fst and Ado.LieModuleHom.snd: the two projections.
• Ado.LieModuleHom.inl and Ado.LieModuleHom.inr: the two inclusions.
• Ado.LieModuleHom.prod: the pairing of two morphisms with the same domain.
• Ado.LieModuleEquiv.prodComm: swapping the factors is an equivalence.
• Ado.lie_prod_apply: the componentwise bracket on a product.
• LieHom.prodRepresentation: the product of two explicit Lie representations.
• LieHom.piRepresentation: the product of a family of explicit Lie representations.

@[instance_reducible]

instance Ado.Prod.instLieRingModule {L : Type v} {M : Type w} {N : Type w₁} [LieRing L] [AddCommGroup M] [LieRingModule L M] [AddCommGroup N] [LieRingModule L N] : LieRingModule L (M × N)

The componentwise bracket makes the product of two L-modules an L-module.

Equations

• Ado.Prod.instLieRingModule = { bracket := fun (x : L) (p : M × N) => (⁅x, p.1⁆, ⁅x, p.2⁆), add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

instance Ado.Prod.instLieModule {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieAlgebra R L] [LieModule R L M] [LieModule R L N] : LieModule R L (M × N)

@[simp]

theorem Ado.lie_prod_apply {L : Type v} {M : Type w} {N : Type w₁} [LieRing L] [AddCommGroup M] [LieRingModule L M] [AddCommGroup N] [LieRingModule L N] (x : L) (p : M × N) : ⁅x, p⁆ = (⁅x, p.1⁆, ⁅x, p.2⁆)

def Ado.LieModuleHom.fst (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] : M × N →ₗ⁅R,L⁆ M

The projection of a product of Lie modules onto its first factor.

Equations

• Ado.LieModuleHom.fst R L M N = { toLinearMap := LinearMap.fst R M N, map_lie' := ⋯ }

def Ado.LieModuleHom.snd (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] : M × N →ₗ⁅R,L⁆ N

The projection of a product of Lie modules onto its second factor.

Equations

• Ado.LieModuleHom.snd R L M N = { toLinearMap := LinearMap.snd R M N, map_lie' := ⋯ }

def Ado.LieModuleHom.inl (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] : M →ₗ⁅R,L⁆ M × N

The inclusion of the first factor into a product of Lie modules.

Equations

• Ado.LieModuleHom.inl R L M N = { toLinearMap := LinearMap.inl R M N, map_lie' := ⋯ }

def Ado.LieModuleHom.inr (R : Type u) (L : Type v) (M : Type w) (N : Type w₁) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] : N →ₗ⁅R,L⁆ M × N

The inclusion of the second factor into a product of Lie modules.

Equations

• Ado.LieModuleHom.inr R L M N = { toLinearMap := LinearMap.inr R M N, map_lie' := ⋯ }

def Ado.LieModuleHom.prod {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {P : Type u_1} [AddCommGroup P] [Module R P] [LieRingModule L P] (f : P →ₗ⁅R,L⁆ M) (g : P →ₗ⁅R,L⁆ N) : P →ₗ⁅R,L⁆ M × N

Pair two morphisms of Lie modules with the same domain.

Equations

• Ado.LieModuleHom.prod f g = { toLinearMap := (↑f).prod ↑g, map_lie' := ⋯ }

@[simp]

theorem Ado.LieModuleHom.fst_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (p : M × N) : (fst R L M N) p = p.1

@[simp]

theorem Ado.LieModuleHom.snd_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (p : M × N) : (snd R L M N) p = p.2

@[simp]

theorem Ado.LieModuleHom.inl_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (m : M) : (inl R L M N) m = (m, 0)

@[simp]

theorem Ado.LieModuleHom.inr_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (n : N) : (inr R L M N) n = (0, n)

@[simp]

theorem Ado.LieModuleHom.prod_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {P : Type u_1} [AddCommGroup P] [Module R P] [LieRingModule L P] (f : P →ₗ⁅R,L⁆ M) (g : P →ₗ⁅R,L⁆ N) (p : P) : (prod f g) p = (f p, g p)

@[simp]

theorem Ado.LieModuleHom.fst_prod {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {P : Type u_1} [AddCommGroup P] [Module R P] [LieRingModule L P] (f : P →ₗ⁅R,L⁆ M) (g : P →ₗ⁅R,L⁆ N) : (fst R L M N).comp (prod f g) = f

@[simp]

theorem Ado.LieModuleHom.snd_prod {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] {P : Type u_1} [AddCommGroup P] [Module R P] [LieRingModule L P] (f : P →ₗ⁅R,L⁆ M) (g : P →ₗ⁅R,L⁆ N) : (snd R L M N).comp (prod f g) = g

def Ado.LieModuleEquiv.prodComm {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] : M × N ≃ₗ⁅R,L⁆ N × M

Swapping the factors is an equivalence of product Lie modules.

Equations

• Ado.LieModuleEquiv.prodComm = { toLinearMap := ↑(LinearEquiv.prodComm R M N), map_lie' := ⋯, invFun := (LinearEquiv.prodComm R M N).invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Ado.LieModuleEquiv.prodComm_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (p : M × N) : prodComm p = p.swap

@[simp]

theorem Ado.LieModuleEquiv.coe_prodComm_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup N] [Module R N] [LieRingModule L N] (p : M × N) : prodComm.toLieModuleHom p = p.swap

def LieHom.prodRepresentation {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rho : L →ₗ⁅R⁆ Module.End R M) (sigma : L →ₗ⁅R⁆ Module.End R N) : L →ₗ⁅R⁆ Module.End R (M × N)

The product of two Lie representations, acting componentwise on the product of their carriers.

Equations

• rho.prodRepresentation sigma = (LinearMap.prodMapAlgHom R M N).toLieHom.comp (rho.prod sigma)

@[simp]

theorem LieHom.prodRepresentation_apply {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rho : L →ₗ⁅R⁆ Module.End R M) (sigma : L →ₗ⁅R⁆ Module.End R N) (x : L) (p : M × N) : ((rho.prodRepresentation sigma) x) p = ((rho x) p.1, (sigma x) p.2)

The product representation acts componentwise.

@[simp]

theorem LieHom.ker_prodRepresentation {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rho : L →ₗ⁅R⁆ Module.End R M) (sigma : L →ₗ⁅R⁆ Module.End R N) : (rho.prodRepresentation sigma).ker = rho.ker ⊓ sigma.ker

The kernel of a product representation is the intersection of the two kernels.

theorem LieHom.prodRepresentation_injective_iff {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (rho : L →ₗ⁅R⁆ Module.End R M) (sigma : L →ₗ⁅R⁆ Module.End R N) : Function.Injective ⇑(rho.prodRepresentation sigma) ↔ Disjoint rho.ker sigma.ker

A product representation is faithful exactly when the kernels of its factors are disjoint.

def LieHom.piRepresentation {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I : Type i} {V : I → Type w₂} [(j : I) → AddCommGroup (V j)] [(j : I) → Module R (V j)] (rho : (j : I) → L →ₗ⁅R⁆ Module.End R (V j)) : L →ₗ⁅R⁆ Module.End R ((j : I) → V j)

The product of a family of Lie representations, acting coordinatewise on the dependent function space. For a finite index type, this product representation is canonically equivalent to the corresponding finite direct-sum representation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LieHom.piRepresentation_apply {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I : Type i} {V : I → Type w₂} [(j : I) → AddCommGroup (V j)] [(j : I) → Module R (V j)] (rho : (j : I) → L →ₗ⁅R⁆ Module.End R (V j)) (x : L) (m : (j : I) → V j) (j : I) : ((piRepresentation rho) x) m j = ((rho j) x) (m j)

A product representation acts coordinatewise.

@[simp]

theorem LieHom.ker_piRepresentation {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I : Type i} {V : I → Type w₂} [(j : I) → AddCommGroup (V j)] [(j : I) → Module R (V j)] (rho : (j : I) → L →ₗ⁅R⁆ Module.End R (V j)) : (piRepresentation rho).ker = ⨅ (j : I), (rho j).ker

The kernel of a family product representation is the intersection of the kernels of its coordinates.

theorem LieHom.piRepresentation_injective_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I : Type i} {V : I → Type w₂} [(j : I) → AddCommGroup (V j)] [(j : I) → Module R (V j)] (rho : (j : I) → L →ₗ⁅R⁆ Module.End R (V j)) : Function.Injective ⇑(piRepresentation rho) ↔ ⨅ (j : I), (rho j).ker = ⊥

A family product representation is faithful exactly when its coordinate kernels have trivial intersection.