Commit 2025-01-23 19:32 f4e2c6d6

View on Github →

feat(CategoryTheory/Abelian): projective dimension (#19604) We introduce a typeclass HasProjectiveDimensionLT X n expressing that Ext X Y i all vanish when n ≤ i. We study how it behaves with respect to short exact sequences. When #19591 will be merged, it will possible to show HasProjectiveDimensionLT X 1 ↔ Projective X.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean

added theorem CategoryTheory.HasExt.standard

Created Mathlib/CategoryTheory/Abelian/ProjectiveDimension.lean

added theorem CategoryTheory.Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT

added theorem CategoryTheory.HasProjectiveDimensionLT.mk

added theorem CategoryTheory.HasProjectiveDimensionLT.subsingleton

added theorem CategoryTheory.Limits.IsZero.hasProjectiveDimensionLT_zero

added theorem CategoryTheory.Retract.hasProjectiveDimensionLT

added theorem CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₁

added theorem CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₂

added theorem CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃

added theorem CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff

added theorem CategoryTheory.hasProjectiveDimensionLT_iff

added theorem CategoryTheory.hasProjectiveDimensionLT_of_ge

added theorem CategoryTheory.hasProjectiveDimensionLT_of_iso

Modified Mathlib/CategoryTheory/Retract.lean

added def CategoryTheory.Iso.retract

added def CategoryTheory.Retract.refl

added def CategoryTheory.Retract.trans