Commit 2023-10-27 07:47 dc43514e

View on Github →

feat: a split short complex is exact (#7816)

Estimated changes

Modified Mathlib/Algebra/Homology/ShortComplex/Exact.lean

added theorem CategoryTheory.ShortComplex.QuasiIso.exact_iff

added theorem CategoryTheory.ShortComplex.Splitting.epi_g

added theorem CategoryTheory.ShortComplex.Splitting.exact

added theorem CategoryTheory.ShortComplex.Splitting.ext_r

added theorem CategoryTheory.ShortComplex.Splitting.ext_s

added theorem CategoryTheory.ShortComplex.Splitting.g_s

added theorem CategoryTheory.ShortComplex.Splitting.isSplitEpi_g

added theorem CategoryTheory.ShortComplex.Splitting.isSplitMono_f

added theorem CategoryTheory.ShortComplex.Splitting.mono_f

added theorem CategoryTheory.ShortComplex.Splitting.r_f

added theorem CategoryTheory.ShortComplex.Splitting.s_r

added def CategoryTheory.ShortComplex.Splitting.splitEpi_g

added def CategoryTheory.ShortComplex.Splitting.splitMono_f

added structure CategoryTheory.ShortComplex.Splitting

added theorem CategoryTheory.ShortComplex.exact_of_f_is_kernel

added theorem CategoryTheory.ShortComplex.exact_of_g_is_cokernel