English
Assume f: L → L' is a surjective Lie algebra homomorphism. Then the image of the bracket of two ideals equals the bracket of their images: f([I1, I2]) = [f(I1), f(I2)].
Русский
Пусть f: L → L' — сюръективный гомоморфизм Ли. Тогда образ.bracket(I1, I2) равен bracket образов: f([I1, I2]) = [f(I1), f(I2)].
LaTeX
$$$$ f([I_1,I_2]) = [f(I_1), f(I_2)]. $$$$
Lean4
theorem map_bracket_eq {I₁ I₂ : LieIdeal R L} (h : Function.Surjective f) : map f ⁅I₁, I₂⁆ = ⁅map f I₁, map f I₂⁆ :=
by
suffices ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆ by exact le_antisymm (map_bracket_le f) this
rw [← LieSubmodule.toSubmodule_le_toSubmodule, coe_map_of_surjective h, LieSubmodule.lieIdeal_oper_eq_linear_span,
LieSubmodule.lieIdeal_oper_eq_linear_span, LinearMap.map_span]
apply Submodule.span_mono
rintro x ⟨⟨z₁, h₁⟩, ⟨z₂, h₂⟩, rfl⟩
obtain ⟨y₁, rfl⟩ := mem_map_of_surjective h h₁
obtain ⟨y₂, rfl⟩ := mem_map_of_surjective h h₂
exact ⟨⁅(y₁ : L), (y₂ : L)⁆, ⟨y₁, y₂, rfl⟩, by apply f.map_lie⟩
