Commit 2023-05-24 10:36 357ecbc8

View on Github →

feat: Algebra.Homology.ShortComplex.Basic (#4203) This PR introduces the category of short complexes X₁ ⟶ X₂ ⟶ X₃ in a category with zero morphisms.

Estimated changes

Modified Mathlib.lean

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

added def CategoryTheory.Functor.mapShortComplex

added def CategoryTheory.ShortComplex.Hom.comp

added def CategoryTheory.ShortComplex.Hom.id

added structure CategoryTheory.ShortComplex.Hom

added theorem CategoryTheory.ShortComplex.comp_τ₁

added theorem CategoryTheory.ShortComplex.comp_τ₂

added theorem CategoryTheory.ShortComplex.comp_τ₃

added def CategoryTheory.ShortComplex.homMk

added theorem CategoryTheory.ShortComplex.hom_ext

added theorem CategoryTheory.ShortComplex.id_τ₁

added theorem CategoryTheory.ShortComplex.id_τ₂

added theorem CategoryTheory.ShortComplex.id_τ₃

added theorem CategoryTheory.ShortComplex.isIso_of_isIso

added def CategoryTheory.ShortComplex.isoMk

added def CategoryTheory.ShortComplex.map

added def CategoryTheory.ShortComplex.mapNatIso

added def CategoryTheory.ShortComplex.mapNatTrans

added def CategoryTheory.ShortComplex.op

added def CategoryTheory.ShortComplex.opEquiv

added def CategoryTheory.ShortComplex.opFunctor

added def CategoryTheory.ShortComplex.opMap

added theorem CategoryTheory.ShortComplex.opMap_id

added def CategoryTheory.ShortComplex.unop

added def CategoryTheory.ShortComplex.unopFunctor

added def CategoryTheory.ShortComplex.unopMap

added theorem CategoryTheory.ShortComplex.unopMap_id

added theorem CategoryTheory.ShortComplex.zero_τ₁

added theorem CategoryTheory.ShortComplex.zero_τ₂

added theorem CategoryTheory.ShortComplex.zero_τ₃

added def CategoryTheory.ShortComplex.π₁

added def CategoryTheory.ShortComplex.π₁Toπ₂

added theorem CategoryTheory.ShortComplex.π₁Toπ₂_comp_π₂Toπ₃

added def CategoryTheory.ShortComplex.π₂

added def CategoryTheory.ShortComplex.π₂Toπ₃

added def CategoryTheory.ShortComplex.π₃

added structure CategoryTheory.ShortComplex