idealRange_eq_top_of_surjective — Mathlib

English

If a Lie algebra hom f: L → L' is onto, the ideal generated by its image is the whole L'.

Русский

Пусть f: L → L' — сюръективный гомоморфизм Ли-алгебр. Тогда образующийся имуществом идеал f(I) порождает всю L'.

LaTeX

$$$\text{Surjective}(f) \Rightarrow f.idealRange = \top$$$

Lean4

@[simp]
theorem idealRange_eq_top_of_surjective (h : Function.Surjective f) : f.idealRange = ⊤ :=
  by
  rw [← f.range_eq_top] at h
  rw [idealRange_eq_lieSpan_range, h, ← LieSubalgebra.coe_toSubmodule, ← LieSubmodule.toSubmodule_inj,
    LieSubmodule.top_toSubmodule, LieSubalgebra.top_toSubmodule, LieSubmodule.coe_lieSpan_submodule_eq_iff]
  use ⊤
  exact LieSubmodule.top_toSubmodule

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