exact_zero_iff_surjective — Mathlib

English

For any linear f: M → N, the sequence f → 0 is exact if and only if f is surjective.

Русский

Для линейного отображения f: M → N последовательность M → N → 0 точна тогда, когда f сюръективна.

LaTeX

$$$$ \\operatorname{Exact}(f, 0: N \\to P) \\;\\Longleftrightarrow\\; \\operatorname{Surjective}(f). $$$$

Lean4

@[simp]
theorem exact_zero_iff_surjective {M N : Type*} (P : Type*) [AddCommGroup M] [AddCommGroup N] [AddCommMonoid P]
    [Module R N] [Module R M] [Module R P] (f : M →ₗ[R] N) : Function.Exact f (0 : N →ₗ[R] P) ↔ Function.Surjective f :=
  by simp [← range_eq_top, exact_iff, eq_comm]

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