Representations of split extensions on enveloping quotients

Let ψ : H →ₗ⁅R⁆ LieDerivation R S S define a split Lie extension, and let J be a two-sided ideal of U(S) preserved by the lifted derivations. On U(S)/J, the element (s, h) acts as left multiplication by the class of ι(s) plus the derivation induced by ψ(h). This gives a representation of S ⋊⁅ψ⁆ H. Evaluating at the unit shows that its kernel on S consists exactly of those s with ι(s) ∈ J.

In particular, if J is contained in the kernel of the enveloping extension of a starting representation σ of S, the new representation detects every direction detected by σ. When the quotient is finite dimensional, this is the kernel control needed to extend finite-dimensional representations through split ideal extensions. If ψ(h) is locally nilpotent on S and the quotient is finitely generated over R, the element (0, h) also acts nilpotently on the quotient.

The construction uses Ado.UniversalEnvelopingAlgebra.envelopingDerivationHom to lift the acting derivations and Ado.derivationQuotientHom to descend them to the quotient.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E, §E.2, Proposition E.5, for the multiplication-plus-derivation construction.
• S. Asgarli, Ado's Theorem, Proposition 2, for the split-extension argument and its kernel control.

noncomputable def Ado.envelopingQuotientDerivation (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) : H →ₗ⁅R⁆ ↥(derivationLieAlgebra R (UniversalEnvelopingAlgebra R S ⧸ J))

The action of H by derivations on a stable two-sided enveloping quotient.

Equations

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

@[simp]

theorem Ado.envelopingQuotientDerivation_apply_mk (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) (h : H) (a : UniversalEnvelopingAlgebra R S) : ↑((envelopingQuotientDerivation R S ψ J hJ) h) ((Ideal.Quotient.mk J) a) = (Ideal.Quotient.mk J) (↑(UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h)) a)

Descended derivations act on a class by differentiating a representative.

theorem Ado.envelopingQuotientDerivation_apply_ι (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) (h : H) (s : S) : ↑((envelopingQuotientDerivation R S ψ J hJ) h) ((Ideal.Quotient.mk J) ((UniversalEnvelopingAlgebra.ι R) s)) = (Ideal.Quotient.mk J) ((UniversalEnvelopingAlgebra.ι R) ((ψ h) s))

On a canonical Lie generator the quotient derivation is the original Lie derivation.

noncomputable def Ado.envelopingQuotientRep (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) : S ⋊⁅ψ⁆ H →ₗ⁅R⁆ Module.End R (UniversalEnvelopingAlgebra R S ⧸ J)

The representation of a split extension on a stable enveloping quotient, by left multiplication for S and descended derivations for H.

Equations

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

@[simp]

theorem Ado.envelopingQuotientRep_apply (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) (x : S ⋊⁅ψ⁆ H) (a : UniversalEnvelopingAlgebra R S ⧸ J) : ((envelopingQuotientRep R S ψ J hJ) x) a = (Ideal.Quotient.mk J) ((UniversalEnvelopingAlgebra.ι R) x.left) * a + ↑((envelopingQuotientDerivation R S ψ J hJ) x.right) a

The multiplication-plus-derivation formula for the split extension action.

@[simp]

theorem Ado.envelopingQuotientRep_mk_zero (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) (s : S) : (envelopingQuotientRep R S ψ J hJ) { left := s, right := 0 } = LinearMap.mulLeft R ((Ideal.Quotient.mk J) ((UniversalEnvelopingAlgebra.ι R) s))

On the ideal summand, the extension acts by left multiplication by the canonical image.

@[simp]

theorem Ado.envelopingQuotientRep_zero_mk (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) (h : H) : (envelopingQuotientRep R S ψ J hJ) { left := 0, right := h } = ↑((envelopingQuotientDerivation R S ψ J hJ) h)

On the complementary summand, the extension acts by the descended enveloping derivation.

theorem Ado.ker_envelopingQuotientRep_comp_inl_le (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) {V : Type u_1} [AddCommGroup V] [Module R V] (σ : S →ₗ⁅R⁆ Module.End R V) (hker : J ≤ RingHom.ker ((UniversalEnvelopingAlgebra.lift R) σ)) : ((envelopingQuotientRep R S ψ J hJ).comp (LieAlgebra.SemiDirectSum.inl ψ)).ker ≤ σ.ker

Refining the enveloping kernel of a representation preserves all directions it detects: the kernel of the new action restricted to S lies in the starting representation's kernel.

theorem Ado.isNilpotent_envelopingQuotientRep_inr (R : Type u) (S : Type v) {H : Type w} [CommRing R] [LieRing S] [LieAlgebra R S] [LieRing H] [LieAlgebra R H] (ψ : H →ₗ⁅R⁆ LieDerivation R S S) (J : Ideal (UniversalEnvelopingAlgebra R S)) [J.IsTwoSided] (hJ : ∀ (h : H), UniversalEnvelopingAlgebra.envelopingDerivation R S (ψ h) ∈ stableDerivations R (Submodule.restrictScalars R J)) [Module.Finite R (UniversalEnvelopingAlgebra R S ⧸ J)] (h : H) (hψ : ∀ (s : S), ∃ (n : ℕ), (↑(ψ h) ^ n) s = 0) : IsNilpotent ((envelopingQuotientRep R S ψ J hJ) ((LieAlgebra.SemiDirectSum.inr ψ) h))

A complementary element whose derivation on the ideal is locally nilpotent acts nilpotently on any stable enveloping quotient that is finitely generated over the coefficient ring.