Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-11-03 07:31
8ddc254c
View on Github →
feat: exactness of short complexes in concrete categories (
#8060
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Algebra/Homology/ShortComplex/Ab.lean
added
theorem
CategoryTheory.ShortComplex.ShortExact.ab_injective_f
added
theorem
CategoryTheory.ShortComplex.ShortExact.ab_surjective_g
Created
Mathlib/Algebra/Homology/ShortComplex/ConcreteCategory.lean
added
theorem
CategoryTheory.Preadditive.epi_iff_injective
added
theorem
CategoryTheory.Preadditive.mono_iff_injective
added
theorem
CategoryTheory.ShortComplex.ShortExact.injective_f
added
theorem
CategoryTheory.ShortComplex.ShortExact.surjective_g
added
theorem
CategoryTheory.ShortComplex.exact_iff_exact_map_forget₂
added
theorem
CategoryTheory.ShortComplex.exact_iff_of_concreteCategory
added
theorem
CategoryTheory.ShortComplex.zero_apply