Commit 2023-11-01 09:55 fa84cf7e

View on Github →

feat: short exact short complexes (#8058)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean

added theorem CategoryTheory.ShortComplex.ShortExact.isIso_f_iff

added theorem CategoryTheory.ShortComplex.ShortExact.isIso_g_iff

added theorem CategoryTheory.ShortComplex.ShortExact.map

added theorem CategoryTheory.ShortComplex.ShortExact.map_of_exact

added theorem CategoryTheory.ShortComplex.ShortExact.mk'

added theorem CategoryTheory.ShortComplex.ShortExact.op

added theorem CategoryTheory.ShortComplex.ShortExact.unop

added structure CategoryTheory.ShortComplex.ShortExact

added theorem CategoryTheory.ShortComplex.Splitting.shortExact

added theorem CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃'

added theorem CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃

added theorem CategoryTheory.ShortComplex.shortExact_iff_of_iso

added theorem CategoryTheory.ShortComplex.shortExact_iff_op

added theorem CategoryTheory.ShortComplex.shortExact_iff_unop

added theorem CategoryTheory.ShortComplex.shortExact_of_iso