comap_bracket_le — Mathlib

English

For a Lie algebra morphism f: L → L' and Lie ideals J1, J2 of L', the bracket of their comaps is contained in the comap of their bracket: [comap f J1, comap f J2] ≤ comap f [J1, J2].

Русский

Для гомоморфизма Ли f: L → L' и Ли-идеалов J1, J2 в L' скобка между их предобразами по f содержится в предобразе их скобки: [comap f J1, comap f J2] ≤ comap f [J1, J2].

LaTeX

$$$$ [\operatorname{comap} f J_1, \operatorname{comap} f J_2] \leq \operatorname{comap} f [J_1, J_2]. $$$$

Lean4

theorem comap_bracket_le {J₁ J₂ : LieIdeal R L'} : ⁅comap f J₁, comap f J₂⁆ ≤ comap f ⁅J₁, J₂⁆ :=
  by
  rw [← map_le_iff_le_comap]
  exact le_trans (map_bracket_le f) (LieSubmodule.mono_lie map_comap_le map_comap_le)

Похожие утверждения