Baer's criterion for injective dimension

Baer's criterion says that an R-module M is injective iff every R-linear map I →ₗ[R] M from an ideal I of R extends to a map R →ₗ[R] M.

This file reformulates that extension condition as the vanishing of Ext (R ⧸ I) M 1. It then uses dimension shifting to give a criterion for injective dimension: to prove that M has injective dimension < n, it suffices to show that Ext (R ⧸ I) M n vanishes for all ideals I.

The statements use Shrink because R, its ideals, and its quotients may live in a larger universe than ModuleCat.{v} R.

Main results

• ModuleCat.ext_quotient_one_subsingleton_iff: Ext (R ⧸ I) M 1 vanishes iff every linear map I →ₗ[R] M extends to R →ₗ[R] M.
• ModuleCat.injective_of_subsingleton_ext_quotient_one: if Ext (R ⧸ I) M 1 vanishes for all ideals I, then M is injective.
• ModuleCat.injective_iff_subsingleton_ext_quotient_one: if and only if version of ModuleCat.injective_of_subsingleton_ext_quotient_one.
• ModuleCat.hasInjectiveDimensionLT_of_quotients: if Ext (R ⧸ I) M n vanishes for all ideals I, then M has injective dimension < n.
• ModuleCat.hasInjectiveDimensionLT_iff_quotients: if and only if version of ModuleCat.hasInjectiveDimensionLT_of_quotients

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⟩

The vanishing of Ext (R ⧸ I) M 1 is equivalent to Baer's extension property for maps I →ₗ[R] M.

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

Baer's criterion in Ext form: if Ext (R ⧸ I) M 1 vanishes for every ideal I, then M is injective.

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

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

If Ext (R ⧸ I) M (n + 1) vanishes for every ideal I, then M has injective dimension at most 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

If Ext (R ⧸ I) M n vanishes for every ideal I, then M has injective dimension strictly less than n.

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