map_comap_bracket_eq — Mathlib

English

For Lie ideals J1, J2 in L', the inequality holds: [comap f J1, comap f J2] ≤ comap f [J1, J2].

Русский

Для Ли-идеалов J1, J2 в L' выполняется неравенство: [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 map_comap_bracket_eq {J₁ J₂ : LieIdeal R L'} (h : f.IsIdealMorphism) :
    map f ⁅comap f J₁, comap f J₂⁆ = ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ :=
  by
  rw [← map_sup_ker_eq_map, ← comap_bracket_eq h, map_comap_eq h, inf_eq_right]
  exact le_trans (LieSubmodule.lie_le_left _ _) inf_le_left

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