exact — Mathlib

English

The sequence of modules and maps 0 → R → G → M → 0 is exact; i.e., the image of the first map equals the kernel of the second, and the last map is surjective.

Русский

Последовательность 0 → R → G → M → 0 точна: образ первого отображения равен ядру второго, и последнее отображение сюръектно.

LaTeX

$$$$ 0 \\to \\mathrm{R} \\xrightarrow{\\mathrm{map}} \\mathrm{G} \\xrightarrow{\\pi} M \\to 0 \\quad \\text{is exact} $$$$

Lean4

/-- The sequence `(relations.R →₀ A) → (relations.G →₀ A) → M → 0` is exact. -/
theorem exact : Function.Exact relations.map solution.π :=
  by
  rw [LinearMap.exact_iff, range_map, ← solution.injective_fromQuotient_iff_ker_π_eq_span]
  exact h.bijective.1

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