Commit 2025-10-02 11:57 570711a9

View on Github →

feat(Algebra/Homology): add injective dimension (#30080) In this PR, we created Mathlib.CategoryTheory.Abelian.Injective.Dimension corresponding to Mathlib.CategoryTheory.Abelian.Projective.Dimension This is a preliminary for Gorenstein ring.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Abelian/Injective/Dimension.lean

added theorem CategoryTheory.Abelian.Ext.eq_zero_of_hasInjectiveDimensionLT

added theorem CategoryTheory.HasInjectiveDimensionLT.mk

added theorem CategoryTheory.HasInjectiveDimensionLT.subsingleton

added theorem CategoryTheory.Limits.IsZero.hasInjectiveDimensionLT_zero

added theorem CategoryTheory.Retract.hasInjectiveDimensionLT

added theorem CategoryTheory.Retract.injectiveDimension_le

added theorem CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₁

added theorem CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₂

added theorem CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃

added theorem CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₃_iff

added theorem CategoryTheory.hasInjectiveDimensionLT_iff

added theorem CategoryTheory.hasInjectiveDimensionLT_of_ge

added theorem CategoryTheory.hasInjectiveDimensionLT_of_iso

added theorem CategoryTheory.hasInjectiveDimensionLT_zero_iff_isZero

added theorem CategoryTheory.injectiveDimension_eq_bot_iff

added theorem CategoryTheory.injectiveDimension_eq_of_iso

added theorem CategoryTheory.injectiveDimension_ge_iff

added theorem CategoryTheory.injectiveDimension_le_iff

added theorem CategoryTheory.injectiveDimension_lt_iff

added theorem CategoryTheory.injectiveDimension_ne_top_iff

added theorem CategoryTheory.injective_iff_hasInjectiveDimensionLT_one

added theorem CategoryTheory.injective_iff_subsingleton_ext_one

added theorem CategoryTheory.isZero_of_hasInjectiveDimensionLT_zero