exact_iff_isIso_imageToKernel — Mathlib

English

A short complex S is exact iff imageToKernel S.f S.g S.zero is an isomorphism.

Русский

Краткая последовательность S точна тогда и только тогда, когда imageToKernel S.f S.g S.zero является изоморфизмом.

LaTeX

$$$S\\text{.Exact} \\iff \\mathrm{IsIso}(\\mathrm{imageToKernel}(S.f,S.g,S.zero))$$$

Lean4

theorem exact_iff_isIso_imageToKernel : S.Exact ↔ IsIso (imageToKernel S.f S.g S.zero) :=
  by
  rw [S.exact_iff_epi_imageToKernel]
  constructor
  · intro
    apply isIso_of_mono_of_epi
  · intro
    infer_instance

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