Projective Dimension in ModuleCat

This file deals with preservation of projectiveDimension in (semi) linear equivalences. Previously we only know this for linear equivalence within same universe level, now it works with all universe level where the ring R is small.

Main Results

• ModuleCat.hasProjectiveDimensionLE_of_semiLinearEquiv: a module N satisfy HasProjectiveDimensionLE N n if it is semi-linear equivalent to a module M that HasProjectiveDimensionLE M n.

• ModuleCat.projectiveDimension_eq_of_semiLinearEquiv: projectiveDimension is preserved under arbitrary semi-linear equivalence.

• ModuleCat.hasProjectiveDimensionLE_of_linearEquiv: a module N satisfy HasProjectiveDimensionLE N n if it is linear equivalent to a module M that HasProjectiveDimensionLE M n.

• ModuleCat.projectiveDimension_eq_of_linearEquiv: projectiveDimension is preserved under arbitrary linear equivalence.

theorem ModuleCat.hasProjectiveDimensionLE_of_semiLinearEquiv {R : Type u} [Ring R] [Small.{v, u} R] {R' : Type u'} [Ring R'] [Small.{v', u'} R'] (e : R ≃+* R') {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) (n : ℕ) [CategoryTheory.HasProjectiveDimensionLE M n] : CategoryTheory.HasProjectiveDimensionLE N n

@[deprecated ModuleCat.hasProjectiveDimensionLE_of_semiLinearEquiv (since := "2026-04-04")]

theorem CategoryTheory.hasProjectiveDimensionLE_of_semiLinearEquiv {R : Type u} [Ring R] [Small.{v, u} R] {R' : Type u'} [Ring R'] [Small.{v', u'} R'] (e : R ≃+* R') {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) (n : ℕ) [HasProjectiveDimensionLE M n] : HasProjectiveDimensionLE N n

Alias of ModuleCat.hasProjectiveDimensionLE_of_semiLinearEquiv.

theorem ModuleCat.projectiveDimension_eq_of_semiLinearEquiv {R : Type u} [Ring R] [Small.{v, u} R] {R' : Type u'} [Ring R'] [Small.{v', u'} R'] (e : R ≃+* R') {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) : CategoryTheory.projectiveDimension M = CategoryTheory.projectiveDimension N

@[deprecated ModuleCat.projectiveDimension_eq_of_semiLinearEquiv (since := "2026-04-04")]

theorem CategoryTheory.projectiveDimension_eq_of_semiLinearEquiv {R : Type u} [Ring R] [Small.{v, u} R] {R' : Type u'} [Ring R'] [Small.{v', u'} R'] (e : R ≃+* R') {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) : projectiveDimension M = projectiveDimension N

Alias of ModuleCat.projectiveDimension_eq_of_semiLinearEquiv.

theorem ModuleCat.hasProjectiveDimensionLE_of_linearEquiv {R : Type u} [Ring R] [Small.{v, u} R] [Small.{v', u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N) (n : ℕ) [CategoryTheory.HasProjectiveDimensionLE M n] : CategoryTheory.HasProjectiveDimensionLE N n

@[deprecated ModuleCat.hasProjectiveDimensionLE_of_linearEquiv (since := "2026-04-04")]

theorem CategoryTheory.hasProjectiveDimensionLE_of_linearEquiv {R : Type u} [Ring R] [Small.{v, u} R] [Small.{v', u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N) (n : ℕ) [HasProjectiveDimensionLE M n] : HasProjectiveDimensionLE N n

Alias of ModuleCat.hasProjectiveDimensionLE_of_linearEquiv.

theorem ModuleCat.projectiveDimension_eq_of_linearEquiv {R : Type u} [Ring R] [Small.{v, u} R] [Small.{v', u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N) : CategoryTheory.projectiveDimension M = CategoryTheory.projectiveDimension N

@[deprecated ModuleCat.projectiveDimension_eq_of_linearEquiv (since := "2026-04-04")]

theorem CategoryTheory.projectiveDimension_eq_of_linearEquiv {R : Type u} [Ring R] [Small.{v, u} R] [Small.{v', u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N) : projectiveDimension M = projectiveDimension N

Alias of ModuleCat.projectiveDimension_eq_of_linearEquiv.

theorem ModuleCat.projectiveDimension_eq_zero_of_projective {R : Type u} [Ring R] (M : ModuleCat R) [Nontrivial ↑M] [CategoryTheory.Projective M] : CategoryTheory.projectiveDimension M = 0