Universal enveloping algebras of products

The universal enveloping algebra of a product of Lie algebras is the tensor product of their universal enveloping algebras. The equivalence sends a canonical generator (x, y) to ι(x) ⊗ 1 + 1 ⊗ ι(y). Its inverse sends a pure tensor to the product of the two canonical inclusions.

This construction uses only the universal properties of enveloping algebras and tensor products; it does not require a Poincare--Birkhoff--Witt theorem or any freeness hypothesis. The componentwise product representation preserves products of stable lattices.

Main results

• TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor: the algebra equivalence U(L × M) ≃ₐ[R] U(L) ⊗[R] U(M).
• TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor_ι: its value on a canonical generator.
• TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor_map_inl and prodEquivTensor_map_inr: its values on the canonical factor inclusions.
• TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor_naturality: compatibility with maps of both Lie-algebra factors.
• TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor_symm_tmul: the inverse on a pure tensor.
• AlgHom.prodRepresentation: the componentwise product of two representations of the same enveloping algebra, with stability of product lattices.

References

• N. Bourbaki, Lie Groups and Lie Algebras, Chapter I, §2, no. 2, Proposition 2, for the enveloping algebra of a product and its tensor-product description.
• Mathlib's product-equivalence proof architecture in Mathlib.LinearAlgebra.CliffordAlgebra.Prod, adapted here to ordinary tensor products and universal enveloping algebras.
• The tensor-lift, commuting-factor induction, and inverse-composition proof pattern in TauCeti.Algebra.Bialgebra.MonoidAlgebra.Product, adapted here to universal enveloping algebras.
• Mathlib's UniversalEnvelopingAlgebra.lift in Mathlib.Algebra.Lie.UniversalEnveloping.
• Mathlib's Algebra.TensorProduct.lift in Mathlib.RingTheory.TensorProduct.Maps.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] : UniversalEnvelopingAlgebra R (L × M) ≃ₐ[R] TensorProduct R (UniversalEnvelopingAlgebra R L) (UniversalEnvelopingAlgebra R M)

The universal enveloping algebra of a product of Lie algebras is the tensor product of their universal enveloping algebras.

Equations

• TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor R L M = AlgEquiv.ofAlgHom (TauCeti.UniversalEnvelopingAlgebra.toTensor✝ R L M) (TauCeti.UniversalEnvelopingAlgebra.fromTensor✝ R L M) ⋯ ⋯

theorem TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor_ι (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (x : L × M) : (prodEquivTensor R L M) ((UniversalEnvelopingAlgebra.ι R) x) = (UniversalEnvelopingAlgebra.ι R) x.1 ⊗ₜ[R] 1 + 1 ⊗ₜ[R] (UniversalEnvelopingAlgebra.ι R) x.2

The product-to-tensor equivalence sends a canonical generator x to ι(x.1) ⊗ 1 + 1 ⊗ ι(x.2).

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor_ι' (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (x : L × M) : (prodEquivTensor R L M) ((UniversalEnvelopingAlgebra.mkAlgHom R (L × M)) ((TensorAlgebra.ι R) x)) = (UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x.1) ⊗ₜ[R] 1 + 1 ⊗ₜ[R] (UniversalEnvelopingAlgebra.mkAlgHom R M) ((TensorAlgebra.ι R) x.2)

The simp-normal form of prodEquivTensor_ι, stated for the canonical generators as simp writes them: ι R x unfolds to mkAlgHom R L (TensorAlgebra.ι R x).

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor_map_inl (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (x : UniversalEnvelopingAlgebra R L) : (prodEquivTensor R L M) ((map R (LieHom.inl R L M)) x) = x ⊗ₜ[R] 1

On the left canonical factor, the product-to-tensor equivalence is tensoring with one.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor_map_inr (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (y : UniversalEnvelopingAlgebra R M) : (prodEquivTensor R L M) ((map R (LieHom.inr R L M)) y) = 1 ⊗ₜ[R] y

On the right canonical factor, the product-to-tensor equivalence is tensoring one with it.

theorem TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor_naturality (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] {L' : Type u_1} {M' : Type u_2} [LieRing L'] [LieAlgebra R L'] [LieRing M'] [LieAlgebra R M'] (f : L →ₗ⁅R⁆ L') (g : M →ₗ⁅R⁆ M') : (Algebra.TensorProduct.map (map R f) (map R g)).comp ↑(prodEquivTensor R L M) = (↑(prodEquivTensor R L' M')).comp (map R (f.prodMap g))

The product-to-tensor equivalence is natural in both Lie-algebra factors.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.prodEquivTensor_symm_tmul (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (x : UniversalEnvelopingAlgebra R L) (y : UniversalEnvelopingAlgebra R M) : (prodEquivTensor R L M).symm (x ⊗ₜ[R] y) = (map R (LieHom.inl R L M)) x * (map R (LieHom.inr R L M)) y

The inverse product-to-tensor equivalence sends a pure tensor to the product of the two canonical inclusions.

noncomputable def AlgHom.prodRepresentation {L : Type u} [LieRing L] [LieAlgebra ℚ L] {V : Type v} [AddCommGroup V] [Module ℚ V] {W : Type w} [AddCommGroup W] [Module ℚ W] (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (σ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ W) : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ (V × W)

The product of two enveloping-algebra representations acts componentwise on the product of their carriers.

Equations

• ρ.prodRepresentation σ = (LinearMap.prodMapAlgHom ℚ V W).comp (ρ.prod σ)

@[simp]

theorem AlgHom.prodRepresentation_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {V : Type v} [AddCommGroup V] [Module ℚ V] {W : Type w} [AddCommGroup W] [Module ℚ W] (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (σ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ W) (u : UniversalEnvelopingAlgebra ℚ L) (v : V × W) : ((ρ.prodRepresentation σ) u) v = ((ρ u) v.1, (σ u) v.2)

The product representation applies its two factors componentwise.

theorem AlgHom.prodRepresentation_apply_mem_of_mem {L : Type u} [LieRing L] [LieAlgebra ℚ L] {V : Type v} [AddCommGroup V] [Module ℚ V] {W : Type w} [AddCommGroup W] [Module ℚ W] (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (σ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ W) (S : Set (UniversalEnvelopingAlgebra ℚ L)) (M : Submodule ℤ V) (N : Submodule ℤ W) (hM : ∀ u ∈ S, ∀ v ∈ M, (ρ u) v ∈ M) (hN : ∀ u ∈ S, ∀ w ∈ N, (σ u) w ∈ N) (u : UniversalEnvelopingAlgebra ℚ L) (hu : u ∈ S) (v : V × W) (hv : v ∈ M.prod N) : ((ρ.prodRepresentation σ) u) v ∈ M.prod N

Componentwise stability of a product lattice under a set of enveloping-algebra elements.

theorem AlgHom.prodRepresentation_apply_mem {L : Type u} [LieRing L] [LieAlgebra ℚ L] {V : Type v} [AddCommGroup V] [Module ℚ V] {W : Type w} [AddCommGroup W] [Module ℚ W] (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (σ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ W) (M : Submodule ℤ V) (N : Submodule ℤ W) (hM : ∀ (u : UniversalEnvelopingAlgebra ℚ L), ∀ v ∈ M, (ρ u) v ∈ M) (hN : ∀ (u : UniversalEnvelopingAlgebra ℚ L), ∀ w ∈ N, (σ u) w ∈ N) (u : UniversalEnvelopingAlgebra ℚ L) (v : V × W) (hv : v ∈ M.prod N) : ((ρ.prodRepresentation σ) u) v ∈ M.prod N

A product representation preserves a product lattice if both factors preserve their respective lattices under every enveloping-algebra element. This specializes prodRepresentation_apply_mem_of_mem to the full enveloping algebra, accepting the usual unrestricted stability hypotheses directly.