isExtension_of_surjective — Mathlib

English

A surjective Lie algebra homomorphism f: L → M yields an extension; equivalently, the short exact sequence 0 → ker(f) → L → M → 0 holds in the Lie algebra sense.

Русский

Гомоморфизм Лиг-алгебр с сюръективностью образует расширение: 0 → ker(f) → L → M → 0.

LaTeX

$$IsExtension(f.ker.incl, f)$$

Lean4

/-- A surjective Lie algebra homomorphism yields an extension. -/
theorem isExtension_of_surjective (f : L →ₗ⁅R⁆ M) (hf : Function.Surjective f) : IsExtension f.ker.incl f
    where
  ker_eq_bot := LieIdeal.ker_incl f.ker
  range_eq_top := (LieHom.range_eq_top f).mpr hf
  exact := LieIdeal.incl_range f.ker

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