map_eq_bot_iff

Mathlib.Algebra.Lie.Ideal

URI: https://scilib.ai/kg/mathlib#LieIdeal.map_eq_bot_iff

English

For a Lie algebra hom f and Lie ideal I, the image I.map f is zero iff I is contained in the kernel of f.

Русский

Для гомоморфизма Lie f и Lie-ideала I выполняется I.map f = {0} тогда и только тогда, когда I ⊆ ker f.

LaTeX

$$$I.\mathrm{map}\ f = \{0\} \iff I \leq \ker f$$$

Lean4

@[simp]
theorem map_eq_bot_iff : I.map f = ⊥ ↔ I ≤ f.ker :=
  by
  rw [← le_bot_iff]
  exact LieIdeal.map_le_iff_le_comap

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru