The projective-dimension exit from idempotent saturation

For a submodule N of a projective module P, projective dimension at most one of P/N forces N to be projective. Applied to an idempotent saturation, this isolates the exact final homological obligation in Iyama's construction.

theorem MagnitudeConjecture.IdempotentSaturation.projectiveDimensionLE_one_of_shortExact {R : Type u} [Ring R] {S : CategoryTheory.ShortComplex (ModuleCat R)} (hS : S.ShortExact) (hmiddle : CategoryTheory.HasProjectiveDimensionLE S.X₂ 1) (hright : CategoryTheory.HasProjectiveDimensionLE S.X₃ 2) : CategoryTheory.HasProjectiveDimensionLE S.X₁ 1

Dimension shifting in the form used at the end of Iyama's saturation argument: in a short exact sequence, projective dimension at most one of the middle term and at most two of the right term force projective dimension at most one of the left term.

theorem MagnitudeConjecture.IdempotentSaturation.projectiveDimensionLE_one_of_injective {R : Type u} [Ring R] {W Z : Type u} [AddCommGroup W] [Module R W] [AddCommGroup Z] [Module R Z] (f : W →ₗ[R] Z) (hf : Function.Injective ⇑f) (hZ : CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of R Z) 1) (hcokernel : CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of R (Z ⧸ f.range)) 2) : CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of R W) 1

Concrete monomorphism form of the same dimension shift. This is the precise step used after embedding a saturated quotient into its injective hull.

theorem MagnitudeConjecture.IdempotentSaturation.submodule_projective_of_quotient_projectiveDimensionLE_one {R V : Type u} [Ring R] [AddCommGroup V] [Module R V] (N : Submodule R V) (hV : CategoryTheory.Projective (ModuleCat.of R V)) (hquotient : CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of R (V ⧸ N)) 1) : CategoryTheory.Projective (ModuleCat.of R ↥N)

A submodule of a projective module is projective as soon as the quotient has projective dimension at most one.

theorem MagnitudeConjecture.IdempotentSaturation.saturation_projective_of_quotient_projectiveDimensionLE_one {R V : Type u} [Ring R] [AddCommGroup V] [Module R V] (e : R) (L : Submodule R V) (hV : CategoryTheory.Projective (ModuleCat.of R V)) (hquotient : CategoryTheory.HasProjectiveDimensionLE (ModuleCat.of R (V ⧸ saturation e L)) 1) : CategoryTheory.Projective (ModuleCat.of R ↥(saturation e L))

In particular, an idempotent saturation is projective once its quotient in the ambient projective has projective dimension at most one.