map_sup_ker_eq_map — Mathlib

English

For any LieIdeal I, the image of I under f composed with ker f satisfies Im f(I ⊔ ker f) = Im f(I).

Русский

Для идеала I вернемся к Im f (I ⊔ ker f) = Im f(I).

LaTeX

$$$\operatorname{map}(f, I \oplus \ker f) = \operatorname{map}(f, I)$$$

Lean4

theorem map_sup_ker_eq_map : LieIdeal.map f (I ⊔ f.ker) = LieIdeal.map f I :=
  by
  refine le_antisymm ?_ (LieIdeal.map_mono le_sup_left)
  apply LieSubmodule.lieSpan_mono
  rintro x ⟨y, hy₁, hy₂⟩
  rw [← hy₂]
  erw [LieSubmodule.mem_sup] at hy₁
  obtain ⟨z₁, hz₁, z₂, hz₂, hy⟩ := hy₁
  rw [← hy]
  rw [f.coe_toLinearMap, f.map_add, LieHom.mem_ker.mp hz₂, add_zero]; exact ⟨z₁, hz₁, rfl⟩

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