Descent of membership and of bracket equations after extension of scalars

Over a faithfully flat coefficient algebra, membership of 1 ⊗ₜ x in the extension of a Lie submodule descends to membership of x in the submodule itself; this is the underlying Submodule.one_tmul_mem_baseChange_iff read through LieSubmodule.coe_baseChange.

The adjoint endomorphism of a Lie algebra commutes with extension of scalars. Consequently, a bracket equation x = ⁅x, y⁆ that has a solution after a faithfully flat extension already has a solution over the original coefficient ring. In particular, passing to an algebraic closure cannot create a solution to such an equation.

The compatibility with the adjoint action uses LieModule.toEnd_baseChange from Mathlib/Algebra/Lie/BaseChange.lean.

Main results

• LieSubmodule.one_tmul_mem_baseChange_iff: membership in a Lie submodule may be checked after a faithfully flat extension of scalars.
• LieAlgebra.exists_eq_lie_of_one_tmul_mem_range_ad: membership of 1 ⊗ₜ x in the range of the extended adjoint endomorphism descends to an equation x = ⁅x, y⁆.

@[simp]

theorem LieSubmodule.one_tmul_mem_baseChange_iff {R : Type u} {A : Type v} {L : Type w} {M : Type x} [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [Module.FaithfullyFlat R A] (N : LieSubmodule R L M) (m : M) : 1 ⊗ₜ[R] m ∈ baseChange A N ↔ m ∈ N

Over a faithfully flat coefficient algebra, a vector lies in a Lie submodule exactly when its canonical image lies in the extension of that submodule.

theorem LieAlgebra.exists_eq_lie_of_one_tmul_mem_range_ad (R : Type u) (A : Type v) (L : Type w) [CommRing R] [CommRing A] [Algebra R A] [LieRing L] [LieAlgebra R L] [Module.FaithfullyFlat R A] (x : L) (hx : 1 ⊗ₜ[R] x ∈ LinearMap.range ((ad A (TensorProduct R A L)) (1 ⊗ₜ[R] x))) : ∃ (y : L), x = ⁅x, y⁆

A bracket equation that becomes solvable after a faithfully flat extension of scalars was already solvable over the original coefficient ring.