Commit 2025-09-23 17:30 608b610f

View on Github →

feat(Algebra/Homology): define projective dimension as a number (#29882) In this PR, we gave the definition of projective dimension in WithBot ℕ∞ as projectiveDimension, projectiveDimension X = ⊥ iff X is zero and acts in common sense in the non-negative values.

Estimated changes

Modified Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean

added theorem CategoryTheory.Retract.projectiveDimension_le

added theorem CategoryTheory.hasProjectiveDimensionLT_zero_iff_isZero

added theorem CategoryTheory.projectiveDimension_eq_bot_iff

added theorem CategoryTheory.projectiveDimension_eq_of_iso

added theorem CategoryTheory.projectiveDimension_ge_iff

added theorem CategoryTheory.projectiveDimension_le_iff

added theorem CategoryTheory.projectiveDimension_lt_iff

added theorem CategoryTheory.projectiveDimension_ne_top_iff

added theorem CategoryTheory.projective_iff_hasProjectiveDimensionLT_one

added theorem CategoryTheory.projective_iff_subsingleton_ext_one