Baer criterion for injective dimension

The Baer criterion describes that an R-module M is injective iff any ideal I of R, any I →ₗ[R] M can be extended to R →ₗ[R] M. The later condition has an equivalent charaterization using the vanishing of Ext (R ⧸ I) M 1, which is introduced in this file. This characterization is also useful for proving injective dimension not exceeding n only needs to check vanishing of all Ext (R ⧸ I) M (n + 1) for all ideals I.

Main Results

• ModuleCat.ext_quotient_one_subsingleton_iff : Ext (R ⧸ I) M 1 = 0 iff any linear map I →ₗ[R] M can be extended to R →ₗ[R] M.

• ModuleCat.injective_of_subsingleton_ext_quotient_one : An R-module M is injective iff Ext (R ⧸ I) M 1 = 0 for all ideals I.

• ModuleCat.hasInjectiveDimensionLT_of_quotients : An R-module M has injective dimension strictly less than n iff Ext (R ⧸ I) M n = 0 for all ideals I.

theorem ModuleCat.ext_one_subsingleton_iff_of_projective {R : Type u} [CommRing R] [Small.{v, u} R] (M : ModuleCat R) (S : CategoryTheory.ShortComplex (ModuleCat R)) (S_exact : S.ShortExact) (proj : CategoryTheory.Projective S.X₂) : Subsingleton (CategoryTheory.Abelian.Ext S.X₃ M 1) ↔ Function.Surjective ⇑((CategoryTheory.Abelian.Ext.mk₀ S.f).precomp M ⋯)

theorem ModuleCat.ext_quotient_one_subsingleton_iff {R : Type u} [CommRing R] [Small.{v, u} R] (M : ModuleCat R) (I : Ideal R) : Subsingleton (CategoryTheory.Abelian.Ext (of R (Shrink.{v, u} (R ⧸ I))) M 1) ↔ ∀ (g : ↥I →ₗ[R] ↑M), ∃ (g' : R →ₗ[R] ↑M), ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

theorem ModuleCat.injective_of_subsingleton_ext_quotient_one {R : Type u} [CommRing R] [Small.{v, u} R] (M : ModuleCat R) (h : ∀ (I : Ideal R), Subsingleton (CategoryTheory.Abelian.Ext (of R (Shrink.{v, u} (R ⧸ I))) M 1)) : CategoryTheory.Injective M

theorem ModuleCat.hasInjectiveDimensionLE_of_quotients {R : Type u} [CommRing R] [Small.{v, u} R] (M : ModuleCat R) (n : ℕ) (h : ∀ (I : Ideal R), Subsingleton (CategoryTheory.Abelian.Ext (of R (Shrink.{v, u} (R ⧸ I))) M (n + 1))) : CategoryTheory.HasInjectiveDimensionLE M n

theorem ModuleCat.hasInjectiveDimensionLT_of_quotients {R : Type u} [CommRing R] [Small.{v, u} R] (M : ModuleCat R) (n : ℕ) (h : ∀ (I : Ideal R), Subsingleton (CategoryTheory.Abelian.Ext (of R (Shrink.{v, u} (R ⧸ I))) M n)) : CategoryTheory.HasInjectiveDimensionLT M n