Lean4
/-- Given a family of Lie algebras `L i`, together with a family of morphisms of Lie algebras
`f i : L i →ₗ⁅R⁆ L'` into a fixed Lie algebra `L'`, we have a natural linear map:
`(⨁ i, L i) →ₗ[R] L'`. If in addition `⁅f i x, f j y⁆ = 0` for any `x ∈ L i` and `y ∈ L j` (`i ≠ j`)
then this map is a morphism of Lie algebras. -/
@[simps]
def toLieAlgebra [DecidableEq ι] (L' : Type w₁) [LieRing L'] [LieAlgebra R L'] (f : ∀ i, L i →ₗ⁅R⁆ L')
(hf : Pairwise fun i j => ∀ (x : L i) (y : L j), ⁅f i x, f j y⁆ = 0) : (⨁ i, L i) →ₗ⁅R⁆ L' :=
{
toModule R ι L' fun i =>
(f i : L i →ₗ[R] L') with
toFun := toModule R ι L' fun i => (f i : L i →ₗ[R] L')
map_lie' := fun {x y} =>
by
let f' i :=
(f i : L i →ₗ[R] L')
/- The goal is linear in `y`. We can use this to reduce to the case that `y` has only one
non-zero component. -/
suffices
∀ (i : ι) (y : L i), toModule R ι L' f' ⁅x, of L i y⁆ = ⁅toModule R ι L' f' x, toModule R ι L' f' (of L i y)⁆
by
simp only [← LieAlgebra.ad_apply R]
rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]
congr; clear y; ext i y; exact this i y
suffices
∀ (i j) (y : L i) (x : L j),
toModule R ι L' f' ⁅of L j x, of L i y⁆ = ⁅toModule R ι L' f' (of L j x), toModule R ι L' f' (of L i y)⁆
by
intro i y
rw [← lie_skew x, ← lie_skew (toModule R ι L' f' x)]
simp only [LinearMap.map_neg, neg_inj, ← LieAlgebra.ad_apply R]
rw [← LinearMap.comp_apply, ← LinearMap.comp_apply]
congr; clear x; ext j x; exact this j i x y
intro i j y x
simp only [f', coe_toModule_eq_coe_toAddMonoid, toAddMonoid_of]
-- And finish with trivial case analysis.
obtain rfl | hij := Decidable.eq_or_ne i j
· simp_rw [lie_of_same, toAddMonoid_of, LinearMap.toAddMonoidHom_coe, LieHom.coe_toLinearMap, LieHom.map_lie]
·
simp_rw [lie_of_of_ne _ hij.symm, map_zero, LinearMap.toAddMonoidHom_coe, LieHom.coe_toLinearMap,
hf hij.symm x y] }
