English
Let f be a Lie algebra homomorphism over R between Lie algebras L and L'. Then the image of f equals the whole target if and only if for every element of L' there exists a preimage in L, i.e., im(f) = L' ⇔ ∀ y ∈ L', ∃ x ∈ L with f(x) = y.
Русский
Пусть f — гомоморфизм Lie-алгебр над кольцом R между Lie-алгебрами L и L'. Тогда образ f равен всей целевой алгебре тогда и только тогда, когда для каждого элемента y из L' существует элемент x из L такой, что f(x) = y, т.е. im(f) = L' ⇔ ∀ y ∈ L', ∃ x ∈ L: f(x) = y.
LaTeX
$$$\operatorname{im}(f) = L' \ \Longleftrightarrow\ \forall y \in L',\ \exists x \in L:\ f(x)=y$$$
Lean4
theorem range_eq_top : f.range = ⊤ ↔ Function.Surjective f :=
by
rw [← LieSubalgebra.toSubmodule_inj, range_toSubmodule, LieSubalgebra.top_toSubmodule]
exact LinearMap.range_eq_top
