Functoriality of universal enveloping algebras

A homomorphism of Lie algebras induces an algebra homomorphism of their universal enveloping algebras. This file constructs that map directly from Mathlib's universal property and proves its characteristic equation on the canonical Lie generators, its identity and composition laws, and its behaviour on split monomorphisms and split epimorphisms. A Lie algebra equivalence consequently induces an algebra equivalence of universal enveloping algebras.

The split-morphism results avoid any freeness or Poincare--Birkhoff--Witt hypothesis: a chosen one-sided inverse of a Lie homomorphism lifts to the same one-sided inverse on enveloping algebras. In particular, the equivalence construction is available over an arbitrary commutative ring.

Main definitions

• Ado.UniversalEnvelopingAlgebra.map: the algebra homomorphism induced by a Lie algebra homomorphism.
• Ado.UniversalEnvelopingAlgebra.mapEquiv: the algebra equivalence induced by a Lie algebra equivalence.

Main results

• Ado.UniversalEnvelopingAlgebra.map_ι: the induced map agrees with the original Lie homomorphism on the canonical generators.
• Ado.UniversalEnvelopingAlgebra.map_id and Ado.UniversalEnvelopingAlgebra.map_comp: enveloping-algebra maps are functorial.
• Ado.UniversalEnvelopingAlgebra.map_surjective_of_surjective: surjective Lie maps induce surjective enveloping-algebra maps.
• Ado.UniversalEnvelopingAlgebra.map_injective_of_leftInverse and Ado.UniversalEnvelopingAlgebra.map_surjective_of_rightInverse: split morphisms remain split after passing to enveloping algebras.

Roadmap

This supplies functoriality needed by the explicit Chevalley--Demazure construction in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. That construction forms the Kostant integral form inside the universal enveloping algebra of a Chevalley Lie algebra. Isomorphisms of the pinned root data act first on the Chevalley generators; map and mapEquiv lift those actions to the enveloping algebra, where preservation of the Kostant form can be stated and proved. The pinned isomorphism theorem then consumes that construction, and TauCetiRoadmap/CFSGStatement/README.md milestone L1 uses it to realize diagram permutations as graph automorphisms of the pinned group.

No Poincare--Birkhoff--Witt theorem or injectivity of the canonical Lie map is asserted here.

noncomputable def Ado.UniversalEnvelopingAlgebra.map (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) : UniversalEnvelopingAlgebra R L →ₐ[R] UniversalEnvelopingAlgebra R M

The algebra homomorphism of universal enveloping algebras induced by a Lie algebra homomorphism.

It is the unique algebra homomorphism sending the canonical generator ι R x to ι R (f x); map_ι is the corresponding computation rule and map_unique is the universal property in that form.

Equations

• Ado.UniversalEnvelopingAlgebra.map R f = (UniversalEnvelopingAlgebra.lift R) ((UniversalEnvelopingAlgebra.ι R).comp f)

theorem Ado.UniversalEnvelopingAlgebra.map_ι (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (x : L) : (map R f) ((UniversalEnvelopingAlgebra.ι R) x) = (UniversalEnvelopingAlgebra.ι R) (f x)

An enveloping-algebra map acts on the canonical Lie generators by the original Lie homomorphism.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.map_ι' (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (x : L) : (map R f) ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)) = (UniversalEnvelopingAlgebra.mkAlgHom R M) ((TensorAlgebra.ι R) (f x))

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

theorem Ado.UniversalEnvelopingAlgebra.map_unique (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (g : UniversalEnvelopingAlgebra R L →ₐ[R] UniversalEnvelopingAlgebra R M) : (∀ (x : L), g ((UniversalEnvelopingAlgebra.ι R) x) = (UniversalEnvelopingAlgebra.ι R) (f x)) ↔ g = map R f

An algebra homomorphism out of an enveloping algebra is the map induced by f exactly when it sends every canonical generator to the image prescribed by f.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.map_id (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] : map R LieHom.id = AlgHom.id R (UniversalEnvelopingAlgebra R L)

The identity Lie homomorphism induces the identity algebra homomorphism.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.map_comp (R : Type u) [CommRing R] {L : Type v} {M : Type w} {N : Type x} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [LieRing N] [LieAlgebra R N] (f : L →ₗ⁅R⁆ M) (g : M →ₗ⁅R⁆ N) : map R (g.comp f) = (map R g).comp (map R f)

Composition of Lie homomorphisms becomes composition of the induced algebra homomorphisms.

theorem Ado.UniversalEnvelopingAlgebra.map_leftInverse (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] {f : L →ₗ⁅R⁆ M} {g : M →ₗ⁅R⁆ L} (h : g.comp f = LieHom.id) : Function.LeftInverse ⇑(map R g) ⇑(map R f)

A left inverse of Lie homomorphisms induces a left inverse of the corresponding enveloping-algebra maps.

theorem Ado.UniversalEnvelopingAlgebra.map_rightInverse (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] {f : L →ₗ⁅R⁆ M} {g : M →ₗ⁅R⁆ L} (h : f.comp g = LieHom.id) : Function.RightInverse ⇑(map R g) ⇑(map R f)

A right inverse of Lie homomorphisms induces a right inverse of the corresponding enveloping-algebra maps.

theorem Ado.UniversalEnvelopingAlgebra.map_injective_of_leftInverse (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (g : M →ₗ⁅R⁆ L) (h : g.comp f = LieHom.id) : Function.Injective ⇑(map R f)

A split monomorphism of Lie algebras induces an injective homomorphism of enveloping algebras.

theorem Ado.UniversalEnvelopingAlgebra.map_surjective_of_surjective (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(map R f)

A surjective Lie homomorphism induces a surjective homomorphism of universal enveloping algebras.

theorem Ado.UniversalEnvelopingAlgebra.map_surjective_of_rightInverse (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (g : M →ₗ⁅R⁆ L) (h : f.comp g = LieHom.id) : Function.Surjective ⇑(map R f)

A split epimorphism of Lie algebras induces a surjective homomorphism of enveloping algebras.

noncomputable def Ado.UniversalEnvelopingAlgebra.mapEquiv (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (e : L ≃ₗ⁅R⁆ M) : UniversalEnvelopingAlgebra R L ≃ₐ[R] UniversalEnvelopingAlgebra R M

A Lie algebra equivalence induces an algebra equivalence of universal enveloping algebras.

Equations

• Ado.UniversalEnvelopingAlgebra.mapEquiv R e = AlgEquiv.ofAlgHom (Ado.UniversalEnvelopingAlgebra.map R e.toLieHom) (Ado.UniversalEnvelopingAlgebra.map R e.symm.toLieHom) ⋯ ⋯

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.mapEquiv_toAlgHom (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (e : L ≃ₗ⁅R⁆ M) : ↑(mapEquiv R e) = map R e.toLieHom

The algebra homomorphism underlying mapEquiv is the map induced by the underlying Lie homomorphism.

theorem Ado.UniversalEnvelopingAlgebra.mapEquiv_ι (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (e : L ≃ₗ⁅R⁆ M) (x : L) : (mapEquiv R e) ((UniversalEnvelopingAlgebra.ι R) x) = (UniversalEnvelopingAlgebra.ι R) (e x)

The algebra equivalence induced by a Lie equivalence acts on canonical generators by that Lie equivalence.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.mapEquiv_ι' (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (e : L ≃ₗ⁅R⁆ M) (x : L) : (mapEquiv R e) ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)) = (UniversalEnvelopingAlgebra.mkAlgHom R M) ((TensorAlgebra.ι R) (e x))

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

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.mapEquiv_symm (R : Type u) [CommRing R] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (e : L ≃ₗ⁅R⁆ M) : (mapEquiv R e).symm = mapEquiv R e.symm

Passing the inverse Lie equivalence to enveloping algebras gives the inverse algebra equivalence.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.mapEquiv_refl (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] : mapEquiv R LieEquiv.refl = AlgEquiv.refl

The identity Lie equivalence induces the identity algebra equivalence.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.mapEquiv_trans (R : Type u) [CommRing R] {L : Type v} {M : Type w} {N : Type x} [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [LieRing N] [LieAlgebra R N] (e : L ≃ₗ⁅R⁆ M) (d : M ≃ₗ⁅R⁆ N) : (mapEquiv R e).trans (mapEquiv R d) = mapEquiv R (e.trans d)

Composition of Lie equivalences becomes composition of the induced algebra equivalences.