English
For any f: L → L' that is an ideal morphism and any J1, J2 Lie ideals in L', the equality holds: map f ( [comap f J1, comap f J2] ) = [ f.idealRange ∩ J1, f.idealRange ∩ J2 ].
Русский
Для любого f: L → L', являющегося морфизмом по идеалам, и любых J1, J2 — Ли-идеалов в L', выполняется равенство: map f([comap f J1, comap f J2]) = [f(idealRange) ∩ J1, f(idealRange) ∩ J2].
LaTeX
$$$$ \operatorname{map} f \bigl([\operatorname{comap} f J_1, \operatorname{comap} f J_2]\bigr) = [ f(\operatorname{idealRange}) \cap J_1, f(\operatorname{idealRange}) \cap J_2 ]. $$$$
Lean4
theorem comap_bracket_eq {J₁ J₂ : LieIdeal R L'} (h : f.IsIdealMorphism) :
comap f ⁅f.idealRange ⊓ J₁, f.idealRange ⊓ J₂⁆ = ⁅comap f J₁, comap f J₂⁆ ⊔ f.ker :=
by
rw [← LieSubmodule.toSubmodule_inj, comap_toSubmodule, LieSubmodule.sup_toSubmodule, f.ker_toSubmodule, ←
Submodule.comap_map_eq, LieSubmodule.lieIdeal_oper_eq_linear_span, LieSubmodule.lieIdeal_oper_eq_linear_span,
LinearMap.map_span]
congr
ext
simp_all only [Subtype.exists, LieSubmodule.mem_inf, LieHom.mem_idealRange_iff, exists_prop, Set.mem_setOf_eq,
LieHom.coe_toLinearMap, mem_comap, exists_exists_and_exists_and_eq_and, LieHom.map_lie]
grind
