Commit 2023-11-10 12:46 101dcc0c

View on Github →

feat(CategoryTheory): exact sequences (#8152) This PR defines the predicate ComposableArrows.Exact.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Homology/ExactSequence.lean

added structure CategoryTheory.ComposableArrows.Exact

added theorem CategoryTheory.ComposableArrows.IsComplex.zero'

added structure CategoryTheory.ComposableArrows.IsComplex

added theorem CategoryTheory.ComposableArrows.IsExact.exact'

added theorem CategoryTheory.ComposableArrows.exact_iff_of_iso

added theorem CategoryTheory.ComposableArrows.exact_of_iso

added theorem CategoryTheory.ComposableArrows.isComplex_iff_of_iso

added theorem CategoryTheory.ComposableArrows.isComplex_of_iso

added theorem CategoryTheory.ComposableArrows.isComplex₀

added theorem CategoryTheory.ComposableArrows.isComplex₁

added def CategoryTheory.ComposableArrows.sc'

added def CategoryTheory.ComposableArrows.sc'Map

added def CategoryTheory.ComposableArrows.sc'MapIso

added def CategoryTheory.ComposableArrows.scMap

added def CategoryTheory.ComposableArrows.scMapIso

added def CategoryTheory.ShortComplex.toComposableArrows