Documentation

Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension

Projective Dimension in ModuleCat #

source
theorem ModuleCat.hasProjectiveDimensionLE_of_semiLinearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] {R' : Type u'} [CommRing 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
source
@[deprecated ModuleCat.hasProjectiveDimensionLE_of_semiLinearEquiv (since := "2026-04-04")]
theorem CategoryTheory.hasProjectiveDimensionLE_of_semiLinearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] {R' : Type u'} [CommRing 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.

source
theorem ModuleCat.projectiveDimension_eq_of_semiLinearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] {R' : Type u'} [CommRing R'] [Small.{v', u'} R'] (e : R ≃+* R') {M : ModuleCat R} {N : ModuleCat R'} (e' : ↑M ≃ₛₗ[↑e] ↑N) :
CategoryTheory.projectiveDimension M = CategoryTheory.projectiveDimension N
source
@[deprecated ModuleCat.projectiveDimension_eq_of_semiLinearEquiv (since := "2026-04-04")]
theorem CategoryTheory.projectiveDimension_eq_of_semiLinearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] {R' : Type u'} [CommRing 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.

source
theorem ModuleCat.hasProjectiveDimensionLE_of_linearEquiv {R : Type u} [CommRing 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
source
@[deprecated ModuleCat.hasProjectiveDimensionLE_of_linearEquiv (since := "2026-04-04")]
theorem CategoryTheory.hasProjectiveDimensionLE_of_linearEquiv {R : Type u} [CommRing 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.

source
theorem ModuleCat.projectiveDimension_eq_of_linearEquiv {R : Type u} [CommRing 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
source
@[deprecated ModuleCat.projectiveDimension_eq_of_linearEquiv (since := "2026-04-04")]
theorem CategoryTheory.projectiveDimension_eq_of_linearEquiv {R : Type u} [CommRing 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.

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