The antipode of a universal enveloping algebra

The universal enveloping algebra of a Lie algebra has a canonical algebra homomorphism to its opposite algebra, determined by sending every Lie generator x to -x. After identifying the underlying modules of an algebra and its opposite, this is the usual antipode. It fixes scalars, reverses products, and is an involution.

The opposite-algebra formulation records antimultiplicativity in the type. It also makes the construction available before a coalgebra structure has been chosen: only Mathlib's universal property of the enveloping algebra is used here.

Main definitions

• TauCeti.UniversalEnvelopingAlgebra.antipodeOp: the algebra homomorphism from an enveloping algebra to its opposite.
• TauCeti.UniversalEnvelopingAlgebra.antipode: the same map as a linear endomorphism.
• TauCeti.UniversalEnvelopingAlgebra.antipodeComap: the preimage of a subring under the antipode, again a subring.
• TauCeti.UniversalEnvelopingAlgebra.antipodeEquiv: the resulting algebra equivalence with the opposite algebra.

Main results

• TauCeti.UniversalEnvelopingAlgebra.antipode_ι: the antipode negates each canonical Lie generator.
• TauCeti.UniversalEnvelopingAlgebra.antipode_mul_antidistrib: the antipode reverses multiplication.
• TauCeti.UniversalEnvelopingAlgebra.antipode_antipode: the antipode is involutive.

Roadmap

This is a prerequisite for the Chevalley--Demazure construction in Layer 9 of the ReductiveGroups roadmap. The Kostant integral form is generated by divided powers of Chevalley root vectors and binomial coefficients in Cartan generators; stability under the antipode is one of the Hopf operations needed before that integral form can define the explicit group scheme.

References

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

noncomputable def TauCeti.UniversalEnvelopingAlgebra.antipodeOp (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] : UniversalEnvelopingAlgebra R L →ₐ[R] (UniversalEnvelopingAlgebra R L)ᵐᵒᵖ

The canonical algebra homomorphism from a universal enveloping algebra to its opposite.

It is uniquely determined by sending ι R x to op (-ι R x). Viewing the codomain as the opposite algebra makes the usual antimultiplicativity of the antipode ordinary multiplicativity.

Equations

• TauCeti.UniversalEnvelopingAlgebra.antipodeOp R = (UniversalEnvelopingAlgebra.lift R) (TauCeti.UniversalEnvelopingAlgebra.opNegι✝ R)

theorem TauCeti.UniversalEnvelopingAlgebra.antipodeOp_ι (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (x : L) : (antipodeOp R) ((UniversalEnvelopingAlgebra.ι R) x) = MulOpposite.op (-(UniversalEnvelopingAlgebra.ι R) x)

The opposite-valued antipode negates every canonical Lie generator.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipodeOp_mkAlgHom_ι (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (x : L) : (antipodeOp R) ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)) = MulOpposite.op (-(UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x))

The simp-normal form of antipodeOp_ι, stated for the canonical generators as simp writes them.

theorem TauCeti.UniversalEnvelopingAlgebra.antipodeOp_unique (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (f : UniversalEnvelopingAlgebra R L →ₐ[R] (UniversalEnvelopingAlgebra R L)ᵐᵒᵖ) : (∀ (x : L), f ((UniversalEnvelopingAlgebra.ι R) x) = MulOpposite.op (-(UniversalEnvelopingAlgebra.ι R) x)) ↔ f = antipodeOp R

An algebra homomorphism to the opposite enveloping algebra is the antipode exactly when it negates every canonical Lie generator.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.antipode (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] : UniversalEnvelopingAlgebra R L →ₗ[R] UniversalEnvelopingAlgebra R L

The antipode of a universal enveloping algebra, as a linear endomorphism of its underlying module.

Equations

• TauCeti.UniversalEnvelopingAlgebra.antipode R = ↑(MulOpposite.opLinearEquiv R).symm ∘ₗ (TauCeti.UniversalEnvelopingAlgebra.antipodeOp R).toLinearMap

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_apply (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (a : UniversalEnvelopingAlgebra R L) : (antipode R) a = MulOpposite.unop ((antipodeOp R) a)

The linear antipode is the unopposite of the opposite-valued algebra homomorphism.

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_ι (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (x : L) : (antipode R) ((UniversalEnvelopingAlgebra.ι R) x) = -(UniversalEnvelopingAlgebra.ι R) x

The antipode negates every canonical Lie generator.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_mkAlgHom_ι (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (x : L) : (antipode R) ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)) = -(UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)

The simp-normal form of antipode_ι, stated for the canonical generators as simp writes them.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_one (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] : (antipode R) 1 = 1

The antipode fixes the multiplicative identity.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_algebraMap (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (r : R) : (antipode R) ((algebraMap R (UniversalEnvelopingAlgebra R L)) r) = (algebraMap R (UniversalEnvelopingAlgebra R L)) r

The antipode fixes the image of every scalar.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_mul_antidistrib (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (a b : UniversalEnvelopingAlgebra R L) : (antipode R) (a * b) = (antipode R) b * (antipode R) a

The antipode reverses multiplication.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_pow (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (a : UniversalEnvelopingAlgebra R L) (n : ℕ) : (antipode R) (a ^ n) = (antipode R) a ^ n

The antipode commutes with powers of one element.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.antipodeEquiv (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] : UniversalEnvelopingAlgebra R L ≃ₐ[R] (UniversalEnvelopingAlgebra R L)ᵐᵒᵖ

A universal enveloping algebra is canonically equivalent to its opposite algebra by negating the Lie generators.

Equations

• TauCeti.UniversalEnvelopingAlgebra.antipodeEquiv R = AlgEquiv.ofAlgHom (TauCeti.UniversalEnvelopingAlgebra.antipodeOp R) (AlgHom.opComm (TauCeti.UniversalEnvelopingAlgebra.antipodeOp R)) ⋯ ⋯

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipodeEquiv_toAlgHom (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] : ↑(antipodeEquiv R) = antipodeOp R

The algebra homomorphism underlying antipodeEquiv is antipodeOp.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipodeEquiv_apply (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (a : UniversalEnvelopingAlgebra R L) : (antipodeEquiv R) a = (antipodeOp R) a

The opposite-algebra equivalence agrees with antipodeOp on every element.

theorem TauCeti.UniversalEnvelopingAlgebra.antipodeEquiv_ι (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (x : L) : (antipodeEquiv R) ((UniversalEnvelopingAlgebra.ι R) x) = MulOpposite.op (-(UniversalEnvelopingAlgebra.ι R) x)

The opposite-algebra equivalence negates every canonical Lie generator.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipodeEquiv_symm_toAlgHom (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] : ↑(antipodeEquiv R).symm = AlgHom.opComm (antipodeOp R)

The inverse of antipodeEquiv is the opposite transform of antipodeOp.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipodeEquiv_symm_apply (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (a : (UniversalEnvelopingAlgebra R L)ᵐᵒᵖ) : (antipodeEquiv R).symm a = (antipode R) (MulOpposite.unop a)

The inverse opposite-algebra equivalence acts by the same underlying antipode.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_antipode (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (a : UniversalEnvelopingAlgebra R L) : (antipode R) ((antipode R) a) = a

The antipode is involutive.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.antipodeComap (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (S : Subring (UniversalEnvelopingAlgebra R L)) : Subring (UniversalEnvelopingAlgebra R L)

The preimage of a subring under the antipode.

Antimultiplicativity is no obstruction: it is the preimage of the opposite subring Subring.op S under the genuine ring homomorphism antipodeOp.

Equations

• TauCeti.UniversalEnvelopingAlgebra.antipodeComap R S = Subring.comap (TauCeti.UniversalEnvelopingAlgebra.antipodeOp R).toRingHom S.op

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_antipodeComap (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] {S : Subring (UniversalEnvelopingAlgebra R L)} {a : UniversalEnvelopingAlgebra R L} : a ∈ antipodeComap R S ↔ (antipode R) a ∈ S

theorem TauCeti.UniversalEnvelopingAlgebra.antipode_bijective (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] : Function.Bijective ⇑(antipode R)

The antipode is bijective.