Injective Dimension in ModuleCat

This file deals with preservation of injectiveDimension 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.hasInjectiveDimensionLE_iff_of_linearEquiv: HasInjectiveDimensionLE is preserved under arbitrary linear equivalence.

• ModuleCat.hasInjectiveDimensionLE_iff_of_semiLinearEquiv: HasInjectiveDimensionLE is preserved under arbitrary semi-linear equivalence.

• ModuleCat.injectiveDimension_eq_of_semiLinearEquiv: injectiveDimension is preserved under arbitrary semi-linear equivalence.

• ModuleCat.injectiveDimension_eq_of_linearEquiv: injectiveDimension is preserved under arbitrary linear equivalence.

theorem ModuleCat.hasInjectiveDimensionLE_iff_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.HasInjectiveDimensionLE M n ↔ CategoryTheory.HasInjectiveDimensionLE N n

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

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

theorem ModuleCat.injectiveDimension_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.injectiveDimension M = CategoryTheory.injectiveDimension N