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