exact_zero_iff_injective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem exact_zero_iff_injective {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 (0 : P →ₗ[R] M) f ↔ Function.Injective f :=
  by simp [← ker_eq_bot, exact_iff]

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