surjective — Mathlib

English

Let R be a commutative ring, L a Lie ring, and M,N Lie R-modules with L-action. For any Lie module equivalence e: M ≃ₗ⁅R,L⁆ N, the underlying function e: M → N is surjective.

Русский

Пусть R — коммутативное кольцо, L — Ли-количество, M,N — Ли-модули над R с действием L. Для любой эквивалентности Ли-модуля e: M ≃ₗ⁅R,L⁆ N отображение e: M → N является сюрьективным.

LaTeX

$$$e[M] = N$$$

Lean4

theorem surjective (e : M ≃ₗ⁅R,L⁆ N) : Function.Surjective e :=
  e.toEquiv.surjective

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