English
For a LieHom f: L → L' that is an ideal morphism and Lie ideals J1, J2 in L', one has: comap f [J1, J2] = [comap f J1, comap f J2].
Русский
Пусть f: L → L' — гомоморфизм по идеалам и J1, J2 — Ли-идеалы в L'. Тогда comap f [J1, J2] = [comap f J1, comap f J2].
LaTeX
$$$$ \operatorname{comap} f [J_1, J_2] = [\operatorname{comap} f J_1, \operatorname{comap} f J_2]. $$$$
Lean4
/-- This is a very useful result; it allows us to use the fact that inclusion distributes over the
Lie bracket operation on ideals, subject to the conditions shown. -/
theorem comap_bracket_incl_of_le {I₁ I₂ : LieIdeal R L} (h₁ : I₁ ≤ I) (h₂ : I₂ ≤ I) :
⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I₁, I₂⁆ := by rw [comap_bracket_incl];
rw [← inf_eq_right] at h₁ h₂; rw [h₁, h₂]
