Extension of scalars commutes with quotients of Lie algebras #

For a Lie ideal I of L and an R-algebra A, extending the scalars of the quotient L ⧸ I gives the same Lie algebra over A as quotienting the extension A ⊗[R] L by the extension of I:

(A ⊗[R] L) ⧸ I.baseChange A ≃ₗ⁅A⁆ A ⊗[R] (L ⧸ I).

Nothing is asked of the coefficient algebra; in particular A need not be flat over R. The isomorphism is the obvious one on pure tensors, and it and its inverse are both characterized there, so the bundled equivalence is not opaque. Its use is to move a question about an ideal of A ⊗[R] L containing an extended ideal to the extension of the corresponding quotient of L, as the base change of the solvable radical does.

Main definitions #

LieIdeal.quotientBaseChangeEquiv: extension of scalars commutes with quotients.

Main results #

LieIdeal.ker_baseChange_mkQ: the extension of scalars of the quotient map of I kills exactly the extension of I.

References #

[N. Bourbaki, Algebra I, Chapters 1-3][bourbaki1989], Chapter II, §3, n°6, for the right-exactness of the tensor product that the kernel computation rests on.

source

@[simp]

theorem LieIdeal.ker_baseChange_mkQ {R : Type u} {L : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] (A : Type v) [CommRing A] [Algebra R A] (I : LieIdeal R L) :

(LieHom.baseChange A I.mkQ).ker = LieSubmodule.baseChange A I

The extension of scalars of the quotient map of I kills exactly the extension of I.

source

noncomputable def LieIdeal.quotientBaseChangeEquiv {R : Type u} {L : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] (A : Type v) [CommRing A] [Algebra R A] (I : LieIdeal R L) :

(TensorProduct R A L ⧸ LieSubmodule.baseChange A I) ≃ₗ⁅A⁆ TensorProduct R A (L ⧸ I)

Extension of scalars commutes with quotients of Lie algebras. The extension of L ⧸ I is the quotient of the extension of L by the extension of I, for an arbitrary coefficient algebra A.

The isomorphism sends the class of a ⊗ₜ x to a ⊗ₜ the class of x, which is LieIdeal.quotientBaseChangeEquiv_mk_tmul; LieIdeal.quotientBaseChangeEquiv_symm_tmul describes its inverse. Both are phrased with LieSubmodule.Quotient.mk rather than LieIdeal.mkQ, the form in which the quotient's induction principle presents a class.

Equations