The Kostant integral form is stable under the antipode #

Let L be a Lie algebra over ℚ, let e : ι → L be root vectors and h : κ → L Cartan vectors, and let kostantForm e h be the subring of UniversalEnvelopingAlgebra ℚ L they generate in the sense of TauCeti.UniversalEnvelopingAlgebra.kostantForm. This file proves that the antipode maps that subring into itself, and packages the restriction as a ring anti-automorphism of the form.

The antipode negates each Lie generator, so the question is what negating the argument does to the two families of generators. For a root vector the answer is a sign: (-x)⁽ⁿ⁾ = (-1)ⁿ x⁽ⁿ⁾, and a subring is closed under negation. For a Cartan vector it is not, because (-x choose n) is not a multiple of (x choose n); it is instead the Chu--Vandermonde combination TauCeti.Ring.choose_neg_mem supplies, an integer combination of the coefficients (x choose k) for k ≤ n. That is the one substantive point, and it is what makes the Cartan generators behave.

The enveloping algebra is not commutative, so the antipode is only an anti-homomorphism. Nothing is lost: a subring is closed under multiplication in either order, so the elements the antipode sends into a given subring form a subring themselves, which is what TauCeti.UniversalEnvelopingAlgebra.antipodeComap records and what the universal property of the form is applied to. The packaged equivalence then lands in the opposite ring.

Together with the comultiplication and counit of the same generators this is one of the Hopf operations that must restrict to the integral form before it can define the pinned Chevalley--Demazure group scheme; the comultiplication is not proved here.

Main definitions and results #

TauCeti.UniversalEnvelopingAlgebra.antipode_dividedPower and TauCeti.UniversalEnvelopingAlgebra.antipode_ringChoose: the antipode passes through a divided power and through a generalized binomial coefficient.
TauCeti.UniversalEnvelopingAlgebra.antipode_mem_kostantForm and TauCeti.UniversalEnvelopingAlgebra.antipode_mem_kostantForm_iff: the antipode maps the Kostant integral form into itself, and membership is unchanged by it.
TauCeti.UniversalEnvelopingAlgebra.map_antipodeEquiv_kostantForm: the image of the form under the opposite-valued antipode is exactly the opposite subring, so the inclusion above is an equality of subrings.
TauCeti.UniversalEnvelopingAlgebra.kostantFormAntipode: the restriction of the antipode to the form, as a ring equivalence onto the opposite of the form.

References #

J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §26.
J. C. Jantzen, Representations of Algebraic Groups, II.1.

The antipode on the two families of generators #

source

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_dividedPower {L : Type u} [LieRing L] [LieAlgebra ℚ L] (a : UniversalEnvelopingAlgebra ℚ L) (n : ℕ) :

(antipode ℚ) (Associative.dividedPower n a) = Associative.dividedPower n ((antipode ℚ) a)

The antipode passes through a divided power. Antimultiplicativity is invisible here because a divided power is a rational multiple of a power of a single element.

source

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_ringChoose {L : Type u} [LieRing L] [LieAlgebra ℚ L] (a : UniversalEnvelopingAlgebra ℚ L) (n : ℕ) :

(antipode ℚ) (Ring.choose a n) = Ring.choose ((antipode ℚ) a) n

The antipode passes through a generalized binomial coefficient.

Stability of the integral form #

source

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_dividedPower_mem_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) (i : ι) (n : ℕ) :

(antipode ℚ) (Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ∈ kostantForm e h

The antipode of a divided power of a designated root vector lies in the Kostant integral form.

source

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_ringChoose_mem_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) (j : κ) (n : ℕ) :

(antipode ℚ) (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h j)) n) ∈ kostantForm e h

The antipode of a generalized binomial coefficient of a designated Cartan vector lies in the Kostant integral form.

source

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_mem_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) {a : UniversalEnvelopingAlgebra ℚ L} (ha : a ∈ kostantForm e h) :

(antipode ℚ) a ∈ kostantForm e h

The Kostant integral form is stable under the antipode.

source

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_mem_kostantForm_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) {a : UniversalEnvelopingAlgebra ℚ L} :

(antipode ℚ) a ∈ kostantForm e h ↔ a ∈ kostantForm e h

Membership in the Kostant integral form is unchanged by the antipode, since the antipode is involutive.

source

theorem TauCeti.UniversalEnvelopingAlgebra.map_antipodeEquiv_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) :

Subring.map (antipodeEquiv ℚ).toRingEquiv.toRingHom (kostantForm e h) = (kostantForm e h).op

The antipode maps the Kostant integral form onto itself: the image of the form under the opposite-valued antipode is the opposite subring, not merely contained in it.

source

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

↥(kostantForm e h) ≃+* (↥(kostantForm e h))ᵐᵒᵖ

The antipode restricted to the Kostant integral form, as a ring equivalence onto the opposite ring of the form. This is the anti-automorphism a Hopf order carries.

Equations