Comultiplication and counit of the Kostant integral form

Let L be a Lie algebra over ℚ, and let kostantForm e h be the subring of its universal enveloping algebra generated by the divided powers of the designated root vectors e and the generalized binomial coefficients of the designated Cartan vectors h. This file proves that the rational bialgebra comultiplication and counit are integral on that form.

For the comultiplication, the integral target is represented inside the rational tensor square. The canonical map

kostantForm e h ⊗[ℤ] kostantForm e h → U(L) ⊗[ℚ] U(L)

sends a pure tensor to the pure tensor of its two underlying elements. It is injective because a subring of a rational algebra is torsion-free, hence flat over ℤ; this is the general theorem Subring.tensorSquareMap_injective. Its range is kostantTensorForm e h, so it gives the equivalence kostantTensorEquiv between the integral tensor square and that range.

The coefficient-one coproduct formulas for divided powers and generalized binomial coefficients show that the rational comultiplication of every element of the Kostant form lies in this range. Transporting the range-valued restriction back through kostantTensorEquiv gives the canonical integral coproduct kostantFormComul : U_ℤ →ₐ[ℤ] U_ℤ ⊗[ℤ] U_ℤ. Thus integrality now means an actual algebra homomorphism, rather than only the existence of an integral tensor representative.

The counit has no such issue. It sends every positive generator to zero and hence the entire form to the integer-cast subring of ℚ. The map kostantFormCounit is its canonical restriction to ℤ, and intCast_kostantFormCounit_apply identifies it with the rational counit.

Main definitions and results

• TauCeti.UniversalEnvelopingAlgebra.kostantTensorMap: the canonical map from the integral tensor square to the rational tensor square.
• TauCeti.UniversalEnvelopingAlgebra.kostantTensorMap_injective: the canonical tensor map is injective.
• TauCeti.UniversalEnvelopingAlgebra.kostantTensorForm: the range of that map.
• TauCeti.UniversalEnvelopingAlgebra.kostantTensorEquiv: the equivalence from the integral tensor square onto that range.
• TauCeti.UniversalEnvelopingAlgebra.comul_mem_kostantTensorForm: the rational coproduct of an element of the Kostant form has an integral tensor representative.
• TauCeti.UniversalEnvelopingAlgebra.counit_mem_bot_of_mem_kostantForm: the rational counit of an element of the Kostant form is an integer.
• TauCeti.UniversalEnvelopingAlgebra.kostantFormComul: the canonical integral comultiplication.
• TauCeti.UniversalEnvelopingAlgebra.kostantFormComul_dividedPower and TauCeti.UniversalEnvelopingAlgebra.kostantFormComul_ringChoose: its formulas on the generators of the Kostant form.
• TauCeti.UniversalEnvelopingAlgebra.kostantFormCounit: the counit of the Kostant form, valued in ℤ.

References

The coproduct formulas and the resulting Hopf order are standard; see J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §26, and J. C. Jantzen, Representations of Algebraic Groups, II.1. This supplies the comultiplication and counit part of the Kostant-form input to the Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md.

The integral tensor form

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTensorMap {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) : TensorProduct ℤ ↥(kostantForm e h) ↥(kostantForm e h) →ₐ[ℤ] TensorProduct ℚ (UniversalEnvelopingAlgebra ℚ L) (UniversalEnvelopingAlgebra ℚ L)

The canonical map from the tensor square of a Kostant form over ℤ to the tensor square of the ambient universal enveloping algebra over ℚ.

On pure tensors this is x ⊗ y ↦ (x : U(L)) ⊗ (y : U(L)).

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantTensorMap e h = Subring.tensorSquareMap ℚ (TauCeti.UniversalEnvelopingAlgebra.kostantForm e h)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTensorMap_tmul {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) (x y : ↥(kostantForm e h)) : (kostantTensorMap e h) (x ⊗ₜ[ℤ] y) = ↑x ⊗ₜ[ℚ] ↑y

The canonical integral tensor map sends a pure tensor to the pure tensor of the underlying elements in the rational tensor square.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTensorForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) : Subring (TensorProduct ℚ (UniversalEnvelopingAlgebra ℚ L) (UniversalEnvelopingAlgebra ℚ L))

The integral tensor form inside the rational tensor square: the range of the canonical map from kostantForm e h ⊗[ℤ] kostantForm e h.

This range is the codomain of the rational restriction; kostantTensorEquiv below identifies it with the integral tensor square.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantTensorForm e h = Subring.tensorSquareRange ℚ (TauCeti.UniversalEnvelopingAlgebra.kostantForm e h)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_kostantTensorForm_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) (z : TensorProduct ℚ (UniversalEnvelopingAlgebra ℚ L) (UniversalEnvelopingAlgebra ℚ L)) : z ∈ kostantTensorForm e h ↔ ∃ (t : TensorProduct ℤ ↥(kostantForm e h) ↥(kostantForm e h)), (kostantTensorMap e h) t = z

Membership in the integral tensor form is equivalent to having an integral tensor representative under the canonical tensor map.

theorem TauCeti.UniversalEnvelopingAlgebra.tmul_mem_kostantTensorForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) {x y : UniversalEnvelopingAlgebra ℚ L} (hx : x ∈ kostantForm e h) (hy : y ∈ kostantForm e h) : x ⊗ₜ[ℚ] y ∈ kostantTensorForm e h

A pure rational tensor whose two factors lie in the Kostant form belongs to the integral tensor form.

Stability under comultiplication

theorem TauCeti.UniversalEnvelopingAlgebra.comul_mem_kostantTensorForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) {a : UniversalEnvelopingAlgebra ℚ L} (ha : a ∈ kostantForm e h) : CoalgebraStruct.comul a ∈ kostantTensorForm e h

The rational comultiplication is integral on the Kostant form. Every coproduct of an element of kostantForm e h lies in the range of its integral tensor square.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTensorMap_injective {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) : Function.Injective ⇑(kostantTensorMap e h)

The canonical map from the integral tensor square of a Kostant form to the rational tensor square of its enveloping algebra is injective.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantTensorEquiv {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) : TensorProduct ℤ ↥(kostantForm e h) ↥(kostantForm e h) ≃ₐ[ℤ] ↥(kostantTensorForm e h)

The canonical equivalence from the integral tensor square of a Kostant form onto its image in the rational tensor square.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantTensorEquiv e h = (TauCeti.UniversalEnvelopingAlgebra.kostantForm e h).tensorSquareEquivRange

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantTensorEquiv_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) (t : TensorProduct ℤ ↥(kostantForm e h) ↥(kostantForm e h)) : ↑((kostantTensorEquiv e h) t) = (kostantTensorMap e h) t

The tensor equivalence acts by the canonical map into the rational tensor square.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantFormComul {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) : ↥(kostantForm e h) →ₐ[ℤ] TensorProduct ℤ ↥(kostantForm e h) ↥(kostantForm e h)

The integral comultiplication of a Kostant form. It is the unique algebra homomorphism whose composition with kostantTensorMap is the rational enveloping-algebra comultiplication.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantTensorMap_kostantFormComul_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) (a : ↥(kostantForm e h)) : (kostantTensorMap e h) ((kostantFormComul e h) a) = CoalgebraStruct.comul ↑a

The integral comultiplication becomes the rational enveloping-algebra comultiplication under the canonical tensor embedding.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantFormComul_unique {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) (f : ↥(kostantForm e h) →ₐ[ℤ] TensorProduct ℤ ↥(kostantForm e h) ↥(kostantForm e h)) (hf : ∀ (a : ↥(kostantForm e h)), (kostantTensorMap e h) (f a) = CoalgebraStruct.comul ↑a) : f = kostantFormComul e h

The integral comultiplication is uniquely determined by its agreement with the rational enveloping-algebra comultiplication.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantFormComul_dividedPower {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) (i : ι) (n : ℕ) : (kostantFormComul e h) ⟨Associative.dividedPower n ((UniversalEnvelopingAlgebra.mkAlgHom ℚ L) ((TensorAlgebra.ι ℚ) (e i))), ⋯⟩ = ∑ ij ∈ Finset.antidiagonal n, ⟨Associative.dividedPower ij.1 ((UniversalEnvelopingAlgebra.ι ℚ) (e i)), ⋯⟩ ⊗ₜ[ℤ] ⟨Associative.dividedPower ij.2 ((UniversalEnvelopingAlgebra.ι ℚ) (e i)), ⋯⟩

The integral coproduct of a divided power is the coefficient-one antidiagonal sum.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantFormComul_ringChoose {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) (j : κ) (n : ℕ) : (kostantFormComul e h) ⟨Ring.choose ((UniversalEnvelopingAlgebra.mkAlgHom ℚ L) ((TensorAlgebra.ι ℚ) (h j))) n, ⋯⟩ = ∑ ij ∈ Finset.antidiagonal n, ⟨Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h j)) ij.1, ⋯⟩ ⊗ₜ[ℤ] ⟨Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h j)) ij.2, ⋯⟩

The integral coproduct of a generalized Cartan binomial is the coefficient-one antidiagonal sum.

The integral counit

theorem TauCeti.UniversalEnvelopingAlgebra.counit_mem_bot_of_mem_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) {a : UniversalEnvelopingAlgebra ℚ L} (ha : a ∈ kostantForm e h) : CoalgebraStruct.counit a ∈ ⊥

The rational counit of an element of the Kostant form belongs to the integer-cast subring of ℚ.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantFormCounit {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) : ↥(kostantForm e h) →ₐ[ℤ] ℤ

The counit of the Kostant integral form, valued in ℤ.

It is the rational bialgebra counit restricted along the canonical identification of ℤ with the integer-cast subring of ℚ.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.intCast_kostantFormCounit_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type v} {κ : Type w} (e : ι → L) (h : κ → L) (a : ↥(kostantForm e h)) : ↑((kostantFormCounit e h) a) = CoalgebraStruct.counit ↑a

After casting to ℚ, the integral counit agrees with the rational bialgebra counit.