English
Let f: L → L' be a Lie algebra homomorphism and I1, I2 be Lie ideals of L. Then the image under f of the bracket [I1, I2] is contained in the bracket of the images: f([I1, I2]) ⊆ [f(I1), f(I2)]. Note that the inclusion can be strict in general.
Русский
Пусть f: L → L' — гомоморфизм по Ли, а I1, I2 — Ли-идеалы L. Тогда образ brackets [I1, I2] под действием f содержится в скобке образов: f([I1, I2]) ⊆ [f(I1), f(I2)]. Замечаем, что включение может быть строгим.
LaTeX
$$$$ f([I_1,I_2]) \subseteq [f(I_1), f(I_2)]. $$$$
Lean4
/-- Note that the inequality can be strict; e.g., the inclusion of an Abelian subalgebra of a
simple algebra. -/
theorem map_bracket_le {I₁ I₂ : LieIdeal R L} : map f ⁅I₁, I₂⁆ ≤ ⁅map f I₁, map f I₂⁆ :=
by
rw [map_le_iff_le_comap, LieSubmodule.lieIdeal_oper_eq_span, LieSubmodule.lieSpan_le]
intro x hx
obtain ⟨⟨y₁, hy₁⟩, ⟨y₂, hy₂⟩, hx⟩ := hx
rw [← hx]
let fy₁ : ↥(map f I₁) := ⟨f y₁, mem_map hy₁⟩
let fy₂ : ↥(map f I₂) := ⟨f y₂, mem_map hy₂⟩
change _ ∈ comap f ⁅map f I₁, map f I₂⁆
simp only [mem_comap, LieHom.map_lie]
exact LieSubmodule.lie_coe_mem_lie fy₁ fy₂
