exact_iff_exact_map_forget₂ — Mathlib

English

Let S be a Short Complex in C with HasHomology. Then S is exact if and only if its image under the forgetful functor to Ab, S.map(forget₂ C Ab), is exact.

Русский

Пусть S — краткая комплексная последовательность в C с условием наличия гомологии. Тогда точность S эквивалентна точности образа S под забыванием в категорию абелевых групп.

LaTeX

$$$S.Exact \\iff (S.map(\\forget_2\\ C\\ Ab)).Exact$$$

Lean4

theorem exact_iff_exact_map_forget₂ [S.HasHomology] : S.Exact ↔ (S.map (forget₂ C Ab)).Exact :=
  (S.exact_map_iff_of_faithful (forget₂ C Ab)).symm

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