moduleCat_exact_iff_range_eq_ker

Mathlib.Algebra.Homology.ShortComplex.ModuleCat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.moduleCat_exact_iff_range_eq_ker

← MathLib Explorer

English

Exactness is equivalent to equality of the image of f and the kernel of g: range f = ker g.

Русский

Точность эквивалентна равенству образа f и ядра g: \\operatorname{range}(f) = \\ker(g).

LaTeX

$$$S.Exact \\iff \\mathrm{range} S.f.hom = \\ker S.g.hom$$$

Lean4

theorem moduleCat_exact_iff_range_eq_ker : S.Exact ↔ LinearMap.range S.f.hom = LinearMap.ker S.g.hom :=
  by
  rw [moduleCat_exact_iff_ker_sub_range]
  aesop

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru