Commit 2023-10-30 19:25 35528f8c

View on Github →

feat: exactness of short complexes in balanced categories (#7996)

Estimated changes

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

added theorem CategoryTheory.ShortComplex.Exact.desc'

added theorem CategoryTheory.ShortComplex.Exact.g_desc

added theorem CategoryTheory.ShortComplex.Exact.isIso_f'

added theorem CategoryTheory.ShortComplex.Exact.isIso_fromOpcycles

added theorem CategoryTheory.ShortComplex.Exact.isIso_g'

added theorem CategoryTheory.ShortComplex.Exact.isIso_toCycles

added theorem CategoryTheory.ShortComplex.Exact.lift'

added theorem CategoryTheory.ShortComplex.Exact.lift_f

added theorem CategoryTheory.ShortComplex.Exact.map_of_epi_of_preservesCokernel

added theorem CategoryTheory.ShortComplex.Exact.map_of_mono_of_preservesKernel

added theorem CategoryTheory.ShortComplex.epi_τ₂_of_exact_of_epi

added theorem CategoryTheory.ShortComplex.mono_τ₂_of_exact_of_mono