moduleCat_range_eq_ker — Mathlib

English

Exactness of the short complex is equivalent to the exactness of the pair of functions at the underlying level of sets/maps.

Русский

Точность короткого комплекса эквивалентна точности пары отображений на уровне функций.

LaTeX

$$$S.Exact \\iff \\mathrm{Exact} (f,g)$$$

Lean4

theorem moduleCat_range_eq_ker (hS : S.Exact) : LinearMap.range S.f.hom = LinearMap.ker S.g.hom := by
  simpa only [moduleCat_exact_iff_range_eq_ker] using hS

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