Direct sums of Kostant-stable lattices

Two rational representations of the same Lie algebra combine by a binary direct sum, realized as a product. The product of Kostant-stable lattices is stable, and the union of their integral weight bases is a weight basis of the product. The root subgroup action after any scalar extension is the componentwise action on the two summands.

These results allow a representation with the required weights to be added to a faithful representation while retaining explicit integral root subgroup actions. The representation, lattice, and basis use Mathlib's product constructions directly.

theorem UniversalEnvelopingAlgebra.kostantForm_apply_mem_prod {L : Type u_1} {V : Type u_2} {W : Type u_3} [LieRing L] [LieAlgebra ℚ L] [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {ι : Type u_4} {κ : Type u_5} (u : UniversalEnvelopingAlgebra ℚ L) (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (σ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ W) (M : AddSubgroup V) (N : AddSubgroup W) (hM : ∀ u ∈ TauCeti.UniversalEnvelopingAlgebra.kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hN : ∀ u ∈ TauCeti.UniversalEnvelopingAlgebra.kostantForm e h, ∀ w ∈ N, (σ u) w ∈ N) (hu : u ∈ TauCeti.UniversalEnvelopingAlgebra.kostantForm e h) (v : V × W) (hv : v ∈ M.prod N) : (((LinearMap.prodMapAlgHom ℚ V W).comp (ρ.prod σ)) u) v ∈ M.prod N

The product of two Kostant-stable lattices is stable in the direct sum representation.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.isCartanWeightVector_prod_iff {L : Type u_1} {V : Type u_2} {W : Type u_3} [LieRing L] [LieAlgebra ℚ L] [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {κ : Type u_5} (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (σ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ W) (μ : κ → ℤ) (v : V × W) : IsCartanWeightVector h ((LinearMap.prodMapAlgHom ℚ V W).comp (ρ.prod σ)) μ v ↔ IsCartanWeightVector h ρ μ v.1 ∧ IsCartanWeightVector h σ μ v.2

A vector in the direct sum has a given Cartan weight exactly when both components have that weight. Zero components are allowed.

theorem TauCeti.UniversalEnvelopingAlgebra.isCartanWeightVector_prod_basis {L : Type u_1} {V : Type u_2} {W : Type u_3} [LieRing L] [LieAlgebra ℚ L] [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {κ : Type u_5} (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (σ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ W) (M : AddSubgroup V) (N : AddSubgroup W) {η : Type u_6} {θ : Type u_7} (b : Module.Basis η ℤ ↥M) (c : Module.Basis θ ℤ ↥N) (wt : η → κ → ℤ) (wt' : θ → κ → ℤ) (hb : ∀ (i : η), IsCartanWeightVector h ρ (wt i) ↑(b i)) (hc : ∀ (j : θ), IsCartanWeightVector h σ (wt' j) ↑(c j)) (i : η ⊕ θ) : IsCartanWeightVector h ((LinearMap.prodMapAlgHom ℚ V W).comp (ρ.prod σ)) (Sum.elim wt wt' i) ↑(((b.prod c).map (M.prodEquiv N).toIntLinearEquiv.symm) i)

The disjoint union of two integral weight bases is a weight basis of the product lattice.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.prodRight_baseChangeKostantExpHom {L : Type u_1} {V : Type u_2} {W : Type u_3} [LieRing L] [LieAlgebra ℚ L] [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {ι : Type u_4} {κ : Type u_5} (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (σ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ W) (M : AddSubgroup V) (N : AddSubgroup W) {R : Type u_6} [CommRing R] [Algebra ℤ R] (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (hN : ∀ u ∈ kostantForm e h, ∀ w ∈ N, (σ u) w ∈ N) (i : ι) (hρ : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (hσ : IsNilpotent (σ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (t : Multiplicative R) (z : TensorProduct ℤ R ↥(M.prod N)) : have E := fun (z : TensorProduct ℤ R ↥(M.prod N)) => (TensorProduct.prodRight ℤ R R ↥M ↥N) ((LinearEquiv.baseChange ℤ R (↥(M.prod N)) (↥M × ↥N) (M.prodEquiv N).toIntLinearEquiv) z); E (((baseChangeKostantExpHom e h ((LinearMap.prodMapAlgHom ℚ V W).comp (ρ.prod σ)) (M.prod N) ⋯ i ⋯) t) z) = (((baseChangeKostantExpHom e h ρ M hM i hρ) t) (E z).1, ((baseChangeKostantExpHom e h σ N hN i hσ) t) (E z).2)

Root subgroup actions on the product lattice agree with the actions on the two summands, after extension to any commutative coefficient ring.