Extension of scalars of a homomorphism of Lie algebras

Mathlib extends the scalars of a Lie algebra L over R to A ⊗[R] L over an R-algebra A, and LieAlgebra.ExtendScalars.map extends a homomorphism along a map of coefficient algebras. That map is a homomorphism of Lie algebras over R, which is the right generality when the coefficients move. When the coefficients stay put -- the case a descent argument needs -- the same underlying linear map LinearMap.baseChange is A-linear, and the resulting A-Lie homomorphism LieHom.baseChange is what this file records.

The point of the A-linear form is that its kernel is a LieIdeal A (A ⊗[R] L), and so may be compared with LieSubmodule.baseChange. The two agree over a flat coefficient algebra, and, for a surjective homomorphism, over an arbitrary one. Together with functoriality and the preservation of surjectivity, that comparison is what lets a question about an ideal of A ⊗[R] L be moved to one about L; its first use is the identification of a quotient of A ⊗[R] L with the extension of a quotient of L.

Main definitions

• LieHom.baseChange: the extension of scalars A ⊗[R] L →ₗ⁅A⁆ A ⊗[R] L' of a homomorphism of Lie algebras.

Main results

• LieHom.baseChange_id and LieHom.baseChange_comp: extension of scalars is functorial.
• LieHom.baseChange_surjective: extension of scalars preserves surjectivity.
• LieHom.ker_baseChange and LieHom.ker_baseChange_of_surjective: the kernel of an extended homomorphism is the extension of its kernel, over a flat coefficient algebra, respectively for a surjective homomorphism over an arbitrary one.

def LieHom.baseChange {R : Type u} {L : Type w} {L' : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (A : Type v) [CommRing A] [Algebra R A] (f : L →ₗ⁅R⁆ L') : TensorProduct R A L →ₗ⁅A⁆ TensorProduct R A L'

The extension of scalars of a homomorphism of Lie algebras, as a homomorphism of Lie algebras over the extended coefficients.

Its underlying map is LinearMap.baseChange, so it agrees with LieAlgebra.ExtendScalars.map (AlgHom.id R A) f; the difference is that this form is linear over A rather than over R, which is what makes its kernel an ideal of A ⊗[R] L over A.

Equations

• LieHom.baseChange A f = { toLinearMap := LinearMap.baseChange A ↑f, map_lie' := ⋯ }

@[simp]

theorem LieHom.coe_baseChange {R : Type u} {L : Type w} {L' : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (A : Type v) [CommRing A] [Algebra R A] (f : L →ₗ⁅R⁆ L') : ↑(baseChange A f) = LinearMap.baseChange A ↑f

@[simp]

theorem LieHom.baseChange_tmul {R : Type u} {L : Type w} {L' : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (A : Type v) [CommRing A] [Algebra R A] (f : L →ₗ⁅R⁆ L') (a : A) (x : L) : (baseChange A f) (a ⊗ₜ[R] x) = a ⊗ₜ[R] f x

@[simp]

theorem LieHom.baseChange_id {R : Type u} {L : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] (A : Type v) [CommRing A] [Algebra R A] : baseChange A id = id

Extension of scalars is functorial: it takes the identity to the identity.

theorem LieHom.baseChange_comp {R : Type u} {L : Type w} {L' : Type x} {L'' : Type y} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] [LieRing L''] [LieAlgebra R L''] (A : Type v) [CommRing A] [Algebra R A] (f : L →ₗ⁅R⁆ L') (g : L' →ₗ⁅R⁆ L'') : baseChange A (g.comp f) = (baseChange A g).comp (baseChange A f)

Extension of scalars is functorial: it takes a composition to the composition.

theorem LieHom.baseChange_surjective {R : Type u} {L : Type w} {L' : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (A : Type v) [CommRing A] [Algebra R A] (f : L →ₗ⁅R⁆ L') (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(baseChange A f)

Extension of scalars preserves surjectivity: the tensor product is right exact.

@[simp]

theorem LieHom.ker_baseChange {R : Type u} {L : Type w} {L' : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (A : Type v) [CommRing A] [Algebra R A] (f : L →ₗ⁅R⁆ L') [Module.Flat R A] : (baseChange A f).ker = LieSubmodule.baseChange A f.ker

Over a flat coefficient algebra, extension of scalars commutes with kernels: the kernel of the extended homomorphism is the extension of the kernel.

Flatness is what makes the containment (ker f).baseChange A ≤ ker (baseChange A f), which holds for any coefficient algebra, an equality. For a surjective homomorphism it is an equality over an arbitrary coefficient algebra, which is LieHom.ker_baseChange_of_surjective.

@[simp]

theorem LieHom.ker_baseChange_of_surjective {R : Type u} {L : Type w} {L' : Type x} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (A : Type v) [CommRing A] [Algebra R A] (f : L →ₗ⁅R⁆ L') (hf : Function.Surjective ⇑f) : (baseChange A f).ker = LieSubmodule.baseChange A f.ker

For a surjective homomorphism, extension of scalars commutes with kernels over an arbitrary coefficient algebra. Surjectivity of f replaces the flatness of A that LieHom.ker_baseChange assumes.