Rationalizing integral Lie lattices

Let M be a free full Lie lattice over a domain R in a Lie algebra L over its fraction field K. The underlying submodule inclusion exhibits L as the scalar extension K ⊗[R] M. This file proves that the canonical rationalization equivalence respects the Lie bracket, giving

K ⊗[R] M ≃ₗ⁅K⁆ L.

The source carries Mathlib's scalar-extended Lie bracket. Thus the result identifies the generic fibre as a Lie algebra, rather than only as a vector space. Its pure-tensor and inverse equations make the equivalence usable without unfolding either the tensor-product bracket or the lattice rationalization construction.

Main declaration

• LieSubalgebra.rationalizationEquiv: the canonical Lie equivalence from the scalar extension of a free full integral Lie subalgebra to its ambient rational Lie algebra.

References

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

This is the generic-fibre step for the Chevalley integral form used in Layer 9 of the ReductiveGroups roadmap. That pinned Chevalley--Demazure construction is consumed by milestone L0 of the CFSGStatement roadmap.

noncomputable def LieSubalgebra.rationalizationEquiv {R : Type u} {K : Type v} {L : Type w} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [LieRing L] [LieAlgebra R L] [LieAlgebra K L] [IsScalarTower R K L] (M : LieSubalgebra R L) [Module.Free R ↥M] [Submodule.IsLattice K M.toSubmodule] : TensorProduct R K ↥M ≃ₗ⁅K⁆ L

The canonical rationalization of a free full integral Lie subalgebra, as a Lie algebra equivalence.

The underlying linear equivalence is TauCeti.Submodule.rationalizationEquiv. The bracket on its source is Mathlib's scalar-extension bracket on K ⊗[R] M.

Equations

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

@[simp]

theorem LieSubalgebra.rationalizationEquiv_tmul {R : Type u} {K : Type v} {L : Type w} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [LieRing L] [LieAlgebra R L] [LieAlgebra K L] [IsScalarTower R K L] (M : LieSubalgebra R L) [Module.Free R ↥M] [Submodule.IsLattice K M.toSubmodule] (q : K) (x : ↥M) : M.rationalizationEquiv (q ⊗ₜ[R] x) = q • ↑x

Rationalization sends a pure tensor to scalar multiplication of the embedded integral element.

@[simp]

theorem LieSubalgebra.rationalizationEquiv_symm_coe {R : Type u} {K : Type v} {L : Type w} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [LieRing L] [LieAlgebra R L] [LieAlgebra K L] [IsScalarTower R K L] (M : LieSubalgebra R L) [Module.Free R ↥M] [Submodule.IsLattice K M.toSubmodule] (x : ↥M) : M.rationalizationEquiv.symm ↑x = 1 ⊗ₜ[R] x

The inverse rationalization sends an embedded integral element to its unit pure tensor.